This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atanlogsub

Description: A variation on atanlogadd , to show that sqrt ( 1 +i z ) / sqrt ( 1 - i z ) = sqrt ( ( 1 +i z ) / ( 1 - i z ) ) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion atanlogsub ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ax-icn ⊢ i ∈ ℂ
3 atandm2 ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
4 3 simp1bi ⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
5 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
6 2 4 5 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ )
7 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
8 1 6 7 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
9 3 simp3bi ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
10 8 9 logcld ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
11 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
12 1 6 11 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
13 3 simp2bi ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
14 12 13 logcld ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
15 10 14 subcld ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
16 15 adantr ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
17 4 recld ⊢ ( 𝐴 ∈ dom arctan → ( ℜ ‘ 𝐴 ) ∈ ℝ )
18 0re ⊢ 0 ∈ ℝ
19 lttri2 ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) ≠ 0 ↔ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) )
20 17 18 19 sylancl ⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) ≠ 0 ↔ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) )
21 20 biimpa ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) )
22 15 imnegd ⊢ ( 𝐴 ∈ dom arctan → ( ℑ ‘ - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
23 10 14 negsubdi2d ⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
24 mulneg2 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
25 2 4 24 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
26 25 oveq2d ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 + - ( i · 𝐴 ) ) )
27 negsub ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
28 1 6 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 oveq2d ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 − - ( i · 𝐴 ) ) )
32 subneg ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
33 1 6 32 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
34 31 33 eqtrd ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
35 34 fveq2d ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
36 30 35 oveq12d ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
37 23 36 eqtr4d ⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) )
38 37 fveq2d ⊢ ( 𝐴 ∈ dom arctan → ( ℑ ‘ - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) )
39 22 38 eqtr3d ⊢ ( 𝐴 ∈ dom arctan → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) )
40 39 adantr ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) )
41 atandmneg ⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan )
42 17 lt0neg1d ⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) < 0 ↔ 0 < - ( ℜ ‘ 𝐴 ) ) )
43 42 biimpa ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < - ( ℜ ‘ 𝐴 ) )
44 4 adantr ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 𝐴 ∈ ℂ )
45 44 renegd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
46 43 45 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < ( ℜ ‘ - 𝐴 ) )
47 atanlogsublem ⊢ ( ( - 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ - 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
48 41 46 47 syl2an2r ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
49 picn ⊢ π ∈ ℂ
50 49 negnegi ⊢ - - π = π
51 50 oveq2i ⊢ ( - π (,) - - π ) = ( - π (,) π )
52 48 51 eleqtrrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) )
53 40 52 eqeltrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) )
54 pire ⊢ π ∈ ℝ
55 54 renegcli ⊢ - π ∈ ℝ
56 15 adantr ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
57 56 imcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ )
58 iooneg ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ↔ - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) )
59 55 54 57 58 mp3an12i ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ↔ - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) )
60 53 59 mpbird ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
61 atanlogsublem ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
62 60 61 jaodan ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
63 21 62 syldan ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )
64 eliooord ⊢ ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) )
65 63 64 syl ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) )
66 65 simpld ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
67 65 simprd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π )
68 16 imcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ )
69 ltle ⊢ ( ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) )
70 68 54 69 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) )
71 67 70 mpd ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π )
72 ellogrn ⊢ ( ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log ↔ ( ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) )
73 16 66 71 72 syl3anbrc ⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )