Proof of Theorem tanregt0
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 10673 |
. . . . . . 7
⊢ 1 ∈
ℂ |
2 | | recl 14559 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
3 | 2 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
4 | 3 | recnd 10747 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘𝐴) ∈ ℂ) |
5 | 3 | rered 14673 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(ℜ‘𝐴)) = (ℜ‘𝐴)) |
6 | | neghalfpire 25210 |
. . . . . . . . . . . . . 14
⊢ -(π /
2) ∈ ℝ |
7 | 6 | rexri 10777 |
. . . . . . . . . . . . 13
⊢ -(π /
2) ∈ ℝ* |
8 | | 0re 10721 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
9 | | pirp 25206 |
. . . . . . . . . . . . . . . 16
⊢ π
∈ ℝ+ |
10 | | rphalfcl 12499 |
. . . . . . . . . . . . . . . 16
⊢ (π
∈ ℝ+ → (π / 2) ∈
ℝ+) |
11 | | rpgt0 12484 |
. . . . . . . . . . . . . . . 16
⊢ ((π /
2) ∈ ℝ+ → 0 < (π / 2)) |
12 | 9, 10, 11 | mp2b 10 |
. . . . . . . . . . . . . . 15
⊢ 0 <
(π / 2) |
13 | | halfpire 25209 |
. . . . . . . . . . . . . . . 16
⊢ (π /
2) ∈ ℝ |
14 | | lt0neg2 11225 |
. . . . . . . . . . . . . . . 16
⊢ ((π /
2) ∈ ℝ → (0 < (π / 2) ↔ -(π / 2) <
0)) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (0 <
(π / 2) ↔ -(π / 2) < 0) |
16 | 12, 15 | mpbi 233 |
. . . . . . . . . . . . . 14
⊢ -(π /
2) < 0 |
17 | 6, 8, 16 | ltleii 10841 |
. . . . . . . . . . . . 13
⊢ -(π /
2) ≤ 0 |
18 | | iooss1 12856 |
. . . . . . . . . . . . 13
⊢ ((-(π
/ 2) ∈ ℝ* ∧ -(π / 2) ≤ 0) → (0(,)(π /
2)) ⊆ (-(π / 2)(,)(π / 2))) |
19 | 7, 17, 18 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(0(,)(π / 2)) ⊆ (-(π / 2)(,)(π / 2)) |
20 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘𝐴) ∈ (0(,)(π / 2))) |
21 | 19, 20 | sseldi 3875 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘𝐴) ∈ (-(π / 2)(,)(π /
2))) |
22 | 5, 21 | eqeltrd 2833 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(ℜ‘𝐴)) ∈ (-(π / 2)(,)(π /
2))) |
23 | | cosne0 25273 |
. . . . . . . . . 10
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (ℜ‘(ℜ‘𝐴)) ∈ (-(π / 2)(,)(π / 2))) →
(cos‘(ℜ‘𝐴)) ≠ 0) |
24 | 4, 22, 23 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (cos‘(ℜ‘𝐴)) ≠ 0) |
25 | 4, 24 | tancld 15577 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘(ℜ‘𝐴)) ∈ ℂ) |
26 | | ax-icn 10674 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
27 | | imcl 14560 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
28 | 27 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘𝐴) ∈ ℝ) |
29 | 28 | recnd 10747 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘𝐴) ∈ ℂ) |
30 | | mulcl 10699 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
31 | 26, 29, 30 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (i · (ℑ‘𝐴)) ∈ ℂ) |
32 | | rpcoshcl 15602 |
. . . . . . . . . . 11
⊢
((ℑ‘𝐴)
∈ ℝ → (cos‘(i · (ℑ‘𝐴))) ∈
ℝ+) |
33 | 28, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (cos‘(i · (ℑ‘𝐴))) ∈
ℝ+) |
34 | 33 | rpne0d 12519 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (cos‘(i · (ℑ‘𝐴))) ≠ 0) |
35 | 31, 34 | tancld 15577 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘(i · (ℑ‘𝐴))) ∈
ℂ) |
36 | 25, 35 | mulcld 10739 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) |
37 | | subcl 10963 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) → (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))
∈ ℂ) |
38 | 1, 36, 37 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))
∈ ℂ) |
39 | | replim 14565 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
40 | 39 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 𝐴
= ((ℜ‘𝐴) + (i
· (ℑ‘𝐴)))) |
41 | 40 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (cos‘𝐴) = (cos‘((ℜ‘𝐴) + (i ·
(ℑ‘𝐴))))) |
42 | | cosne0 25273 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ≠ 0) |
43 | 21, 42 | syldan 594 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (cos‘𝐴) ≠ 0) |
44 | 41, 43 | eqnetrrd 3002 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (cos‘((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) ≠ 0) |
45 | | tanaddlem 15611 |
. . . . . . . . . 10
⊢
((((ℜ‘𝐴)
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ) ∧
((cos‘(ℜ‘𝐴)) ≠ 0 ∧ (cos‘(i ·
(ℑ‘𝐴))) ≠
0)) → ((cos‘((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) ≠ 0 ↔
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ≠
1)) |
46 | 4, 31, 24, 34, 45 | syl22anc 838 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((cos‘((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) ≠ 0 ↔
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ≠
1)) |
47 | 44, 46 | mpbid 235 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ≠
1) |
48 | 47 | necomd 2989 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 1 ≠ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) |
49 | | subeq0 10990 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) → ((1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) = 0
↔ 1 = ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) |
50 | 49 | necon3bid 2978 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) → ((1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) ≠
0 ↔ 1 ≠ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) |
51 | 1, 36, 50 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))) ≠ 0 ↔ 1 ≠
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) |
52 | 48, 51 | mpbird 260 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) ≠
0) |
53 | 38, 52 | absrpcld 14898 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) ∈
ℝ+) |
54 | | 2z 12095 |
. . . . 5
⊢ 2 ∈
ℤ |
55 | | rpexpcl 13540 |
. . . . 5
⊢
(((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
∈ ℝ+ ∧ 2 ∈ ℤ) → ((abs‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2) ∈
ℝ+) |
56 | 53, 54, 55 | sylancl 589 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))↑2) ∈
ℝ+) |
57 | 56 | rprecred 12525 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ∈
ℝ) |
58 | 38 | cjcld 14645 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
∈ ℂ) |
59 | 25, 35 | addcld 10738 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) |
60 | 58, 59 | mulcld 10739 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))
∈ ℂ) |
61 | 60 | recld 14643 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))
∈ ℝ) |
62 | 56 | rpreccld 12524 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ∈
ℝ+) |
63 | 62 | rpgt0d 12517 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2))) |
64 | 3, 24 | retancld 15590 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘(ℜ‘𝐴)) ∈ ℝ) |
65 | | 1re 10719 |
. . . . . 6
⊢ 1 ∈
ℝ |
66 | | retanhcl 15604 |
. . . . . . . 8
⊢
((ℑ‘𝐴)
∈ ℝ → ((tan‘(i · (ℑ‘𝐴))) / i) ∈ ℝ) |
67 | 28, 66 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(i · (ℑ‘𝐴))) / i) ∈
ℝ) |
68 | 67 | resqcld 13703 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(i · (ℑ‘𝐴))) / i)↑2) ∈
ℝ) |
69 | | resubcl 11028 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ (((tan‘(i · (ℑ‘𝐴))) / i)↑2) ∈ ℝ) → (1
− (((tan‘(i · (ℑ‘𝐴))) / i)↑2)) ∈
ℝ) |
70 | 65, 68, 69 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 − (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2)) ∈ ℝ) |
71 | | tanrpcl 25249 |
. . . . . . 7
⊢
((ℜ‘𝐴)
∈ (0(,)(π / 2)) → (tan‘(ℜ‘𝐴)) ∈
ℝ+) |
72 | 71 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘(ℜ‘𝐴)) ∈
ℝ+) |
73 | 72 | rpgt0d 12517 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (tan‘(ℜ‘𝐴))) |
74 | | absresq 14752 |
. . . . . . . 8
⊢
(((tan‘(i · (ℑ‘𝐴))) / i) ∈ ℝ →
((abs‘((tan‘(i · (ℑ‘𝐴))) / i))↑2) = (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2)) |
75 | 67, 74 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘((tan‘(i ·
(ℑ‘𝐴))) /
i))↑2) = (((tan‘(i · (ℑ‘𝐴))) / i)↑2)) |
76 | | tanhbnd 15606 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝐴)
∈ ℝ → ((tan‘(i · (ℑ‘𝐴))) / i) ∈ (-1(,)1)) |
77 | 28, 76 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(i · (ℑ‘𝐴))) / i) ∈
(-1(,)1)) |
78 | | eliooord 12880 |
. . . . . . . . . . 11
⊢
(((tan‘(i · (ℑ‘𝐴))) / i) ∈ (-1(,)1) → (-1 <
((tan‘(i · (ℑ‘𝐴))) / i) ∧ ((tan‘(i ·
(ℑ‘𝐴))) / i)
< 1)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (-1 < ((tan‘(i · (ℑ‘𝐴))) / i) ∧ ((tan‘(i
· (ℑ‘𝐴))) / i) < 1)) |
80 | | abslt 14764 |
. . . . . . . . . . 11
⊢
((((tan‘(i · (ℑ‘𝐴))) / i) ∈ ℝ ∧ 1 ∈
ℝ) → ((abs‘((tan‘(i · (ℑ‘𝐴))) / i)) < 1 ↔ (-1 <
((tan‘(i · (ℑ‘𝐴))) / i) ∧ ((tan‘(i ·
(ℑ‘𝐴))) / i)
< 1))) |
81 | 67, 65, 80 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘((tan‘(i ·
(ℑ‘𝐴))) / i))
< 1 ↔ (-1 < ((tan‘(i · (ℑ‘𝐴))) / i) ∧ ((tan‘(i ·
(ℑ‘𝐴))) / i)
< 1))) |
82 | 79, 81 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (abs‘((tan‘(i ·
(ℑ‘𝐴))) / i))
< 1) |
83 | 67 | recnd 10747 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(i · (ℑ‘𝐴))) / i) ∈
ℂ) |
84 | 83 | abscld 14886 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (abs‘((tan‘(i ·
(ℑ‘𝐴))) / i))
∈ ℝ) |
85 | 65 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 1 ∈ ℝ) |
86 | 83 | absge0d 14894 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 ≤ (abs‘((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
87 | | 0le1 11241 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
88 | 87 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 ≤ 1) |
89 | 84, 85, 86, 88 | lt2sqd 13711 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘((tan‘(i ·
(ℑ‘𝐴))) / i))
< 1 ↔ ((abs‘((tan‘(i · (ℑ‘𝐴))) / i))↑2) <
(1↑2))) |
90 | 82, 89 | mpbid 235 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘((tan‘(i ·
(ℑ‘𝐴))) /
i))↑2) < (1↑2)) |
91 | | sq1 13650 |
. . . . . . . 8
⊢
(1↑2) = 1 |
92 | 90, 91 | breqtrdi 5071 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘((tan‘(i ·
(ℑ‘𝐴))) /
i))↑2) < 1) |
93 | 75, 92 | eqbrtrrd 5054 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(i · (ℑ‘𝐴))) / i)↑2) <
1) |
94 | | posdif 11211 |
. . . . . . 7
⊢
(((((tan‘(i · (ℑ‘𝐴))) / i)↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((((tan‘(i · (ℑ‘𝐴))) / i)↑2) < 1 ↔ 0
< (1 − (((tan‘(i · (ℑ‘𝐴))) / i)↑2)))) |
95 | 68, 65, 94 | sylancl 589 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((((tan‘(i · (ℑ‘𝐴))) / i)↑2) < 1 ↔ 0
< (1 − (((tan‘(i · (ℑ‘𝐴))) / i)↑2)))) |
96 | 93, 95 | mpbid 235 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (1 − (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2))) |
97 | 64, 70, 73, 96 | mulgt0d 10873 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < ((tan‘(ℜ‘𝐴)) · (1 − (((tan‘(i
· (ℑ‘𝐴))) / i)↑2)))) |
98 | 38 | recjd 14653 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) =
(ℜ‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) |
99 | | resub 14576 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) → (ℜ‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) = ((ℜ‘1) −
(ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) |
100 | 1, 36, 99 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
((ℜ‘1) − (ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))) |
101 | | re1 14603 |
. . . . . . . . . . 11
⊢
(ℜ‘1) = 1 |
102 | 101 | oveq1i 7180 |
. . . . . . . . . 10
⊢
((ℜ‘1) − (ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) = (1 −
(ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) |
103 | 64, 35 | remul2d 14676 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))) = ((tan‘(ℜ‘𝐴)) ·
(ℜ‘(tan‘(i · (ℑ‘𝐴)))))) |
104 | | negicn 10965 |
. . . . . . . . . . . . . . . . . 18
⊢ -i ∈
ℂ |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → -i ∈ ℂ) |
106 | | ine0 11153 |
. . . . . . . . . . . . . . . . . . 19
⊢ i ≠
0 |
107 | 26, 106 | negne0i 11039 |
. . . . . . . . . . . . . . . . . 18
⊢ -i ≠
0 |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → -i ≠ 0) |
109 | 35, 105, 108 | divcld 11494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(i · (ℑ‘𝐴))) / -i) ∈
ℂ) |
110 | | imre 14557 |
. . . . . . . . . . . . . . . 16
⊢
(((tan‘(i · (ℑ‘𝐴))) / -i) ∈ ℂ →
(ℑ‘((tan‘(i · (ℑ‘𝐴))) / -i)) = (ℜ‘(-i ·
((tan‘(i · (ℑ‘𝐴))) / -i)))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(i ·
(ℑ‘𝐴))) / -i))
= (ℜ‘(-i · ((tan‘(i · (ℑ‘𝐴))) / -i)))) |
112 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → i ∈ ℂ) |
113 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → i ≠ 0) |
114 | 35, 112, 113 | divneg2d 11508 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → -((tan‘(i · (ℑ‘𝐴))) / i) = ((tan‘(i
· (ℑ‘𝐴))) / -i)) |
115 | 67 | renegcld 11145 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → -((tan‘(i · (ℑ‘𝐴))) / i) ∈
ℝ) |
116 | 114, 115 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(i · (ℑ‘𝐴))) / -i) ∈
ℝ) |
117 | 116 | reim0d 14674 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(i ·
(ℑ‘𝐴))) / -i))
= 0) |
118 | 35, 105, 108 | divcan2d 11496 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (-i · ((tan‘(i ·
(ℑ‘𝐴))) / -i))
= (tan‘(i · (ℑ‘𝐴)))) |
119 | 118 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(-i · ((tan‘(i ·
(ℑ‘𝐴))) / -i)))
= (ℜ‘(tan‘(i · (ℑ‘𝐴))))) |
120 | 111, 117,
119 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(tan‘(i ·
(ℑ‘𝐴)))) =
0) |
121 | 120 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · (ℜ‘(tan‘(i
· (ℑ‘𝐴))))) = ((tan‘(ℜ‘𝐴)) · 0)) |
122 | 25 | mul01d 10917 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · 0) = 0) |
123 | 103, 121,
122 | 3eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))) = 0) |
124 | 123 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 −
(ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) = (1
− 0)) |
125 | | 1m0e1 11837 |
. . . . . . . . . . 11
⊢ (1
− 0) = 1 |
126 | 124, 125 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 −
(ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
1) |
127 | 102, 126 | syl5eq 2785 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((ℜ‘1) −
(ℜ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
1) |
128 | 98, 100, 127 | 3eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) =
1) |
129 | 35, 112, 113 | divcan2d 11496 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (i · ((tan‘(i ·
(ℑ‘𝐴))) / i)) =
(tan‘(i · (ℑ‘𝐴)))) |
130 | 129 | oveq2d 7186 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) + (i · ((tan‘(i ·
(ℑ‘𝐴))) / i)))
= ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) |
131 | 130 | fveq2d 6678 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((tan‘(ℜ‘𝐴)) + (i · ((tan‘(i
· (ℑ‘𝐴))) / i)))) =
(ℜ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) |
132 | 64, 67 | crred 14680 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((tan‘(ℜ‘𝐴)) + (i · ((tan‘(i
· (ℑ‘𝐴))) / i)))) = (tan‘(ℜ‘𝐴))) |
133 | 131, 132 | eqtr3d 2775 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) =
(tan‘(ℜ‘𝐴))) |
134 | 128, 133 | oveq12d 7188 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((ℜ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℜ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) = (1
· (tan‘(ℜ‘𝐴)))) |
135 | | mulcom 10701 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ (tan‘(ℜ‘𝐴)) ∈ ℂ) → (1 ·
(tan‘(ℜ‘𝐴))) = ((tan‘(ℜ‘𝐴)) · 1)) |
136 | 1, 25, 135 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 · (tan‘(ℜ‘𝐴))) = ((tan‘(ℜ‘𝐴)) · 1)) |
137 | 134, 136 | eqtrd 2773 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((ℜ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℜ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) =
((tan‘(ℜ‘𝐴)) · 1)) |
138 | 25, 83, 83 | mulassd 10742 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) / i))
· ((tan‘(i · (ℑ‘𝐴))) / i)) = ((tan‘(ℜ‘𝐴)) · (((tan‘(i
· (ℑ‘𝐴))) / i) · ((tan‘(i ·
(ℑ‘𝐴))) /
i)))) |
139 | 38 | imcjd 14654 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) =
-(ℑ‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) |
140 | | imsub 14584 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))) ∈
ℂ) → (ℑ‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) = ((ℑ‘1) −
(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) |
141 | 1, 36, 140 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
((ℑ‘1) − (ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))) |
142 | | im1 14604 |
. . . . . . . . . . . . . 14
⊢
(ℑ‘1) = 0 |
143 | 142 | oveq1i 7180 |
. . . . . . . . . . . . 13
⊢
((ℑ‘1) −
(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) = (0
− (ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) |
144 | | df-neg 10951 |
. . . . . . . . . . . . 13
⊢
-(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) = (0
− (ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) |
145 | 143, 144 | eqtr4i 2764 |
. . . . . . . . . . . 12
⊢
((ℑ‘1) −
(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
-(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) |
146 | 64, 35 | immul2d 14677 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))) = ((tan‘(ℜ‘𝐴)) ·
(ℑ‘(tan‘(i · (ℑ‘𝐴)))))) |
147 | | imval 14556 |
. . . . . . . . . . . . . . . . 17
⊢
((tan‘(i · (ℑ‘𝐴))) ∈ ℂ →
(ℑ‘(tan‘(i · (ℑ‘𝐴)))) = (ℜ‘((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
148 | 35, 147 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘(tan‘(i ·
(ℑ‘𝐴)))) =
(ℜ‘((tan‘(i · (ℑ‘𝐴))) / i))) |
149 | 67 | rered 14673 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((tan‘(i ·
(ℑ‘𝐴))) / i)) =
((tan‘(i · (ℑ‘𝐴))) / i)) |
150 | 148, 149 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘(tan‘(i ·
(ℑ‘𝐴)))) =
((tan‘(i · (ℑ‘𝐴))) / i)) |
151 | 150 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · (ℑ‘(tan‘(i
· (ℑ‘𝐴))))) = ((tan‘(ℜ‘𝐴)) · ((tan‘(i
· (ℑ‘𝐴))) / i))) |
152 | 146, 151 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))) = ((tan‘(ℜ‘𝐴)) · ((tan‘(i
· (ℑ‘𝐴))) / i))) |
153 | 152 | negeqd 10958 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → -(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))) = -((tan‘(ℜ‘𝐴)) · ((tan‘(i
· (ℑ‘𝐴))) / i))) |
154 | 145, 153 | syl5eq 2785 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((ℑ‘1) −
(ℑ‘((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
-((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
155 | 141, 154 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
-((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
156 | 155 | negeqd 10958 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → -(ℑ‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
--((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
157 | 64, 67 | remulcld 10749 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) / i))
∈ ℝ) |
158 | 157 | recnd 10747 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) / i))
∈ ℂ) |
159 | 158 | negnegd 11066 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → --((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) / i)) =
((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
160 | 139, 156,
159 | 3eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) =
((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
161 | 130 | fveq2d 6678 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(ℜ‘𝐴)) + (i · ((tan‘(i
· (ℑ‘𝐴))) / i)))) =
(ℑ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) |
162 | 64, 67 | crimd 14681 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(ℜ‘𝐴)) + (i · ((tan‘(i
· (ℑ‘𝐴))) / i)))) = ((tan‘(i ·
(ℑ‘𝐴))) /
i)) |
163 | 161, 162 | eqtr3d 2775 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℑ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) =
((tan‘(i · (ℑ‘𝐴))) / i)) |
164 | 160, 163 | oveq12d 7188 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((ℑ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℑ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) =
(((tan‘(ℜ‘𝐴)) · ((tan‘(i ·
(ℑ‘𝐴))) / i))
· ((tan‘(i · (ℑ‘𝐴))) / i))) |
165 | 83 | sqvald 13599 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(i · (ℑ‘𝐴))) / i)↑2) =
(((tan‘(i · (ℑ‘𝐴))) / i) · ((tan‘(i ·
(ℑ‘𝐴))) /
i))) |
166 | 165 | oveq2d 7186 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2)) = ((tan‘(ℜ‘𝐴)) · (((tan‘(i ·
(ℑ‘𝐴))) / i)
· ((tan‘(i · (ℑ‘𝐴))) / i)))) |
167 | 138, 164,
166 | 3eqtr4d 2783 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((ℑ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℑ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) =
((tan‘(ℜ‘𝐴)) · (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2))) |
168 | 137, 167 | oveq12d 7188 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((ℜ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℜ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))
− ((ℑ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℑ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))) =
(((tan‘(ℜ‘𝐴)) · 1) −
((tan‘(ℜ‘𝐴)) · (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2)))) |
169 | 58, 59 | remuld 14667 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) =
(((ℜ‘(∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))) ·
(ℜ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))
− ((ℑ‘(∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))))
· (ℑ‘((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))))) |
170 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 1 ∈ ℂ) |
171 | 83 | sqcld 13600 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(i · (ℑ‘𝐴))) / i)↑2) ∈
ℂ) |
172 | 25, 170, 171 | subdid 11174 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((tan‘(ℜ‘𝐴)) · (1 − (((tan‘(i
· (ℑ‘𝐴))) / i)↑2))) =
(((tan‘(ℜ‘𝐴)) · 1) −
((tan‘(ℜ‘𝐴)) · (((tan‘(i ·
(ℑ‘𝐴))) /
i)↑2)))) |
173 | 168, 169,
172 | 3eqtr4d 2783 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) =
((tan‘(ℜ‘𝐴)) · (1 − (((tan‘(i
· (ℑ‘𝐴))) / i)↑2)))) |
174 | 97, 173 | breqtrrd 5058 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (ℜ‘((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))) |
175 | 57, 61, 63, 174 | mulgt0d 10873 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < ((1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ·
(ℜ‘((∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) ·
((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))))) |
176 | 40 | fveq2d 6678 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘𝐴) = (tan‘((ℜ‘𝐴) + (i ·
(ℑ‘𝐴))))) |
177 | | tanadd 15612 |
. . . . . . 7
⊢
((((ℜ‘𝐴)
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ) ∧
((cos‘(ℜ‘𝐴)) ≠ 0 ∧ (cos‘(i ·
(ℑ‘𝐴))) ≠ 0
∧ (cos‘((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) ≠ 0)) →
(tan‘((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) =
(((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))) / (1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) |
178 | 4, 31, 24, 34, 44, 177 | syl23anc 1378 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) =
(((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))) / (1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))) |
179 | | recval 14772 |
. . . . . . . . 9
⊢ (((1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))
∈ ℂ ∧ (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))) ≠
0) → (1 / (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
((∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2))) |
180 | 38, 52, 179 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (1 / (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) = ((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2))) |
181 | 180 | oveq1d 7185 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((1 / (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) ·
((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) =
(((∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ·
((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) |
182 | 59, 38, 52 | divrec2d 11498 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))) / (1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
((1 / (1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) |
183 | 38 | abscld 14886 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) ∈ ℝ) |
184 | 183 | resqcld 13703 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))↑2) ∈
ℝ) |
185 | 184 | recnd 10747 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))↑2) ∈
ℂ) |
186 | 56 | rpne0d 12519 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → ((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴))))))↑2) ≠ 0) |
187 | 58, 59, 185, 186 | div23d 11531 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) = (((∗‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ·
((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))) |
188 | 181, 182,
187 | 3eqtr4d 2783 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))) / (1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴)))))) =
(((∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2))) |
189 | 176, 178,
188 | 3eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘𝐴) = (((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2))) |
190 | 60, 185, 186 | divrec2d 11498 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (((∗‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))) /
((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) = ((1 / ((abs‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) · ((∗‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))) |
191 | 189, 190 | eqtrd 2773 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (tan‘𝐴) = ((1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) · ((∗‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))) |
192 | 191 | fveq2d 6678 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(tan‘𝐴)) = (ℜ‘((1 / ((abs‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) · ((∗‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))))) |
193 | 57, 60 | remul2d 14676 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘((1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) · ((∗‘(1
− ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))
· ((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴))))))) =
((1 / ((abs‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ·
(ℜ‘((∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) ·
((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))))) |
194 | 192, 193 | eqtrd 2773 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → (ℜ‘(tan‘𝐴)) = ((1 / ((abs‘(1 −
((tan‘(ℜ‘𝐴)) · (tan‘(i ·
(ℑ‘𝐴))))))↑2)) ·
(ℜ‘((∗‘(1 − ((tan‘(ℜ‘𝐴)) · (tan‘(i
· (ℑ‘𝐴)))))) ·
((tan‘(ℜ‘𝐴)) + (tan‘(i ·
(ℑ‘𝐴)))))))) |
195 | 175, 194 | breqtrrd 5058 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(0(,)(π / 2))) → 0 < (ℜ‘(tan‘𝐴))) |