Step | Hyp | Ref
| Expression |
1 | | elioore 9911 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ β
β) |
2 | 1 | recoscld 11731 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβπ΄) β
β) |
3 | 1, 2 | remulcld 7987 |
. . . 4
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β·
(cosβπ΄)) β
β) |
4 | | 1re 7955 |
. . . . . . 7
β’ 1 β
β |
5 | | rehalfcl 9145 |
. . . . . . . . . 10
β’ (π΄ β β β (π΄ / 2) β
β) |
6 | 1, 5 | syl 14 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ / 2) β
β) |
7 | 6 | resqcld 10679 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2)β2) β
β) |
8 | | 3nn 9080 |
. . . . . . . 8
β’ 3 β
β |
9 | | nndivre 8954 |
. . . . . . . 8
β’ ((((π΄ / 2)β2) β β
β§ 3 β β) β (((π΄ / 2)β2) / 3) β
β) |
10 | 7, 8, 9 | sylancl 413 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2)β2) / 3)
β β) |
11 | | resubcl 8220 |
. . . . . . 7
β’ ((1
β β β§ (((π΄ /
2)β2) / 3) β β) β (1 β (((π΄ / 2)β2) / 3)) β
β) |
12 | 4, 10, 11 | sylancr 414 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
(1 β (((π΄ /
2)β2) / 3)) β β) |
13 | 1, 12 | remulcld 7987 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
β β) |
14 | | 2re 8988 |
. . . . . . 7
β’ 2 β
β |
15 | | remulcl 7938 |
. . . . . . 7
β’ ((2
β β β§ (((π΄ /
2)β2) / 3) β β) β (2 Β· (((π΄ / 2)β2) / 3)) β
β) |
16 | 14, 10, 15 | sylancr 414 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (((π΄ /
2)β2) / 3)) β β) |
17 | | resubcl 8220 |
. . . . . 6
β’ ((1
β β β§ (2 Β· (((π΄ / 2)β2) / 3)) β β) β
(1 β (2 Β· (((π΄
/ 2)β2) / 3))) β β) |
18 | 4, 16, 17 | sylancr 414 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
(1 β (2 Β· (((π΄
/ 2)β2) / 3))) β β) |
19 | 13, 18 | remulcld 7987 |
. . . 4
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) β
β) |
20 | 1 | resincld 11730 |
. . . 4
β’ (π΄ β (0(,)(Ο / 2)) β
(sinβπ΄) β
β) |
21 | 12 | resqcld 10679 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3))β2) β β) |
22 | | remulcl 7938 |
. . . . . . . . 9
β’ ((2
β β β§ ((1 β (((π΄ / 2)β2) / 3))β2) β β)
β (2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) β
β) |
23 | 14, 21, 22 | sylancr 414 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) β
β) |
24 | | resubcl 8220 |
. . . . . . . 8
β’ (((2
Β· ((1 β (((π΄ /
2)β2) / 3))β2)) β β β§ 1 β β) β ((2
Β· ((1 β (((π΄ /
2)β2) / 3))β2)) β 1) β β) |
25 | 23, 4, 24 | sylancl 413 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) β 1)
β β) |
26 | 12, 18 | remulcld 7987 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) β
β) |
27 | 1 | recnd 7985 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ β
β) |
28 | | 2cn 8989 |
. . . . . . . . . . . 12
β’ 2 β
β |
29 | 28 | a1i 9 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
2 β β) |
30 | | 2ap0 9011 |
. . . . . . . . . . . 12
β’ 2 #
0 |
31 | 30 | a1i 9 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
2 # 0) |
32 | 27, 29, 31 | divcanap2d 8748 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (π΄ / 2)) =
π΄) |
33 | 32 | fveq2d 5519 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβ(2 Β· (π΄ /
2))) = (cosβπ΄)) |
34 | 6 | recnd 7985 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ / 2) β
β) |
35 | | cos2t 11757 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β β
(cosβ(2 Β· (π΄ /
2))) = ((2 Β· ((cosβ(π΄ / 2))β2)) β 1)) |
36 | 34, 35 | syl 14 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβ(2 Β· (π΄ /
2))) = ((2 Β· ((cosβ(π΄ / 2))β2)) β 1)) |
37 | 33, 36 | eqtr3d 2212 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβπ΄) = ((2
Β· ((cosβ(π΄ /
2))β2)) β 1)) |
38 | 6 | recoscld 11731 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβ(π΄ / 2)) β
β) |
39 | 38 | resqcld 10679 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((cosβ(π΄ /
2))β2) β β) |
40 | | remulcl 7938 |
. . . . . . . . . 10
β’ ((2
β β β§ ((cosβ(π΄ / 2))β2) β β) β (2
Β· ((cosβ(π΄ /
2))β2)) β β) |
41 | 14, 39, 40 | sylancr 414 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((cosβ(π΄
/ 2))β2)) β β) |
42 | 4 | a1i 9 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
1 β β) |
43 | 14 | a1i 9 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
2 β β) |
44 | | eliooord 9927 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (0(,)(Ο / 2)) β
(0 < π΄ β§ π΄ < (Ο /
2))) |
45 | 44 | simpld 112 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
0 < π΄) |
46 | | 2pos 9009 |
. . . . . . . . . . . . . . . 16
β’ 0 <
2 |
47 | 46 | a1i 9 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
0 < 2) |
48 | 1, 43, 45, 47 | divgt0d 8891 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
0 < (π΄ /
2)) |
49 | | pire 14177 |
. . . . . . . . . . . . . . . . . . 19
β’ Ο
β β |
50 | | rehalfcl 9145 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ο
β β β (Ο / 2) β β) |
51 | 49, 50 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β (0(,)(Ο / 2)) β
(Ο / 2) β β) |
52 | 44 | simprd 114 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ < (Ο /
2)) |
53 | | pigt2lt4 14175 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (2 <
Ο β§ Ο < 4) |
54 | 53 | simpri 113 |
. . . . . . . . . . . . . . . . . . . . 21
β’ Ο <
4 |
55 | | 2t2e4 9072 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2
Β· 2) = 4 |
56 | 54, 55 | breqtrri 4030 |
. . . . . . . . . . . . . . . . . . . 20
β’ Ο <
(2 Β· 2) |
57 | 14, 46 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2 β
β β§ 0 < 2) |
58 | | ltdivmul 8832 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Ο
β β β§ 2 β β β§ (2 β β β§ 0 < 2))
β ((Ο / 2) < 2 β Ο < (2 Β· 2))) |
59 | 49, 14, 57, 58 | mp3an 1337 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Ο /
2) < 2 β Ο < (2 Β· 2)) |
60 | 56, 59 | mpbir 146 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ο /
2) < 2 |
61 | 60 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β (0(,)(Ο / 2)) β
(Ο / 2) < 2) |
62 | 1, 51, 43, 52, 61 | lttrd 8082 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ < 2) |
63 | 28 | mullidi 7959 |
. . . . . . . . . . . . . . . . 17
β’ (1
Β· 2) = 2 |
64 | 62, 63 | breqtrrdi 4045 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ < (1 Β·
2)) |
65 | | ltdivmul2 8834 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ 1 β
β β§ (2 β β β§ 0 < 2)) β ((π΄ / 2) < 1 β π΄ < (1 Β· 2))) |
66 | 1, 42, 43, 47, 65 | syl112anc 1242 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) < 1 β
π΄ < (1 Β·
2))) |
67 | 64, 66 | mpbird 167 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ / 2) <
1) |
68 | 6, 42, 67 | ltled 8075 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ / 2) β€
1) |
69 | | 0xr 8003 |
. . . . . . . . . . . . . . 15
β’ 0 β
β* |
70 | | elioc2 9935 |
. . . . . . . . . . . . . . 15
β’ ((0
β β* β§ 1 β β) β ((π΄ / 2) β (0(,]1) β ((π΄ / 2) β β β§ 0
< (π΄ / 2) β§ (π΄ / 2) β€ 1))) |
71 | 69, 4, 70 | mp2an 426 |
. . . . . . . . . . . . . 14
β’ ((π΄ / 2) β (0(,]1) β
((π΄ / 2) β β
β§ 0 < (π΄ / 2) β§
(π΄ / 2) β€
1)) |
72 | 6, 48, 68, 71 | syl3anbrc 1181 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ / 2) β
(0(,]1)) |
73 | | cos01bnd 11765 |
. . . . . . . . . . . . 13
β’ ((π΄ / 2) β (0(,]1) β ((1
β (2 Β· (((π΄ /
2)β2) / 3))) < (cosβ(π΄ / 2)) β§ (cosβ(π΄ / 2)) < (1 β (((π΄ / 2)β2) / 3)))) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (2 Β· (((π΄ / 2)β2) / 3))) < (cosβ(π΄ / 2)) β§ (cosβ(π΄ / 2)) < (1 β (((π΄ / 2)β2) /
3)))) |
75 | 74 | simprd 114 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβ(π΄ / 2)) < (1
β (((π΄ / 2)β2) /
3))) |
76 | | cos01gt0 11769 |
. . . . . . . . . . . . . 14
β’ ((π΄ / 2) β (0(,]1) β 0
< (cosβ(π΄ /
2))) |
77 | 72, 76 | syl 14 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
0 < (cosβ(π΄ /
2))) |
78 | | 0re 7956 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
79 | | ltle 8044 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (cosβ(π΄ / 2)) β β) β (0 <
(cosβ(π΄ / 2)) β
0 β€ (cosβ(π΄ /
2)))) |
80 | 78, 38, 79 | sylancr 414 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(0 < (cosβ(π΄ / 2))
β 0 β€ (cosβ(π΄
/ 2)))) |
81 | 77, 80 | mpd 13 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
0 β€ (cosβ(π΄ /
2))) |
82 | 78 | a1i 9 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
0 β β) |
83 | 82, 38, 12, 77, 75 | lttrd 8082 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
0 < (1 β (((π΄ /
2)β2) / 3))) |
84 | 82, 12, 83 | ltled 8075 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
0 β€ (1 β (((π΄ /
2)β2) / 3))) |
85 | 38, 12, 81, 84 | lt2sqd 10684 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((cosβ(π΄ / 2)) <
(1 β (((π΄ /
2)β2) / 3)) β ((cosβ(π΄ / 2))β2) < ((1 β (((π΄ / 2)β2) /
3))β2))) |
86 | 75, 85 | mpbid 147 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((cosβ(π΄ /
2))β2) < ((1 β (((π΄ / 2)β2) /
3))β2)) |
87 | | ltmul2 8812 |
. . . . . . . . . . 11
β’
((((cosβ(π΄ /
2))β2) β β β§ ((1 β (((π΄ / 2)β2) / 3))β2) β β
β§ (2 β β β§ 0 < 2)) β (((cosβ(π΄ / 2))β2) < ((1 β (((π΄ / 2)β2) / 3))β2)
β (2 Β· ((cosβ(π΄ / 2))β2)) < (2 Β· ((1 β
(((π΄ / 2)β2) /
3))β2)))) |
88 | 39, 21, 43, 47, 87 | syl112anc 1242 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(((cosβ(π΄ /
2))β2) < ((1 β (((π΄ / 2)β2) / 3))β2) β (2
Β· ((cosβ(π΄ /
2))β2)) < (2 Β· ((1 β (((π΄ / 2)β2) /
3))β2)))) |
89 | 86, 88 | mpbid 147 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((cosβ(π΄
/ 2))β2)) < (2 Β· ((1 β (((π΄ / 2)β2) /
3))β2))) |
90 | 41, 23, 42, 89 | ltsub1dd 8513 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· ((cosβ(π΄
/ 2))β2)) β 1) < ((2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) β
1)) |
91 | 37, 90 | eqbrtrd 4025 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβπ΄) < ((2
Β· ((1 β (((π΄ /
2)β2) / 3))β2)) β 1)) |
92 | | 3re 8992 |
. . . . . . . . . 10
β’ 3 β
β |
93 | | remulcl 7938 |
. . . . . . . . . 10
β’ ((3
β β β§ (((π΄ /
2)β2) / 3) β β) β (3 Β· (((π΄ / 2)β2) / 3)) β
β) |
94 | 92, 10, 93 | sylancr 414 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(3 Β· (((π΄ /
2)β2) / 3)) β β) |
95 | | 4re 8995 |
. . . . . . . . . 10
β’ 4 β
β |
96 | | remulcl 7938 |
. . . . . . . . . 10
β’ ((4
β β β§ (((π΄ /
2)β2) / 3) β β) β (4 Β· (((π΄ / 2)β2) / 3)) β
β) |
97 | 95, 10, 96 | sylancr 414 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(4 Β· (((π΄ /
2)β2) / 3)) β β) |
98 | 10 | resqcld 10679 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((((π΄ / 2)β2) /
3)β2) β β) |
99 | | remulcl 7938 |
. . . . . . . . . . 11
β’ ((2
β β β§ ((((π΄
/ 2)β2) / 3)β2) β β) β (2 Β· ((((π΄ / 2)β2) / 3)β2))
β β) |
100 | 14, 98, 99 | sylancr 414 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((((π΄ /
2)β2) / 3)β2)) β β) |
101 | | readdcl 7936 |
. . . . . . . . . 10
β’ ((1
β β β§ (2 Β· ((((π΄ / 2)β2) / 3)β2)) β β)
β (1 + (2 Β· ((((π΄ / 2)β2) / 3)β2))) β
β) |
102 | 4, 100, 101 | sylancr 414 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(1 + (2 Β· ((((π΄ /
2)β2) / 3)β2))) β β) |
103 | | 3lt4 9090 |
. . . . . . . . . 10
β’ 3 <
4 |
104 | 92 | a1i 9 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
3 β β) |
105 | 95 | a1i 9 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
4 β β) |
106 | 6, 48 | gt0ap0d 8585 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ / 2) #
0) |
107 | 6, 106 | sqgt0apd 10681 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
0 < ((π΄ /
2)β2)) |
108 | | 3pos 9012 |
. . . . . . . . . . . . 13
β’ 0 <
3 |
109 | 108 | a1i 9 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
0 < 3) |
110 | 7, 104, 107, 109 | divgt0d 8891 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
0 < (((π΄ / 2)β2) /
3)) |
111 | | ltmul1 8548 |
. . . . . . . . . . 11
β’ ((3
β β β§ 4 β β β§ ((((π΄ / 2)β2) / 3) β β β§ 0
< (((π΄ / 2)β2) /
3))) β (3 < 4 β (3 Β· (((π΄ / 2)β2) / 3)) < (4 Β·
(((π΄ / 2)β2) /
3)))) |
112 | 104, 105,
10, 110, 111 | syl112anc 1242 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(3 < 4 β (3 Β· (((π΄ / 2)β2) / 3)) < (4 Β·
(((π΄ / 2)β2) /
3)))) |
113 | 103, 112 | mpbii 148 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(3 Β· (((π΄ /
2)β2) / 3)) < (4 Β· (((π΄ / 2)β2) / 3))) |
114 | 94, 97, 102, 113 | ltsub2dd 8514 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
((1 + (2 Β· ((((π΄ /
2)β2) / 3)β2))) β (4 Β· (((π΄ / 2)β2) / 3))) < ((1 + (2 Β·
((((π΄ / 2)β2) /
3)β2))) β (3 Β· (((π΄ / 2)β2) / 3)))) |
115 | 42 | recnd 7985 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
1 β β) |
116 | | ax-1cn 7903 |
. . . . . . . . . . 11
β’ 1 β
β |
117 | 100 | recnd 7985 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((((π΄ /
2)β2) / 3)β2)) β β) |
118 | | addcl 7935 |
. . . . . . . . . . 11
β’ ((1
β β β§ (2 Β· ((((π΄ / 2)β2) / 3)β2)) β β)
β (1 + (2 Β· ((((π΄ / 2)β2) / 3)β2))) β
β) |
119 | 116, 117,
118 | sylancr 414 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(1 + (2 Β· ((((π΄ /
2)β2) / 3)β2))) β β) |
120 | 97 | recnd 7985 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(4 Β· (((π΄ /
2)β2) / 3)) β β) |
121 | 119, 120 | subcld 8267 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((1 + (2 Β· ((((π΄ /
2)β2) / 3)β2))) β (4 Β· (((π΄ / 2)β2) / 3))) β
β) |
122 | | sq1 10613 |
. . . . . . . . . . . . . . 15
β’
(1β2) = 1 |
123 | 122 | a1i 9 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
(1β2) = 1) |
124 | 10 | recnd 7985 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2)β2) / 3)
β β) |
125 | 124 | mulid2d 7975 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
(1 Β· (((π΄ /
2)β2) / 3)) = (((π΄ /
2)β2) / 3)) |
126 | 125 | oveq2d 5890 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (1 Β· (((π΄ / 2)β2) / 3))) = (2 Β· (((π΄ / 2)β2) /
3))) |
127 | 123, 126 | oveq12d 5892 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
((1β2) β (2 Β· (1 Β· (((π΄ / 2)β2) / 3)))) = (1 β (2
Β· (((π΄ / 2)β2)
/ 3)))) |
128 | 127 | oveq1d 5889 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
(((1β2) β (2 Β· (1 Β· (((π΄ / 2)β2) / 3)))) + ((((π΄ / 2)β2) / 3)β2)) =
((1 β (2 Β· (((π΄ / 2)β2) / 3))) + ((((π΄ / 2)β2) /
3)β2))) |
129 | | binom2sub 10633 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (((π΄ /
2)β2) / 3) β β) β ((1 β (((π΄ / 2)β2) / 3))β2) = (((1β2)
β (2 Β· (1 Β· (((π΄ / 2)β2) / 3)))) + ((((π΄ / 2)β2) /
3)β2))) |
130 | 116, 124,
129 | sylancr 414 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3))β2) = (((1β2) β (2 Β· (1 Β·
(((π΄ / 2)β2) / 3)))) +
((((π΄ / 2)β2) /
3)β2))) |
131 | 98 | recnd 7985 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
((((π΄ / 2)β2) /
3)β2) β β) |
132 | 16 | recnd 7985 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (((π΄ /
2)β2) / 3)) β β) |
133 | 115, 131,
132 | addsubd 8288 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((1 + ((((π΄ / 2)β2) /
3)β2)) β (2 Β· (((π΄ / 2)β2) / 3))) = ((1 β (2
Β· (((π΄ / 2)β2)
/ 3))) + ((((π΄ / 2)β2)
/ 3)β2))) |
134 | 128, 130,
133 | 3eqtr4d 2220 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3))β2) = ((1 + ((((π΄ / 2)β2) / 3)β2)) β (2
Β· (((π΄ / 2)β2)
/ 3)))) |
135 | 134 | oveq2d 5890 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) = (2 Β·
((1 + ((((π΄ / 2)β2) /
3)β2)) β (2 Β· (((π΄ / 2)β2) / 3))))) |
136 | | addcl 7935 |
. . . . . . . . . . . 12
β’ ((1
β β β§ ((((π΄
/ 2)β2) / 3)β2) β β) β (1 + ((((π΄ / 2)β2) / 3)β2)) β
β) |
137 | 116, 131,
136 | sylancr 414 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(1 + ((((π΄ / 2)β2) /
3)β2)) β β) |
138 | 29, 137, 132 | subdid 8370 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((1 + ((((π΄ /
2)β2) / 3)β2)) β (2 Β· (((π΄ / 2)β2) / 3)))) = ((2 Β· (1 +
((((π΄ / 2)β2) /
3)β2))) β (2 Β· (2 Β· (((π΄ / 2)β2) / 3))))) |
139 | 29, 115, 131 | adddid 7981 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (1 + ((((π΄ /
2)β2) / 3)β2))) = ((2 Β· 1) + (2 Β· ((((π΄ / 2)β2) /
3)β2)))) |
140 | 116 | 2timesi 9048 |
. . . . . . . . . . . . . . 15
β’ (2
Β· 1) = (1 + 1) |
141 | 140 | oveq1i 5884 |
. . . . . . . . . . . . . 14
β’ ((2
Β· 1) + (2 Β· ((((π΄ / 2)β2) / 3)β2))) = ((1 + 1) + (2
Β· ((((π΄ / 2)β2)
/ 3)β2))) |
142 | 115, 115,
117 | addassd 7979 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
((1 + 1) + (2 Β· ((((π΄ / 2)β2) / 3)β2))) = (1 + (1 + (2
Β· ((((π΄ / 2)β2)
/ 3)β2))))) |
143 | 141, 142 | eqtrid 2222 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· 1) + (2 Β· ((((π΄ / 2)β2) / 3)β2))) = (1 + (1 + (2
Β· ((((π΄ / 2)β2)
/ 3)β2))))) |
144 | 139, 143 | eqtrd 2210 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (1 + ((((π΄ /
2)β2) / 3)β2))) = (1 + (1 + (2 Β· ((((π΄ / 2)β2) /
3)β2))))) |
145 | 29, 29, 124 | mulassd 7980 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· 2) Β· (((π΄ / 2)β2) / 3)) = (2 Β· (2
Β· (((π΄ / 2)β2)
/ 3)))) |
146 | 55 | oveq1i 5884 |
. . . . . . . . . . . . 13
β’ ((2
Β· 2) Β· (((π΄ /
2)β2) / 3)) = (4 Β· (((π΄ / 2)β2) / 3)) |
147 | 145, 146 | eqtr3di 2225 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (2 Β· (((π΄ / 2)β2) / 3))) = (4 Β· (((π΄ / 2)β2) /
3))) |
148 | 144, 147 | oveq12d 5892 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· (1 + ((((π΄ /
2)β2) / 3)β2))) β (2 Β· (2 Β· (((π΄ / 2)β2) / 3)))) = ((1 + (1 + (2
Β· ((((π΄ / 2)β2)
/ 3)β2)))) β (4 Β· (((π΄ / 2)β2) / 3)))) |
149 | 115, 119,
120, 148 | assraddsubd 8324 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· (1 + ((((π΄ /
2)β2) / 3)β2))) β (2 Β· (2 Β· (((π΄ / 2)β2) / 3)))) = (1 + ((1 + (2
Β· ((((π΄ / 2)β2)
/ 3)β2))) β (4 Β· (((π΄ / 2)β2) / 3))))) |
150 | 135, 138,
149 | 3eqtrd 2214 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) = (1 + ((1 + (2
Β· ((((π΄ / 2)β2)
/ 3)β2))) β (4 Β· (((π΄ / 2)β2) / 3))))) |
151 | 115, 121,
150 | mvrladdd 8323 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) β 1) =
((1 + (2 Β· ((((π΄ /
2)β2) / 3)β2))) β (4 Β· (((π΄ / 2)β2) / 3)))) |
152 | | subcl 8155 |
. . . . . . . . . . 11
β’ ((1
β β β§ (((π΄ /
2)β2) / 3) β β) β (1 β (((π΄ / 2)β2) / 3)) β
β) |
153 | 116, 124,
152 | sylancr 414 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(1 β (((π΄ /
2)β2) / 3)) β β) |
154 | 153, 115,
132 | subdid 8370 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) = (((1 β
(((π΄ / 2)β2) / 3))
Β· 1) β ((1 β (((π΄ / 2)β2) / 3)) Β· (2 Β·
(((π΄ / 2)β2) /
3))))) |
155 | 153 | mulridd 7973 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) Β· 1) = (1 β (((π΄ / 2)β2) / 3))) |
156 | 115, 124,
132 | subdird 8371 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) Β· (2 Β· (((π΄ / 2)β2) / 3))) = ((1 Β· (2
Β· (((π΄ / 2)β2)
/ 3))) β ((((π΄ /
2)β2) / 3) Β· (2 Β· (((π΄ / 2)β2) / 3))))) |
157 | 132 | mulid2d 7975 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
(1 Β· (2 Β· (((π΄ / 2)β2) / 3))) = (2 Β· (((π΄ / 2)β2) /
3))) |
158 | 124, 29, 124 | mul12d 8108 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
((((π΄ / 2)β2) / 3)
Β· (2 Β· (((π΄ /
2)β2) / 3))) = (2 Β· ((((π΄ / 2)β2) / 3) Β· (((π΄ / 2)β2) /
3)))) |
159 | 124 | sqvald 10650 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
((((π΄ / 2)β2) /
3)β2) = ((((π΄ /
2)β2) / 3) Β· (((π΄ / 2)β2) / 3))) |
160 | 159 | oveq2d 5890 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((((π΄ /
2)β2) / 3)β2)) = (2 Β· ((((π΄ / 2)β2) / 3) Β· (((π΄ / 2)β2) /
3)))) |
161 | 158, 160 | eqtr4d 2213 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((((π΄ / 2)β2) / 3)
Β· (2 Β· (((π΄ /
2)β2) / 3))) = (2 Β· ((((π΄ / 2)β2) /
3)β2))) |
162 | 157, 161 | oveq12d 5892 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((1 Β· (2 Β· (((π΄ / 2)β2) / 3))) β ((((π΄ / 2)β2) / 3) Β· (2
Β· (((π΄ / 2)β2)
/ 3)))) = ((2 Β· (((π΄
/ 2)β2) / 3)) β (2 Β· ((((π΄ / 2)β2) /
3)β2)))) |
163 | 156, 162 | eqtrd 2210 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) Β· (2 Β· (((π΄ / 2)β2) / 3))) = ((2 Β· (((π΄ / 2)β2) / 3)) β (2
Β· ((((π΄ / 2)β2)
/ 3)β2)))) |
164 | 155, 163 | oveq12d 5892 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(((1 β (((π΄ /
2)β2) / 3)) Β· 1) β ((1 β (((π΄ / 2)β2) / 3)) Β· (2 Β·
(((π΄ / 2)β2) / 3)))) =
((1 β (((π΄ /
2)β2) / 3)) β ((2 Β· (((π΄ / 2)β2) / 3)) β (2 Β·
((((π΄ / 2)β2) /
3)β2))))) |
165 | 115, 124,
132, 117 | subadd4d 8315 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) β ((2 Β· (((π΄ / 2)β2) / 3)) β (2 Β·
((((π΄ / 2)β2) /
3)β2)))) = ((1 + (2 Β· ((((π΄ / 2)β2) / 3)β2))) β
((((π΄ / 2)β2) / 3) +
(2 Β· (((π΄ /
2)β2) / 3))))) |
166 | | df-3 8978 |
. . . . . . . . . . . . . 14
β’ 3 = (2 +
1) |
167 | 28, 116 | addcomi 8100 |
. . . . . . . . . . . . . 14
β’ (2 + 1) =
(1 + 2) |
168 | 166, 167 | eqtri 2198 |
. . . . . . . . . . . . 13
β’ 3 = (1 +
2) |
169 | 168 | oveq1i 5884 |
. . . . . . . . . . . 12
β’ (3
Β· (((π΄ / 2)β2)
/ 3)) = ((1 + 2) Β· (((π΄ / 2)β2) / 3)) |
170 | 125 | oveq1d 5889 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
((1 Β· (((π΄ /
2)β2) / 3)) + (2 Β· (((π΄ / 2)β2) / 3))) = ((((π΄ / 2)β2) / 3) + (2 Β· (((π΄ / 2)β2) /
3)))) |
171 | 115, 124,
29, 170 | joinlmuladdmuld 7984 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((1 + 2) Β· (((π΄ /
2)β2) / 3)) = ((((π΄ /
2)β2) / 3) + (2 Β· (((π΄ / 2)β2) / 3)))) |
172 | 169, 171 | eqtrid 2222 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(3 Β· (((π΄ /
2)β2) / 3)) = ((((π΄ /
2)β2) / 3) + (2 Β· (((π΄ / 2)β2) / 3)))) |
173 | 172 | oveq2d 5890 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((1 + (2 Β· ((((π΄ /
2)β2) / 3)β2))) β (3 Β· (((π΄ / 2)β2) / 3))) = ((1 + (2 Β·
((((π΄ / 2)β2) /
3)β2))) β ((((π΄
/ 2)β2) / 3) + (2 Β· (((π΄ / 2)β2) / 3))))) |
174 | 165, 173 | eqtr4d 2213 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) β ((2 Β· (((π΄ / 2)β2) / 3)) β (2 Β·
((((π΄ / 2)β2) /
3)β2)))) = ((1 + (2 Β· ((((π΄ / 2)β2) / 3)β2))) β (3
Β· (((π΄ / 2)β2)
/ 3)))) |
175 | 154, 164,
174 | 3eqtrd 2214 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (((π΄ /
2)β2) / 3)) Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) = ((1 + (2 Β·
((((π΄ / 2)β2) /
3)β2))) β (3 Β· (((π΄ / 2)β2) / 3)))) |
176 | 114, 151,
175 | 3brtr4d 4035 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· ((1 β (((π΄ / 2)β2) / 3))β2)) β 1) <
((1 β (((π΄ /
2)β2) / 3)) Β· (1 β (2 Β· (((π΄ / 2)β2) / 3))))) |
177 | 2, 25, 26, 91, 176 | lttrd 8082 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβπ΄) < ((1
β (((π΄ / 2)β2) /
3)) Β· (1 β (2 Β· (((π΄ / 2)β2) / 3))))) |
178 | | ltmul2 8812 |
. . . . . . 7
β’
(((cosβπ΄)
β β β§ ((1 β (((π΄ / 2)β2) / 3)) Β· (1 β (2
Β· (((π΄ / 2)β2)
/ 3)))) β β β§ (π΄ β β β§ 0 < π΄)) β ((cosβπ΄) < ((1 β (((π΄ / 2)β2) / 3)) Β· (1
β (2 Β· (((π΄ /
2)β2) / 3)))) β (π΄ Β· (cosβπ΄)) < (π΄ Β· ((1 β (((π΄ / 2)β2) / 3)) Β· (1 β (2
Β· (((π΄ / 2)β2)
/ 3))))))) |
179 | 2, 26, 1, 45, 178 | syl112anc 1242 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
((cosβπ΄) < ((1
β (((π΄ / 2)β2) /
3)) Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) β (π΄ Β· (cosβπ΄)) < (π΄ Β· ((1 β (((π΄ / 2)β2) / 3)) Β· (1 β (2
Β· (((π΄ / 2)β2)
/ 3))))))) |
180 | 177, 179 | mpbid 147 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β·
(cosβπ΄)) < (π΄ Β· ((1 β (((π΄ / 2)β2) / 3)) Β· (1
β (2 Β· (((π΄ /
2)β2) / 3)))))) |
181 | 18 | recnd 7985 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
(1 β (2 Β· (((π΄
/ 2)β2) / 3))) β β) |
182 | 27, 153, 181 | mulassd 7980 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) = (π΄ Β· ((1 β (((π΄ / 2)β2) / 3)) Β· (1 β (2
Β· (((π΄ / 2)β2)
/ 3)))))) |
183 | 180, 182 | breqtrrd 4031 |
. . . 4
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β·
(cosβπ΄)) < ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) Β· (1
β (2 Β· (((π΄ /
2)β2) / 3))))) |
184 | 13, 38 | remulcld 7987 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (cosβ(π΄ /
2))) β β) |
185 | 74 | simpld 112 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
(1 β (2 Β· (((π΄
/ 2)β2) / 3))) < (cosβ(π΄ / 2))) |
186 | 1, 12, 45, 83 | mulgt0d 8079 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
0 < (π΄ Β· (1
β (((π΄ / 2)β2) /
3)))) |
187 | | ltmul2 8812 |
. . . . . . 7
β’ (((1
β (2 Β· (((π΄ /
2)β2) / 3))) β β β§ (cosβ(π΄ / 2)) β β β§ ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) β
β β§ 0 < (π΄
Β· (1 β (((π΄ /
2)β2) / 3))))) β ((1 β (2 Β· (((π΄ / 2)β2) / 3))) < (cosβ(π΄ / 2)) β ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) Β· (1
β (2 Β· (((π΄ /
2)β2) / 3)))) < ((π΄
Β· (1 β (((π΄ /
2)β2) / 3))) Β· (cosβ(π΄ / 2))))) |
188 | 18, 38, 13, 186, 187 | syl112anc 1242 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
((1 β (2 Β· (((π΄ / 2)β2) / 3))) < (cosβ(π΄ / 2)) β ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) Β· (1
β (2 Β· (((π΄ /
2)β2) / 3)))) < ((π΄
Β· (1 β (((π΄ /
2)β2) / 3))) Β· (cosβ(π΄ / 2))))) |
189 | 185, 188 | mpbid 147 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) < ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) Β·
(cosβ(π΄ /
2)))) |
190 | 29, 34, 153 | mulassd 7980 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· (π΄ / 2))
Β· (1 β (((π΄ /
2)β2) / 3))) = (2 Β· ((π΄ / 2) Β· (1 β (((π΄ / 2)β2) /
3))))) |
191 | 32 | oveq1d 5889 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· (π΄ / 2))
Β· (1 β (((π΄ /
2)β2) / 3))) = (π΄
Β· (1 β (((π΄ /
2)β2) / 3)))) |
192 | 34, 115, 124 | subdid 8370 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) Β· (1
β (((π΄ / 2)β2) /
3))) = (((π΄ / 2) Β·
1) β ((π΄ / 2)
Β· (((π΄ / 2)β2)
/ 3)))) |
193 | 34 | mulridd 7973 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) Β· 1) =
(π΄ / 2)) |
194 | 166 | oveq2i 5885 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ / 2)β3) = ((π΄ / 2)β(2 +
1)) |
195 | | 2nn0 9192 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β0 |
196 | | expp1 10526 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ / 2) β β β§ 2
β β0) β ((π΄ / 2)β(2 + 1)) = (((π΄ / 2)β2) Β· (π΄ / 2))) |
197 | 34, 195, 196 | sylancl 413 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2)β(2 + 1)) =
(((π΄ / 2)β2) Β·
(π΄ / 2))) |
198 | 194, 197 | eqtrid 2222 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2)β3) = (((π΄ / 2)β2) Β· (π΄ / 2))) |
199 | 7 | recnd 7985 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2)β2) β
β) |
200 | 199, 34 | mulcomd 7978 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2)β2) Β·
(π΄ / 2)) = ((π΄ / 2) Β· ((π΄ / 2)β2))) |
201 | 198, 200 | eqtrd 2210 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2)β3) = ((π΄ / 2) Β· ((π΄ / 2)β2))) |
202 | 201 | oveq1d 5889 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2)β3) / 3) =
(((π΄ / 2) Β· ((π΄ / 2)β2)) /
3)) |
203 | | 3cn 8993 |
. . . . . . . . . . . . . . 15
β’ 3 β
β |
204 | 203 | a1i 9 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
3 β β) |
205 | 104, 109 | gt0ap0d 8585 |
. . . . . . . . . . . . . 14
β’ (π΄ β (0(,)(Ο / 2)) β
3 # 0) |
206 | 34, 199, 204, 205 | divassapd 8782 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2) Β· ((π΄ / 2)β2)) / 3) = ((π΄ / 2) Β· (((π΄ / 2)β2) /
3))) |
207 | 202, 206 | eqtr2d 2211 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) Β· (((π΄ / 2)β2) / 3)) = (((π΄ / 2)β3) /
3)) |
208 | 193, 207 | oveq12d 5892 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2) Β· 1)
β ((π΄ / 2) Β·
(((π΄ / 2)β2) / 3))) =
((π΄ / 2) β (((π΄ / 2)β3) /
3))) |
209 | 192, 208 | eqtrd 2210 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) Β· (1
β (((π΄ / 2)β2) /
3))) = ((π΄ / 2) β
(((π΄ / 2)β3) /
3))) |
210 | 209 | oveq2d 5890 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((π΄ / 2)
Β· (1 β (((π΄ /
2)β2) / 3)))) = (2 Β· ((π΄ / 2) β (((π΄ / 2)β3) / 3)))) |
211 | 190, 191,
210 | 3eqtr3d 2218 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β· (1 β
(((π΄ / 2)β2) / 3))) =
(2 Β· ((π΄ / 2)
β (((π΄ / 2)β3) /
3)))) |
212 | | sin01bnd 11764 |
. . . . . . . . . . 11
β’ ((π΄ / 2) β (0(,]1) β
(((π΄ / 2) β (((π΄ / 2)β3) / 3)) <
(sinβ(π΄ / 2)) β§
(sinβ(π΄ / 2)) <
(π΄ / 2))) |
213 | 72, 212 | syl 14 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2) β (((π΄ / 2)β3) / 3)) <
(sinβ(π΄ / 2)) β§
(sinβ(π΄ / 2)) <
(π΄ / 2))) |
214 | 213 | simpld 112 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) β (((π΄ / 2)β3) / 3)) <
(sinβ(π΄ /
2))) |
215 | | 3nn0 9193 |
. . . . . . . . . . . . 13
β’ 3 β
β0 |
216 | | reexpcl 10536 |
. . . . . . . . . . . . 13
β’ (((π΄ / 2) β β β§ 3
β β0) β ((π΄ / 2)β3) β
β) |
217 | 6, 215, 216 | sylancl 413 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2)β3) β
β) |
218 | | nndivre 8954 |
. . . . . . . . . . . 12
β’ ((((π΄ / 2)β3) β β
β§ 3 β β) β (((π΄ / 2)β3) / 3) β
β) |
219 | 217, 8, 218 | sylancl 413 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2)β3) / 3)
β β) |
220 | 6, 219 | resubcld 8337 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ / 2) β (((π΄ / 2)β3) / 3)) β
β) |
221 | 6 | resincld 11730 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(sinβ(π΄ / 2)) β
β) |
222 | | ltmul2 8812 |
. . . . . . . . . 10
β’ ((((π΄ / 2) β (((π΄ / 2)β3) / 3)) β
β β§ (sinβ(π΄
/ 2)) β β β§ (2 β β β§ 0 < 2)) β (((π΄ / 2) β (((π΄ / 2)β3) / 3)) <
(sinβ(π΄ / 2)) β
(2 Β· ((π΄ / 2)
β (((π΄ / 2)β3) /
3))) < (2 Β· (sinβ(π΄ / 2))))) |
223 | 220, 221,
43, 47, 222 | syl112anc 1242 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(((π΄ / 2) β (((π΄ / 2)β3) / 3)) <
(sinβ(π΄ / 2)) β
(2 Β· ((π΄ / 2)
β (((π΄ / 2)β3) /
3))) < (2 Β· (sinβ(π΄ / 2))))) |
224 | 214, 223 | mpbid 147 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· ((π΄ / 2)
β (((π΄ / 2)β3) /
3))) < (2 Β· (sinβ(π΄ / 2)))) |
225 | 211, 224 | eqbrtrd 4025 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
< (2 Β· (sinβ(π΄ / 2)))) |
226 | | remulcl 7938 |
. . . . . . . . 9
β’ ((2
β β β§ (sinβ(π΄ / 2)) β β) β (2 Β·
(sinβ(π΄ / 2))) β
β) |
227 | 14, 221, 226 | sylancr 414 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(2 Β· (sinβ(π΄ /
2))) β β) |
228 | | ltmul1 8548 |
. . . . . . . 8
β’ (((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) β
β β§ (2 Β· (sinβ(π΄ / 2))) β β β§
((cosβ(π΄ / 2)) β
β β§ 0 < (cosβ(π΄ / 2)))) β ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) < (2 Β·
(sinβ(π΄ / 2))) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (cosβ(π΄ /
2))) < ((2 Β· (sinβ(π΄ / 2))) Β· (cosβ(π΄ / 2))))) |
229 | 13, 227, 38, 77, 228 | syl112anc 1242 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
< (2 Β· (sinβ(π΄ / 2))) β ((π΄ Β· (1 β (((π΄ / 2)β2) / 3))) Β·
(cosβ(π΄ / 2))) <
((2 Β· (sinβ(π΄
/ 2))) Β· (cosβ(π΄ / 2))))) |
230 | 225, 229 | mpbid 147 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (cosβ(π΄ /
2))) < ((2 Β· (sinβ(π΄ / 2))) Β· (cosβ(π΄ / 2)))) |
231 | 221 | recnd 7985 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(sinβ(π΄ / 2)) β
β) |
232 | 38 | recnd 7985 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβ(π΄ / 2)) β
β) |
233 | 29, 231, 232 | mulassd 7980 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
((2 Β· (sinβ(π΄
/ 2))) Β· (cosβ(π΄ / 2))) = (2 Β· ((sinβ(π΄ / 2)) Β·
(cosβ(π΄ /
2))))) |
234 | | sin2t 11756 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
235 | 34, 234 | syl 14 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
236 | 32 | fveq2d 5519 |
. . . . . . 7
β’ (π΄ β (0(,)(Ο / 2)) β
(sinβ(2 Β· (π΄ /
2))) = (sinβπ΄)) |
237 | 233, 235,
236 | 3eqtr2rd 2217 |
. . . . . 6
β’ (π΄ β (0(,)(Ο / 2)) β
(sinβπ΄) = ((2
Β· (sinβ(π΄ /
2))) Β· (cosβ(π΄
/ 2)))) |
238 | 230, 237 | breqtrrd 4031 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (cosβ(π΄ /
2))) < (sinβπ΄)) |
239 | 19, 184, 20, 189, 238 | lttrd 8082 |
. . . 4
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β· (1 β
(((π΄ / 2)β2) / 3)))
Β· (1 β (2 Β· (((π΄ / 2)β2) / 3)))) < (sinβπ΄)) |
240 | 3, 19, 20, 183, 239 | lttrd 8082 |
. . 3
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ Β·
(cosβπ΄)) <
(sinβπ΄)) |
241 | | sincosq1sgn 14217 |
. . . . 5
β’ (π΄ β (0(,)(Ο / 2)) β
(0 < (sinβπ΄) β§
0 < (cosβπ΄))) |
242 | 241 | simprd 114 |
. . . 4
β’ (π΄ β (0(,)(Ο / 2)) β
0 < (cosβπ΄)) |
243 | | ltmuldiv 8830 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β
β β§ ((cosβπ΄) β β β§ 0 <
(cosβπ΄))) β
((π΄ Β·
(cosβπ΄)) <
(sinβπ΄) β π΄ < ((sinβπ΄) / (cosβπ΄)))) |
244 | 1, 20, 2, 242, 243 | syl112anc 1242 |
. . 3
β’ (π΄ β (0(,)(Ο / 2)) β
((π΄ Β·
(cosβπ΄)) <
(sinβπ΄) β π΄ < ((sinβπ΄) / (cosβπ΄)))) |
245 | 240, 244 | mpbid 147 |
. 2
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ < ((sinβπ΄) / (cosβπ΄))) |
246 | 2, 242 | gt0ap0d 8585 |
. . 3
β’ (π΄ β (0(,)(Ο / 2)) β
(cosβπ΄) #
0) |
247 | | tanvalap 11715 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) # 0) β
(tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
248 | 27, 246, 247 | syl2anc 411 |
. 2
β’ (π΄ β (0(,)(Ο / 2)) β
(tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
249 | 245, 248 | breqtrrd 4031 |
1
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ < (tanβπ΄)) |