Step | Hyp | Ref
| Expression |
1 | | ax-icn 11115 |
. . . . . . 7
β’ i β
β |
2 | | recn 11146 |
. . . . . . 7
β’ (π΄ β β β π΄ β
β) |
3 | | mulcl 11140 |
. . . . . . 7
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
4 | 1, 2, 3 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (i
Β· π΄) β
β) |
5 | | rpcoshcl 16044 |
. . . . . . 7
β’ (π΄ β β β
(cosβ(i Β· π΄))
β β+) |
6 | 5 | rpne0d 12967 |
. . . . . 6
β’ (π΄ β β β
(cosβ(i Β· π΄))
β 0) |
7 | | tanval 16015 |
. . . . . 6
β’ (((i
Β· π΄) β β
β§ (cosβ(i Β· π΄)) β 0) β (tanβ(i Β·
π΄)) = ((sinβ(i
Β· π΄)) /
(cosβ(i Β· π΄)))) |
8 | 4, 6, 7 | syl2anc 585 |
. . . . 5
β’ (π΄ β β β
(tanβ(i Β· π΄))
= ((sinβ(i Β· π΄)) / (cosβ(i Β· π΄)))) |
9 | 8 | oveq1d 7373 |
. . . 4
β’ (π΄ β β β
((tanβ(i Β· π΄))
/ i) = (((sinβ(i Β· π΄)) / (cosβ(i Β· π΄))) / i)) |
10 | 4 | sincld 16017 |
. . . . 5
β’ (π΄ β β β
(sinβ(i Β· π΄))
β β) |
11 | | recoshcl 16045 |
. . . . . 6
β’ (π΄ β β β
(cosβ(i Β· π΄))
β β) |
12 | 11 | recnd 11188 |
. . . . 5
β’ (π΄ β β β
(cosβ(i Β· π΄))
β β) |
13 | 1 | a1i 11 |
. . . . 5
β’ (π΄ β β β i β
β) |
14 | | ine0 11595 |
. . . . . 6
β’ i β
0 |
15 | 14 | a1i 11 |
. . . . 5
β’ (π΄ β β β i β
0) |
16 | 10, 12, 13, 6, 15 | divdiv32d 11961 |
. . . 4
β’ (π΄ β β β
(((sinβ(i Β· π΄)) / (cosβ(i Β· π΄))) / i) = (((sinβ(i
Β· π΄)) / i) /
(cosβ(i Β· π΄)))) |
17 | | sinhval 16041 |
. . . . . 6
β’ (π΄ β β β
((sinβ(i Β· π΄))
/ i) = (((expβπ΄)
β (expβ-π΄)) /
2)) |
18 | 2, 17 | syl 17 |
. . . . 5
β’ (π΄ β β β
((sinβ(i Β· π΄))
/ i) = (((expβπ΄)
β (expβ-π΄)) /
2)) |
19 | | coshval 16042 |
. . . . . 6
β’ (π΄ β β β
(cosβ(i Β· π΄))
= (((expβπ΄) +
(expβ-π΄)) /
2)) |
20 | 2, 19 | syl 17 |
. . . . 5
β’ (π΄ β β β
(cosβ(i Β· π΄))
= (((expβπ΄) +
(expβ-π΄)) /
2)) |
21 | 18, 20 | oveq12d 7376 |
. . . 4
β’ (π΄ β β β
(((sinβ(i Β· π΄)) / i) / (cosβ(i Β· π΄))) = ((((expβπ΄) β (expβ-π΄)) / 2) / (((expβπ΄) + (expβ-π΄)) / 2))) |
22 | 9, 16, 21 | 3eqtrd 2777 |
. . 3
β’ (π΄ β β β
((tanβ(i Β· π΄))
/ i) = ((((expβπ΄)
β (expβ-π΄)) /
2) / (((expβπ΄) +
(expβ-π΄)) /
2))) |
23 | | reefcl 15974 |
. . . . . 6
β’ (π΄ β β β
(expβπ΄) β
β) |
24 | | renegcl 11469 |
. . . . . . 7
β’ (π΄ β β β -π΄ β
β) |
25 | 24 | reefcld 15975 |
. . . . . 6
β’ (π΄ β β β
(expβ-π΄) β
β) |
26 | 23, 25 | resubcld 11588 |
. . . . 5
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) β
β) |
27 | 26 | recnd 11188 |
. . . 4
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) β
β) |
28 | 23, 25 | readdcld 11189 |
. . . . 5
β’ (π΄ β β β
((expβπ΄) +
(expβ-π΄)) β
β) |
29 | 28 | recnd 11188 |
. . . 4
β’ (π΄ β β β
((expβπ΄) +
(expβ-π΄)) β
β) |
30 | | 2cnd 12236 |
. . . 4
β’ (π΄ β β β 2 β
β) |
31 | 20, 6 | eqnetrrd 3009 |
. . . . 5
β’ (π΄ β β β
(((expβπ΄) +
(expβ-π΄)) / 2) β
0) |
32 | | 2ne0 12262 |
. . . . . . 7
β’ 2 β
0 |
33 | 32 | a1i 11 |
. . . . . 6
β’ (π΄ β β β 2 β
0) |
34 | 29, 30, 33 | divne0bd 11948 |
. . . . 5
β’ (π΄ β β β
(((expβπ΄) +
(expβ-π΄)) β 0
β (((expβπ΄) +
(expβ-π΄)) / 2) β
0)) |
35 | 31, 34 | mpbird 257 |
. . . 4
β’ (π΄ β β β
((expβπ΄) +
(expβ-π΄)) β
0) |
36 | 27, 29, 30, 35, 33 | divcan7d 11964 |
. . 3
β’ (π΄ β β β
((((expβπ΄) β
(expβ-π΄)) / 2) /
(((expβπ΄) +
(expβ-π΄)) / 2)) =
(((expβπ΄) β
(expβ-π΄)) /
((expβπ΄) +
(expβ-π΄)))) |
37 | 22, 36 | eqtrd 2773 |
. 2
β’ (π΄ β β β
((tanβ(i Β· π΄))
/ i) = (((expβπ΄)
β (expβ-π΄)) /
((expβπ΄) +
(expβ-π΄)))) |
38 | 24 | rpefcld 15992 |
. . . . . 6
β’ (π΄ β β β
(expβ-π΄) β
β+) |
39 | 23, 38 | ltsubrpd 12994 |
. . . . 5
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) <
(expβπ΄)) |
40 | 23, 38 | ltaddrpd 12995 |
. . . . 5
β’ (π΄ β β β
(expβπ΄) <
((expβπ΄) +
(expβ-π΄))) |
41 | 26, 23, 28, 39, 40 | lttrd 11321 |
. . . 4
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) <
((expβπ΄) +
(expβ-π΄))) |
42 | 29 | mulid1d 11177 |
. . . 4
β’ (π΄ β β β
(((expβπ΄) +
(expβ-π΄)) Β· 1)
= ((expβπ΄) +
(expβ-π΄))) |
43 | 41, 42 | breqtrrd 5134 |
. . 3
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) <
(((expβπ΄) +
(expβ-π΄)) Β·
1)) |
44 | | 1red 11161 |
. . . 4
β’ (π΄ β β β 1 β
β) |
45 | | efgt0 15990 |
. . . . 5
β’ (π΄ β β β 0 <
(expβπ΄)) |
46 | | efgt0 15990 |
. . . . . 6
β’ (-π΄ β β β 0 <
(expβ-π΄)) |
47 | 24, 46 | syl 17 |
. . . . 5
β’ (π΄ β β β 0 <
(expβ-π΄)) |
48 | 23, 25, 45, 47 | addgt0d 11735 |
. . . 4
β’ (π΄ β β β 0 <
((expβπ΄) +
(expβ-π΄))) |
49 | | ltdivmul 12035 |
. . . 4
β’
((((expβπ΄)
β (expβ-π΄))
β β β§ 1 β β β§ (((expβπ΄) + (expβ-π΄)) β β β§ 0 <
((expβπ΄) +
(expβ-π΄)))) β
((((expβπ΄) β
(expβ-π΄)) /
((expβπ΄) +
(expβ-π΄))) < 1
β ((expβπ΄)
β (expβ-π΄))
< (((expβπ΄) +
(expβ-π΄)) Β·
1))) |
50 | 26, 44, 28, 48, 49 | syl112anc 1375 |
. . 3
β’ (π΄ β β β
((((expβπ΄) β
(expβ-π΄)) /
((expβπ΄) +
(expβ-π΄))) < 1
β ((expβπ΄)
β (expβ-π΄))
< (((expβπ΄) +
(expβ-π΄)) Β·
1))) |
51 | 43, 50 | mpbird 257 |
. 2
β’ (π΄ β β β
(((expβπ΄) β
(expβ-π΄)) /
((expβπ΄) +
(expβ-π΄))) <
1) |
52 | 37, 51 | eqbrtrd 5128 |
1
β’ (π΄ β β β
((tanβ(i Β· π΄))
/ i) < 1) |