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 ⊢A∈dom⁡arctan∧ℜ⁡A≠0→log⁡1+i⁢A−log⁡1−i⁢A∈ran⁡log

Proof

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