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 ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )

Proof

Step Hyp Ref Expression
1 0red ⊢ ( 𝐴 ∈ dom arctan → 0 ∈ ℝ )
2 atandm2 ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
3 2 simp1bi ⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
4 3 recld ⊢ ( 𝐴 ∈ dom arctan → ( ℜ ‘ 𝐴 ) ∈ ℝ )
5 atanlogaddlem ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )
6 ax-1cn ⊢ 1 ∈ ℂ
7 ax-icn ⊢ i ∈ ℂ
8 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
9 7 3 8 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ )
10 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
11 6 9 10 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
12 2 simp3bi ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
13 11 12 logcld ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
14 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
15 6 9 14 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
16 2 simp2bi ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
17 15 16 logcld ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
18 13 17 addcomd ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) + ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
19 mulneg2 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
20 7 3 19 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
21 20 oveq2d ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 + - ( i · 𝐴 ) ) )
22 negsub ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
23 6 9 22 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
24 21 23 eqtrd ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
25 24 fveq2d ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
26 20 oveq2d ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 − - ( i · 𝐴 ) ) )
27 subneg ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
28 6 9 27 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
29 26 28 eqtrd ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
30 29 fveq2d ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
31 25 30 oveq12d ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) + ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
32 18 31 eqtr4d ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) )
33 32 adantr ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≤ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) )
34 atandmneg ⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan )
35 4 le0neg1d ⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ 0 ≤ - ( ℜ ‘ 𝐴 ) ) )
36 35 biimpa ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ - ( ℜ ‘ 𝐴 ) )
37 3 renegd ⊢ ( 𝐴 ∈ dom arctan → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
38 37 adantr ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≤ 0 ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
39 36 38 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≤ 0 ) → 0 ≤ ( ℜ ‘ - 𝐴 ) )
40 atanlogaddlem ⊢ ( ( - 𝐴 ∈ dom arctan ∧ 0 ≤ ( ℜ ‘ - 𝐴 ) ) → ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ∈ ran log )
41 34 39 40 syl2an2r ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≤ 0 ) → ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ∈ ran log )
42 33 41 eqeltrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≤ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )
43 1 4 5 42 lecasei ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )