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 (-(1/((Sqrt[-3 + 2 Sqrt] l - I Sqrt[6 - 2 Sqrt] τ)
Sqrt[1 + 3/(Sqrt[-3 + 2 Sqrt] l - I Sqrt[6 - 2 Sqrt] τ)^2])) -
1/((Sqrt[-3 + 2 Sqrt] l + I Sqrt[6 - 2 Sqrt] τ)
Sqrt[1 + 3/(Sqrt[-3 + 2 Sqrt] l + I Sqrt[6 - 2 Sqrt] τ)^2]));

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

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[]? 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. 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. 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. 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. 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] l - 2 I \[Tau])^2/(3 + Sqrt)];
intpaperzc =
2/Sqrt[-1 - (Sqrt[-1 + Sqrt] l + 2 I \[Tau])^2/(3 + Sqrt)];
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],
l -> b/Sqrt[-3 + 2 Sqrt]}]

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. 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) \[Tau]. You can add {Re@w > 0, Re@wc > 0} to Simplify to make it output 0. 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^*$). 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]? 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! 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. Jun 28 '16 at 2:16
• Though not that perfect, this approach is indeed more automatic, so 千金市骨 :) 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. Jul 5 '16 at 7:36