Metamath Proof Explorer


Theorem atanlogadd

Description: The rule sqrt ( z w ) = ( sqrt z ) ( sqrt w ) is not always true on the complex numbers, but it is true when the arguments of z and w sum to within the interval ( -upi , pi ] , so there are some cases such as this one with z = 1 +i A and w = 1 - i A which are true unconditionally. This result can also be stated as " sqrt ( 1 + z ) + sqrt ( 1 - z ) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion atanlogadd Adomarctanlog1+iA+log1iAranlog

Proof

Step Hyp Ref Expression
1 0red Adomarctan0
2 atandm2 AdomarctanA1iA01+iA0
3 2 simp1bi AdomarctanA
4 3 recld AdomarctanA
5 atanlogaddlem Adomarctan0Alog1+iA+log1iAranlog
6 ax-1cn 1
7 ax-icn i
8 mulcl iAiA
9 7 3 8 sylancr AdomarctaniA
10 addcl 1iA1+iA
11 6 9 10 sylancr Adomarctan1+iA
12 2 simp3bi Adomarctan1+iA0
13 11 12 logcld Adomarctanlog1+iA
14 subcl 1iA1iA
15 6 9 14 sylancr Adomarctan1iA
16 2 simp2bi Adomarctan1iA0
17 15 16 logcld Adomarctanlog1iA
18 13 17 addcomd Adomarctanlog1+iA+log1iA=log1iA+log1+iA
19 mulneg2 iAiA=iA
20 7 3 19 sylancr AdomarctaniA=iA
21 20 oveq2d Adomarctan1+iA=1+iA
22 negsub 1iA1+iA=1iA
23 6 9 22 sylancr Adomarctan1+iA=1iA
24 21 23 eqtrd Adomarctan1+iA=1iA
25 24 fveq2d Adomarctanlog1+iA=log1iA
26 20 oveq2d Adomarctan1iA=1iA
27 subneg 1iA1iA=1+iA
28 6 9 27 sylancr Adomarctan1iA=1+iA
29 26 28 eqtrd Adomarctan1iA=1+iA
30 29 fveq2d Adomarctanlog1iA=log1+iA
31 25 30 oveq12d Adomarctanlog1+iA+log1iA=log1iA+log1+iA
32 18 31 eqtr4d Adomarctanlog1+iA+log1iA=log1+iA+log1iA
33 32 adantr AdomarctanA0log1+iA+log1iA=log1+iA+log1iA
34 atandmneg AdomarctanAdomarctan
35 4 le0neg1d AdomarctanA00A
36 35 biimpa AdomarctanA00A
37 3 renegd AdomarctanA=A
38 37 adantr AdomarctanA0A=A
39 36 38 breqtrrd AdomarctanA00A
40 atanlogaddlem Adomarctan0Alog1+iA+log1iAranlog
41 34 39 40 syl2an2r AdomarctanA0log1+iA+log1iAranlog
42 33 41 eqeltrd AdomarctanA0log1+iA+log1iAranlog
43 1 4 5 42 lecasei Adomarctanlog1+iA+log1iAranlog