Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . . 8
β’ (π΄ = 0 β (ββπ΄) =
(ββ0)) |
2 | | re0 15043 |
. . . . . . . 8
β’
(ββ0) = 0 |
3 | 1, 2 | eqtrdi 2789 |
. . . . . . 7
β’ (π΄ = 0 β (ββπ΄) = 0) |
4 | 3 | necon3i 2973 |
. . . . . 6
β’
((ββπ΄)
β 0 β π΄ β
0) |
5 | | logcl 25940 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β 0) β (logβπ΄) β
β) |
6 | 4, 5 | sylan2 594 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (logβπ΄) β
β) |
7 | 6 | imcld 15086 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(logβπ΄)) β β) |
8 | 7 | recnd 11188 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββ(logβπ΄)) β β) |
9 | | sqcl 14029 |
. . . . . . 7
β’ (π΄ β β β (π΄β2) β
β) |
10 | 9 | adantr 482 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (π΄β2) β
β) |
11 | | abscl 15169 |
. . . . . . . . 9
β’ (π΄ β β β
(absβπ΄) β
β) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (absβπ΄) β
β) |
13 | 12 | recnd 11188 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (absβπ΄) β
β) |
14 | 13 | sqcld 14055 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((absβπ΄)β2) β β) |
15 | | absrpcl 15179 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β (absβπ΄) β
β+) |
16 | 4, 15 | sylan2 594 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (absβπ΄) β
β+) |
17 | 16 | rpne0d 12967 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (absβπ΄) β
0) |
18 | | sqne0 14034 |
. . . . . . . 8
β’
((absβπ΄)
β β β (((absβπ΄)β2) β 0 β (absβπ΄) β 0)) |
19 | 13, 18 | syl 17 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((absβπ΄)β2) β 0 β (absβπ΄) β 0)) |
20 | 17, 19 | mpbird 257 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((absβπ΄)β2) β 0) |
21 | 10, 14, 14, 20 | divdird 11974 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((π΄β2) +
((absβπ΄)β2)) /
((absβπ΄)β2)) =
(((π΄β2) /
((absβπ΄)β2)) +
(((absβπ΄)β2) /
((absβπ΄)β2)))) |
22 | | ax-icn 11115 |
. . . . . . . . 9
β’ i β
β |
23 | | mulcl 11140 |
. . . . . . . . 9
β’ ((i
β β β§ (ββ(logβπ΄)) β β) β (i Β·
(ββ(logβπ΄))) β β) |
24 | 22, 8, 23 | sylancr 588 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (ββ(logβπ΄))) β β) |
25 | | 2z 12540 |
. . . . . . . 8
β’ 2 β
β€ |
26 | | efexp 15988 |
. . . . . . . 8
β’ (((i
Β· (ββ(logβπ΄))) β β β§ 2 β β€)
β (expβ(2 Β· (i Β· (ββ(logβπ΄))))) = ((expβ(i Β·
(ββ(logβπ΄))))β2)) |
27 | 24, 25, 26 | sylancl 587 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (expβ(2 Β· (i Β· (ββ(logβπ΄))))) = ((expβ(i Β·
(ββ(logβπ΄))))β2)) |
28 | | efiarg 25978 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β (expβ(i
Β· (ββ(logβπ΄)))) = (π΄ / (absβπ΄))) |
29 | 4, 28 | sylan2 594 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (expβ(i Β· (ββ(logβπ΄)))) = (π΄ / (absβπ΄))) |
30 | 29 | oveq1d 7373 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((expβ(i Β· (ββ(logβπ΄))))β2) = ((π΄ / (absβπ΄))β2)) |
31 | | simpl 484 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β π΄ β
β) |
32 | 31, 13, 17 | sqdivd 14070 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄ /
(absβπ΄))β2) =
((π΄β2) /
((absβπ΄)β2))) |
33 | 27, 30, 32 | 3eqtrrd 2778 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) /
((absβπ΄)β2)) =
(expβ(2 Β· (i Β· (ββ(logβπ΄)))))) |
34 | 14, 20 | dividd 11934 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((absβπ΄)β2) / ((absβπ΄)β2)) = 1) |
35 | 33, 34 | oveq12d 7376 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((π΄β2) /
((absβπ΄)β2)) +
(((absβπ΄)β2) /
((absβπ΄)β2))) =
((expβ(2 Β· (i Β· (ββ(logβπ΄))))) + 1)) |
36 | 21, 35 | eqtr2d 2774 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((expβ(2 Β· (i Β· (ββ(logβπ΄))))) + 1) = (((π΄β2) + ((absβπ΄)β2)) / ((absβπ΄)β2))) |
37 | 10, 14 | addcld 11179 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) +
((absβπ΄)β2))
β β) |
38 | 22 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β i β β) |
39 | | 2cn 12233 |
. . . . . . . . . . 11
β’ 2 β
β |
40 | | recl 15001 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(ββπ΄) β
β) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
42 | 41 | recnd 11188 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
43 | 42 | sqcld 14055 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)β2) β β) |
44 | | mulcl 11140 |
. . . . . . . . . . 11
β’ ((2
β β β§ ((ββπ΄)β2) β β) β (2 Β·
((ββπ΄)β2))
β β) |
45 | 39, 43, 44 | sylancr 588 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄)β2)) β β) |
46 | 39 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β 2 β β) |
47 | | imcl 15002 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(ββπ΄) β
β) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
49 | 48 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β β) |
50 | 42, 49 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)
Β· (ββπ΄))
β β) |
51 | 38, 46, 50 | mul12d 11369 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (2 Β· ((ββπ΄) Β· (ββπ΄)))) = (2 Β· (i Β·
((ββπ΄) Β·
(ββπ΄))))) |
52 | 38, 42, 49 | mul12d 11369 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((ββπ΄) Β· (ββπ΄))) = ((ββπ΄) Β· (i Β· (ββπ΄)))) |
53 | 52 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· (i Β· ((ββπ΄) Β· (ββπ΄)))) = (2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄))))) |
54 | 51, 53 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (2 Β· ((ββπ΄) Β· (ββπ΄)))) = (2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄))))) |
55 | | mulcl 11140 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ (ββπ΄) β β) β (i Β·
(ββπ΄)) β
β) |
56 | 22, 49, 55 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (ββπ΄)) β β) |
57 | 42, 56 | mulcld 11180 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)
Β· (i Β· (ββπ΄))) β β) |
58 | | mulcl 11140 |
. . . . . . . . . . . 12
β’ ((2
β β β§ ((ββπ΄) Β· (i Β· (ββπ΄))) β β) β (2
Β· ((ββπ΄)
Β· (i Β· (ββπ΄)))) β β) |
59 | 39, 57, 58 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
β) |
60 | 54, 59 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (2 Β· ((ββπ΄) Β· (ββπ΄)))) β β) |
61 | 38, 45, 60 | adddid 11184 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((2 Β· ((ββπ΄)β2)) + (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄)))))) =
((i Β· (2 Β· ((ββπ΄)β2))) + (i Β· (i Β· (2
Β· ((ββπ΄)
Β· (ββπ΄))))))) |
62 | | mulcl 11140 |
. . . . . . . . . . . . 13
β’
(((ββπ΄)
β β β§ i β β) β ((ββπ΄) Β· i) β
β) |
63 | 42, 22, 62 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)
Β· i) β β) |
64 | 46, 63, 42 | mulassd 11183 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) = (2 Β·
(((ββπ΄) Β·
i) Β· (ββπ΄)))) |
65 | 42 | sqvald 14054 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)β2) = ((ββπ΄) Β· (ββπ΄))) |
66 | 65 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄)β2) Β· i) =
(((ββπ΄) Β·
(ββπ΄)) Β·
i)) |
67 | | mulcom 11142 |
. . . . . . . . . . . . . 14
β’
((((ββπ΄)β2) β β β§ i β
β) β (((ββπ΄)β2) Β· i) = (i Β·
((ββπ΄)β2))) |
68 | 43, 22, 67 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄)β2) Β· i) = (i Β·
((ββπ΄)β2))) |
69 | 42, 42, 38 | mul32d 11370 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄)
Β· (ββπ΄))
Β· i) = (((ββπ΄) Β· i) Β· (ββπ΄))) |
70 | 66, 68, 69 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((ββπ΄)β2)) = (((ββπ΄) Β· i) Β·
(ββπ΄))) |
71 | 70 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· (i Β· ((ββπ΄)β2))) = (2 Β·
(((ββπ΄) Β·
i) Β· (ββπ΄)))) |
72 | 46, 38, 43 | mul12d 11369 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· (i Β· ((ββπ΄)β2))) = (i Β· (2 Β·
((ββπ΄)β2)))) |
73 | 64, 71, 72 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) = (i Β· (2 Β·
((ββπ΄)β2)))) |
74 | | ixi 11789 |
. . . . . . . . . . . . 13
β’ (i
Β· i) = -1 |
75 | 74 | oveq1i 7368 |
. . . . . . . . . . . 12
β’ ((i
Β· i) Β· ((2 Β· (ββπ΄)) Β· (ββπ΄))) = (-1 Β· ((2 Β·
(ββπ΄)) Β·
(ββπ΄))) |
76 | | mulcl 11140 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ (ββπ΄) β β) β (2 Β·
(ββπ΄)) β
β) |
77 | 39, 49, 76 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· (ββπ΄)) β β) |
78 | 77, 42 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· (ββπ΄)) Β· (ββπ΄)) β β) |
79 | 38, 38, 78 | mulassd 11183 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i Β· i) Β· ((2 Β· (ββπ΄)) Β· (ββπ΄))) = (i Β· (i Β· ((2 Β·
(ββπ΄)) Β·
(ββπ΄))))) |
80 | 75, 79 | eqtr3id 2787 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (-1 Β· ((2 Β· (ββπ΄)) Β· (ββπ΄))) = (i Β· (i Β· ((2 Β·
(ββπ΄)) Β·
(ββπ΄))))) |
81 | 78 | mulm1d 11612 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (-1 Β· ((2 Β· (ββπ΄)) Β· (ββπ΄))) = -((2 Β· (ββπ΄)) Β· (ββπ΄))) |
82 | 46, 49, 42 | mulassd 11183 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· (ββπ΄)) Β· (ββπ΄)) = (2 Β· ((ββπ΄) Β· (ββπ΄)))) |
83 | 49, 42 | mulcomd 11181 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)
Β· (ββπ΄))
= ((ββπ΄)
Β· (ββπ΄))) |
84 | 83 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄) Β· (ββπ΄))) = (2 Β· ((ββπ΄) Β· (ββπ΄)))) |
85 | 82, 84 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· (ββπ΄)) Β· (ββπ΄)) = (2 Β· ((ββπ΄) Β· (ββπ΄)))) |
86 | 85 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((2 Β· (ββπ΄)) Β· (ββπ΄))) = (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄))))) |
87 | 86 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (i Β· ((2 Β· (ββπ΄)) Β· (ββπ΄)))) = (i Β· (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄)))))) |
88 | 80, 81, 87 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β -((2 Β· (ββπ΄)) Β· (ββπ΄)) = (i Β· (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄)))))) |
89 | 73, 88 | oveq12d 7376 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) + -((2 Β·
(ββπ΄)) Β·
(ββπ΄))) = ((i
Β· (2 Β· ((ββπ΄)β2))) + (i Β· (i Β· (2
Β· ((ββπ΄)
Β· (ββπ΄))))))) |
90 | | mulcl 11140 |
. . . . . . . . . . . 12
β’ ((2
β β β§ ((ββπ΄) Β· i) β β) β (2
Β· ((ββπ΄)
Β· i)) β β) |
91 | 39, 63, 90 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄) Β· i)) β
β) |
92 | 91, 42 | mulcld 11180 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) β
β) |
93 | 92, 78 | negsubd 11523 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) + -((2 Β·
(ββπ΄)) Β·
(ββπ΄))) = (((2
Β· ((ββπ΄)
Β· i)) Β· (ββπ΄)) β ((2 Β· (ββπ΄)) Β· (ββπ΄)))) |
94 | 61, 89, 93 | 3eqtr2d 2779 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((2 Β· ((ββπ΄)β2)) + (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄)))))) =
(((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) β ((2 Β·
(ββπ΄)) Β·
(ββπ΄)))) |
95 | 49 | sqcld 14055 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)β2) β β) |
96 | 59, 95 | subcld 11517 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2))
β β) |
97 | 43, 96, 43, 95 | add4d 11388 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((ββπ΄)β2) + ((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β ((ββπ΄)β2))) +
(((ββπ΄)β2)
+ ((ββπ΄)β2))) = ((((ββπ΄)β2) + ((ββπ΄)β2)) + (((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β ((ββπ΄)β2)) +
((ββπ΄)β2)))) |
98 | | replim 15007 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β π΄ = ((ββπ΄) + (i Β·
(ββπ΄)))) |
99 | 98 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β π΄ =
((ββπ΄) + (i
Β· (ββπ΄)))) |
100 | 99 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (π΄β2) =
(((ββπ΄) + (i
Β· (ββπ΄)))β2)) |
101 | | binom2 14127 |
. . . . . . . . . . . . . 14
β’
(((ββπ΄)
β β β§ (i Β· (ββπ΄)) β β) β
(((ββπ΄) + (i
Β· (ββπ΄)))β2) = ((((ββπ΄)β2) + (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) + ((i Β· (ββπ΄))β2))) |
102 | 42, 56, 101 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄) +
(i Β· (ββπ΄)))β2) = ((((ββπ΄)β2) + (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) + ((i Β· (ββπ΄))β2))) |
103 | | sqmul 14030 |
. . . . . . . . . . . . . . . . 17
β’ ((i
β β β§ (ββπ΄) β β) β ((i Β·
(ββπ΄))β2)
= ((iβ2) Β· ((ββπ΄)β2))) |
104 | 22, 49, 103 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i Β· (ββπ΄))β2) = ((iβ2) Β·
((ββπ΄)β2))) |
105 | | i2 14112 |
. . . . . . . . . . . . . . . . 17
β’
(iβ2) = -1 |
106 | 105 | oveq1i 7368 |
. . . . . . . . . . . . . . . 16
β’
((iβ2) Β· ((ββπ΄)β2)) = (-1 Β·
((ββπ΄)β2)) |
107 | 104, 106 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i Β· (ββπ΄))β2) = (-1 Β·
((ββπ΄)β2))) |
108 | 95 | mulm1d 11612 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (-1 Β· ((ββπ΄)β2)) = -((ββπ΄)β2)) |
109 | 107, 108 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i Β· (ββπ΄))β2) = -((ββπ΄)β2)) |
110 | 109 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((ββπ΄)β2) + (2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄))))) + ((i
Β· (ββπ΄))β2)) = ((((ββπ΄)β2) + (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) + -((ββπ΄)β2))) |
111 | 43, 59 | addcld 11179 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄)β2) + (2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄)))))
β β) |
112 | 111, 95 | negsubd 11523 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((ββπ΄)β2) + (2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄))))) +
-((ββπ΄)β2)) = ((((ββπ΄)β2) + (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) β ((ββπ΄)β2))) |
113 | 102, 110,
112 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄) +
(i Β· (ββπ΄)))β2) = ((((ββπ΄)β2) + (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) β ((ββπ΄)β2))) |
114 | 43, 59, 95 | addsubassd 11537 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((ββπ΄)β2) + (2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄)))))
β ((ββπ΄)β2)) = (((ββπ΄)β2) + ((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β ((ββπ΄)β2)))) |
115 | 100, 113,
114 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (π΄β2) =
(((ββπ΄)β2)
+ ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2)))) |
116 | | absvalsq2 15172 |
. . . . . . . . . . . 12
β’ (π΄ β β β
((absβπ΄)β2) =
(((ββπ΄)β2)
+ ((ββπ΄)β2))) |
117 | 116 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((absβπ΄)β2) = (((ββπ΄)β2) +
((ββπ΄)β2))) |
118 | 115, 117 | oveq12d 7376 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) +
((absβπ΄)β2)) =
((((ββπ΄)β2)
+ ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2))) + (((ββπ΄)β2) +
((ββπ΄)β2)))) |
119 | 43 | 2timesd 12401 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄)β2)) = (((ββπ΄)β2) + ((ββπ΄)β2))) |
120 | 59, 95 | npcand 11521 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2))
+ ((ββπ΄)β2)) = (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) |
121 | 53, 51, 120 | 3eqtr4d 2783 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· (2 Β· ((ββπ΄) Β· (ββπ΄)))) = (((2 Β· ((ββπ΄) Β· (i Β·
(ββπ΄))))
β ((ββπ΄)β2)) + ((ββπ΄)β2))) |
122 | 119, 121 | oveq12d 7376 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄)β2)) + (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄))))) =
((((ββπ΄)β2)
+ ((ββπ΄)β2)) + (((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β ((ββπ΄)β2)) +
((ββπ΄)β2)))) |
123 | 97, 118, 122 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) +
((absβπ΄)β2)) =
((2 Β· ((ββπ΄)β2)) + (i Β· (2 Β·
((ββπ΄) Β·
(ββπ΄)))))) |
124 | 123 | oveq2d 7374 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((π΄β2) + ((absβπ΄)β2))) = (i Β· ((2 Β·
((ββπ΄)β2))
+ (i Β· (2 Β· ((ββπ΄) Β· (ββπ΄))))))) |
125 | 91, 77, 42 | subdird 11617 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄))
= (((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) β ((2 Β·
(ββπ΄)) Β·
(ββπ΄)))) |
126 | 94, 124, 125 | 3eqtr4d 2783 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((π΄β2) + ((absβπ΄)β2))) = (((2 Β·
((ββπ΄) Β·
i)) β (2 Β· (ββπ΄))) Β· (ββπ΄))) |
127 | 91, 77 | subcld 11517 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄))) β
β) |
128 | | mulcom 11142 |
. . . . . . . . . . 11
β’
(((ββπ΄)
β β β§ i β β) β ((ββπ΄) Β· i) = (i Β·
(ββπ΄))) |
129 | 42, 22, 128 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)
Β· i) = (i Β· (ββπ΄))) |
130 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (ββπ΄)
β 0) |
131 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ ((i
Β· (ββπ΄))
= (ββπ΄) β
((i Β· (ββπ΄)) β β β
(ββπ΄) β
β)) |
132 | 48, 131 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i Β· (ββπ΄)) = (ββπ΄) β (i Β· (ββπ΄)) β
β)) |
133 | | rimul 12149 |
. . . . . . . . . . . . 13
β’
(((ββπ΄)
β β β§ (i Β· (ββπ΄)) β β) β
(ββπ΄) =
0) |
134 | 41, 132, 133 | syl6an 683 |
. . . . . . . . . . . 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 11527 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄))) = 0
β (2 Β· ((ββπ΄) Β· i)) = (2 Β·
(ββπ΄)))) |
139 | | 2ne0 12262 |
. . . . . . . . . . . . 13
β’ 2 β
0 |
140 | 139 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β 0)
β 2 β 0) |
141 | 63, 49, 46, 140 | mulcand 11793 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) = (2 Β·
(ββπ΄)) β
((ββπ΄) Β·
i) = (ββπ΄))) |
142 | 138, 141 | bitrd 279 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄))) = 0
β ((ββπ΄)
Β· i) = (ββπ΄))) |
143 | 142 | necon3bid 2985 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄))) β 0
β ((ββπ΄)
Β· i) β (ββπ΄))) |
144 | 137, 143 | mpbird 257 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄))) β
0) |
145 | 127, 42, 144, 130 | mulne0d 11812 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄))
β 0) |
146 | 126, 145 | eqnetrd 3008 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((π΄β2) + ((absβπ΄)β2))) β 0) |
147 | | oveq2 7366 |
. . . . . . . 8
β’ (((π΄β2) + ((absβπ΄)β2)) = 0 β (i
Β· ((π΄β2) +
((absβπ΄)β2))) =
(i Β· 0)) |
148 | | it0e0 12380 |
. . . . . . . 8
β’ (i
Β· 0) = 0 |
149 | 147, 148 | eqtrdi 2789 |
. . . . . . 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 11952 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((π΄β2) +
((absβπ΄)β2)) /
((absβπ΄)β2))
β 0) |
153 | 36, 152 | eqnetrd 3008 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((expβ(2 Β· (i Β· (ββ(logβπ΄))))) + 1) β
0) |
154 | | tanval3 16021 |
. . 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 585 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (tanβ(ββ(logβπ΄))) = (((expβ(2 Β· (i Β·
(ββ(logβπ΄))))) β 1) / (i Β·
((expβ(2 Β· (i Β· (ββ(logβπ΄))))) + 1)))) |
156 | 10, 14, 14, 20 | divsubdird 11975 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((π΄β2) β
((absβπ΄)β2)) /
((absβπ΄)β2)) =
(((π΄β2) /
((absβπ΄)β2))
β (((absβπ΄)β2) / ((absβπ΄)β2)))) |
157 | 33, 34 | oveq12d 7376 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((π΄β2) /
((absβπ΄)β2))
β (((absβπ΄)β2) / ((absβπ΄)β2))) = ((expβ(2 Β· (i
Β· (ββ(logβπ΄))))) β 1)) |
158 | 156, 157 | eqtr2d 2774 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((expβ(2 Β· (i Β· (ββ(logβπ΄))))) β 1) = (((π΄β2) β
((absβπ΄)β2)) /
((absβπ΄)β2))) |
159 | 36 | oveq2d 7374 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((expβ(2 Β· (i Β·
(ββ(logβπ΄))))) + 1)) = (i Β· (((π΄β2) + ((absβπ΄)β2)) / ((absβπ΄)β2)))) |
160 | 38, 37, 14, 20 | divassd 11971 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((i Β· ((π΄β2) + ((absβπ΄)β2))) / ((absβπ΄)β2)) = (i Β· (((π΄β2) + ((absβπ΄)β2)) / ((absβπ΄)β2)))) |
161 | 159, 160 | eqtr4d 2776 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((expβ(2 Β· (i Β·
(ββ(logβπ΄))))) + 1)) = ((i Β· ((π΄β2) + ((absβπ΄)β2))) / ((absβπ΄)β2))) |
162 | 158, 161 | oveq12d 7376 |
. 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 11517 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) β
((absβπ΄)β2))
β β) |
164 | | mulcl 11140 |
. . . . 5
β’ ((i
β β β§ ((π΄β2) + ((absβπ΄)β2)) β β) β (i
Β· ((π΄β2) +
((absβπ΄)β2)))
β β) |
165 | 22, 37, 164 | sylancr 588 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (i Β· ((π΄β2) + ((absβπ΄)β2))) β β) |
166 | 163, 165,
14, 146, 20 | divcan7d 11964 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((π΄β2)
β ((absβπ΄)β2)) / ((absβπ΄)β2)) / ((i Β· ((π΄β2) + ((absβπ΄)β2))) / ((absβπ΄)β2))) = (((π΄β2) β
((absβπ΄)β2)) /
(i Β· ((π΄β2) +
((absβπ΄)β2))))) |
167 | 115, 117 | oveq12d 7376 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) β
((absβπ΄)β2)) =
((((ββπ΄)β2)
+ ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2))) β (((ββπ΄)β2) +
((ββπ΄)β2)))) |
168 | 43, 96, 95 | pnpcand 11554 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((ββπ΄)β2) + ((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β ((ββπ΄)β2))) β
(((ββπ΄)β2)
+ ((ββπ΄)β2))) = (((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β ((ββπ΄)β2)) β
((ββπ΄)β2))) |
169 | 59, 95, 95 | subsub4d 11548 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2))
β ((ββπ΄)β2)) = ((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β (((ββπ΄)β2) +
((ββπ΄)β2)))) |
170 | 95 | 2timesd 12401 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄)β2)) = (((ββπ΄)β2) +
((ββπ΄)β2))) |
171 | 170 | oveq2d 7374 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β (2 Β·
((ββπ΄)β2))) = ((2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄)))) β (((ββπ΄)β2) +
((ββπ΄)β2)))) |
172 | 46, 63, 49 | mulassd 11183 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) = (2 Β·
(((ββπ΄) Β·
i) Β· (ββπ΄)))) |
173 | 42, 38, 49 | mulassd 11183 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((ββπ΄)
Β· i) Β· (ββπ΄)) = ((ββπ΄) Β· (i Β· (ββπ΄)))) |
174 | 173 | oveq2d 7374 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· (((ββπ΄) Β· i) Β· (ββπ΄))) = (2 Β·
((ββπ΄) Β·
(i Β· (ββπ΄))))) |
175 | 172, 174 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) = ((2 Β·
((ββπ΄) Β·
i)) Β· (ββπ΄))) |
176 | 49 | sqvald 14054 |
. . . . . . . . . 10
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((ββπ΄)β2) = ((ββπ΄) Β· (ββπ΄))) |
177 | 176 | oveq2d 7374 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄)β2)) = (2 Β·
((ββπ΄) Β·
(ββπ΄)))) |
178 | 46, 49, 49 | mulassd 11183 |
. . . . . . . . 9
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· (ββπ΄)) Β· (ββπ΄)) = (2 Β· ((ββπ΄) Β· (ββπ΄)))) |
179 | 177, 178 | eqtr4d 2776 |
. . . . . . . 8
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (2 Β· ((ββπ΄)β2)) = ((2 Β·
(ββπ΄)) Β·
(ββπ΄))) |
180 | 175, 179 | oveq12d 7376 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β (2 Β·
((ββπ΄)β2))) = (((2 Β·
((ββπ΄) Β·
i)) Β· (ββπ΄)) β ((2 Β· (ββπ΄)) Β· (ββπ΄)))) |
181 | 91, 77, 49 | subdird 11617 |
. . . . . . 7
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄))
= (((2 Β· ((ββπ΄) Β· i)) Β· (ββπ΄)) β ((2 Β·
(ββπ΄)) Β·
(ββπ΄)))) |
182 | 180, 181 | eqtr4d 2776 |
. . . . . 6
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β (2 Β·
((ββπ΄)β2))) = (((2 Β·
((ββπ΄) Β·
i)) β (2 Β· (ββπ΄))) Β· (ββπ΄))) |
183 | 169, 171,
182 | 3eqtr2d 2779 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((2 Β· ((ββπ΄) Β· (i Β· (ββπ΄)))) β
((ββπ΄)β2))
β ((ββπ΄)β2)) = (((2 Β·
((ββπ΄) Β·
i)) β (2 Β· (ββπ΄))) Β· (ββπ΄))) |
184 | 167, 168,
183 | 3eqtrd 2777 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((π΄β2) β
((absβπ΄)β2)) =
(((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄))) |
185 | 184, 126 | oveq12d 7376 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (((π΄β2) β
((absβπ΄)β2)) /
(i Β· ((π΄β2) +
((absβπ΄)β2)))) =
((((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄))
/ (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄)))) |
186 | 49, 42, 127, 130, 144 | divcan5d 11962 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄))
/ (((2 Β· ((ββπ΄) Β· i)) β (2 Β·
(ββπ΄)))
Β· (ββπ΄)))
= ((ββπ΄) /
(ββπ΄))) |
187 | 166, 185,
186 | 3eqtrd 2777 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β 0)
β ((((π΄β2)
β ((absβπ΄)β2)) / ((absβπ΄)β2)) / ((i Β· ((π΄β2) + ((absβπ΄)β2))) / ((absβπ΄)β2))) =
((ββπ΄) /
(ββπ΄))) |
188 | 155, 162,
187 | 3eqtrd 2777 |
1
β’ ((π΄ β β β§
(ββπ΄) β 0)
β (tanβ(ββ(logβπ΄))) = ((ββπ΄) / (ββπ΄))) |