Step | Hyp | Ref
| Expression |
1 | | 0xr 11209 |
. . . . . . . . 9
β’ 0 β
β* |
2 | | 1re 11162 |
. . . . . . . . 9
β’ 1 β
β |
3 | | elioc2 13334 |
. . . . . . . . 9
β’ ((0
β β* β§ 1 β β) β (π΄ β (0(,]1) β (π΄ β β β§ 0 < π΄ β§ π΄ β€ 1))) |
4 | 1, 2, 3 | mp2an 691 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β (π΄ β β β§ 0 <
π΄ β§ π΄ β€ 1)) |
5 | 4 | simp1bi 1146 |
. . . . . . 7
β’ (π΄ β (0(,]1) β π΄ β
β) |
6 | | 3nn0 12438 |
. . . . . . . . 9
β’ 3 β
β0 |
7 | | reexpcl 13991 |
. . . . . . . . 9
β’ ((π΄ β β β§ 3 β
β0) β (π΄β3) β β) |
8 | 5, 6, 7 | sylancl 587 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β (π΄β3) β
β) |
9 | | 6nn 12249 |
. . . . . . . 8
β’ 6 β
β |
10 | | nndivre 12201 |
. . . . . . . 8
β’ (((π΄β3) β β β§ 6
β β) β ((π΄β3) / 6) β
β) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . . 7
β’ (π΄ β (0(,]1) β ((π΄β3) / 6) β
β) |
12 | 5, 11 | resubcld 11590 |
. . . . . 6
β’ (π΄ β (0(,]1) β (π΄ β ((π΄β3) / 6)) β
β) |
13 | 12 | recnd 11190 |
. . . . 5
β’ (π΄ β (0(,]1) β (π΄ β ((π΄β3) / 6)) β
β) |
14 | | ax-icn 11117 |
. . . . . . . . 9
β’ i β
β |
15 | 5 | recnd 11190 |
. . . . . . . . 9
β’ (π΄ β (0(,]1) β π΄ β
β) |
16 | | mulcl 11142 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
17 | 14, 15, 16 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β (i
Β· π΄) β
β) |
18 | | 4nn0 12439 |
. . . . . . . 8
β’ 4 β
β0 |
19 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β0
β¦ (((i Β· π΄)βπ) / (!βπ))) = (π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ))) |
20 | 19 | eftlcl 15996 |
. . . . . . . 8
β’ (((i
Β· π΄) β β
β§ 4 β β0) β Ξ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ) β β) |
21 | 17, 18, 20 | sylancl 587 |
. . . . . . 7
β’ (π΄ β (0(,]1) β
Ξ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ) β β) |
22 | 21 | imcld 15087 |
. . . . . 6
β’ (π΄ β (0(,]1) β
(ββΞ£π
β (β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)) β β) |
23 | 22 | recnd 11190 |
. . . . 5
β’ (π΄ β (0(,]1) β
(ββΞ£π
β (β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)) β β) |
24 | 19 | resin4p 16027 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)))) |
25 | 5, 24 | syl 17 |
. . . . 5
β’ (π΄ β (0(,]1) β
(sinβπ΄) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)))) |
26 | 13, 23, 25 | mvrladdd 11575 |
. . . 4
β’ (π΄ β (0(,]1) β
((sinβπ΄) β
(π΄ β ((π΄β3) / 6))) =
(ββΞ£π
β (β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) |
27 | 26 | fveq2d 6851 |
. . 3
β’ (π΄ β (0(,]1) β
(absβ((sinβπ΄)
β (π΄ β ((π΄β3) / 6)))) =
(absβ(ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)))) |
28 | 23 | abscld 15328 |
. . . 4
β’ (π΄ β (0(,]1) β
(absβ(ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) β β) |
29 | 21 | abscld 15328 |
. . . 4
β’ (π΄ β (0(,]1) β
(absβΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)) β β) |
30 | | absimle 15201 |
. . . . 5
β’
(Ξ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ) β β β
(absβ(ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) β€ (absβΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) |
31 | 21, 30 | syl 17 |
. . . 4
β’ (π΄ β (0(,]1) β
(absβ(ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) β€ (absβΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) |
32 | | reexpcl 13991 |
. . . . . . 7
β’ ((π΄ β β β§ 4 β
β0) β (π΄β4) β β) |
33 | 5, 18, 32 | sylancl 587 |
. . . . . 6
β’ (π΄ β (0(,]1) β (π΄β4) β
β) |
34 | | nndivre 12201 |
. . . . . 6
β’ (((π΄β4) β β β§ 6
β β) β ((π΄β4) / 6) β
β) |
35 | 33, 9, 34 | sylancl 587 |
. . . . 5
β’ (π΄ β (0(,]1) β ((π΄β4) / 6) β
β) |
36 | 19 | ef01bndlem 16073 |
. . . . 5
β’ (π΄ β (0(,]1) β
(absβΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)) < ((π΄β4) / 6)) |
37 | 6 | a1i 11 |
. . . . . . 7
β’ (π΄ β (0(,]1) β 3 β
β0) |
38 | | 4z 12544 |
. . . . . . . . 9
β’ 4 β
β€ |
39 | | 3re 12240 |
. . . . . . . . . 10
β’ 3 β
β |
40 | | 4re 12244 |
. . . . . . . . . 10
β’ 4 β
β |
41 | | 3lt4 12334 |
. . . . . . . . . 10
β’ 3 <
4 |
42 | 39, 40, 41 | ltleii 11285 |
. . . . . . . . 9
β’ 3 β€
4 |
43 | | 3z 12543 |
. . . . . . . . . 10
β’ 3 β
β€ |
44 | 43 | eluz1i 12778 |
. . . . . . . . 9
β’ (4 β
(β€β₯β3) β (4 β β€ β§ 3 β€
4)) |
45 | 38, 42, 44 | mpbir2an 710 |
. . . . . . . 8
β’ 4 β
(β€β₯β3) |
46 | 45 | a1i 11 |
. . . . . . 7
β’ (π΄ β (0(,]1) β 4 β
(β€β₯β3)) |
47 | 4 | simp2bi 1147 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β 0 <
π΄) |
48 | | 0re 11164 |
. . . . . . . . 9
β’ 0 β
β |
49 | | ltle 11250 |
. . . . . . . . 9
β’ ((0
β β β§ π΄
β β) β (0 < π΄ β 0 β€ π΄)) |
50 | 48, 5, 49 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β (0 <
π΄ β 0 β€ π΄)) |
51 | 47, 50 | mpd 15 |
. . . . . . 7
β’ (π΄ β (0(,]1) β 0 β€
π΄) |
52 | 4 | simp3bi 1148 |
. . . . . . 7
β’ (π΄ β (0(,]1) β π΄ β€ 1) |
53 | 5, 37, 46, 51, 52 | leexp2rd 14165 |
. . . . . 6
β’ (π΄ β (0(,]1) β (π΄β4) β€ (π΄β3)) |
54 | | 6re 12250 |
. . . . . . . 8
β’ 6 β
β |
55 | 54 | a1i 11 |
. . . . . . 7
β’ (π΄ β (0(,]1) β 6 β
β) |
56 | | 6pos 12270 |
. . . . . . . 8
β’ 0 <
6 |
57 | 56 | a1i 11 |
. . . . . . 7
β’ (π΄ β (0(,]1) β 0 <
6) |
58 | | lediv1 12027 |
. . . . . . 7
β’ (((π΄β4) β β β§
(π΄β3) β β
β§ (6 β β β§ 0 < 6)) β ((π΄β4) β€ (π΄β3) β ((π΄β4) / 6) β€ ((π΄β3) / 6))) |
59 | 33, 8, 55, 57, 58 | syl112anc 1375 |
. . . . . 6
β’ (π΄ β (0(,]1) β ((π΄β4) β€ (π΄β3) β ((π΄β4) / 6) β€ ((π΄β3) / 6))) |
60 | 53, 59 | mpbid 231 |
. . . . 5
β’ (π΄ β (0(,]1) β ((π΄β4) / 6) β€ ((π΄β3) / 6)) |
61 | 29, 35, 11, 36, 60 | ltletrd 11322 |
. . . 4
β’ (π΄ β (0(,]1) β
(absβΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ)) < ((π΄β3) / 6)) |
62 | 28, 29, 11, 31, 61 | lelttrd 11320 |
. . 3
β’ (π΄ β (0(,]1) β
(absβ(ββΞ£π β
(β€β₯β4)((π β β0 β¦ (((i
Β· π΄)βπ) / (!βπ)))βπ))) < ((π΄β3) / 6)) |
63 | 27, 62 | eqbrtrd 5132 |
. 2
β’ (π΄ β (0(,]1) β
(absβ((sinβπ΄)
β (π΄ β ((π΄β3) / 6)))) < ((π΄β3) / 6)) |
64 | 5 | resincld 16032 |
. . . 4
β’ (π΄ β (0(,]1) β
(sinβπ΄) β
β) |
65 | 64, 12, 11 | absdifltd 15325 |
. . 3
β’ (π΄ β (0(,]1) β
((absβ((sinβπ΄)
β (π΄ β ((π΄β3) / 6)))) < ((π΄β3) / 6) β (((π΄ β ((π΄β3) / 6)) β ((π΄β3) / 6)) < (sinβπ΄) β§ (sinβπ΄) < ((π΄ β ((π΄β3) / 6)) + ((π΄β3) / 6))))) |
66 | 11 | recnd 11190 |
. . . . . . 7
β’ (π΄ β (0(,]1) β ((π΄β3) / 6) β
β) |
67 | 15, 66, 66 | subsub4d 11550 |
. . . . . 6
β’ (π΄ β (0(,]1) β ((π΄ β ((π΄β3) / 6)) β ((π΄β3) / 6)) = (π΄ β (((π΄β3) / 6) + ((π΄β3) / 6)))) |
68 | 8 | recnd 11190 |
. . . . . . . . . . 11
β’ (π΄ β (0(,]1) β (π΄β3) β
β) |
69 | | 3cn 12241 |
. . . . . . . . . . . . 13
β’ 3 β
β |
70 | | 3ne0 12266 |
. . . . . . . . . . . . 13
β’ 3 β
0 |
71 | 69, 70 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (3 β
β β§ 3 β 0) |
72 | | 2cnne0 12370 |
. . . . . . . . . . . 12
β’ (2 β
β β§ 2 β 0) |
73 | | divdiv1 11873 |
. . . . . . . . . . . 12
β’ (((π΄β3) β β β§ (3
β β β§ 3 β 0) β§ (2 β β β§ 2 β 0)) β
(((π΄β3) / 3) / 2) =
((π΄β3) / (3 Β·
2))) |
74 | 71, 72, 73 | mp3an23 1454 |
. . . . . . . . . . 11
β’ ((π΄β3) β β β
(((π΄β3) / 3) / 2) =
((π΄β3) / (3 Β·
2))) |
75 | 68, 74 | syl 17 |
. . . . . . . . . 10
β’ (π΄ β (0(,]1) β (((π΄β3) / 3) / 2) = ((π΄β3) / (3 Β·
2))) |
76 | | 3t2e6 12326 |
. . . . . . . . . . 11
β’ (3
Β· 2) = 6 |
77 | 76 | oveq2i 7373 |
. . . . . . . . . 10
β’ ((π΄β3) / (3 Β· 2)) =
((π΄β3) /
6) |
78 | 75, 77 | eqtr2di 2794 |
. . . . . . . . 9
β’ (π΄ β (0(,]1) β ((π΄β3) / 6) = (((π΄β3) / 3) /
2)) |
79 | 78, 78 | oveq12d 7380 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β (((π΄β3) / 6) + ((π΄β3) / 6)) = ((((π΄β3) / 3) / 2) + (((π΄β3) / 3) /
2))) |
80 | | 3nn 12239 |
. . . . . . . . . . 11
β’ 3 β
β |
81 | | nndivre 12201 |
. . . . . . . . . . 11
β’ (((π΄β3) β β β§ 3
β β) β ((π΄β3) / 3) β
β) |
82 | 8, 80, 81 | sylancl 587 |
. . . . . . . . . 10
β’ (π΄ β (0(,]1) β ((π΄β3) / 3) β
β) |
83 | 82 | recnd 11190 |
. . . . . . . . 9
β’ (π΄ β (0(,]1) β ((π΄β3) / 3) β
β) |
84 | 83 | 2halvesd 12406 |
. . . . . . . 8
β’ (π΄ β (0(,]1) β ((((π΄β3) / 3) / 2) + (((π΄β3) / 3) / 2)) = ((π΄β3) / 3)) |
85 | 79, 84 | eqtrd 2777 |
. . . . . . 7
β’ (π΄ β (0(,]1) β (((π΄β3) / 6) + ((π΄β3) / 6)) = ((π΄β3) / 3)) |
86 | 85 | oveq2d 7378 |
. . . . . 6
β’ (π΄ β (0(,]1) β (π΄ β (((π΄β3) / 6) + ((π΄β3) / 6))) = (π΄ β ((π΄β3) / 3))) |
87 | 67, 86 | eqtrd 2777 |
. . . . 5
β’ (π΄ β (0(,]1) β ((π΄ β ((π΄β3) / 6)) β ((π΄β3) / 6)) = (π΄ β ((π΄β3) / 3))) |
88 | 87 | breq1d 5120 |
. . . 4
β’ (π΄ β (0(,]1) β (((π΄ β ((π΄β3) / 6)) β ((π΄β3) / 6)) < (sinβπ΄) β (π΄ β ((π΄β3) / 3)) < (sinβπ΄))) |
89 | 15, 66 | npcand 11523 |
. . . . 5
β’ (π΄ β (0(,]1) β ((π΄ β ((π΄β3) / 6)) + ((π΄β3) / 6)) = π΄) |
90 | 89 | breq2d 5122 |
. . . 4
β’ (π΄ β (0(,]1) β
((sinβπ΄) < ((π΄ β ((π΄β3) / 6)) + ((π΄β3) / 6)) β (sinβπ΄) < π΄)) |
91 | 88, 90 | anbi12d 632 |
. . 3
β’ (π΄ β (0(,]1) β ((((π΄ β ((π΄β3) / 6)) β ((π΄β3) / 6)) < (sinβπ΄) β§ (sinβπ΄) < ((π΄ β ((π΄β3) / 6)) + ((π΄β3) / 6))) β ((π΄ β ((π΄β3) / 3)) < (sinβπ΄) β§ (sinβπ΄) < π΄))) |
92 | 65, 91 | bitrd 279 |
. 2
β’ (π΄ β (0(,]1) β
((absβ((sinβπ΄)
β (π΄ β ((π΄β3) / 6)))) < ((π΄β3) / 6) β ((π΄ β ((π΄β3) / 3)) < (sinβπ΄) β§ (sinβπ΄) < π΄))) |
93 | 63, 92 | mpbid 231 |
1
β’ (π΄ β (0(,]1) β ((π΄ β ((π΄β3) / 3)) < (sinβπ΄) β§ (sinβπ΄) < π΄)) |