Step | Hyp | Ref
| Expression |
1 | | halfpire 25837 |
. . . . . 6
β’ (Ο /
2) β β |
2 | 1 | recni 11174 |
. . . . 5
β’ (Ο /
2) β β |
3 | | simpl 484 |
. . . . 5
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β π΄ β β) |
4 | | nncan 11435 |
. . . . 5
β’ (((Ο /
2) β β β§ π΄
β β) β ((Ο / 2) β ((Ο / 2) β π΄)) = π΄) |
5 | 2, 3, 4 | sylancr 588 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((Ο / 2) β ((Ο / 2) β
π΄)) = π΄) |
6 | 5 | fveq2d 6847 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ((Ο / 2) β ((Ο / 2)
β π΄))) =
(cosβπ΄)) |
7 | | subcl 11405 |
. . . . 5
β’ (((Ο /
2) β β β§ π΄
β β) β ((Ο / 2) β π΄) β β) |
8 | 2, 3, 7 | sylancr 588 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((Ο / 2) β π΄) β β) |
9 | | coshalfpim 25868 |
. . . 4
β’ (((Ο /
2) β π΄) β
β β (cosβ((Ο / 2) β ((Ο / 2) β π΄))) = (sinβ((Ο / 2)
β π΄))) |
10 | 8, 9 | syl 17 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβ((Ο / 2) β ((Ο / 2)
β π΄))) =
(sinβ((Ο / 2) β π΄))) |
11 | 6, 10 | eqtr3d 2775 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) = (sinβ((Ο / 2) β π΄))) |
12 | 5 | adantr 482 |
. . . . . . . 8
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β ((Ο / 2)
β ((Ο / 2) β π΄)) = π΄) |
13 | | picn 25832 |
. . . . . . . . . . . . 13
β’ Ο
β β |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β Ο β β) |
15 | | pire 25831 |
. . . . . . . . . . . . . 14
β’ Ο
β β |
16 | | pipos 25833 |
. . . . . . . . . . . . . 14
β’ 0 <
Ο |
17 | 15, 16 | gt0ne0ii 11696 |
. . . . . . . . . . . . 13
β’ Ο β
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β Ο β 0) |
19 | 8, 14, 18 | divcan1d 11937 |
. . . . . . . . . . 11
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((((Ο / 2) β π΄) / Ο) Β· Ο) = ((Ο / 2)
β π΄)) |
20 | 19 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β ((((Ο /
2) β π΄) / Ο)
Β· Ο) = ((Ο / 2) β π΄)) |
21 | | zre 12508 |
. . . . . . . . . . . 12
β’ ((((Ο
/ 2) β π΄) / Ο)
β β€ β (((Ο / 2) β π΄) / Ο) β β) |
22 | 21 | adantl 483 |
. . . . . . . . . . 11
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β (((Ο /
2) β π΄) / Ο)
β β) |
23 | | remulcl 11141 |
. . . . . . . . . . 11
β’ (((((Ο
/ 2) β π΄) / Ο)
β β β§ Ο β β) β ((((Ο / 2) β π΄) / Ο) Β· Ο) β
β) |
24 | 22, 15, 23 | sylancl 587 |
. . . . . . . . . 10
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β ((((Ο /
2) β π΄) / Ο)
Β· Ο) β β) |
25 | 20, 24 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β ((Ο / 2)
β π΄) β
β) |
26 | | resubcl 11470 |
. . . . . . . . 9
β’ (((Ο /
2) β β β§ ((Ο / 2) β π΄) β β) β ((Ο / 2) β
((Ο / 2) β π΄))
β β) |
27 | 1, 25, 26 | sylancr 588 |
. . . . . . . 8
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β ((Ο / 2)
β ((Ο / 2) β π΄)) β β) |
28 | 12, 27 | eqeltrrd 2835 |
. . . . . . 7
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β π΄ β
β) |
29 | 28 | rered 15115 |
. . . . . 6
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β
(ββπ΄) = π΄) |
30 | | simplr 768 |
. . . . . 6
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) |
31 | 29, 30 | eqeltrrd 2835 |
. . . . 5
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β π΄ β (-(Ο / 2)(,)(Ο /
2))) |
32 | | 0zd 12516 |
. . . . . 6
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β 0 β β€) |
33 | | elioore 13300 |
. . . . . . . 8
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β π΄ β
β) |
34 | | resubcl 11470 |
. . . . . . . 8
β’ (((Ο /
2) β β β§ π΄
β β) β ((Ο / 2) β π΄) β β) |
35 | 1, 33, 34 | sylancr 588 |
. . . . . . 7
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β ((Ο / 2) β π΄) β β) |
36 | 15 | a1i 11 |
. . . . . . 7
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β Ο β β) |
37 | | eliooord 13329 |
. . . . . . . . 9
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β (-(Ο / 2) < π΄ β§ π΄ < (Ο / 2))) |
38 | 37 | simprd 497 |
. . . . . . . 8
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β π΄ < (Ο /
2)) |
39 | | posdif 11653 |
. . . . . . . . 9
β’ ((π΄ β β β§ (Ο / 2)
β β) β (π΄
< (Ο / 2) β 0 < ((Ο / 2) β π΄))) |
40 | 33, 1, 39 | sylancl 587 |
. . . . . . . 8
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β (π΄ < (Ο /
2) β 0 < ((Ο / 2) β π΄))) |
41 | 38, 40 | mpbid 231 |
. . . . . . 7
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β 0 < ((Ο / 2) β π΄)) |
42 | 16 | a1i 11 |
. . . . . . 7
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β 0 < Ο) |
43 | 35, 36, 41, 42 | divgt0d 12095 |
. . . . . 6
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β 0 < (((Ο / 2) β π΄) / Ο)) |
44 | 1 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β (Ο / 2) β β) |
45 | 2 | negcli 11474 |
. . . . . . . . . . . 12
β’ -(Ο /
2) β β |
46 | 13, 2 | negsubi 11484 |
. . . . . . . . . . . . 13
β’ (Ο +
-(Ο / 2)) = (Ο β (Ο / 2)) |
47 | | pidiv2halves 25840 |
. . . . . . . . . . . . . 14
β’ ((Ο /
2) + (Ο / 2)) = Ο |
48 | 13, 2, 2, 47 | subaddrii 11495 |
. . . . . . . . . . . . 13
β’ (Ο
β (Ο / 2)) = (Ο / 2) |
49 | 46, 48 | eqtri 2761 |
. . . . . . . . . . . 12
β’ (Ο +
-(Ο / 2)) = (Ο / 2) |
50 | 2, 13, 45, 49 | subaddrii 11495 |
. . . . . . . . . . 11
β’ ((Ο /
2) β Ο) = -(Ο / 2) |
51 | 37 | simpld 496 |
. . . . . . . . . . 11
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β -(Ο / 2) < π΄) |
52 | 50, 51 | eqbrtrid 5141 |
. . . . . . . . . 10
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β ((Ο / 2) β Ο) < π΄) |
53 | 44, 36, 33, 52 | ltsub23d 11765 |
. . . . . . . . 9
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β ((Ο / 2) β π΄) < Ο) |
54 | 13 | mulid1i 11164 |
. . . . . . . . 9
β’ (Ο
Β· 1) = Ο |
55 | 53, 54 | breqtrrdi 5148 |
. . . . . . . 8
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β ((Ο / 2) β π΄) < (Ο Β· 1)) |
56 | | 1red 11161 |
. . . . . . . . 9
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β 1 β β) |
57 | | ltdivmul 12035 |
. . . . . . . . 9
β’ ((((Ο
/ 2) β π΄) β
β β§ 1 β β β§ (Ο β β β§ 0 < Ο))
β ((((Ο / 2) β π΄) / Ο) < 1 β ((Ο / 2) β
π΄) < (Ο Β·
1))) |
58 | 35, 56, 36, 42, 57 | syl112anc 1375 |
. . . . . . . 8
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β ((((Ο / 2) β π΄) / Ο) < 1 β ((Ο / 2) β
π΄) < (Ο Β·
1))) |
59 | 55, 58 | mpbird 257 |
. . . . . . 7
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β (((Ο / 2) β π΄) / Ο) < 1) |
60 | | 1e0p1 12665 |
. . . . . . 7
β’ 1 = (0 +
1) |
61 | 59, 60 | breqtrdi 5147 |
. . . . . 6
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β (((Ο / 2) β π΄) / Ο) < (0 + 1)) |
62 | | btwnnz 12584 |
. . . . . 6
β’ ((0
β β€ β§ 0 < (((Ο / 2) β π΄) / Ο) β§ (((Ο / 2) β π΄) / Ο) < (0 + 1)) β
Β¬ (((Ο / 2) β π΄) / Ο) β β€) |
63 | 32, 43, 61, 62 | syl3anc 1372 |
. . . . 5
β’ (π΄ β (-(Ο / 2)(,)(Ο /
2)) β Β¬ (((Ο / 2) β π΄) / Ο) β β€) |
64 | 31, 63 | syl 17 |
. . . 4
β’ (((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β§ (((Ο / 2) β π΄) / Ο) β β€) β Β¬
(((Ο / 2) β π΄) /
Ο) β β€) |
65 | 64 | pm2.01da 798 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β Β¬ (((Ο / 2) β π΄) / Ο) β β€) |
66 | | sineq0 25896 |
. . . . 5
β’ (((Ο /
2) β π΄) β
β β ((sinβ((Ο / 2) β π΄)) = 0 β (((Ο / 2) β π΄) / Ο) β
β€)) |
67 | 8, 66 | syl 17 |
. . . 4
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((sinβ((Ο / 2) β π΄)) = 0 β (((Ο / 2)
β π΄) / Ο) β
β€)) |
68 | 67 | necon3abid 2977 |
. . 3
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β ((sinβ((Ο / 2) β π΄)) β 0 β Β¬ (((Ο /
2) β π΄) / Ο)
β β€)) |
69 | 65, 68 | mpbird 257 |
. 2
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (sinβ((Ο / 2) β π΄)) β 0) |
70 | 11, 69 | eqnetrd 3008 |
1
β’ ((π΄ β β β§
(ββπ΄) β
(-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) β 0) |