Step | Hyp | Ref
| Expression |
1 | | cosz12 14204 |
. 2
β’
βπ β
(1(,)2)(cosβπ) =
0 |
2 | | simpr 110 |
. . . . 5
β’ ((π β (1(,)2) β§
(cosβπ) = 0) β
(cosβπ) =
0) |
3 | | 2re 8989 |
. . . . . . . . . . . 12
β’ 2 β
β |
4 | 3 | a1i 9 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β 2 β
β) |
5 | | elioore 9912 |
. . . . . . . . . . . 12
β’ (π β (1(,)2) β π β
β) |
6 | 5 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π β β) |
7 | 4, 6 | remulcld 7988 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (2 Β· π) β
β) |
8 | | elioore 9912 |
. . . . . . . . . . 11
β’ (π₯ β (π(,)(2 Β· π)) β π₯ β β) |
9 | 8 | adantl 277 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π₯ β β) |
10 | 7, 9 | resubcld 8338 |
. . . . . . . . 9
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) β β) |
11 | | eliooord 9928 |
. . . . . . . . . . . 12
β’ (π₯ β (π(,)(2 Β· π)) β (π < π₯ β§ π₯ < (2 Β· π))) |
12 | 11 | simprd 114 |
. . . . . . . . . . 11
β’ (π₯ β (π(,)(2 Β· π)) β π₯ < (2 Β· π)) |
13 | 12 | adantl 277 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π₯ < (2 Β· π)) |
14 | 9, 7 | posdifd 8489 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (π₯ < (2 Β· π) β 0 < ((2 Β· π) β π₯))) |
15 | 13, 14 | mpbid 147 |
. . . . . . . . 9
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β 0 < ((2 Β·
π) β π₯)) |
16 | 11 | simpld 112 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π(,)(2 Β· π)) β π < π₯) |
17 | 16 | adantl 277 |
. . . . . . . . . . . . . . 15
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π < π₯) |
18 | 6, 9, 7, 17 | ltsub2dd 8515 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) < ((2 Β· π) β π)) |
19 | 6 | recnd 7986 |
. . . . . . . . . . . . . . . 16
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π β β) |
20 | 19 | mulid2d 7976 |
. . . . . . . . . . . . . . 15
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (1 Β· π) = π) |
21 | 20 | oveq2d 5891 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β (1 Β· π)) = ((2 Β· π) β π)) |
22 | 18, 21 | breqtrrd 4032 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) < ((2 Β· π) β (1 Β· π))) |
23 | 4 | recnd 7986 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β 2 β
β) |
24 | | 1cnd 7973 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β 1 β
β) |
25 | 23, 24, 19 | subdird 8372 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 β 1)
Β· π) = ((2 Β·
π) β (1 Β·
π))) |
26 | 22, 25 | breqtrrd 4032 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) < ((2 β 1) Β· π)) |
27 | | 2m1e1 9037 |
. . . . . . . . . . . . . 14
β’ (2
β 1) = 1 |
28 | 27 | oveq1i 5885 |
. . . . . . . . . . . . 13
β’ ((2
β 1) Β· π) = (1
Β· π) |
29 | 28, 20 | eqtrid 2222 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 β 1)
Β· π) = π) |
30 | 26, 29 | breqtrd 4030 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) < π) |
31 | | eliooord 9928 |
. . . . . . . . . . . . 13
β’ (π β (1(,)2) β (1 <
π β§ π < 2)) |
32 | 31 | simprd 114 |
. . . . . . . . . . . 12
β’ (π β (1(,)2) β π < 2) |
33 | 32 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π < 2) |
34 | 10, 6, 4, 30, 33 | lttrd 8083 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) < 2) |
35 | 10, 4, 34 | ltled 8076 |
. . . . . . . . 9
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) β€ 2) |
36 | | 0xr 8004 |
. . . . . . . . . 10
β’ 0 β
β* |
37 | | elioc2 9936 |
. . . . . . . . . 10
β’ ((0
β β* β§ 2 β β) β (((2 Β· π) β π₯) β (0(,]2) β (((2 Β· π) β π₯) β β β§ 0 < ((2 Β·
π) β π₯) β§ ((2 Β· π) β π₯) β€ 2))) |
38 | 36, 3, 37 | mp2an 426 |
. . . . . . . . 9
β’ (((2
Β· π) β π₯) β (0(,]2) β (((2
Β· π) β π₯) β β β§ 0 <
((2 Β· π) β
π₯) β§ ((2 Β· π) β π₯) β€ 2)) |
39 | 10, 15, 35, 38 | syl3anbrc 1181 |
. . . . . . . 8
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) β (0(,]2)) |
40 | | sin02gt0 11771 |
. . . . . . . 8
β’ (((2
Β· π) β π₯) β (0(,]2) β 0 <
(sinβ((2 Β· π)
β π₯))) |
41 | 39, 40 | syl 14 |
. . . . . . 7
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β 0 < (sinβ((2
Β· π) β π₯))) |
42 | 7 | recnd 7986 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (2 Β· π) β
β) |
43 | 9 | recnd 7986 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β π₯ β β) |
44 | 42, 43 | subcld 8268 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β π₯) β β) |
45 | | sinsub 11748 |
. . . . . . . . . . . 12
β’ (((2
Β· π) β β
β§ ((2 Β· π)
β π₯) β β)
β (sinβ((2 Β· π) β ((2 Β· π) β π₯))) = (((sinβ(2 Β· π)) Β· (cosβ((2
Β· π) β π₯))) β ((cosβ(2
Β· π)) Β·
(sinβ((2 Β· π)
β π₯))))) |
46 | 42, 44, 45 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβ((2
Β· π) β ((2
Β· π) β π₯))) = (((sinβ(2 Β·
π)) Β· (cosβ((2
Β· π) β π₯))) β ((cosβ(2
Β· π)) Β·
(sinβ((2 Β· π)
β π₯))))) |
47 | 42, 43 | nncand 8273 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β· π) β ((2 Β· π) β π₯)) = π₯) |
48 | 47 | fveq2d 5520 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβ((2
Β· π) β ((2
Β· π) β π₯))) = (sinβπ₯)) |
49 | | cos2t 11758 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(cosβ(2 Β· π))
= ((2 Β· ((cosβπ)β2)) β 1)) |
50 | 19, 49 | syl 14 |
. . . . . . . . . . . . . . 15
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (cosβ(2
Β· π)) = ((2 Β·
((cosβπ)β2))
β 1)) |
51 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (cosβπ) = 0) |
52 | 51 | sq0id 10613 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((cosβπ)β2) = 0) |
53 | 52 | oveq2d 5891 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (2 Β·
((cosβπ)β2)) =
(2 Β· 0)) |
54 | | 2t0e0 9078 |
. . . . . . . . . . . . . . . . . 18
β’ (2
Β· 0) = 0 |
55 | 53, 54 | eqtrdi 2226 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (2 Β·
((cosβπ)β2)) =
0) |
56 | 55 | oveq1d 5890 |
. . . . . . . . . . . . . . . 16
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β·
((cosβπ)β2))
β 1) = (0 β 1)) |
57 | | df-neg 8131 |
. . . . . . . . . . . . . . . 16
β’ -1 = (0
β 1) |
58 | 56, 57 | eqtr4di 2228 |
. . . . . . . . . . . . . . 15
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((2 Β·
((cosβπ)β2))
β 1) = -1) |
59 | 50, 58 | eqtrd 2210 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (cosβ(2
Β· π)) =
-1) |
60 | 59 | oveq1d 5890 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((cosβ(2
Β· π)) Β·
(sinβ((2 Β· π)
β π₯))) = (-1 Β·
(sinβ((2 Β· π)
β π₯)))) |
61 | 44 | sincld 11718 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβ((2
Β· π) β π₯)) β
β) |
62 | 61 | mulm1d 8367 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (-1 Β·
(sinβ((2 Β· π)
β π₯))) =
-(sinβ((2 Β· π)
β π₯))) |
63 | 60, 62 | eqtrd 2210 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((cosβ(2
Β· π)) Β·
(sinβ((2 Β· π)
β π₯))) =
-(sinβ((2 Β· π)
β π₯))) |
64 | 63 | oveq2d 5891 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (((sinβ(2
Β· π)) Β·
(cosβ((2 Β· π)
β π₯))) β
((cosβ(2 Β· π))
Β· (sinβ((2 Β· π) β π₯)))) = (((sinβ(2 Β· π)) Β· (cosβ((2
Β· π) β π₯))) β -(sinβ((2
Β· π) β π₯)))) |
65 | 46, 48, 64 | 3eqtr3d 2218 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβπ₯) = (((sinβ(2 Β·
π)) Β· (cosβ((2
Β· π) β π₯))) β -(sinβ((2
Β· π) β π₯)))) |
66 | 42 | sincld 11718 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβ(2
Β· π)) β
β) |
67 | 44 | coscld 11719 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (cosβ((2
Β· π) β π₯)) β
β) |
68 | 66, 67 | mulcld 7978 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((sinβ(2
Β· π)) Β·
(cosβ((2 Β· π)
β π₯))) β
β) |
69 | 68, 61 | subnegd 8275 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (((sinβ(2
Β· π)) Β·
(cosβ((2 Β· π)
β π₯))) β
-(sinβ((2 Β· π)
β π₯))) =
(((sinβ(2 Β· π)) Β· (cosβ((2 Β· π) β π₯))) + (sinβ((2 Β· π) β π₯)))) |
70 | 65, 69 | eqtrd 2210 |
. . . . . . . . 9
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβπ₯) = (((sinβ(2 Β·
π)) Β· (cosβ((2
Β· π) β π₯))) + (sinβ((2 Β·
π) β π₯)))) |
71 | | sin2t 11757 |
. . . . . . . . . . . . . 14
β’ (π β β β
(sinβ(2 Β· π))
= (2 Β· ((sinβπ) Β· (cosβπ)))) |
72 | 19, 71 | syl 14 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβ(2
Β· π)) = (2 Β·
((sinβπ) Β·
(cosβπ)))) |
73 | 51 | oveq2d 5891 |
. . . . . . . . . . . . . . . 16
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((sinβπ) Β· (cosβπ)) = ((sinβπ) Β· 0)) |
74 | 19 | sincld 11718 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβπ) β
β) |
75 | 74 | mul01d 8350 |
. . . . . . . . . . . . . . . 16
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((sinβπ) Β· 0) =
0) |
76 | 73, 75 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((sinβπ) Β· (cosβπ)) = 0) |
77 | 76 | oveq2d 5891 |
. . . . . . . . . . . . . 14
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (2 Β·
((sinβπ) Β·
(cosβπ))) = (2
Β· 0)) |
78 | 77, 54 | eqtrdi 2226 |
. . . . . . . . . . . . 13
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (2 Β·
((sinβπ) Β·
(cosβπ))) =
0) |
79 | 72, 78 | eqtrd 2210 |
. . . . . . . . . . . 12
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβ(2
Β· π)) =
0) |
80 | 79 | oveq1d 5890 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((sinβ(2
Β· π)) Β·
(cosβ((2 Β· π)
β π₯))) = (0 Β·
(cosβ((2 Β· π)
β π₯)))) |
81 | 67 | mul02d 8349 |
. . . . . . . . . . 11
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (0 Β·
(cosβ((2 Β· π)
β π₯))) =
0) |
82 | 80, 81 | eqtrd 2210 |
. . . . . . . . . 10
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β ((sinβ(2
Β· π)) Β·
(cosβ((2 Β· π)
β π₯))) =
0) |
83 | 82 | oveq1d 5890 |
. . . . . . . . 9
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (((sinβ(2
Β· π)) Β·
(cosβ((2 Β· π)
β π₯))) +
(sinβ((2 Β· π)
β π₯))) = (0 +
(sinβ((2 Β· π)
β π₯)))) |
84 | 70, 83 | eqtrd 2210 |
. . . . . . . 8
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβπ₯) = (0 + (sinβ((2 Β·
π) β π₯)))) |
85 | 61 | addid2d 8107 |
. . . . . . . 8
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (0 + (sinβ((2
Β· π) β π₯))) = (sinβ((2 Β·
π) β π₯))) |
86 | 84, 85 | eqtrd 2210 |
. . . . . . 7
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β (sinβπ₯) = (sinβ((2 Β·
π) β π₯))) |
87 | 41, 86 | breqtrrd 4032 |
. . . . . 6
β’ (((π β (1(,)2) β§
(cosβπ) = 0) β§
π₯ β (π(,)(2 Β· π))) β 0 <
(sinβπ₯)) |
88 | 87 | ralrimiva 2550 |
. . . . 5
β’ ((π β (1(,)2) β§
(cosβπ) = 0) β
βπ₯ β (π(,)(2 Β· π))0 < (sinβπ₯)) |
89 | 2, 88 | jca 306 |
. . . 4
β’ ((π β (1(,)2) β§
(cosβπ) = 0) β
((cosβπ) = 0 β§
βπ₯ β (π(,)(2 Β· π))0 < (sinβπ₯))) |
90 | 89 | ex 115 |
. . 3
β’ (π β (1(,)2) β
((cosβπ) = 0 β
((cosβπ) = 0 β§
βπ₯ β (π(,)(2 Β· π))0 < (sinβπ₯)))) |
91 | 90 | reximia 2572 |
. 2
β’
(βπ β
(1(,)2)(cosβπ) = 0
β βπ β
(1(,)2)((cosβπ) = 0
β§ βπ₯ β
(π(,)(2 Β· π))0 < (sinβπ₯))) |
92 | 1, 91 | ax-mp 5 |
1
β’
βπ β
(1(,)2)((cosβπ) = 0
β§ βπ₯ β
(π(,)(2 Β· π))0 < (sinβπ₯)) |