Step | Hyp | Ref
| Expression |
1 | | sin0pilem1 14205 |
. 2
β’
βπ β
(1(,)2)((cosβπ) = 0
β§ βπ¦ β
(π(,)(2 Β· π))0 < (sinβπ¦)) |
2 | | 2re 8989 |
. . . . . . . 8
β’ 2 β
β |
3 | 2 | a1i 9 |
. . . . . . 7
β’ (π β (1(,)2) β 2 β
β) |
4 | | elioore 9912 |
. . . . . . 7
β’ (π β (1(,)2) β π β
β) |
5 | 3, 4 | remulcld 7988 |
. . . . . 6
β’ (π β (1(,)2) β (2
Β· π) β
β) |
6 | 5 | adantr 276 |
. . . . 5
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (2 Β· π) β
β) |
7 | | 2t1e2 9072 |
. . . . . . 7
β’ (2
Β· 1) = 2 |
8 | | 1red 7972 |
. . . . . . . 8
β’ (π β (1(,)2) β 1 β
β) |
9 | | 2rp 9658 |
. . . . . . . . 9
β’ 2 β
β+ |
10 | 9 | a1i 9 |
. . . . . . . 8
β’ (π β (1(,)2) β 2 β
β+) |
11 | | eliooord 9928 |
. . . . . . . . 9
β’ (π β (1(,)2) β (1 <
π β§ π < 2)) |
12 | 11 | simpld 112 |
. . . . . . . 8
β’ (π β (1(,)2) β 1 <
π) |
13 | 8, 4, 10, 12 | ltmul2dd 9753 |
. . . . . . 7
β’ (π β (1(,)2) β (2
Β· 1) < (2 Β· π)) |
14 | 7, 13 | eqbrtrrid 4040 |
. . . . . 6
β’ (π β (1(,)2) β 2 < (2
Β· π)) |
15 | 14 | adantr 276 |
. . . . 5
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β 2 < (2 Β·
π)) |
16 | 11 | simprd 114 |
. . . . . . . 8
β’ (π β (1(,)2) β π < 2) |
17 | 4, 3, 10, 16 | ltmul2dd 9753 |
. . . . . . 7
β’ (π β (1(,)2) β (2
Β· π) < (2
Β· 2)) |
18 | | 2t2e4 9073 |
. . . . . . 7
β’ (2
Β· 2) = 4 |
19 | 17, 18 | breqtrdi 4045 |
. . . . . 6
β’ (π β (1(,)2) β (2
Β· π) <
4) |
20 | 19 | adantr 276 |
. . . . 5
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (2 Β· π) < 4) |
21 | 2 | rexri 8015 |
. . . . . 6
β’ 2 β
β* |
22 | | 4re 8996 |
. . . . . . 7
β’ 4 β
β |
23 | 22 | rexri 8015 |
. . . . . 6
β’ 4 β
β* |
24 | | elioo2 9921 |
. . . . . 6
β’ ((2
β β* β§ 4 β β*) β ((2
Β· π) β (2(,)4)
β ((2 Β· π)
β β β§ 2 < (2 Β· π) β§ (2 Β· π) < 4))) |
25 | 21, 23, 24 | mp2an 426 |
. . . . 5
β’ ((2
Β· π) β (2(,)4)
β ((2 Β· π)
β β β§ 2 < (2 Β· π) β§ (2 Β· π) < 4)) |
26 | 6, 15, 20, 25 | syl3anbrc 1181 |
. . . 4
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (2 Β· π) β
(2(,)4)) |
27 | 4 | recnd 7986 |
. . . . . . 7
β’ (π β (1(,)2) β π β
β) |
28 | 27 | adantr 276 |
. . . . . 6
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β π β β) |
29 | | sin2t 11757 |
. . . . . 6
β’ (π β β β
(sinβ(2 Β· π))
= (2 Β· ((sinβπ) Β· (cosβπ)))) |
30 | 28, 29 | syl 14 |
. . . . 5
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (sinβ(2
Β· π)) = (2 Β·
((sinβπ) Β·
(cosβπ)))) |
31 | | simprl 529 |
. . . . . . . . 9
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (cosβπ) = 0) |
32 | 31 | oveq2d 5891 |
. . . . . . . 8
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β ((sinβπ) Β· (cosβπ)) = ((sinβπ) Β· 0)) |
33 | 28 | sincld 11718 |
. . . . . . . . 9
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (sinβπ) β
β) |
34 | 33 | mul01d 8350 |
. . . . . . . 8
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β ((sinβπ) Β· 0) =
0) |
35 | 32, 34 | eqtrd 2210 |
. . . . . . 7
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β ((sinβπ) Β· (cosβπ)) = 0) |
36 | 35 | oveq2d 5891 |
. . . . . 6
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (2 Β·
((sinβπ) Β·
(cosβπ))) = (2
Β· 0)) |
37 | | 2cnd 8992 |
. . . . . . 7
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β 2 β
β) |
38 | 37 | mul01d 8350 |
. . . . . 6
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (2 Β· 0) =
0) |
39 | 36, 38 | eqtrd 2210 |
. . . . 5
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (2 Β·
((sinβπ) Β·
(cosβπ))) =
0) |
40 | 30, 39 | eqtrd 2210 |
. . . 4
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (sinβ(2
Β· π)) =
0) |
41 | | fveq2 5516 |
. . . . . . . 8
β’ (π¦ = π₯ β (sinβπ¦) = (sinβπ₯)) |
42 | 41 | breq2d 4016 |
. . . . . . 7
β’ (π¦ = π₯ β (0 < (sinβπ¦) β 0 < (sinβπ₯))) |
43 | | simprr 531 |
. . . . . . . 8
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦)) |
44 | 43 | ad2antrr 488 |
. . . . . . 7
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦)) |
45 | | elioore 9912 |
. . . . . . . . . 10
β’ (π₯ β (0(,)(2 Β· π)) β π₯ β β) |
46 | 45 | adantl 277 |
. . . . . . . . 9
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β π₯ β β) |
47 | 46 | adantr 276 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β π₯ β β) |
48 | | simpr 110 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β π < π₯) |
49 | | eliooord 9928 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)(2 Β· π)) β (0 < π₯ β§ π₯ < (2 Β· π))) |
50 | 49 | adantl 277 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β (0 < π₯ β§ π₯ < (2 Β· π))) |
51 | 50 | adantr 276 |
. . . . . . . . 9
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β (0 < π₯ β§ π₯ < (2 Β· π))) |
52 | 51 | simprd 114 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β π₯ < (2 Β· π)) |
53 | 4 | rexrd 8007 |
. . . . . . . . . . 11
β’ (π β (1(,)2) β π β
β*) |
54 | 5 | rexrd 8007 |
. . . . . . . . . . 11
β’ (π β (1(,)2) β (2
Β· π) β
β*) |
55 | | elioo2 9921 |
. . . . . . . . . . 11
β’ ((π β β*
β§ (2 Β· π) β
β*) β (π₯ β (π(,)(2 Β· π)) β (π₯ β β β§ π < π₯ β§ π₯ < (2 Β· π)))) |
56 | 53, 54, 55 | syl2anc 411 |
. . . . . . . . . 10
β’ (π β (1(,)2) β (π₯ β (π(,)(2 Β· π)) β (π₯ β β β§ π < π₯ β§ π₯ < (2 Β· π)))) |
57 | 56 | adantr 276 |
. . . . . . . . 9
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β (π₯ β (π(,)(2 Β· π)) β (π₯ β β β§ π < π₯ β§ π₯ < (2 Β· π)))) |
58 | 57 | ad2antrr 488 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β (π₯ β (π(,)(2 Β· π)) β (π₯ β β β§ π < π₯ β§ π₯ < (2 Β· π)))) |
59 | 47, 48, 52, 58 | mpbir3and 1180 |
. . . . . . 7
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β π₯ β (π(,)(2 Β· π))) |
60 | 42, 44, 59 | rspcdva 2847 |
. . . . . 6
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π < π₯) β 0 < (sinβπ₯)) |
61 | 46 | adantr 276 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β π₯ β β) |
62 | 50 | adantr 276 |
. . . . . . . . 9
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β (0 < π₯ β§ π₯ < (2 Β· π))) |
63 | 62 | simpld 112 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β 0 < π₯) |
64 | 2 | a1i 9 |
. . . . . . . . 9
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β 2 β
β) |
65 | | simpr 110 |
. . . . . . . . 9
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β π₯ < 2) |
66 | 61, 64, 65 | ltled 8076 |
. . . . . . . 8
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β π₯ β€ 2) |
67 | | 0xr 8004 |
. . . . . . . . 9
β’ 0 β
β* |
68 | | elioc2 9936 |
. . . . . . . . 9
β’ ((0
β β* β§ 2 β β) β (π₯ β (0(,]2) β (π₯ β β β§ 0 < π₯ β§ π₯ β€ 2))) |
69 | 67, 2, 68 | mp2an 426 |
. . . . . . . 8
β’ (π₯ β (0(,]2) β (π₯ β β β§ 0 <
π₯ β§ π₯ β€ 2)) |
70 | 61, 63, 66, 69 | syl3anbrc 1181 |
. . . . . . 7
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β π₯ β (0(,]2)) |
71 | | sin02gt0 11771 |
. . . . . . 7
β’ (π₯ β (0(,]2) β 0 <
(sinβπ₯)) |
72 | 70, 71 | syl 14 |
. . . . . 6
β’ ((((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β§ π₯ < 2) β 0 < (sinβπ₯)) |
73 | 16 | ad2antrr 488 |
. . . . . . 7
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β π < 2) |
74 | 4 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β π β β) |
75 | 2 | a1i 9 |
. . . . . . . 8
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β 2 β β) |
76 | | axltwlin 8025 |
. . . . . . . 8
β’ ((π β β β§ 2 β
β β§ π₯ β
β) β (π < 2
β (π < π₯ β¨ π₯ < 2))) |
77 | 74, 75, 46, 76 | syl3anc 1238 |
. . . . . . 7
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β (π < 2 β (π < π₯ β¨ π₯ < 2))) |
78 | 73, 77 | mpd 13 |
. . . . . 6
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β (π < π₯ β¨ π₯ < 2)) |
79 | 60, 72, 78 | mpjaodan 798 |
. . . . 5
β’ (((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β§ π₯ β (0(,)(2 Β· π))) β 0 < (sinβπ₯)) |
80 | 79 | ralrimiva 2550 |
. . . 4
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β βπ₯ β (0(,)(2 Β· π))0 < (sinβπ₯)) |
81 | | fveqeq2 5525 |
. . . . . 6
β’ (π = (2 Β· π) β ((sinβπ) = 0 β (sinβ(2
Β· π)) =
0)) |
82 | | oveq2 5883 |
. . . . . . 7
β’ (π = (2 Β· π) β (0(,)π) = (0(,)(2 Β· π))) |
83 | 82 | raleqdv 2679 |
. . . . . 6
β’ (π = (2 Β· π) β (βπ₯ β (0(,)π)0 < (sinβπ₯) β βπ₯ β (0(,)(2 Β· π))0 < (sinβπ₯))) |
84 | 81, 83 | anbi12d 473 |
. . . . 5
β’ (π = (2 Β· π) β (((sinβπ) = 0 β§ βπ₯ β (0(,)π)0 < (sinβπ₯)) β ((sinβ(2 Β· π)) = 0 β§ βπ₯ β (0(,)(2 Β· π))0 < (sinβπ₯)))) |
85 | 84 | rspcev 2842 |
. . . 4
β’ (((2
Β· π) β (2(,)4)
β§ ((sinβ(2 Β· π)) = 0 β§ βπ₯ β (0(,)(2 Β· π))0 < (sinβπ₯))) β βπ β (2(,)4)((sinβπ) = 0 β§ βπ₯ β (0(,)π)0 < (sinβπ₯))) |
86 | 26, 40, 80, 85 | syl12anc 1236 |
. . 3
β’ ((π β (1(,)2) β§
((cosβπ) = 0 β§
βπ¦ β (π(,)(2 Β· π))0 < (sinβπ¦))) β βπ β (2(,)4)((sinβπ) = 0 β§ βπ₯ β (0(,)π)0 < (sinβπ₯))) |
87 | 86 | rexlimiva 2589 |
. 2
β’
(βπ β
(1(,)2)((cosβπ) = 0
β§ βπ¦ β
(π(,)(2 Β· π))0 < (sinβπ¦)) β βπ β (2(,)4)((sinβπ) = 0 β§ βπ₯ β (0(,)π)0 < (sinβπ₯))) |
88 | 1, 87 | ax-mp 5 |
1
β’
βπ β
(2(,)4)((sinβπ) = 0
β§ βπ₯ β
(0(,)π)0 <
(sinβπ₯)) |