Proof of Theorem atantan
| Step | Hyp | Ref
| Expression |
| 1 | | cosne0 26571 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0) |
| 2 | | atandmtan 26963 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) ∈
dom arctan) |
| 3 | 1, 2 | syldan 591 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ dom arctan) |
| 4 | | atanval 26927 |
. . 3
⊢
((tan‘𝐴)
∈ dom arctan → (arctan‘(tan‘𝐴)) = ((i / 2) · ((log‘(1
− (i · (tan‘𝐴)))) − (log‘(1 + (i ·
(tan‘𝐴))))))) |
| 5 | 3, 4 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = ((i / 2) · ((log‘(1
− (i · (tan‘𝐴)))) − (log‘(1 + (i ·
(tan‘𝐴))))))) |
| 6 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 7 | | ax-icn 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 8 | | tancl 16165 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) ∈
ℂ) |
| 9 | 1, 8 | syldan 591 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ ℂ) |
| 10 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (tan‘𝐴) ∈ ℂ) → (i ·
(tan‘𝐴)) ∈
ℂ) |
| 11 | 7, 9, 10 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) ∈ ℂ) |
| 12 | | addcl 11237 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 + (i ·
(tan‘𝐴))) ∈
ℂ) |
| 13 | 6, 11, 12 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ∈
ℂ) |
| 14 | | atandm2 26920 |
. . . . . . . 8
⊢
((tan‘𝐴)
∈ dom arctan ↔ ((tan‘𝐴) ∈ ℂ ∧ (1 − (i
· (tan‘𝐴)))
≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0)) |
| 15 | 3, 14 | sylib 218 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((tan‘𝐴) ∈ ℂ ∧ (1 − (i
· (tan‘𝐴)))
≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0)) |
| 16 | 15 | simp3d 1145 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ≠ 0) |
| 17 | 13, 16 | logcld 26612 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(1 + (i · (tan‘𝐴)))) ∈
ℂ) |
| 18 | | subcl 11507 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 − (i
· (tan‘𝐴)))
∈ ℂ) |
| 19 | 6, 11, 18 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ∈
ℂ) |
| 20 | 15 | simp2d 1144 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ≠ 0) |
| 21 | 19, 20 | logcld 26612 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(1 − (i ·
(tan‘𝐴)))) ∈
ℂ) |
| 22 | 17, 21 | negsubdi2d 11636 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) = ((log‘(1 − (i ·
(tan‘𝐴)))) −
(log‘(1 + (i · (tan‘𝐴)))))) |
| 23 | | efsub 16136 |
. . . . . . . . 9
⊢
(((log‘(1 + (i · (tan‘𝐴)))) ∈ ℂ ∧ (log‘(1
− (i · (tan‘𝐴)))) ∈ ℂ) →
(exp‘((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i
· (tan‘𝐴))))))
= ((exp‘(log‘(1 + (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i
· (tan‘𝐴))))))) |
| 24 | 17, 21, 23 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) = ((exp‘(log‘(1 + (i
· (tan‘𝐴)))))
/ (exp‘(log‘(1 − (i · (tan‘𝐴))))))) |
| 25 | | coscl 16163 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ) |
| 27 | | sincl 16162 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ) |
| 29 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
| 30 | 7, 28, 29 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ) |
| 31 | 26, 30, 26, 1 | divdird 12081 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴)))) |
| 32 | 26, 1 | dividd 12041 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘𝐴) / (cos‘𝐴)) = 1) |
| 33 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → i ∈ ℂ) |
| 34 | 33, 28, 26, 1 | divassd 12078 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴)))) |
| 35 | | tanval 16164 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
| 36 | 1, 35 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴))) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴)))) |
| 38 | 34, 37 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · (tan‘𝐴))) |
| 39 | 32, 38 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 + (i ·
(tan‘𝐴)))) |
| 40 | 31, 39 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 + (i · (tan‘𝐴)))) |
| 41 | | efival 16188 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴))) |
| 44 | | eflog 26618 |
. . . . . . . . . . 11
⊢ (((1 + (i
· (tan‘𝐴)))
∈ ℂ ∧ (1 + (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1
+ (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴)))) |
| 45 | 13, 16, 44 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 + (i ·
(tan‘𝐴))))) = (1 + (i
· (tan‘𝐴)))) |
| 46 | 40, 43, 45 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 + (i ·
(tan‘𝐴)))))) |
| 47 | 26, 30, 26, 1 | divsubdird 12082 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴)))) |
| 48 | 32, 38 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 − (i ·
(tan‘𝐴)))) |
| 49 | 47, 48 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 − (i ·
(tan‘𝐴)))) |
| 50 | | negcl 11508 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ) |
| 52 | | efival 16188 |
. . . . . . . . . . . . . 14
⊢ (-𝐴 ∈ ℂ →
(exp‘(i · -𝐴))
= ((cos‘-𝐴) + (i
· (sin‘-𝐴)))) |
| 53 | 51, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴)))) |
| 54 | | cosneg 16183 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(cos‘-𝐴) =
(cos‘𝐴)) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘-𝐴) = (cos‘𝐴)) |
| 56 | | sinneg 16182 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(sin‘-𝐴) =
-(sin‘𝐴)) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘-𝐴) = -(sin‘𝐴)) |
| 58 | 57 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = (i · -(sin‘𝐴))) |
| 59 | | mulneg2 11700 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
-(sin‘𝐴)) = -(i
· (sin‘𝐴))) |
| 60 | 7, 28, 59 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴))) |
| 61 | 58, 60 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = -(i · (sin‘𝐴))) |
| 62 | 55, 61 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘-𝐴) + (i · (sin‘-𝐴))) = ((cos‘𝐴) + -(i ·
(sin‘𝐴)))) |
| 63 | 53, 62 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘𝐴) + -(i · (sin‘𝐴)))) |
| 64 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
| 65 | | mulneg2 11700 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · -𝐴) = -(i · 𝐴)) |
| 66 | 7, 64, 65 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · -𝐴) = -(i · 𝐴)) |
| 67 | 66 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = (exp‘-(i · 𝐴))) |
| 68 | 26, 30 | negsubd 11626 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘𝐴) + -(i · (sin‘𝐴))) = ((cos‘𝐴) − (i ·
(sin‘𝐴)))) |
| 69 | 63, 67, 68 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴)))) |
| 70 | 69 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴))) |
| 71 | | eflog 26618 |
. . . . . . . . . . 11
⊢ (((1
− (i · (tan‘𝐴))) ∈ ℂ ∧ (1 − (i
· (tan‘𝐴)))
≠ 0) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i ·
(tan‘𝐴)))) |
| 72 | 19, 20, 71 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 − (i ·
(tan‘𝐴))))) = (1
− (i · (tan‘𝐴)))) |
| 73 | 49, 70, 72 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 − (i
· (tan‘𝐴)))))) |
| 74 | 46, 73 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(log‘(1
+ (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i
· (tan‘𝐴))))))) |
| 75 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 76 | 7, 64, 75 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
| 77 | | efcl 16118 |
. . . . . . . . . . 11
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
| 78 | 76, 77 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ) |
| 79 | 76 | negcld 11607 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(i · 𝐴) ∈ ℂ) |
| 80 | | efcl 16118 |
. . . . . . . . . . 11
⊢ (-(i
· 𝐴) ∈ ℂ
→ (exp‘-(i · 𝐴)) ∈ ℂ) |
| 81 | 79, 80 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ∈ ℂ) |
| 82 | | efne0 16133 |
. . . . . . . . . . 11
⊢ (-(i
· 𝐴) ∈ ℂ
→ (exp‘-(i · 𝐴)) ≠ 0) |
| 83 | 79, 82 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ≠ 0) |
| 84 | 78, 81, 26, 83, 1 | divcan7d 12071 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(i ·
𝐴)) / (exp‘-(i
· 𝐴)))) |
| 85 | | efsub 16136 |
. . . . . . . . . 10
⊢ (((i
· 𝐴) ∈ ℂ
∧ -(i · 𝐴)
∈ ℂ) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i ·
𝐴)))) |
| 86 | 76, 79, 85 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i ·
𝐴)))) |
| 87 | 76, 76 | subnegd 11627 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = ((i · 𝐴) + (i · 𝐴))) |
| 88 | 76 | 2timesd 12509 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴))) |
| 89 | 87, 88 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = (2 · (i · 𝐴))) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = (exp‘(2 · (i ·
𝐴)))) |
| 91 | 84, 86, 90 | 3eqtr2d 2783 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = (exp‘(2 · (i
· 𝐴)))) |
| 92 | 24, 74, 91 | 3eqtr2d 2783 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) = (exp‘(2 · (i ·
𝐴)))) |
| 93 | 92 | fveq2d 6910 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))))) = (log‘(exp‘(2 ·
(i · 𝐴))))) |
| 94 | 64 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 𝐴 ∈ ℂ) |
| 95 | 94 | renegd 15248 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
| 96 | 94 | recld 15233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) ∈
ℝ) |
| 97 | 96 | renegcld 11690 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈
ℝ) |
| 98 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) < 0) |
| 99 | 96 | lt0neg1d 11832 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘𝐴) < 0 ↔ 0 <
-(ℜ‘𝐴))) |
| 100 | 98, 99 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘𝐴)) |
| 101 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
| 102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
| 103 | 102 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴)) |
| 104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(π / 2) <
(ℜ‘𝐴)) |
| 105 | | halfpire 26506 |
. . . . . . . . . . . . . . . . 17
⊢ (π /
2) ∈ ℝ |
| 106 | | ltnegcon1 11764 |
. . . . . . . . . . . . . . . . 17
⊢ (((π /
2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (-(π / 2) <
(ℜ‘𝐴) ↔
-(ℜ‘𝐴) <
(π / 2))) |
| 107 | 105, 96, 106 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (-(π / 2) <
(ℜ‘𝐴) ↔
-(ℜ‘𝐴) <
(π / 2))) |
| 108 | 104, 107 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) < (π /
2)) |
| 109 | | 0xr 11308 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
| 110 | 105 | rexri 11319 |
. . . . . . . . . . . . . . . 16
⊢ (π /
2) ∈ ℝ* |
| 111 | | elioo2 13428 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
(-(ℜ‘𝐴) ∈
(0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 <
-(ℜ‘𝐴) ∧
-(ℜ‘𝐴) <
(π / 2)))) |
| 112 | 109, 110,
111 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢
(-(ℜ‘𝐴)
∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 <
-(ℜ‘𝐴) ∧
-(ℜ‘𝐴) <
(π / 2))) |
| 113 | 97, 100, 108, 112 | syl3anbrc 1344 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ (0(,)(π /
2))) |
| 114 | 95, 113 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) ∈ (0(,)(π /
2))) |
| 115 | | tanregt0 26581 |
. . . . . . . . . . . . 13
⊢ ((-𝐴 ∈ ℂ ∧
(ℜ‘-𝐴) ∈
(0(,)(π / 2))) → 0 < (ℜ‘(tan‘-𝐴))) |
| 116 | 51, 114, 115 | syl2an2r 685 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 <
(ℜ‘(tan‘-𝐴))) |
| 117 | | tanneg 16184 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘-𝐴) =
-(tan‘𝐴)) |
| 118 | 1, 117 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘-𝐴) = -(tan‘𝐴)) |
| 119 | 118 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘-𝐴) = -(tan‘𝐴)) |
| 120 | 119 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘-𝐴)) = (ℜ‘-(tan‘𝐴))) |
| 121 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘𝐴) ∈
ℂ) |
| 122 | 121 | renegd 15248 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘-(tan‘𝐴)) = -(ℜ‘(tan‘𝐴))) |
| 123 | 120, 122 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘-𝐴)) = -(ℜ‘(tan‘𝐴))) |
| 124 | 116, 123 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 <
-(ℜ‘(tan‘𝐴))) |
| 125 | 9 | recld 15233 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(tan‘𝐴)) ∈ ℝ) |
| 126 | 125 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘𝐴)) ∈ ℝ) |
| 127 | 126 | lt0neg1d 11832 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
((ℜ‘(tan‘𝐴)) < 0 ↔ 0 <
-(ℜ‘(tan‘𝐴)))) |
| 128 | 124, 127 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘𝐴)) < 0) |
| 129 | 128 | lt0ne0d 11828 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘𝐴)) ≠ 0) |
| 130 | | atanlogsub 26959 |
. . . . . . . . 9
⊢
(((tan‘𝐴)
∈ dom arctan ∧ (ℜ‘(tan‘𝐴)) ≠ 0) → ((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
| 131 | 3, 129, 130 | syl2an2r 685 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
| 132 | | 1re 11261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
| 133 | | ioossre 13448 |
. . . . . . . . . . . . . 14
⊢ (-1(,)1)
⊆ ℝ |
| 134 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ∈
ℂ) |
| 135 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈
ℂ) |
| 136 | | ine0 11698 |
. . . . . . . . . . . . . . . . 17
⊢ i ≠
0 |
| 137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ≠ 0) |
| 138 | | ixi 11892 |
. . . . . . . . . . . . . . . . . . 19
⊢ (i
· i) = -1 |
| 139 | 138 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
· i) · (tan‘𝐴)) = (-1 · (tan‘𝐴)) |
| 140 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘𝐴) ∈ ℂ) |
| 141 | 140 | mulm1d 11715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = -(tan‘𝐴)) |
| 142 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = -(tan‘𝐴)) |
| 143 | 141, 142 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = (tan‘-𝐴)) |
| 144 | 139, 143 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) ·
(tan‘𝐴)) =
(tan‘-𝐴)) |
| 145 | 134, 134,
140 | mulassd 11284 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) ·
(tan‘𝐴)) = (i
· (i · (tan‘𝐴)))) |
| 146 | 138 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((i
· i) · 𝐴) =
(-1 · 𝐴) |
| 147 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 𝐴 ∈ ℂ) |
| 148 | 147 | mulm1d 11715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · 𝐴) = -𝐴) |
| 149 | 146, 148 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = -𝐴) |
| 150 | 134, 134,
147 | mulassd 11284 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = (i · (i ·
𝐴))) |
| 151 | 149, 150 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -𝐴 = (i · (i · 𝐴))) |
| 152 | 151 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = (tan‘(i · (i · 𝐴)))) |
| 153 | 144, 145,
152 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (i ·
(tan‘𝐴))) =
(tan‘(i · (i · 𝐴)))) |
| 154 | 134, 135,
137, 153 | mvllmuld 12099 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) = ((tan‘(i · (i
· 𝐴))) /
i)) |
| 155 | 76 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℂ) |
| 156 | | reim 15148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) =
(ℑ‘(i · 𝐴))) |
| 157 | 156 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴))) |
| 158 | 157 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) = 0 ↔ (ℑ‘(i ·
𝐴)) = 0)) |
| 159 | 158 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (ℑ‘(i ·
𝐴)) = 0) |
| 160 | 155, 159 | reim0bd 15239 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℝ) |
| 161 | | tanhbnd 16197 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· 𝐴) ∈ ℝ
→ ((tan‘(i · (i · 𝐴))) / i) ∈ (-1(,)1)) |
| 162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((tan‘(i · (i
· 𝐴))) / i) ∈
(-1(,)1)) |
| 163 | 154, 162 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈
(-1(,)1)) |
| 164 | 133, 163 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈
ℝ) |
| 165 | | readdcl 11238 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ (i · (tan‘𝐴)) ∈ ℝ) → (1 + (i ·
(tan‘𝐴))) ∈
ℝ) |
| 166 | 132, 164,
165 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i ·
(tan‘𝐴))) ∈
ℝ) |
| 167 | | df-neg 11495 |
. . . . . . . . . . . . . 14
⊢ -1 = (0
− 1) |
| 168 | | eliooord 13446 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· (tan‘𝐴))
∈ (-1(,)1) → (-1 < (i · (tan‘𝐴)) ∧ (i · (tan‘𝐴)) < 1)) |
| 169 | 163, 168 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 < (i ·
(tan‘𝐴)) ∧ (i
· (tan‘𝐴))
< 1)) |
| 170 | 169 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -1 < (i ·
(tan‘𝐴))) |
| 171 | 167, 170 | eqbrtrrid 5179 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (0 − 1) < (i ·
(tan‘𝐴))) |
| 172 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 ∈
ℝ) |
| 173 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 1 ∈
ℝ) |
| 174 | 172, 173,
164 | ltsubadd2d 11861 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((0 − 1) < (i
· (tan‘𝐴))
↔ 0 < (1 + (i · (tan‘𝐴))))) |
| 175 | 171, 174 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 < (1 + (i ·
(tan‘𝐴)))) |
| 176 | 166, 175 | elrpd 13074 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i ·
(tan‘𝐴))) ∈
ℝ+) |
| 177 | 176 | relogcld 26665 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 + (i ·
(tan‘𝐴)))) ∈
ℝ) |
| 178 | 169 | simprd 495 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) < 1) |
| 179 | | difrp 13073 |
. . . . . . . . . . . . 13
⊢ (((i
· (tan‘𝐴))
∈ ℝ ∧ 1 ∈ ℝ) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i
· (tan‘𝐴)))
∈ ℝ+)) |
| 180 | 164, 132,
179 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i
· (tan‘𝐴)))
∈ ℝ+)) |
| 181 | 178, 180 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 − (i ·
(tan‘𝐴))) ∈
ℝ+) |
| 182 | 181 | relogcld 26665 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 − (i
· (tan‘𝐴))))
∈ ℝ) |
| 183 | 177, 182 | resubcld 11691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ) |
| 184 | | relogrn 26603 |
. . . . . . . . 9
⊢
(((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i
· (tan‘𝐴)))))
∈ ℝ → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i
· (tan‘𝐴)))))
∈ ran log) |
| 185 | 183, 184 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
| 186 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ) |
| 187 | 186 | recld 15233 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ) |
| 188 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴)) |
| 189 | 102 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2)) |
| 190 | 189 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) < (π / 2)) |
| 191 | | elioo2 13428 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
((ℜ‘𝐴) ∈
(0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2)))) |
| 192 | 109, 110,
191 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((ℜ‘𝐴)
∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 193 | 187, 188,
190, 192 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ (0(,)(π / 2))) |
| 194 | | tanregt0 26581 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴))) |
| 195 | 64, 193, 194 | syl2an2r 685 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 <
(ℜ‘(tan‘𝐴))) |
| 196 | 195 | gt0ne0d 11827 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(tan‘𝐴)) ≠ 0) |
| 197 | 3, 196, 130 | syl2an2r 685 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
| 198 | | recl 15149 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
| 199 | 198 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
| 200 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 201 | | lttri4 11345 |
. . . . . . . . 9
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 <
(ℜ‘𝐴))) |
| 202 | 199, 200,
201 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 <
(ℜ‘𝐴))) |
| 203 | 131, 185,
197, 202 | mpjao3dan 1434 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
| 204 | | logef 26623 |
. . . . . . 7
⊢
(((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i
· (tan‘𝐴)))))
∈ ran log → (log‘(exp‘((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))))) = ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) |
| 205 | 203, 204 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))))) = ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) |
| 206 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 207 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · (i
· 𝐴)) ∈
ℂ) |
| 208 | 206, 76, 207 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ℂ) |
| 209 | | picn 26501 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
| 210 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 211 | | divneg 11959 |
. . . . . . . . . . . 12
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) =
(-π / 2)) |
| 212 | 209, 206,
210, 211 | mp3an 1463 |
. . . . . . . . . . 11
⊢ -(π /
2) = (-π / 2) |
| 213 | 212, 103 | eqbrtrrid 5179 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-π / 2) < (ℜ‘𝐴)) |
| 214 | | pire 26500 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
| 215 | 214 | renegcli 11570 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ |
| 216 | 215 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π ∈ ℝ) |
| 217 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 218 | 217 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ∈ ℝ) |
| 219 | | 2pos 12369 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
| 220 | 219 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < 2) |
| 221 | | ltdivmul 12143 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 ·
(ℜ‘𝐴)))) |
| 222 | 216, 199,
218, 220, 221 | syl112anc 1376 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 ·
(ℜ‘𝐴)))) |
| 223 | 213, 222 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (2 · (ℜ‘𝐴))) |
| 224 | | immul2 15176 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(2
· (i · 𝐴))) =
(2 · (ℑ‘(i · 𝐴)))) |
| 225 | 217, 76, 224 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 ·
(ℑ‘(i · 𝐴)))) |
| 226 | 157 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) = (2 · (ℑ‘(i ·
𝐴)))) |
| 227 | 225, 226 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 ·
(ℜ‘𝐴))) |
| 228 | 223, 227 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (ℑ‘(2 · (i
· 𝐴)))) |
| 229 | | remulcl 11240 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (2 ·
(ℜ‘𝐴)) ∈
ℝ) |
| 230 | 217, 199,
229 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ∈ ℝ) |
| 231 | 214 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → π ∈ ℝ) |
| 232 | | ltmuldiv2 12142 |
. . . . . . . . . . . 12
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 <
2)) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π /
2))) |
| 233 | 199, 231,
218, 220, 232 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π /
2))) |
| 234 | 189, 233 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) < π) |
| 235 | 230, 231,
234 | ltled 11409 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ≤ π) |
| 236 | 227, 235 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) ≤ π) |
| 237 | | ellogrn 26601 |
. . . . . . . 8
⊢ ((2
· (i · 𝐴))
∈ ran log ↔ ((2 · (i · 𝐴)) ∈ ℂ ∧ -π <
(ℑ‘(2 · (i · 𝐴))) ∧ (ℑ‘(2 · (i
· 𝐴))) ≤
π)) |
| 238 | 208, 228,
236, 237 | syl3anbrc 1344 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ran log) |
| 239 | | logef 26623 |
. . . . . . 7
⊢ ((2
· (i · 𝐴))
∈ ran log → (log‘(exp‘(2 · (i · 𝐴)))) = (2 · (i ·
𝐴))) |
| 240 | 238, 239 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘(2 · (i
· 𝐴)))) = (2
· (i · 𝐴))) |
| 241 | 93, 205, 240 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) = (2 · (i · 𝐴))) |
| 242 | 241 | negeqd 11502 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) = -(2 · (i · 𝐴))) |
| 243 | 22, 242 | eqtr3d 2779 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((log‘(1 − (i ·
(tan‘𝐴)))) −
(log‘(1 + (i · (tan‘𝐴))))) = -(2 · (i · 𝐴))) |
| 244 | 243 | oveq2d 7447 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i / 2) · ((log‘(1 − (i
· (tan‘𝐴))))
− (log‘(1 + (i · (tan‘𝐴)))))) = ((i / 2) · -(2 · (i
· 𝐴)))) |
| 245 | | halfcl 12491 |
. . . . 5
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
| 246 | 7, 245 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i / 2) ∈ ℂ) |
| 247 | 206 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ∈ ℂ) |
| 248 | 246, 247,
79 | mulassd 11284 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i ·
𝐴)) = ((i / 2) · (2
· -(i · 𝐴)))) |
| 249 | 7, 206, 210 | divcan1i 12011 |
. . . . 5
⊢ ((i / 2)
· 2) = i |
| 250 | 249 | oveq1i 7441 |
. . . 4
⊢ (((i / 2)
· 2) · -(i · 𝐴)) = (i · -(i · 𝐴)) |
| 251 | 33, 33, 51 | mulassd 11284 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = (i · (i · -𝐴))) |
| 252 | 138 | oveq1i 7441 |
. . . . . 6
⊢ ((i
· i) · -𝐴) =
(-1 · -𝐴) |
| 253 | | mul2neg 11702 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (-1 · -𝐴) = (1 · 𝐴)) |
| 254 | 6, 64, 253 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = (1 · 𝐴)) |
| 255 | | mullid 11260 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 256 | 255 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
| 257 | 254, 256 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = 𝐴) |
| 258 | 252, 257 | eqtrid 2789 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = 𝐴) |
| 259 | 66 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (i · -𝐴)) = (i · -(i · 𝐴))) |
| 260 | 251, 258,
259 | 3eqtr3rd 2786 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · -(i · 𝐴)) = 𝐴) |
| 261 | 250, 260 | eqtrid 2789 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i ·
𝐴)) = 𝐴) |
| 262 | | mulneg2 11700 |
. . . . 5
⊢ ((2
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · -(i
· 𝐴)) = -(2 ·
(i · 𝐴))) |
| 263 | 206, 76, 262 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴))) |
| 264 | 263 | oveq2d 7447 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i / 2) · (2 · -(i ·
𝐴))) = ((i / 2) ·
-(2 · (i · 𝐴)))) |
| 265 | 248, 261,
264 | 3eqtr3rd 2786 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i / 2) · -(2 · (i ·
𝐴))) = 𝐴) |
| 266 | 5, 244, 265 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴) |