Step | Hyp | Ref
| Expression |
1 | | tanvalap 11715 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
2 | | 2cn 8989 |
. . . . . . 7
β’ 2 β
β |
3 | | ax-icn 7905 |
. . . . . . 7
β’ i β
β |
4 | 2, 3 | mulcomi 7962 |
. . . . . 6
β’ (2
Β· i) = (i Β· 2) |
5 | 4 | oveq2i 5885 |
. . . . 5
β’
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (i Β·
2)) |
6 | | sinval 11709 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
7 | 6 | adantr 276 |
. . . . 5
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(sinβπ΄) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
8 | | simpl 109 |
. . . . . . . . 9
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
π΄ β
β) |
9 | | mulcl 7937 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
10 | 3, 8, 9 | sylancr 414 |
. . . . . . . 8
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(i Β· π΄) β
β) |
11 | | efcl 11671 |
. . . . . . . 8
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) β β) |
12 | 10, 11 | syl 14 |
. . . . . . 7
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(expβ(i Β· π΄))
β β) |
13 | | negicn 8157 |
. . . . . . . . 9
β’ -i β
β |
14 | | mulcl 7937 |
. . . . . . . . 9
β’ ((-i
β β β§ π΄
β β) β (-i Β· π΄) β β) |
15 | 13, 8, 14 | sylancr 414 |
. . . . . . . 8
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(-i Β· π΄) β
β) |
16 | | efcl 11671 |
. . . . . . . 8
β’ ((-i
Β· π΄) β β
β (expβ(-i Β· π΄)) β β) |
17 | 15, 16 | syl 14 |
. . . . . . 7
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(expβ(-i Β· π΄))
β β) |
18 | 12, 17 | subcld 8267 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) β β) |
19 | 3 | a1i 9 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) # 0) β i
β β) |
20 | 2 | a1i 9 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) # 0) β 2
β β) |
21 | | iap0 9141 |
. . . . . . 7
β’ i #
0 |
22 | 21 | a1i 9 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) # 0) β i
# 0) |
23 | | 2ap0 9011 |
. . . . . . 7
β’ 2 #
0 |
24 | 23 | a1i 9 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) # 0) β 2
# 0) |
25 | 18, 19, 20, 22, 24 | divdivap1d 8778 |
. . . . 5
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) / 2) = (((expβ(i
Β· π΄)) β
(expβ(-i Β· π΄))) / (i Β· 2))) |
26 | 5, 7, 25 | 3eqtr4a 2236 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(sinβπ΄) =
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) / 2)) |
27 | | cosval 11710 |
. . . . 5
β’ (π΄ β β β
(cosβπ΄) =
(((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2)) |
28 | 27 | adantr 276 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(cosβπ΄) =
(((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2)) |
29 | 26, 28 | oveq12d 5892 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
((sinβπ΄) /
(cosβπ΄)) =
(((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) / 2) / (((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄))) / 2))) |
30 | 1, 29 | eqtrd 2210 |
. 2
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(tanβπ΄) =
(((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) / 2) / (((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄))) / 2))) |
31 | 18, 19, 22 | divclapd 8746 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) β
β) |
32 | 12, 17 | addcld 7976 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄))) β β) |
33 | | simpr 110 |
. . . . 5
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(cosβπ΄) #
0) |
34 | 28, 33 | eqbrtrrd 4027 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2) # 0) |
35 | 32, 20, 24 | divap0bd 8758 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) # 0 β (((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄))) / 2) # 0)) |
36 | 34, 35 | mpbird 167 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄))) # 0) |
37 | 31, 32, 20, 36, 24 | divcanap7d 8775 |
. 2
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) / 2) / (((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄))) / 2)) = ((((expβ(i Β· π΄)) β (expβ(-i
Β· π΄))) / i) /
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄))))) |
38 | 18, 19, 32, 22, 36 | divdivap1d 8778 |
. 2
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / i) / ((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄)))) = (((expβ(i Β· π΄)) β (expβ(-i
Β· π΄))) / (i Β·
((expβ(i Β· π΄))
+ (expβ(-i Β· π΄)))))) |
39 | 30, 37, 38 | 3eqtrd 2214 |
1
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(tanβπ΄) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (i Β· ((expβ(i
Β· π΄)) +
(expβ(-i Β· π΄)))))) |