# Symbolically prove that two expressions are identical

I encountered this problem when trying to reproduce the result of this paper. (The relevant parts are all included in the preview i.e. the 1st page of the article. This link is just given as background information, the following question is still self-contained without it.)

I want to prove int == intpaper assuming l > 0, τ > 0 where

int =
Sqrt[3] (-(1/((Sqrt[-3 + 2 Sqrt[3]] l - I Sqrt[6 - 2 Sqrt[3]] τ)
Sqrt[1 + 3/(Sqrt[-3 + 2 Sqrt[3]] l - I Sqrt[6 - 2 Sqrt[3]] τ)^2])) -
1/((Sqrt[-3 + 2 Sqrt[3]] l + I Sqrt[6 - 2 Sqrt[3]] τ)
Sqrt[1 + 3/(Sqrt[-3 + 2 Sqrt[3]] l + I Sqrt[6 - 2 Sqrt[3]] τ)^2]));

intpaper = Im[2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l - 2 I τ)^2/(3 + Sqrt[3])]];


It's easy to verify their equivalence numerically.

Block[{l, τ}, {l, τ} = RandomReal[1, 2]; intpaper == int]


always returns True. But I don't know how to verify it symbolically. I tried

Simplify[int == intpaper, {l > 0, τ > 0}]


but it was returned unevaluated.

• Since all the variables are real, why not do a preliminary ComplexExpand[]? – J. M. will be back soon Jun 25 '16 at 13:13
• @J.M. Just tried, but at least Simplify[int == intpaper // ComplexExpand, {l > 0, τ > 0}] doesn't help. The Im is rather troublesome. – xzczd Jun 25 '16 at 13:14
• You might consider providing a open-access link to the publication (possibly after uploading the pdf there by yourself, since the copyright issues are likely to be long expired), so that everybody can access it. – anderstood Jun 27 '16 at 21:44
• @anderstood It's not quite necessary actually, because the paper is short (Only 2 pages) and the relevant part is already shown in the preview i.e. the first page, and that link is just given as background information, without that my question is still answerable. I'll edit my question to note this. – xzczd Jun 28 '16 at 2:03
• @ShutaoTANG I think there's no doubt that it's a Mathematica problem: I have a equation and I'm sure it's correct, now I want to verify it with Mathematica (notice I don't need a step-to-step proof) but Simplify doesn't work, can I achieve the goal with other built-in functions/options or a minimal effort of coding? These are all about the usage of Mathematica. – xzczd Jun 28 '16 at 2:21

You can consider the difference diff = int - intpaper, and check that it vanishes.

Rather than having Mathematica take the imaginary part, do it "by hand":

intpaperz =
2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l - 2 I \[Tau])^2/(3 + Sqrt[3])];
intpaperzc =
2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l + 2 I \[Tau])^2/(3 + Sqrt[3])];
intpaper = 1/(2 I) (intpaperz - intpaperzc);


which uses $\textrm{Im}(z) = (z-z^*)/(2i)$. Note: I assume $\tau$ and $l$ are real.

By inspection of the the resulting expression for diff:

a good change of variables appears to be

$$a = \sqrt{6-2\sqrt{3}} \tau , \quad b = l \sqrt{-3 + 2\sqrt{3}} ,$$

which can be implemeneted by:

out = FullSimplify[
diff /. {\[Tau] -> a/Sqrt[6 - 2 Sqrt[3]],
l -> b/Sqrt[-3 + 2 Sqrt[3]]}]


The resulting expression is

This suggests another change of variables:

out = out /. {a + I b -> w, a - I b -> wc, -I a + b -> -I w, I a + b -> I wc};
FullSimplify[out]


This is the trivial last step that I stopped fighting Mathematica on. For a complex number (such as w and wc), it's true that $\sqrt{w^2} = w$, so both terms vanish. This last step is not so trivial. As @xzczd pointed out in the comment, this only vanishes if $\textrm{Re}(w)>0$ and $\textrm{Re}(w^*)> 0$. Well,

$$\textrm{Re}(w) = a = \sqrt{6-2\sqrt{3}} \tau$$

and

$$\textrm{Re}(w^*) = a ,$$ so I guess $\tau\ge 0$ in the original problem statement.

In Mathematica:

FullSimplify[out,{Re@w > 0, Re@wc > 0}];
(* 0 *)

• I guess the more generally applicable answer is to try to change variables that un-clutter the expression before simplifying. – jjstankowicz Jun 26 '16 at 4:36
• Thanks for your answer! Then, "For a complex number (such as w and wc), it's true that $\sqrt{w^2}=w$, so both terms vanish." I'm afraid it's not true, a counter example is w -> -1 + I. I'm not familiar with complex analysis, but I think one sufficient condition for $\sqrt{w^2}=w$ is Re@w>0, and this is indeed satisfied, given a -> (6 - 2 Sqrt[3]) \[Tau]. You can add {Re@w > 0, Re@wc > 0} to Simplify to make it output 0. – xzczd Jun 26 '16 at 5:58
• Hah, sorry for the incorrect statement about $\sqrt{w^2}$ - as you say, they are not equal in general. I guess the correct statement is that the two expressions only match if $\textrm{Re}(w) > 0$ and $\textrm{Im}(w) = \textrm{Im}(w^*) >0$ (wc $= w^*$). – jjstankowicz Jun 26 '16 at 6:18
• Er… I think there're some typos? The $Im(w)=$ seems to be redundant, and the lc and \[Tau]c at beginning should be l and \[Tau]? – xzczd Jun 26 '16 at 7:10
• Yeah, the lc and \[Tau]c happened from accidentally closing the window and having an old version restored - I corrected them. And in my previous comment, I meant $\textrm{Im}(w)= \textrm{Re}(w^∗)>0$ (which I at least got right in the answer). Sorry about that! – jjstankowicz Jun 26 '16 at 7:25

My solution is in the experimental mathematics style:

Series[int - intpaper, {τ, \[Infinity], 12}] // Normal // FullSimplify
(* 0 *)


You have to believe that if two series expansions are equal up to 12th order this is an identity. Advantage of the approach is its unbeatable simplicity. Of course, sceptics with faster computers can verify even higher orders. However, it can never be made fully rigorous, but what is verity after all?

• Normally, in the series approach, you want to first make sure that a differential equation of appropriate order is satisfied (using e.g. DifferentialRootReduce[]), and then use Series[] to expand up to an appropriate order to check that what should be zero is actually zero. – J. M. will be back soon Jun 28 '16 at 2:16
• Though not that perfect, this approach is indeed more automatic, so 千金市骨 :) – xzczd Jul 5 '16 at 2:28
• @xzczd Thank you! Your post gives an example showing that not all MA algorithms are equally strong, and it might be useful to try different things. – yarchik Jul 5 '16 at 7:36