Proof of Theorem atantan
Step | Hyp | Ref
| Expression |
1 | | cosne0 24276 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0) |
2 | | atandmtan 24647 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) ∈
dom arctan) |
3 | 1, 2 | syldan 487 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ dom arctan) |
4 | | atanval 24611 |
. . 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 9994 |
. . . . . . 7
⊢ 1 ∈
ℂ |
7 | | ax-icn 9995 |
. . . . . . . 8
⊢ i ∈
ℂ |
8 | | tancl 14859 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) ∈
ℂ) |
9 | 1, 8 | syldan 487 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘𝐴) ∈ ℂ) |
10 | | mulcl 10020 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (tan‘𝐴) ∈ ℂ) → (i ·
(tan‘𝐴)) ∈
ℂ) |
11 | 7, 9, 10 | sylancr 695 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) ∈ ℂ) |
12 | | addcl 10018 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 + (i ·
(tan‘𝐴))) ∈
ℂ) |
13 | 6, 11, 12 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ∈
ℂ) |
14 | | atandm2 24604 |
. . . . . . . 8
⊢
((tan‘𝐴)
∈ dom arctan ↔ ((tan‘𝐴) ∈ ℂ ∧ (1 − (i
· (tan‘𝐴)))
≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0)) |
15 | 3, 14 | sylib 208 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((tan‘𝐴) ∈ ℂ ∧ (1 − (i
· (tan‘𝐴)))
≠ 0 ∧ (1 + (i · (tan‘𝐴))) ≠ 0)) |
16 | 15 | simp3d 1075 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 + (i · (tan‘𝐴))) ≠ 0) |
17 | 13, 16 | logcld 24317 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(1 + (i · (tan‘𝐴)))) ∈
ℂ) |
18 | | subcl 10280 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · (tan‘𝐴)) ∈ ℂ) → (1 − (i
· (tan‘𝐴)))
∈ ℂ) |
19 | 6, 11, 18 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ∈
ℂ) |
20 | 15 | simp2d 1074 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 − (i · (tan‘𝐴))) ≠ 0) |
21 | 19, 20 | logcld 24317 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(1 − (i ·
(tan‘𝐴)))) ∈
ℂ) |
22 | 17, 21 | negsubdi2d 10408 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) = ((log‘(1 − (i ·
(tan‘𝐴)))) −
(log‘(1 + (i · (tan‘𝐴)))))) |
23 | | efsub 14830 |
. . . . . . . . 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 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) = ((exp‘(log‘(1 + (i
· (tan‘𝐴)))))
/ (exp‘(log‘(1 − (i · (tan‘𝐴))))))) |
25 | | coscl 14857 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
26 | 25 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ) |
27 | | sincl 14856 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ) |
29 | | mulcl 10020 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
30 | 7, 28, 29 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ) |
31 | 26, 30, 26, 1 | divdird 10839 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴)))) |
32 | 26, 1 | dividd 10799 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘𝐴) / (cos‘𝐴)) = 1) |
33 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → i ∈ ℂ) |
34 | 33, 28, 26, 1 | divassd 10836 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴)))) |
35 | | tanval 14858 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
36 | 1, 35 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴))) |
37 | 36 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (tan‘𝐴)) = (i · ((sin‘𝐴) / (cos‘𝐴)))) |
38 | 34, 37 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) / (cos‘𝐴)) = (i · (tan‘𝐴))) |
39 | 32, 38 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) + ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 + (i ·
(tan‘𝐴)))) |
40 | 31, 39 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 + (i · (tan‘𝐴)))) |
41 | | efival 14882 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
42 | 41 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) |
43 | 42 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) + (i · (sin‘𝐴))) / (cos‘𝐴))) |
44 | | eflog 24323 |
. . . . . . . . . . 11
⊢ (((1 + (i
· (tan‘𝐴)))
∈ ℂ ∧ (1 + (i · (tan‘𝐴))) ≠ 0) → (exp‘(log‘(1
+ (i · (tan‘𝐴))))) = (1 + (i · (tan‘𝐴)))) |
45 | 13, 16, 44 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 + (i ·
(tan‘𝐴))))) = (1 + (i
· (tan‘𝐴)))) |
46 | 40, 43, 45 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 + (i ·
(tan‘𝐴)))))) |
47 | 26, 30, 26, 1 | divsubdird 10840 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴)))) |
48 | 32, 38 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) / (cos‘𝐴)) − ((i · (sin‘𝐴)) / (cos‘𝐴))) = (1 − (i ·
(tan‘𝐴)))) |
49 | 47, 48 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴)) = (1 − (i ·
(tan‘𝐴)))) |
50 | | negcl 10281 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ) |
52 | | efival 14882 |
. . . . . . . . . . . . . 14
⊢ (-𝐴 ∈ ℂ →
(exp‘(i · -𝐴))
= ((cos‘-𝐴) + (i
· (sin‘-𝐴)))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘-𝐴) + (i · (sin‘-𝐴)))) |
54 | | cosneg 14877 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(cos‘-𝐴) =
(cos‘𝐴)) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘-𝐴) = (cos‘𝐴)) |
56 | | sinneg 14876 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(sin‘-𝐴) =
-(sin‘𝐴)) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘-𝐴) = -(sin‘𝐴)) |
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = (i · -(sin‘𝐴))) |
59 | | mulneg2 10467 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
-(sin‘𝐴)) = -(i
· (sin‘𝐴))) |
60 | 7, 28, 59 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · -(sin‘𝐴)) = -(i · (sin‘𝐴))) |
61 | 58, 60 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘-𝐴)) = -(i · (sin‘𝐴))) |
62 | 55, 61 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘-𝐴) + (i · (sin‘-𝐴))) = ((cos‘𝐴) + -(i ·
(sin‘𝐴)))) |
63 | 53, 62 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = ((cos‘𝐴) + -(i · (sin‘𝐴)))) |
64 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
65 | | mulneg2 10467 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · -𝐴) = -(i · 𝐴)) |
66 | 7, 64, 65 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · -𝐴) = -(i · 𝐴)) |
67 | 66 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · -𝐴)) = (exp‘-(i · 𝐴))) |
68 | 26, 30 | negsubd 10398 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘𝐴) + -(i · (sin‘𝐴))) = ((cos‘𝐴) − (i ·
(sin‘𝐴)))) |
69 | 63, 67, 68 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴)))) |
70 | 69 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (((cos‘𝐴) − (i · (sin‘𝐴))) / (cos‘𝐴))) |
71 | | eflog 24323 |
. . . . . . . . . . 11
⊢ (((1
− (i · (tan‘𝐴))) ∈ ℂ ∧ (1 − (i
· (tan‘𝐴)))
≠ 0) → (exp‘(log‘(1 − (i · (tan‘𝐴))))) = (1 − (i ·
(tan‘𝐴)))) |
72 | 19, 20, 71 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(log‘(1 − (i ·
(tan‘𝐴))))) = (1
− (i · (tan‘𝐴)))) |
73 | 49, 70, 72 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘-(i · 𝐴)) / (cos‘𝐴)) = (exp‘(log‘(1 − (i
· (tan‘𝐴)))))) |
74 | 46, 73 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(log‘(1
+ (i · (tan‘𝐴))))) / (exp‘(log‘(1 − (i
· (tan‘𝐴))))))) |
75 | | mulcl 10020 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
76 | 7, 64, 75 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
77 | | efcl 14813 |
. . . . . . . . . . 11
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ) |
79 | 76 | negcld 10379 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(i · 𝐴) ∈ ℂ) |
80 | | efcl 14813 |
. . . . . . . . . . 11
⊢ (-(i
· 𝐴) ∈ ℂ
→ (exp‘-(i · 𝐴)) ∈ ℂ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ∈ ℂ) |
82 | | efne0 14827 |
. . . . . . . . . . 11
⊢ (-(i
· 𝐴) ∈ ℂ
→ (exp‘-(i · 𝐴)) ≠ 0) |
83 | 79, 82 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘-(i · 𝐴)) ≠ 0) |
84 | 78, 81, 26, 83, 1 | divcan7d 10829 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = ((exp‘(i ·
𝐴)) / (exp‘-(i
· 𝐴)))) |
85 | | efsub 14830 |
. . . . . . . . . 10
⊢ (((i
· 𝐴) ∈ ℂ
∧ -(i · 𝐴)
∈ ℂ) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i ·
𝐴)))) |
86 | 76, 79, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = ((exp‘(i · 𝐴)) / (exp‘-(i ·
𝐴)))) |
87 | 76, 76 | subnegd 10399 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = ((i · 𝐴) + (i · 𝐴))) |
88 | 76 | 2timesd 11275 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴))) |
89 | 87, 88 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · 𝐴) − -(i · 𝐴)) = (2 · (i · 𝐴))) |
90 | 89 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((i · 𝐴) − -(i · 𝐴))) = (exp‘(2 · (i ·
𝐴)))) |
91 | 84, 86, 90 | 3eqtr2d 2662 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) / (cos‘𝐴)) / ((exp‘-(i · 𝐴)) / (cos‘𝐴))) = (exp‘(2 · (i
· 𝐴)))) |
92 | 24, 74, 91 | 3eqtr2d 2662 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) = (exp‘(2 · (i ·
𝐴)))) |
93 | 92 | fveq2d 6195 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))))) = (log‘(exp‘(2 ·
(i · 𝐴))))) |
94 | 3 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘𝐴) ∈ dom
arctan) |
95 | 51 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -𝐴 ∈ ℂ) |
96 | 64 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 𝐴 ∈ ℂ) |
97 | 96 | renegd 13949 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
98 | 96 | recld 13934 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) ∈
ℝ) |
99 | 98 | renegcld 10457 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈
ℝ) |
100 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘𝐴) < 0) |
101 | 98 | lt0neg1d 10597 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((ℜ‘𝐴) < 0 ↔ 0 <
-(ℜ‘𝐴))) |
102 | 100, 101 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 < -(ℜ‘𝐴)) |
103 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
105 | 104 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴)) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(π / 2) <
(ℜ‘𝐴)) |
107 | | halfpire 24216 |
. . . . . . . . . . . . . . . . 17
⊢ (π /
2) ∈ ℝ |
108 | | ltnegcon1 10529 |
. . . . . . . . . . . . . . . . 17
⊢ (((π /
2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (-(π / 2) <
(ℜ‘𝐴) ↔
-(ℜ‘𝐴) <
(π / 2))) |
109 | 107, 98, 108 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (-(π / 2) <
(ℜ‘𝐴) ↔
-(ℜ‘𝐴) <
(π / 2))) |
110 | 106, 109 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) < (π /
2)) |
111 | | 0xr 10086 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
112 | 107 | rexri 10097 |
. . . . . . . . . . . . . . . 16
⊢ (π /
2) ∈ ℝ* |
113 | | elioo2 12216 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
(-(ℜ‘𝐴) ∈
(0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 <
-(ℜ‘𝐴) ∧
-(ℜ‘𝐴) <
(π / 2)))) |
114 | 111, 112,
113 | mp2an 708 |
. . . . . . . . . . . . . . 15
⊢
(-(ℜ‘𝐴)
∈ (0(,)(π / 2)) ↔ (-(ℜ‘𝐴) ∈ ℝ ∧ 0 <
-(ℜ‘𝐴) ∧
-(ℜ‘𝐴) <
(π / 2))) |
115 | 99, 102, 110, 114 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → -(ℜ‘𝐴) ∈ (0(,)(π /
2))) |
116 | 97, 115 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (ℜ‘-𝐴) ∈ (0(,)(π /
2))) |
117 | | tanregt0 24285 |
. . . . . . . . . . . . 13
⊢ ((-𝐴 ∈ ℂ ∧
(ℜ‘-𝐴) ∈
(0(,)(π / 2))) → 0 < (ℜ‘(tan‘-𝐴))) |
118 | 95, 116, 117 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 <
(ℜ‘(tan‘-𝐴))) |
119 | | tanneg 14878 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘-𝐴) =
-(tan‘𝐴)) |
120 | 1, 119 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (tan‘-𝐴) = -(tan‘𝐴)) |
121 | 120 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘-𝐴) = -(tan‘𝐴)) |
122 | 121 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘-𝐴)) = (ℜ‘-(tan‘𝐴))) |
123 | 9 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → (tan‘𝐴) ∈
ℂ) |
124 | 123 | renegd 13949 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘-(tan‘𝐴)) = -(ℜ‘(tan‘𝐴))) |
125 | 122, 124 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘-𝐴)) = -(ℜ‘(tan‘𝐴))) |
126 | 118, 125 | breqtrd 4679 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → 0 <
-(ℜ‘(tan‘𝐴))) |
127 | 9 | recld 13934 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(tan‘𝐴)) ∈ ℝ) |
128 | 127 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘𝐴)) ∈ ℝ) |
129 | 128 | lt0neg1d 10597 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
((ℜ‘(tan‘𝐴)) < 0 ↔ 0 <
-(ℜ‘(tan‘𝐴)))) |
130 | 126, 129 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘𝐴)) < 0) |
131 | 130 | lt0ne0d 10593 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) →
(ℜ‘(tan‘𝐴)) ≠ 0) |
132 | | atanlogsub 24643 |
. . . . . . . . 9
⊢
(((tan‘𝐴)
∈ dom arctan ∧ (ℜ‘(tan‘𝐴)) ≠ 0) → ((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
133 | 94, 131, 132 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) < 0) → ((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
134 | | 1re 10039 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
135 | | ioossre 12235 |
. . . . . . . . . . . . . 14
⊢ (-1(,)1)
⊆ ℝ |
136 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ∈
ℂ) |
137 | 11 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈
ℂ) |
138 | | ine0 10465 |
. . . . . . . . . . . . . . . . 17
⊢ i ≠
0 |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → i ≠ 0) |
140 | | ixi 10656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (i
· i) = -1 |
141 | 140 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
· i) · (tan‘𝐴)) = (-1 · (tan‘𝐴)) |
142 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘𝐴) ∈ ℂ) |
143 | 142 | mulm1d 10482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = -(tan‘𝐴)) |
144 | 120 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = -(tan‘𝐴)) |
145 | 143, 144 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · (tan‘𝐴)) = (tan‘-𝐴)) |
146 | 141, 145 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) ·
(tan‘𝐴)) =
(tan‘-𝐴)) |
147 | 136, 136,
142 | mulassd 10063 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) ·
(tan‘𝐴)) = (i
· (i · (tan‘𝐴)))) |
148 | 140 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((i
· i) · 𝐴) =
(-1 · 𝐴) |
149 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 𝐴 ∈ ℂ) |
150 | 149 | mulm1d 10482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 · 𝐴) = -𝐴) |
151 | 148, 150 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = -𝐴) |
152 | 136, 136,
149 | mulassd 10063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · i) · 𝐴) = (i · (i ·
𝐴))) |
153 | 151, 152 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -𝐴 = (i · (i · 𝐴))) |
154 | 153 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (tan‘-𝐴) = (tan‘(i · (i · 𝐴)))) |
155 | 146, 147,
154 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (i ·
(tan‘𝐴))) =
(tan‘(i · (i · 𝐴)))) |
156 | 136, 137,
139, 155 | mvllmuld 10857 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) = ((tan‘(i · (i
· 𝐴))) /
i)) |
157 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℂ) |
158 | | reim 13849 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) =
(ℑ‘(i · 𝐴))) |
159 | 158 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) = (ℑ‘(i · 𝐴))) |
160 | 159 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) = 0 ↔ (ℑ‘(i ·
𝐴)) = 0)) |
161 | 160 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (ℑ‘(i ·
𝐴)) = 0) |
162 | 157, 161 | reim0bd 13940 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · 𝐴) ∈ ℝ) |
163 | | tanhbnd 14891 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· 𝐴) ∈ ℝ
→ ((tan‘(i · (i · 𝐴))) / i) ∈ (-1(,)1)) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((tan‘(i · (i
· 𝐴))) / i) ∈
(-1(,)1)) |
165 | 156, 164 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈
(-1(,)1)) |
166 | 135, 165 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) ∈
ℝ) |
167 | | readdcl 10019 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ (i · (tan‘𝐴)) ∈ ℝ) → (1 + (i ·
(tan‘𝐴))) ∈
ℝ) |
168 | 134, 166,
167 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i ·
(tan‘𝐴))) ∈
ℝ) |
169 | | df-neg 10269 |
. . . . . . . . . . . . . 14
⊢ -1 = (0
− 1) |
170 | | eliooord 12233 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· (tan‘𝐴))
∈ (-1(,)1) → (-1 < (i · (tan‘𝐴)) ∧ (i · (tan‘𝐴)) < 1)) |
171 | 165, 170 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (-1 < (i ·
(tan‘𝐴)) ∧ (i
· (tan‘𝐴))
< 1)) |
172 | 171 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → -1 < (i ·
(tan‘𝐴))) |
173 | 169, 172 | syl5eqbrr 4689 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (0 − 1) < (i ·
(tan‘𝐴))) |
174 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 ∈
ℝ) |
175 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 1 ∈
ℝ) |
176 | 174, 175,
166 | ltsubadd2d 10625 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((0 − 1) < (i
· (tan‘𝐴))
↔ 0 < (1 + (i · (tan‘𝐴))))) |
177 | 173, 176 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → 0 < (1 + (i ·
(tan‘𝐴)))) |
178 | 168, 177 | elrpd 11869 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 + (i ·
(tan‘𝐴))) ∈
ℝ+) |
179 | 178 | relogcld 24369 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 + (i ·
(tan‘𝐴)))) ∈
ℝ) |
180 | 171 | simprd 479 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (i · (tan‘𝐴)) < 1) |
181 | | difrp 11868 |
. . . . . . . . . . . . 13
⊢ (((i
· (tan‘𝐴))
∈ ℝ ∧ 1 ∈ ℝ) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i
· (tan‘𝐴)))
∈ ℝ+)) |
182 | 166, 134,
181 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((i · (tan‘𝐴)) < 1 ↔ (1 − (i
· (tan‘𝐴)))
∈ ℝ+)) |
183 | 180, 182 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (1 − (i ·
(tan‘𝐴))) ∈
ℝ+) |
184 | 183 | relogcld 24369 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → (log‘(1 − (i
· (tan‘𝐴))))
∈ ℝ) |
185 | 179, 184 | resubcld 10458 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ℝ) |
186 | | relogrn 24308 |
. . . . . . . . 9
⊢
(((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i
· (tan‘𝐴)))))
∈ ℝ → ((log‘(1 + (i · (tan‘𝐴)))) − (log‘(1 − (i
· (tan‘𝐴)))))
∈ ran log) |
187 | 185, 186 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ (ℜ‘𝐴) = 0) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
188 | 3 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (tan‘𝐴) ∈ dom arctan) |
189 | 64 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ) |
190 | 189 | recld 13934 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ) |
191 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴)) |
192 | 104 | simprd 479 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2)) |
193 | 192 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) < (π / 2)) |
194 | | elioo2 12216 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
((ℜ‘𝐴) ∈
(0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2)))) |
195 | 111, 112,
194 | mp2an 708 |
. . . . . . . . . . . 12
⊢
((ℜ‘𝐴)
∈ (0(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ 0 <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
196 | 190, 191,
193, 195 | syl3anbrc 1246 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ (0(,)(π / 2))) |
197 | | tanregt0 24285 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴))) |
198 | 189, 196,
197 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → 0 <
(ℜ‘(tan‘𝐴))) |
199 | 198 | gt0ne0d 10592 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(tan‘𝐴)) ≠ 0) |
200 | 188, 199,
132 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) ∧ 0 < (ℜ‘𝐴)) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
201 | | recl 13850 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
202 | 201 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
203 | | 0re 10040 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
204 | | lttri4 10122 |
. . . . . . . . 9
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 <
(ℜ‘𝐴))) |
205 | 202, 203,
204 | sylancl 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) < 0 ∨ (ℜ‘𝐴) = 0 ∨ 0 <
(ℜ‘𝐴))) |
206 | 133, 187,
200, 205 | mpjao3dan 1395 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) ∈ ran log) |
207 | | logef 24328 |
. . . . . . 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‘𝐴)))))) |
208 | 206, 207 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘((log‘(1 + (i
· (tan‘𝐴))))
− (log‘(1 − (i · (tan‘𝐴))))))) = ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴)))))) |
209 | | 2cn 11091 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
210 | | mulcl 10020 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · (i
· 𝐴)) ∈
ℂ) |
211 | 209, 76, 210 | sylancr 695 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ℂ) |
212 | | picn 24211 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
213 | | 2ne0 11113 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
214 | | divneg 10719 |
. . . . . . . . . . . 12
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) =
(-π / 2)) |
215 | 212, 209,
213, 214 | mp3an 1424 |
. . . . . . . . . . 11
⊢ -(π /
2) = (-π / 2) |
216 | 215, 105 | syl5eqbrr 4689 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-π / 2) < (ℜ‘𝐴)) |
217 | | pire 24210 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
218 | 217 | renegcli 10342 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ |
219 | 218 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π ∈ ℝ) |
220 | | 2re 11090 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
221 | 220 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ∈ ℝ) |
222 | | 2pos 11112 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
223 | 222 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < 2) |
224 | | ltdivmul 10898 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 ·
(ℜ‘𝐴)))) |
225 | 219, 202,
221, 223, 224 | syl112anc 1330 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-π / 2) < (ℜ‘𝐴) ↔ -π < (2 ·
(ℜ‘𝐴)))) |
226 | 216, 225 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (2 · (ℜ‘𝐴))) |
227 | | immul2 13877 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (i · 𝐴) ∈ ℂ) → (ℑ‘(2
· (i · 𝐴))) =
(2 · (ℑ‘(i · 𝐴)))) |
228 | 220, 76, 227 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 ·
(ℑ‘(i · 𝐴)))) |
229 | 159 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) = (2 · (ℑ‘(i ·
𝐴)))) |
230 | 228, 229 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) = (2 ·
(ℜ‘𝐴))) |
231 | 226, 230 | breqtrrd 4681 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (ℑ‘(2 · (i
· 𝐴)))) |
232 | | remulcl 10021 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (2 ·
(ℜ‘𝐴)) ∈
ℝ) |
233 | 220, 202,
232 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ∈ ℝ) |
234 | 217 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → π ∈ ℝ) |
235 | | ltmuldiv2 10897 |
. . . . . . . . . . . 12
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 <
2)) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π /
2))) |
236 | 202, 234,
221, 223, 235 | syl112anc 1330 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((2 · (ℜ‘𝐴)) < π ↔ (ℜ‘𝐴) < (π /
2))) |
237 | 192, 236 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) < π) |
238 | 233, 234,
237 | ltled 10185 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (ℜ‘𝐴)) ≤ π) |
239 | 230, 238 | eqbrtrd 4675 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(2 · (i · 𝐴))) ≤ π) |
240 | | ellogrn 24306 |
. . . . . . . 8
⊢ ((2
· (i · 𝐴))
∈ ran log ↔ ((2 · (i · 𝐴)) ∈ ℂ ∧ -π <
(ℑ‘(2 · (i · 𝐴))) ∧ (ℑ‘(2 · (i
· 𝐴))) ≤
π)) |
241 | 211, 231,
239, 240 | syl3anbrc 1246 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · 𝐴)) ∈ ran log) |
242 | | logef 24328 |
. . . . . . 7
⊢ ((2
· (i · 𝐴))
∈ ran log → (log‘(exp‘(2 · (i · 𝐴)))) = (2 · (i ·
𝐴))) |
243 | 241, 242 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘(2 · (i
· 𝐴)))) = (2
· (i · 𝐴))) |
244 | 93, 208, 243 | 3eqtr3d 2664 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) = (2 · (i · 𝐴))) |
245 | 244 | negeqd 10275 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -((log‘(1 + (i ·
(tan‘𝐴)))) −
(log‘(1 − (i · (tan‘𝐴))))) = -(2 · (i · 𝐴))) |
246 | 22, 245 | eqtr3d 2658 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((log‘(1 − (i ·
(tan‘𝐴)))) −
(log‘(1 + (i · (tan‘𝐴))))) = -(2 · (i · 𝐴))) |
247 | 246 | oveq2d 6666 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i / 2) · ((log‘(1 − (i
· (tan‘𝐴))))
− (log‘(1 + (i · (tan‘𝐴)))))) = ((i / 2) · -(2 · (i
· 𝐴)))) |
248 | | halfcl 11257 |
. . . . 5
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
249 | 7, 248 | mp1i 13 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i / 2) ∈ ℂ) |
250 | 209 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ∈ ℂ) |
251 | 249, 250,
79 | mulassd 10063 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i ·
𝐴)) = ((i / 2) · (2
· -(i · 𝐴)))) |
252 | 7, 209, 213 | divcan1i 10769 |
. . . . 5
⊢ ((i / 2)
· 2) = i |
253 | 252 | oveq1i 6660 |
. . . 4
⊢ (((i / 2)
· 2) · -(i · 𝐴)) = (i · -(i · 𝐴)) |
254 | 33, 33, 51 | mulassd 10063 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = (i · (i · -𝐴))) |
255 | 140 | oveq1i 6660 |
. . . . . 6
⊢ ((i
· i) · -𝐴) =
(-1 · -𝐴) |
256 | | mul2neg 10469 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (-1 · -𝐴) = (1 · 𝐴)) |
257 | 6, 64, 256 | sylancr 695 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = (1 · 𝐴)) |
258 | | mulid2 10038 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
259 | 258 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
260 | 257, 259 | eqtrd 2656 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-1 · -𝐴) = 𝐴) |
261 | 255, 260 | syl5eq 2668 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · i) · -𝐴) = 𝐴) |
262 | 66 | oveq2d 6666 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (i · -𝐴)) = (i · -(i · 𝐴))) |
263 | 254, 261,
262 | 3eqtr3rd 2665 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · -(i · 𝐴)) = 𝐴) |
264 | 253, 263 | syl5eq 2668 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((i / 2) · 2) · -(i ·
𝐴)) = 𝐴) |
265 | | mulneg2 10467 |
. . . . 5
⊢ ((2
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · -(i
· 𝐴)) = -(2 ·
(i · 𝐴))) |
266 | 209, 76, 265 | sylancr 695 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · -(i · 𝐴)) = -(2 · (i · 𝐴))) |
267 | 266 | oveq2d 6666 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i / 2) · (2 · -(i ·
𝐴))) = ((i / 2) ·
-(2 · (i · 𝐴)))) |
268 | 251, 264,
267 | 3eqtr3rd 2665 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i / 2) · -(2 · (i ·
𝐴))) = 𝐴) |
269 | 5, 247, 268 | 3eqtrd 2660 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴) |