Proof of Theorem efiatan
| Step | Hyp | Ref
| Expression |
| 1 | | atanval 26927 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
| 2 | 1 | oveq2d 7447 |
. . . 4
⊢ (𝐴 ∈ dom arctan → (i
· (arctan‘𝐴))
= (i · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))))) |
| 3 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → i
∈ ℂ) |
| 5 | | halfcl 12491 |
. . . . . 6
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
| 6 | 3, 5 | mp1i 13 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (i /
2) ∈ ℂ) |
| 7 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 8 | | atandm2 26920 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
| 9 | 8 | simp1bi 1146 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) |
| 10 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 11 | 3, 9, 10 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) |
| 12 | | subcl 11507 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
| 13 | 7, 11, 12 | sylancr 587 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) |
| 14 | 8 | simp2bi 1147 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) |
| 15 | 13, 14 | logcld 26612 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
| 16 | | addcl 11237 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
| 17 | 7, 11, 16 | sylancr 587 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) |
| 18 | 8 | simp3bi 1148 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) |
| 19 | 17, 18 | logcld 26612 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
| 20 | 15, 19 | subcld 11620 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) |
| 21 | 4, 6, 20 | mulassd 11284 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((i
· (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (i · ((i /
2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) |
| 22 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 23 | | 2ne0 12370 |
. . . . . . . 8
⊢ 2 ≠
0 |
| 24 | | divneg 11959 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(1 / 2) = (-1 /
2)) |
| 25 | 7, 22, 23, 24 | mp3an 1463 |
. . . . . . 7
⊢ -(1 / 2)
= (-1 / 2) |
| 26 | | ixi 11892 |
. . . . . . . 8
⊢ (i
· i) = -1 |
| 27 | 26 | oveq1i 7441 |
. . . . . . 7
⊢ ((i
· i) / 2) = (-1 / 2) |
| 28 | 3, 3, 22, 23 | divassi 12023 |
. . . . . . 7
⊢ ((i
· i) / 2) = (i · (i / 2)) |
| 29 | 25, 27, 28 | 3eqtr2i 2771 |
. . . . . 6
⊢ -(1 / 2)
= (i · (i / 2)) |
| 30 | 29 | oveq1i 7441 |
. . . . 5
⊢ (-(1 / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = ((i · (i /
2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
| 31 | | halfcn 12481 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
| 32 | | mulneg12 11701 |
. . . . . . 7
⊢ (((1 / 2)
∈ ℂ ∧ ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈ ℂ)
→ (-(1 / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = ((1 / 2) ·
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
| 33 | 31, 20, 32 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (-(1 /
2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = ((1 / 2) ·
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
| 34 | 15, 19 | negsubdi2d 11636 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) = ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) |
| 35 | 34 | oveq2d 7447 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · -((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = ((1 / 2) ·
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
| 36 | 31 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1 /
2) ∈ ℂ) |
| 37 | 36, 19, 15 | subdid 11719 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) = (((1 / 2)
· (log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴)))))) |
| 38 | 33, 35, 37 | 3eqtrd 2781 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (-(1 /
2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (((1 / 2) ·
(log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴)))))) |
| 39 | 30, 38 | eqtr3id 2791 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((i
· (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = (((1 / 2) ·
(log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴)))))) |
| 40 | 2, 21, 39 | 3eqtr2d 2783 |
. . 3
⊢ (𝐴 ∈ dom arctan → (i
· (arctan‘𝐴))
= (((1 / 2) · (log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴)))))) |
| 41 | 40 | fveq2d 6910 |
. 2
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) = (exp‘(((1 / 2) ·
(log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴))))))) |
| 42 | | mulcl 11239 |
. . . 4
⊢ (((1 / 2)
∈ ℂ ∧ (log‘(1 + (i · 𝐴))) ∈ ℂ) → ((1 / 2) ·
(log‘(1 + (i · 𝐴)))) ∈ ℂ) |
| 43 | 31, 19, 42 | sylancr 587 |
. . 3
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · (log‘(1 + (i · 𝐴)))) ∈ ℂ) |
| 44 | | mulcl 11239 |
. . . 4
⊢ (((1 / 2)
∈ ℂ ∧ (log‘(1 − (i · 𝐴))) ∈ ℂ) → ((1 / 2) ·
(log‘(1 − (i · 𝐴)))) ∈ ℂ) |
| 45 | 31, 15, 44 | sylancr 587 |
. . 3
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · (log‘(1 − (i · 𝐴)))) ∈ ℂ) |
| 46 | | efsub 16136 |
. . 3
⊢ ((((1 /
2) · (log‘(1 + (i · 𝐴)))) ∈ ℂ ∧ ((1 / 2) ·
(log‘(1 − (i · 𝐴)))) ∈ ℂ) → (exp‘(((1
/ 2) · (log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴))))))
= ((exp‘((1 / 2) · (log‘(1 + (i · 𝐴))))) / (exp‘((1 / 2) ·
(log‘(1 − (i · 𝐴))))))) |
| 47 | 43, 45, 46 | syl2anc 584 |
. 2
⊢ (𝐴 ∈ dom arctan →
(exp‘(((1 / 2) · (log‘(1 + (i · 𝐴)))) − ((1 / 2) · (log‘(1
− (i · 𝐴))))))
= ((exp‘((1 / 2) · (log‘(1 + (i · 𝐴))))) / (exp‘((1 / 2) ·
(log‘(1 − (i · 𝐴))))))) |
| 48 | 17, 18, 36 | cxpefd 26754 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((1 +
(i · 𝐴))↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘(1 + (i · 𝐴)))))) |
| 49 | | cxpsqrt 26745 |
. . . . 5
⊢ ((1 + (i
· 𝐴)) ∈ ℂ
→ ((1 + (i · 𝐴))↑𝑐(1 / 2)) =
(√‘(1 + (i · 𝐴)))) |
| 50 | 17, 49 | syl 17 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((1 +
(i · 𝐴))↑𝑐(1 / 2)) =
(√‘(1 + (i · 𝐴)))) |
| 51 | 48, 50 | eqtr3d 2779 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(exp‘((1 / 2) · (log‘(1 + (i · 𝐴))))) = (√‘(1 + (i ·
𝐴)))) |
| 52 | 13, 14, 36 | cxpefd 26754 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((1
− (i · 𝐴))↑𝑐(1 / 2)) =
(exp‘((1 / 2) · (log‘(1 − (i · 𝐴)))))) |
| 53 | | cxpsqrt 26745 |
. . . . 5
⊢ ((1
− (i · 𝐴))
∈ ℂ → ((1 − (i · 𝐴))↑𝑐(1 / 2)) =
(√‘(1 − (i · 𝐴)))) |
| 54 | 13, 53 | syl 17 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((1
− (i · 𝐴))↑𝑐(1 / 2)) =
(√‘(1 − (i · 𝐴)))) |
| 55 | 52, 54 | eqtr3d 2779 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(exp‘((1 / 2) · (log‘(1 − (i · 𝐴))))) = (√‘(1
− (i · 𝐴)))) |
| 56 | 51, 55 | oveq12d 7449 |
. 2
⊢ (𝐴 ∈ dom arctan →
((exp‘((1 / 2) · (log‘(1 + (i · 𝐴))))) / (exp‘((1 / 2) ·
(log‘(1 − (i · 𝐴)))))) = ((√‘(1 + (i ·
𝐴))) / (√‘(1
− (i · 𝐴))))) |
| 57 | 41, 47, 56 | 3eqtrd 2781 |
1
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) = ((√‘(1 + (i · 𝐴))) / (√‘(1 −
(i · 𝐴))))) |