Proof of Theorem tanarg
Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝐴 = 0 → (ℜ‘𝐴) =
(ℜ‘0)) |
2 | | re0 14715 |
. . . . . . . 8
⊢
(ℜ‘0) = 0 |
3 | 1, 2 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝐴 = 0 → (ℜ‘𝐴) = 0) |
4 | 3 | necon3i 2973 |
. . . . . 6
⊢
((ℜ‘𝐴)
≠ 0 → 𝐴 ≠
0) |
5 | | logcl 25457 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (log‘𝐴) ∈
ℂ) |
6 | 4, 5 | sylan2 596 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (log‘𝐴) ∈
ℂ) |
7 | 6 | imcld 14758 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘(log‘𝐴)) ∈ ℝ) |
8 | 7 | recnd 10861 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘(log‘𝐴)) ∈ ℂ) |
9 | | sqcl 13690 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈
ℂ) |
10 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (𝐴↑2) ∈
ℂ) |
11 | | abscl 14842 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
12 | 11 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (abs‘𝐴) ∈
ℝ) |
13 | 12 | recnd 10861 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (abs‘𝐴) ∈
ℂ) |
14 | 13 | sqcld 13714 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((abs‘𝐴)↑2) ∈ ℂ) |
15 | | absrpcl 14852 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
16 | 4, 15 | sylan2 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (abs‘𝐴) ∈
ℝ+) |
17 | 16 | rpne0d 12633 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (abs‘𝐴) ≠
0) |
18 | | sqne0 13695 |
. . . . . . . 8
⊢
((abs‘𝐴)
∈ ℂ → (((abs‘𝐴)↑2) ≠ 0 ↔ (abs‘𝐴) ≠ 0)) |
19 | 13, 18 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((abs‘𝐴)↑2) ≠ 0 ↔ (abs‘𝐴) ≠ 0)) |
20 | 17, 19 | mpbird 260 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((abs‘𝐴)↑2) ≠ 0) |
21 | 10, 14, 14, 20 | divdird 11646 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((𝐴↑2) +
((abs‘𝐴)↑2)) /
((abs‘𝐴)↑2)) =
(((𝐴↑2) /
((abs‘𝐴)↑2)) +
(((abs‘𝐴)↑2) /
((abs‘𝐴)↑2)))) |
22 | | ax-icn 10788 |
. . . . . . . . 9
⊢ i ∈
ℂ |
23 | | mulcl 10813 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (ℑ‘(log‘𝐴)) ∈ ℂ) → (i ·
(ℑ‘(log‘𝐴))) ∈ ℂ) |
24 | 22, 8, 23 | sylancr 590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (ℑ‘(log‘𝐴))) ∈ ℂ) |
25 | | 2z 12209 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
26 | | efexp 15662 |
. . . . . . . 8
⊢ (((i
· (ℑ‘(log‘𝐴))) ∈ ℂ ∧ 2 ∈ ℤ)
→ (exp‘(2 · (i · (ℑ‘(log‘𝐴))))) = ((exp‘(i ·
(ℑ‘(log‘𝐴))))↑2)) |
27 | 24, 25, 26 | sylancl 589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (exp‘(2 · (i · (ℑ‘(log‘𝐴))))) = ((exp‘(i ·
(ℑ‘(log‘𝐴))))↑2)) |
28 | | efiarg 25495 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(i
· (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
29 | 4, 28 | sylan2 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴))) |
30 | 29 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((exp‘(i · (ℑ‘(log‘𝐴))))↑2) = ((𝐴 / (abs‘𝐴))↑2)) |
31 | | simpl 486 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ 𝐴 ∈
ℂ) |
32 | 31, 13, 17 | sqdivd 13729 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴 /
(abs‘𝐴))↑2) =
((𝐴↑2) /
((abs‘𝐴)↑2))) |
33 | 27, 30, 32 | 3eqtrrd 2782 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) /
((abs‘𝐴)↑2)) =
(exp‘(2 · (i · (ℑ‘(log‘𝐴)))))) |
34 | 14, 20 | dividd 11606 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((abs‘𝐴)↑2) / ((abs‘𝐴)↑2)) = 1) |
35 | 33, 34 | oveq12d 7231 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((𝐴↑2) /
((abs‘𝐴)↑2)) +
(((abs‘𝐴)↑2) /
((abs‘𝐴)↑2))) =
((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) + 1)) |
36 | 21, 35 | eqtr2d 2778 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) + 1) = (((𝐴↑2) + ((abs‘𝐴)↑2)) / ((abs‘𝐴)↑2))) |
37 | 10, 14 | addcld 10852 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) +
((abs‘𝐴)↑2))
∈ ℂ) |
38 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ i ∈ ℂ) |
39 | | 2cn 11905 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
40 | | recl 14673 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
41 | 40 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℜ‘𝐴)
∈ ℝ) |
42 | 41 | recnd 10861 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℜ‘𝐴)
∈ ℂ) |
43 | 42 | sqcld 13714 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)↑2) ∈ ℂ) |
44 | | mulcl 10813 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ ((ℜ‘𝐴)↑2) ∈ ℂ) → (2 ·
((ℜ‘𝐴)↑2))
∈ ℂ) |
45 | 39, 43, 44 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℜ‘𝐴)↑2)) ∈ ℂ) |
46 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ 2 ∈ ℂ) |
47 | | imcl 14674 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
48 | 47 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘𝐴)
∈ ℝ) |
49 | 48 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘𝐴)
∈ ℂ) |
50 | 42, 49 | mulcld 10853 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
· (ℑ‘𝐴))
∈ ℂ) |
51 | 38, 46, 50 | mul12d 11041 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (2 · ((ℜ‘𝐴) · (ℑ‘𝐴)))) = (2 · (i ·
((ℜ‘𝐴) ·
(ℑ‘𝐴))))) |
52 | 38, 42, 49 | mul12d 11041 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((ℜ‘𝐴) · (ℑ‘𝐴))) = ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) |
53 | 52 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · (i · ((ℜ‘𝐴) · (ℑ‘𝐴)))) = (2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴))))) |
54 | 51, 53 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (2 · ((ℜ‘𝐴) · (ℑ‘𝐴)))) = (2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴))))) |
55 | | mulcl 10813 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
56 | 22, 49, 55 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (ℑ‘𝐴)) ∈ ℂ) |
57 | 42, 56 | mulcld 10853 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
· (i · (ℑ‘𝐴))) ∈ ℂ) |
58 | | mulcl 10813 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ ((ℜ‘𝐴) · (i · (ℑ‘𝐴))) ∈ ℂ) → (2
· ((ℜ‘𝐴)
· (i · (ℑ‘𝐴)))) ∈ ℂ) |
59 | 39, 57, 58 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) ∈
ℂ) |
60 | 54, 59 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (2 · ((ℜ‘𝐴) · (ℑ‘𝐴)))) ∈ ℂ) |
61 | 38, 45, 60 | adddid 10857 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((2 · ((ℜ‘𝐴)↑2)) + (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴)))))) =
((i · (2 · ((ℜ‘𝐴)↑2))) + (i · (i · (2
· ((ℜ‘𝐴)
· (ℑ‘𝐴))))))) |
62 | | mulcl 10813 |
. . . . . . . . . . . . 13
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ i ∈ ℂ) → ((ℜ‘𝐴) · i) ∈
ℂ) |
63 | 42, 22, 62 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
· i) ∈ ℂ) |
64 | 46, 63, 42 | mulassd 10856 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) = (2 ·
(((ℜ‘𝐴) ·
i) · (ℜ‘𝐴)))) |
65 | 42 | sqvald 13713 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)↑2) = ((ℜ‘𝐴) · (ℜ‘𝐴))) |
66 | 65 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴)↑2) · i) =
(((ℜ‘𝐴) ·
(ℜ‘𝐴)) ·
i)) |
67 | | mulcom 10815 |
. . . . . . . . . . . . . 14
⊢
((((ℜ‘𝐴)↑2) ∈ ℂ ∧ i ∈
ℂ) → (((ℜ‘𝐴)↑2) · i) = (i ·
((ℜ‘𝐴)↑2))) |
68 | 43, 22, 67 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴)↑2) · i) = (i ·
((ℜ‘𝐴)↑2))) |
69 | 42, 42, 38 | mul32d 11042 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴)
· (ℜ‘𝐴))
· i) = (((ℜ‘𝐴) · i) · (ℜ‘𝐴))) |
70 | 66, 68, 69 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((ℜ‘𝐴)↑2)) = (((ℜ‘𝐴) · i) ·
(ℜ‘𝐴))) |
71 | 70 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · (i · ((ℜ‘𝐴)↑2))) = (2 ·
(((ℜ‘𝐴) ·
i) · (ℜ‘𝐴)))) |
72 | 46, 38, 43 | mul12d 11041 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · (i · ((ℜ‘𝐴)↑2))) = (i · (2 ·
((ℜ‘𝐴)↑2)))) |
73 | 64, 71, 72 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) = (i · (2 ·
((ℜ‘𝐴)↑2)))) |
74 | | ixi 11461 |
. . . . . . . . . . . . 13
⊢ (i
· i) = -1 |
75 | 74 | oveq1i 7223 |
. . . . . . . . . . . 12
⊢ ((i
· i) · ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴))) = (-1 · ((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴))) |
76 | | mulcl 10813 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (2 ·
(ℑ‘𝐴)) ∈
ℂ) |
77 | 39, 49, 76 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · (ℑ‘𝐴)) ∈ ℂ) |
78 | 77, 42 | mulcld 10853 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴)) ∈ ℂ) |
79 | 38, 38, 78 | mulassd 10856 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · i) · ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴))) = (i · (i · ((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴))))) |
80 | 75, 79 | eqtr3id 2792 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (-1 · ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴))) = (i · (i · ((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴))))) |
81 | 78 | mulm1d 11284 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (-1 · ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴))) = -((2 · (ℑ‘𝐴)) · (ℜ‘𝐴))) |
82 | 46, 49, 42 | mulassd 10856 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴)) = (2 · ((ℑ‘𝐴) · (ℜ‘𝐴)))) |
83 | 49, 42 | mulcomd 10854 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℑ‘𝐴)
· (ℜ‘𝐴))
= ((ℜ‘𝐴)
· (ℑ‘𝐴))) |
84 | 83 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℑ‘𝐴) · (ℜ‘𝐴))) = (2 · ((ℜ‘𝐴) · (ℑ‘𝐴)))) |
85 | 82, 84 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴)) = (2 · ((ℜ‘𝐴) · (ℑ‘𝐴)))) |
86 | 85 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴))) = (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴))))) |
87 | 86 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (i · ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴)))) = (i · (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴)))))) |
88 | 80, 81, 87 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ -((2 · (ℑ‘𝐴)) · (ℜ‘𝐴)) = (i · (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴)))))) |
89 | 73, 88 | oveq12d 7231 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) + -((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴))) = ((i
· (2 · ((ℜ‘𝐴)↑2))) + (i · (i · (2
· ((ℜ‘𝐴)
· (ℑ‘𝐴))))))) |
90 | | mulcl 10813 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ ((ℜ‘𝐴) · i) ∈ ℂ) → (2
· ((ℜ‘𝐴)
· i)) ∈ ℂ) |
91 | 39, 63, 90 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℜ‘𝐴) · i)) ∈
ℂ) |
92 | 91, 42 | mulcld 10853 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) ∈
ℂ) |
93 | 92, 78 | negsubd 11195 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) + -((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴))) = (((2
· ((ℜ‘𝐴)
· i)) · (ℜ‘𝐴)) − ((2 · (ℑ‘𝐴)) · (ℜ‘𝐴)))) |
94 | 61, 89, 93 | 3eqtr2d 2783 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((2 · ((ℜ‘𝐴)↑2)) + (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴)))))) =
(((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) − ((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴)))) |
95 | 49 | sqcld 13714 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℑ‘𝐴)↑2) ∈ ℂ) |
96 | 59, 95 | subcld 11189 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2))
∈ ℂ) |
97 | 43, 96, 43, 95 | add4d 11060 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((ℜ‘𝐴)↑2) + ((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − ((ℑ‘𝐴)↑2))) +
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) = ((((ℜ‘𝐴)↑2) + ((ℜ‘𝐴)↑2)) + (((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − ((ℑ‘𝐴)↑2)) +
((ℑ‘𝐴)↑2)))) |
98 | | replim 14679 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
99 | 98 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ 𝐴 =
((ℜ‘𝐴) + (i
· (ℑ‘𝐴)))) |
100 | 99 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (𝐴↑2) =
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴)))↑2)) |
101 | | binom2 13785 |
. . . . . . . . . . . . . 14
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (i · (ℑ‘𝐴)) ∈ ℂ) →
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴)))↑2) = ((((ℜ‘𝐴)↑2) + (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) + ((i · (ℑ‘𝐴))↑2))) |
102 | 42, 56, 101 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴) +
(i · (ℑ‘𝐴)))↑2) = ((((ℜ‘𝐴)↑2) + (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) + ((i · (ℑ‘𝐴))↑2))) |
103 | | sqmul 13691 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → ((i ·
(ℑ‘𝐴))↑2)
= ((i↑2) · ((ℑ‘𝐴)↑2))) |
104 | 22, 49, 103 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · (ℑ‘𝐴))↑2) = ((i↑2) ·
((ℑ‘𝐴)↑2))) |
105 | | i2 13771 |
. . . . . . . . . . . . . . . . 17
⊢
(i↑2) = -1 |
106 | 105 | oveq1i 7223 |
. . . . . . . . . . . . . . . 16
⊢
((i↑2) · ((ℑ‘𝐴)↑2)) = (-1 ·
((ℑ‘𝐴)↑2)) |
107 | 104, 106 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · (ℑ‘𝐴))↑2) = (-1 ·
((ℑ‘𝐴)↑2))) |
108 | 95 | mulm1d 11284 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (-1 · ((ℑ‘𝐴)↑2)) = -((ℑ‘𝐴)↑2)) |
109 | 107, 108 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · (ℑ‘𝐴))↑2) = -((ℑ‘𝐴)↑2)) |
110 | 109 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((ℜ‘𝐴)↑2) + (2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴))))) + ((i
· (ℑ‘𝐴))↑2)) = ((((ℜ‘𝐴)↑2) + (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) + -((ℑ‘𝐴)↑2))) |
111 | 43, 59 | addcld 10852 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴)↑2) + (2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴)))))
∈ ℂ) |
112 | 111, 95 | negsubd 11195 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((ℜ‘𝐴)↑2) + (2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴))))) +
-((ℑ‘𝐴)↑2)) = ((((ℜ‘𝐴)↑2) + (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) − ((ℑ‘𝐴)↑2))) |
113 | 102, 110,
112 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴) +
(i · (ℑ‘𝐴)))↑2) = ((((ℜ‘𝐴)↑2) + (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) − ((ℑ‘𝐴)↑2))) |
114 | 43, 59, 95 | addsubassd 11209 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((ℜ‘𝐴)↑2) + (2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴)))))
− ((ℑ‘𝐴)↑2)) = (((ℜ‘𝐴)↑2) + ((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − ((ℑ‘𝐴)↑2)))) |
115 | 100, 113,
114 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (𝐴↑2) =
(((ℜ‘𝐴)↑2)
+ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2)))) |
116 | | absvalsq2 14845 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) |
117 | 116 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) +
((ℑ‘𝐴)↑2))) |
118 | 115, 117 | oveq12d 7231 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) +
((abs‘𝐴)↑2)) =
((((ℜ‘𝐴)↑2)
+ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2))) + (((ℜ‘𝐴)↑2) +
((ℑ‘𝐴)↑2)))) |
119 | 43 | 2timesd 12073 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℜ‘𝐴)↑2)) = (((ℜ‘𝐴)↑2) + ((ℜ‘𝐴)↑2))) |
120 | 59, 95 | npcand 11193 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2))
+ ((ℑ‘𝐴)↑2)) = (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) |
121 | 53, 51, 120 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (2 · ((ℜ‘𝐴) · (ℑ‘𝐴)))) = (((2 · ((ℜ‘𝐴) · (i ·
(ℑ‘𝐴))))
− ((ℑ‘𝐴)↑2)) + ((ℑ‘𝐴)↑2))) |
122 | 119, 121 | oveq12d 7231 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴)↑2)) + (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴))))) =
((((ℜ‘𝐴)↑2)
+ ((ℜ‘𝐴)↑2)) + (((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − ((ℑ‘𝐴)↑2)) +
((ℑ‘𝐴)↑2)))) |
123 | 97, 118, 122 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) +
((abs‘𝐴)↑2)) =
((2 · ((ℜ‘𝐴)↑2)) + (i · (2 ·
((ℜ‘𝐴) ·
(ℑ‘𝐴)))))) |
124 | 123 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((𝐴↑2) + ((abs‘𝐴)↑2))) = (i · ((2 ·
((ℜ‘𝐴)↑2))
+ (i · (2 · ((ℜ‘𝐴) · (ℑ‘𝐴))))))) |
125 | 91, 77, 42 | subdird 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℜ‘𝐴))
= (((2 · ((ℜ‘𝐴) · i)) · (ℜ‘𝐴)) − ((2 ·
(ℑ‘𝐴)) ·
(ℜ‘𝐴)))) |
126 | 94, 124, 125 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((𝐴↑2) + ((abs‘𝐴)↑2))) = (((2 ·
((ℜ‘𝐴) ·
i)) − (2 · (ℑ‘𝐴))) · (ℜ‘𝐴))) |
127 | 91, 77 | subcld 11189 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴))) ∈
ℂ) |
128 | | mulcom 10815 |
. . . . . . . . . . 11
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ i ∈ ℂ) → ((ℜ‘𝐴) · i) = (i ·
(ℜ‘𝐴))) |
129 | 42, 22, 128 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
· i) = (i · (ℜ‘𝐴))) |
130 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (ℜ‘𝐴)
≠ 0) |
131 | | eleq1 2825 |
. . . . . . . . . . . . . 14
⊢ ((i
· (ℜ‘𝐴))
= (ℑ‘𝐴) →
((i · (ℜ‘𝐴)) ∈ ℝ ↔
(ℑ‘𝐴) ∈
ℝ)) |
132 | 48, 131 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · (ℜ‘𝐴)) = (ℑ‘𝐴) → (i · (ℜ‘𝐴)) ∈
ℝ)) |
133 | | rimul 11821 |
. . . . . . . . . . . . 13
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ (i · (ℜ‘𝐴)) ∈ ℝ) →
(ℜ‘𝐴) =
0) |
134 | 41, 132, 133 | syl6an 684 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · (ℜ‘𝐴)) = (ℑ‘𝐴) → (ℜ‘𝐴) = 0)) |
135 | 134 | necon3d 2961 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
≠ 0 → (i · (ℜ‘𝐴)) ≠ (ℑ‘𝐴))) |
136 | 130, 135 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · (ℜ‘𝐴)) ≠ (ℑ‘𝐴)) |
137 | 129, 136 | eqnetrd 3008 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
· i) ≠ (ℑ‘𝐴)) |
138 | 91, 77 | subeq0ad 11199 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴))) = 0
↔ (2 · ((ℜ‘𝐴) · i)) = (2 ·
(ℑ‘𝐴)))) |
139 | | 2ne0 11934 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
140 | 139 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ 2 ≠ 0) |
141 | 63, 49, 46, 140 | mulcand 11465 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) = (2 ·
(ℑ‘𝐴)) ↔
((ℜ‘𝐴) ·
i) = (ℑ‘𝐴))) |
142 | 138, 141 | bitrd 282 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴))) = 0
↔ ((ℜ‘𝐴)
· i) = (ℑ‘𝐴))) |
143 | 142 | necon3bid 2985 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴))) ≠ 0
↔ ((ℜ‘𝐴)
· i) ≠ (ℑ‘𝐴))) |
144 | 137, 143 | mpbird 260 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴))) ≠
0) |
145 | 127, 42, 144, 130 | mulne0d 11484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℜ‘𝐴))
≠ 0) |
146 | 126, 145 | eqnetrd 3008 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((𝐴↑2) + ((abs‘𝐴)↑2))) ≠ 0) |
147 | | oveq2 7221 |
. . . . . . . 8
⊢ (((𝐴↑2) + ((abs‘𝐴)↑2)) = 0 → (i
· ((𝐴↑2) +
((abs‘𝐴)↑2))) =
(i · 0)) |
148 | | it0e0 12052 |
. . . . . . . 8
⊢ (i
· 0) = 0 |
149 | 147, 148 | eqtrdi 2794 |
. . . . . . 7
⊢ (((𝐴↑2) + ((abs‘𝐴)↑2)) = 0 → (i
· ((𝐴↑2) +
((abs‘𝐴)↑2))) =
0) |
150 | 149 | necon3i 2973 |
. . . . . 6
⊢ ((i
· ((𝐴↑2) +
((abs‘𝐴)↑2)))
≠ 0 → ((𝐴↑2) +
((abs‘𝐴)↑2))
≠ 0) |
151 | 146, 150 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) +
((abs‘𝐴)↑2))
≠ 0) |
152 | 37, 14, 151, 20 | divne0d 11624 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((𝐴↑2) +
((abs‘𝐴)↑2)) /
((abs‘𝐴)↑2))
≠ 0) |
153 | 36, 152 | eqnetrd 3008 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) + 1) ≠
0) |
154 | | tanval3 15695 |
. . 3
⊢
(((ℑ‘(log‘𝐴)) ∈ ℂ ∧ ((exp‘(2
· (i · (ℑ‘(log‘𝐴))))) + 1) ≠ 0) →
(tan‘(ℑ‘(log‘𝐴))) = (((exp‘(2 · (i ·
(ℑ‘(log‘𝐴))))) − 1) / (i ·
((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) + 1)))) |
155 | 8, 153, 154 | syl2anc 587 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (tan‘(ℑ‘(log‘𝐴))) = (((exp‘(2 · (i ·
(ℑ‘(log‘𝐴))))) − 1) / (i ·
((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) + 1)))) |
156 | 10, 14, 14, 20 | divsubdird 11647 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((𝐴↑2) −
((abs‘𝐴)↑2)) /
((abs‘𝐴)↑2)) =
(((𝐴↑2) /
((abs‘𝐴)↑2))
− (((abs‘𝐴)↑2) / ((abs‘𝐴)↑2)))) |
157 | 33, 34 | oveq12d 7231 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((𝐴↑2) /
((abs‘𝐴)↑2))
− (((abs‘𝐴)↑2) / ((abs‘𝐴)↑2))) = ((exp‘(2 · (i
· (ℑ‘(log‘𝐴))))) − 1)) |
158 | 156, 157 | eqtr2d 2778 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) − 1) = (((𝐴↑2) −
((abs‘𝐴)↑2)) /
((abs‘𝐴)↑2))) |
159 | 36 | oveq2d 7229 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((exp‘(2 · (i ·
(ℑ‘(log‘𝐴))))) + 1)) = (i · (((𝐴↑2) + ((abs‘𝐴)↑2)) / ((abs‘𝐴)↑2)))) |
160 | 38, 37, 14, 20 | divassd 11643 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((i · ((𝐴↑2) + ((abs‘𝐴)↑2))) / ((abs‘𝐴)↑2)) = (i · (((𝐴↑2) + ((abs‘𝐴)↑2)) / ((abs‘𝐴)↑2)))) |
161 | 159, 160 | eqtr4d 2780 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((exp‘(2 · (i ·
(ℑ‘(log‘𝐴))))) + 1)) = ((i · ((𝐴↑2) + ((abs‘𝐴)↑2))) / ((abs‘𝐴)↑2))) |
162 | 158, 161 | oveq12d 7231 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) − 1) / (i ·
((exp‘(2 · (i · (ℑ‘(log‘𝐴))))) + 1))) = ((((𝐴↑2) − ((abs‘𝐴)↑2)) / ((abs‘𝐴)↑2)) / ((i ·
((𝐴↑2) +
((abs‘𝐴)↑2))) /
((abs‘𝐴)↑2)))) |
163 | 10, 14 | subcld 11189 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) −
((abs‘𝐴)↑2))
∈ ℂ) |
164 | | mulcl 10813 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ((𝐴↑2) + ((abs‘𝐴)↑2)) ∈ ℂ) → (i
· ((𝐴↑2) +
((abs‘𝐴)↑2)))
∈ ℂ) |
165 | 22, 37, 164 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (i · ((𝐴↑2) + ((abs‘𝐴)↑2))) ∈ ℂ) |
166 | 163, 165,
14, 146, 20 | divcan7d 11636 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((𝐴↑2)
− ((abs‘𝐴)↑2)) / ((abs‘𝐴)↑2)) / ((i · ((𝐴↑2) + ((abs‘𝐴)↑2))) / ((abs‘𝐴)↑2))) = (((𝐴↑2) −
((abs‘𝐴)↑2)) /
(i · ((𝐴↑2) +
((abs‘𝐴)↑2))))) |
167 | 115, 117 | oveq12d 7231 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) −
((abs‘𝐴)↑2)) =
((((ℜ‘𝐴)↑2)
+ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2))) − (((ℜ‘𝐴)↑2) +
((ℑ‘𝐴)↑2)))) |
168 | 43, 96, 95 | pnpcand 11226 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((ℜ‘𝐴)↑2) + ((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − ((ℑ‘𝐴)↑2))) −
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) = (((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − ((ℑ‘𝐴)↑2)) −
((ℑ‘𝐴)↑2))) |
169 | 59, 95, 95 | subsub4d 11220 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2))
− ((ℑ‘𝐴)↑2)) = ((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − (((ℑ‘𝐴)↑2) +
((ℑ‘𝐴)↑2)))) |
170 | 95 | 2timesd 12073 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℑ‘𝐴)↑2)) = (((ℑ‘𝐴)↑2) +
((ℑ‘𝐴)↑2))) |
171 | 170 | oveq2d 7229 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) − (2 ·
((ℑ‘𝐴)↑2))) = ((2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴)))) − (((ℑ‘𝐴)↑2) +
((ℑ‘𝐴)↑2)))) |
172 | 46, 63, 49 | mulassd 10856 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · i)) · (ℑ‘𝐴)) = (2 ·
(((ℜ‘𝐴) ·
i) · (ℑ‘𝐴)))) |
173 | 42, 38, 49 | mulassd 10856 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((ℜ‘𝐴)
· i) · (ℑ‘𝐴)) = ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) |
174 | 173 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · (((ℜ‘𝐴) · i) · (ℑ‘𝐴))) = (2 ·
((ℜ‘𝐴) ·
(i · (ℑ‘𝐴))))) |
175 | 172, 174 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) = ((2 ·
((ℜ‘𝐴) ·
i)) · (ℑ‘𝐴))) |
176 | 49 | sqvald 13713 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℑ‘𝐴)↑2) = ((ℑ‘𝐴) · (ℑ‘𝐴))) |
177 | 176 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℑ‘𝐴)↑2)) = (2 ·
((ℑ‘𝐴) ·
(ℑ‘𝐴)))) |
178 | 46, 49, 49 | mulassd 10856 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · (ℑ‘𝐴)) · (ℑ‘𝐴)) = (2 · ((ℑ‘𝐴) · (ℑ‘𝐴)))) |
179 | 177, 178 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (2 · ((ℑ‘𝐴)↑2)) = ((2 ·
(ℑ‘𝐴)) ·
(ℑ‘𝐴))) |
180 | 175, 179 | oveq12d 7231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) − (2 ·
((ℑ‘𝐴)↑2))) = (((2 ·
((ℜ‘𝐴) ·
i)) · (ℑ‘𝐴)) − ((2 · (ℑ‘𝐴)) · (ℑ‘𝐴)))) |
181 | 91, 77, 49 | subdird 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℑ‘𝐴))
= (((2 · ((ℜ‘𝐴) · i)) · (ℑ‘𝐴)) − ((2 ·
(ℑ‘𝐴)) ·
(ℑ‘𝐴)))) |
182 | 180, 181 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) − (2 ·
((ℑ‘𝐴)↑2))) = (((2 ·
((ℜ‘𝐴) ·
i)) − (2 · (ℑ‘𝐴))) · (ℑ‘𝐴))) |
183 | 169, 171,
182 | 3eqtr2d 2783 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((2 · ((ℜ‘𝐴) · (i · (ℑ‘𝐴)))) −
((ℑ‘𝐴)↑2))
− ((ℑ‘𝐴)↑2)) = (((2 ·
((ℜ‘𝐴) ·
i)) − (2 · (ℑ‘𝐴))) · (ℑ‘𝐴))) |
184 | 167, 168,
183 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((𝐴↑2) −
((abs‘𝐴)↑2)) =
(((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℑ‘𝐴))) |
185 | 184, 126 | oveq12d 7231 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (((𝐴↑2) −
((abs‘𝐴)↑2)) /
(i · ((𝐴↑2) +
((abs‘𝐴)↑2)))) =
((((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℑ‘𝐴))
/ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℜ‘𝐴)))) |
186 | 49, 42, 127, 130, 144 | divcan5d 11634 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℑ‘𝐴))
/ (((2 · ((ℜ‘𝐴) · i)) − (2 ·
(ℑ‘𝐴)))
· (ℜ‘𝐴)))
= ((ℑ‘𝐴) /
(ℜ‘𝐴))) |
187 | 166, 185,
186 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ ((((𝐴↑2)
− ((abs‘𝐴)↑2)) / ((abs‘𝐴)↑2)) / ((i · ((𝐴↑2) + ((abs‘𝐴)↑2))) / ((abs‘𝐴)↑2))) =
((ℑ‘𝐴) /
(ℜ‘𝐴))) |
188 | 155, 162,
187 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ≠ 0)
→ (tan‘(ℑ‘(log‘𝐴))) = ((ℑ‘𝐴) / (ℜ‘𝐴))) |