Step | Hyp | Ref
| Expression |
1 | | dirkercncflem1.a |
. . . 4
β’ π΄ = (π β Ο) |
2 | | dirkercncflem1.y |
. . . . . 6
β’ (π β π β β) |
3 | | pire 25831 |
. . . . . . 7
β’ Ο
β β |
4 | 3 | a1i 11 |
. . . . . 6
β’ (π β Ο β
β) |
5 | 2, 4 | resubcld 11588 |
. . . . 5
β’ (π β (π β Ο) β
β) |
6 | 5 | rexrd 11210 |
. . . 4
β’ (π β (π β Ο) β
β*) |
7 | 1, 6 | eqeltrid 2838 |
. . 3
β’ (π β π΄ β
β*) |
8 | | dirkercncflem1.b |
. . . 4
β’ π΅ = (π + Ο) |
9 | 2, 4 | readdcld 11189 |
. . . . 5
β’ (π β (π + Ο) β β) |
10 | 9 | rexrd 11210 |
. . . 4
β’ (π β (π + Ο) β
β*) |
11 | 8, 10 | eqeltrid 2838 |
. . 3
β’ (π β π΅ β
β*) |
12 | | pipos 25833 |
. . . . . 6
β’ 0 <
Ο |
13 | | ltsubpos 11652 |
. . . . . 6
β’ ((Ο
β β β§ π
β β) β (0 < Ο β (π β Ο) < π)) |
14 | 12, 13 | mpbii 232 |
. . . . 5
β’ ((Ο
β β β§ π
β β) β (π
β Ο) < π) |
15 | 4, 2, 14 | syl2anc 585 |
. . . 4
β’ (π β (π β Ο) < π) |
16 | 1, 15 | eqbrtrid 5141 |
. . 3
β’ (π β π΄ < π) |
17 | | ltaddpos 11650 |
. . . . . 6
β’ ((Ο
β β β§ π
β β) β (0 < Ο β π < (π + Ο))) |
18 | 12, 17 | mpbii 232 |
. . . . 5
β’ ((Ο
β β β§ π
β β) β π
< (π +
Ο)) |
19 | 4, 2, 18 | syl2anc 585 |
. . . 4
β’ (π β π < (π + Ο)) |
20 | 19, 8 | breqtrrdi 5148 |
. . 3
β’ (π β π < π΅) |
21 | 7, 11, 2, 16, 20 | eliood 43822 |
. 2
β’ (π β π β (π΄(,)π΅)) |
22 | | eldifi 4087 |
. . . . . . . . . . 11
β’ (π¦ β ((π΄(,)π΅) β {π}) β π¦ β (π΄(,)π΅)) |
23 | 22 | elioored 43873 |
. . . . . . . . . 10
β’ (π¦ β ((π΄(,)π΅) β {π}) β π¦ β β) |
24 | 23 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π¦ β β) |
25 | 24 | recnd 11188 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π¦ β β) |
26 | | 2cnd 12236 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β 2 β
β) |
27 | | picn 25832 |
. . . . . . . . 9
β’ Ο
β β |
28 | 27 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Ο β
β) |
29 | | 2ne0 12262 |
. . . . . . . . 9
β’ 2 β
0 |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β 2 β 0) |
31 | 3, 12 | gt0ne0ii 11696 |
. . . . . . . . 9
β’ Ο β
0 |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Ο β 0) |
33 | 25, 26, 28, 30, 32 | divdiv1d 11967 |
. . . . . . 7
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π¦ / 2) / Ο) = (π¦ / (2 Β· Ο))) |
34 | | dirkercncflem1.ymod0 |
. . . . . . . . . . . 12
β’ (π β (π mod (2 Β· Ο)) =
0) |
35 | | 2rp 12925 |
. . . . . . . . . . . . . . 15
β’ 2 β
β+ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β
β+) |
37 | | pirp 25834 |
. . . . . . . . . . . . . . 15
β’ Ο
β β+ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β Ο β
β+) |
39 | 36, 38 | rpmulcld 12978 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· Ο) β
β+) |
40 | | mod0 13787 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (2
Β· Ο) β β+) β ((π mod (2 Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
41 | 2, 39, 40 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((π mod (2 Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
42 | 34, 41 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π / (2 Β· Ο)) β
β€) |
43 | | peano2zm 12551 |
. . . . . . . . . . 11
β’ ((π / (2 Β· Ο)) β
β€ β ((π / (2
Β· Ο)) β 1) β β€) |
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π / (2 Β· Ο)) β 1) β
β€) |
45 | 44 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β ((π / (2 Β· Ο)) β 1) β
β€) |
46 | 44 | zred 12612 |
. . . . . . . . . . . 12
β’ (π β ((π / (2 Β· Ο)) β 1) β
β) |
47 | 46 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π / (2 Β· Ο)) β 1) β
β) |
48 | 1, 5 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
49 | 48, 39 | rerpdivcld 12993 |
. . . . . . . . . . . 12
β’ (π β (π΄ / (2 Β· Ο)) β
β) |
50 | 49 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π΄ / (2 Β· Ο)) β
β) |
51 | 39 | rpred 12962 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· Ο) β
β) |
52 | 51 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (2 Β· Ο) β
β) |
53 | 39 | rpne0d 12967 |
. . . . . . . . . . . . 13
β’ (π β (2 Β· Ο) β
0) |
54 | 53 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (2 Β· Ο) β
0) |
55 | 24, 52, 54 | redivcld 11988 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π¦ / (2 Β· Ο)) β
β) |
56 | 51 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2 Β· Ο) β
β) |
57 | 56, 53 | dividd 11934 |
. . . . . . . . . . . . . . . 16
β’ (π β ((2 Β· Ο) / (2
Β· Ο)) = 1) |
58 | 57 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (π β 1 = ((2 Β· Ο) /
(2 Β· Ο))) |
59 | 58 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (π β ((π / (2 Β· Ο)) β 1) = ((π / (2 Β· Ο)) β
((2 Β· Ο) / (2 Β· Ο)))) |
60 | 2 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
61 | 60, 56, 56, 53 | divsubdird 11975 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (2 Β· Ο)) / (2 Β·
Ο)) = ((π / (2 Β·
Ο)) β ((2 Β· Ο) / (2 Β· Ο)))) |
62 | 59, 61 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (π β ((π / (2 Β· Ο)) β 1) = ((π β (2 Β· Ο)) / (2
Β· Ο))) |
63 | 2, 51 | resubcld 11588 |
. . . . . . . . . . . . . 14
β’ (π β (π β (2 Β· Ο)) β
β) |
64 | 27 | mulid2i 11165 |
. . . . . . . . . . . . . . . . . . 19
β’ (1
Β· Ο) = Ο |
65 | 64 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . 18
β’ Ο = (1
Β· Ο) |
66 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 <
2 |
67 | | 1re 11160 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β |
68 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
69 | 67, 68, 3, 12 | ltmul1ii 12088 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 < 2
β (1 Β· Ο) < (2 Β· Ο)) |
70 | 66, 69 | mpbi 229 |
. . . . . . . . . . . . . . . . . 18
β’ (1
Β· Ο) < (2 Β· Ο) |
71 | 65, 70 | eqbrtri 5127 |
. . . . . . . . . . . . . . . . 17
β’ Ο <
(2 Β· Ο) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο < (2 Β·
Ο)) |
73 | 4, 51, 2, 72 | ltsub2dd 11773 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (2 Β· Ο)) < (π β Ο)) |
74 | 73, 1 | breqtrrdi 5148 |
. . . . . . . . . . . . . 14
β’ (π β (π β (2 Β· Ο)) < π΄) |
75 | 63, 48, 39, 74 | ltdiv1dd 13019 |
. . . . . . . . . . . . 13
β’ (π β ((π β (2 Β· Ο)) / (2 Β·
Ο)) < (π΄ / (2
Β· Ο))) |
76 | 62, 75 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ (π β ((π / (2 Β· Ο)) β 1) < (π΄ / (2 Β·
Ο))) |
77 | 76 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π / (2 Β· Ο)) β 1) < (π΄ / (2 Β·
Ο))) |
78 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π΄ β β) |
79 | 39 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (2 Β· Ο) β
β+) |
80 | 22 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π¦ β (π΄(,)π΅)) |
81 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π΄ β
β*) |
82 | 11 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π΅ β
β*) |
83 | | elioo2 13311 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β*
β§ π΅ β
β*) β (π¦ β (π΄(,)π΅) β (π¦ β β β§ π΄ < π¦ β§ π¦ < π΅))) |
84 | 81, 82, 83 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π¦ β (π΄(,)π΅) β (π¦ β β β§ π΄ < π¦ β§ π¦ < π΅))) |
85 | 80, 84 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π¦ β β β§ π΄ < π¦ β§ π¦ < π΅)) |
86 | 85 | simp2d 1144 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π΄ < π¦) |
87 | 78, 24, 79, 86 | ltdiv1dd 13019 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π΄ / (2 Β· Ο)) < (π¦ / (2 Β·
Ο))) |
88 | 47, 50, 55, 77, 87 | lttrd 11321 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π / (2 Β· Ο)) β 1) < (π¦ / (2 Β·
Ο))) |
89 | 88 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β ((π / (2 Β· Ο)) β 1) < (π¦ / (2 Β·
Ο))) |
90 | 23 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β π¦ β β) |
91 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β π β β) |
92 | 39 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β (2 Β· Ο) β
β+) |
93 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β π¦ < π) |
94 | 90, 91, 92, 93 | ltdiv1dd 13019 |
. . . . . . . . . 10
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β (π¦ / (2 Β· Ο)) < (π / (2 Β· Ο))) |
95 | 60, 56, 53 | divcld 11936 |
. . . . . . . . . . . . . 14
β’ (π β (π / (2 Β· Ο)) β
β) |
96 | 95 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π / (2 Β· Ο)) β
β) |
97 | | 1cnd 11155 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β 1 β
β) |
98 | 96, 97 | npcand 11521 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (((π / (2 Β· Ο)) β 1) + 1) =
(π / (2 Β·
Ο))) |
99 | 98 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π / (2 Β· Ο)) = (((π / (2 Β· Ο)) β 1) +
1)) |
100 | 99 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β (π / (2 Β· Ο)) = (((π / (2 Β· Ο)) β 1) +
1)) |
101 | 94, 100 | breqtrd 5132 |
. . . . . . . . 9
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β (π¦ / (2 Β· Ο)) < (((π / (2 Β· Ο)) β 1)
+ 1)) |
102 | | btwnnz 12584 |
. . . . . . . . 9
β’ ((((π / (2 Β· Ο)) β 1)
β β€ β§ ((π /
(2 Β· Ο)) β 1) < (π¦ / (2 Β· Ο)) β§ (π¦ / (2 Β· Ο)) <
(((π / (2 Β· Ο))
β 1) + 1)) β Β¬ (π¦ / (2 Β· Ο)) β
β€) |
103 | 45, 89, 101, 102 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ < π) β Β¬ (π¦ / (2 Β· Ο)) β
β€) |
104 | 42 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β (π / (2 Β· Ο)) β
β€) |
105 | 2 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β π β β) |
106 | 24 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β π¦ β β) |
107 | 79 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β (2 Β· Ο) β
β+) |
108 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ β€ π) β π¦ β β) |
109 | 2 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ β€ π) β π β β) |
110 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ β€ π) β π¦ β€ π) |
111 | | eldifsni 4751 |
. . . . . . . . . . . . . . 15
β’ (π¦ β ((π΄(,)π΅) β {π}) β π¦ β π) |
112 | 111 | necomd 2996 |
. . . . . . . . . . . . . 14
β’ (π¦ β ((π΄(,)π΅) β {π}) β π β π¦) |
113 | 112 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ β€ π) β π β π¦) |
114 | 108, 109,
110, 113 | leneltd 11314 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ π¦ β€ π) β π¦ < π) |
115 | 114 | stoic1a 1775 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β Β¬ π¦ β€ π) |
116 | 105, 106 | ltnled 11307 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β (π < π¦ β Β¬ π¦ β€ π)) |
117 | 115, 116 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β π < π¦) |
118 | 105, 106,
107, 117 | ltdiv1dd 13019 |
. . . . . . . . 9
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β (π / (2 Β· Ο)) < (π¦ / (2 Β·
Ο))) |
119 | 8, 9 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (π β π΅ β β) |
120 | 119, 39 | rerpdivcld 12993 |
. . . . . . . . . . . 12
β’ (π β (π΅ / (2 Β· Ο)) β
β) |
121 | 120 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π΅ / (2 Β· Ο)) β
β) |
122 | 2, 39 | rerpdivcld 12993 |
. . . . . . . . . . . . 13
β’ (π β (π / (2 Β· Ο)) β
β) |
123 | 122 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π / (2 Β· Ο)) β
β) |
124 | | 1red 11161 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β 1 β
β) |
125 | 123, 124 | readdcld 11189 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π / (2 Β· Ο)) + 1) β
β) |
126 | 119 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π΅ β β) |
127 | 85 | simp3d 1145 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β π¦ < π΅) |
128 | 24, 126, 79, 127 | ltdiv1dd 13019 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π¦ / (2 Β· Ο)) < (π΅ / (2 Β· Ο))) |
129 | 8 | oveq1i 7368 |
. . . . . . . . . . . . 13
β’ (π΅ / (2 Β· Ο)) = ((π + Ο) / (2 Β·
Ο)) |
130 | 27 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β
β) |
131 | 60, 130, 56, 53 | divdird 11974 |
. . . . . . . . . . . . . 14
β’ (π β ((π + Ο) / (2 Β· Ο)) = ((π / (2 Β· Ο)) + (Ο /
(2 Β· Ο)))) |
132 | 4, 39 | rerpdivcld 12993 |
. . . . . . . . . . . . . . 15
β’ (π β (Ο / (2 Β· Ο))
β β) |
133 | | 1red 11161 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β
β) |
134 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
135 | 134, 27 | mulcomi 11168 |
. . . . . . . . . . . . . . . . . . 19
β’ (2
Β· Ο) = (Ο Β· 2) |
136 | 135 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (Ο /
(2 Β· Ο)) = (Ο / (Ο Β· 2)) |
137 | 27, 31 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ο
β β β§ Ο β 0) |
138 | | 2cnne0 12368 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β
β β§ 2 β 0) |
139 | | divdiv1 11871 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Ο
β β β§ (Ο β β β§ Ο β 0) β§ (2 β
β β§ 2 β 0)) β ((Ο / Ο) / 2) = (Ο / (Ο Β·
2))) |
140 | 27, 137, 138, 139 | mp3an 1462 |
. . . . . . . . . . . . . . . . . 18
β’ ((Ο /
Ο) / 2) = (Ο / (Ο Β· 2)) |
141 | 27, 31 | dividi 11893 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ο /
Ο) = 1 |
142 | 141 | oveq1i 7368 |
. . . . . . . . . . . . . . . . . 18
β’ ((Ο /
Ο) / 2) = (1 / 2) |
143 | 136, 140,
142 | 3eqtr2i 2767 |
. . . . . . . . . . . . . . . . 17
β’ (Ο /
(2 Β· Ο)) = (1 / 2) |
144 | | halflt1 12376 |
. . . . . . . . . . . . . . . . 17
β’ (1 / 2)
< 1 |
145 | 143, 144 | eqbrtri 5127 |
. . . . . . . . . . . . . . . 16
β’ (Ο /
(2 Β· Ο)) < 1 |
146 | 145 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (Ο / (2 Β· Ο))
< 1) |
147 | 132, 133,
122, 146 | ltadd2dd 11319 |
. . . . . . . . . . . . . 14
β’ (π β ((π / (2 Β· Ο)) + (Ο / (2 Β·
Ο))) < ((π / (2
Β· Ο)) + 1)) |
148 | 131, 147 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
β’ (π β ((π + Ο) / (2 Β· Ο)) < ((π / (2 Β· Ο)) +
1)) |
149 | 129, 148 | eqbrtrid 5141 |
. . . . . . . . . . . 12
β’ (π β (π΅ / (2 Β· Ο)) < ((π / (2 Β· Ο)) +
1)) |
150 | 149 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π΅ / (2 Β· Ο)) < ((π / (2 Β· Ο)) +
1)) |
151 | 55, 121, 125, 128, 150 | lttrd 11321 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π¦ / (2 Β· Ο)) < ((π / (2 Β· Ο)) +
1)) |
152 | 151 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β (π¦ / (2 Β· Ο)) < ((π / (2 Β· Ο)) +
1)) |
153 | | btwnnz 12584 |
. . . . . . . . 9
β’ (((π / (2 Β· Ο)) β
β€ β§ (π / (2
Β· Ο)) < (π¦ /
(2 Β· Ο)) β§ (π¦
/ (2 Β· Ο)) < ((π / (2 Β· Ο)) + 1)) β Β¬
(π¦ / (2 Β· Ο))
β β€) |
154 | 104, 118,
152, 153 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π¦ β ((π΄(,)π΅) β {π})) β§ Β¬ π¦ < π) β Β¬ (π¦ / (2 Β· Ο)) β
β€) |
155 | 103, 154 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Β¬ (π¦ / (2 Β· Ο)) β
β€) |
156 | 33, 155 | eqneltrd 2854 |
. . . . . 6
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Β¬ ((π¦ / 2) / Ο) β
β€) |
157 | 25 | halfcld 12403 |
. . . . . . 7
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π¦ / 2) β β) |
158 | | sineq0 25896 |
. . . . . . 7
β’ ((π¦ / 2) β β β
((sinβ(π¦ / 2)) = 0
β ((π¦ / 2) / Ο)
β β€)) |
159 | 157, 158 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((sinβ(π¦ / 2)) = 0 β ((π¦ / 2) / Ο) β
β€)) |
160 | 156, 159 | mtbird 325 |
. . . . 5
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Β¬ (sinβ(π¦ / 2)) = 0) |
161 | 160 | neqned 2947 |
. . . 4
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (sinβ(π¦ / 2)) β 0) |
162 | 33 | oveq1d 7373 |
. . . . . . 7
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (((π¦ / 2) / Ο) + (1 / 2)) = ((π¦ / (2 Β· Ο)) + (1 /
2))) |
163 | 42 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π / (2 Β· Ο)) β
β€) |
164 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β π΄ = (π β Ο)) |
165 | 164 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π β (π΄ + Ο) = ((π β Ο) + Ο)) |
166 | 60, 130 | npcand 11521 |
. . . . . . . . . . . . 13
β’ (π β ((π β Ο) + Ο) = π) |
167 | 165, 166 | eqtr2d 2774 |
. . . . . . . . . . . 12
β’ (π β π = (π΄ + Ο)) |
168 | 167 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β (π / (2 Β· Ο)) = ((π΄ + Ο) / (2 Β·
Ο))) |
169 | 48 | recnd 11188 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
170 | 169, 130,
56, 53 | divdird 11974 |
. . . . . . . . . . 11
β’ (π β ((π΄ + Ο) / (2 Β· Ο)) = ((π΄ / (2 Β· Ο)) + (Ο /
(2 Β· Ο)))) |
171 | 130 | mulid1d 11177 |
. . . . . . . . . . . . . . 15
β’ (π β (Ο Β· 1) =
Ο) |
172 | 171 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ (π β Ο = (Ο Β·
1)) |
173 | | 2cnd 12236 |
. . . . . . . . . . . . . . 15
β’ (π β 2 β
β) |
174 | 173, 130 | mulcomd 11181 |
. . . . . . . . . . . . . 14
β’ (π β (2 Β· Ο) = (Ο
Β· 2)) |
175 | 172, 174 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π β (Ο / (2 Β· Ο))
= ((Ο Β· 1) / (Ο Β· 2))) |
176 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
177 | 29 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β 0) |
178 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β Ο β
0) |
179 | 176, 173,
130, 177, 178 | divcan5d 11962 |
. . . . . . . . . . . . 13
β’ (π β ((Ο Β· 1) / (Ο
Β· 2)) = (1 / 2)) |
180 | 175, 179 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β (Ο / (2 Β· Ο))
= (1 / 2)) |
181 | 180 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β ((π΄ / (2 Β· Ο)) + (Ο / (2 Β·
Ο))) = ((π΄ / (2 Β·
Ο)) + (1 / 2))) |
182 | 168, 170,
181 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π β (π / (2 Β· Ο)) = ((π΄ / (2 Β· Ο)) + (1 /
2))) |
183 | 182 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π / (2 Β· Ο)) = ((π΄ / (2 Β· Ο)) + (1 /
2))) |
184 | 124 | rehalfcld 12405 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (1 / 2) β
β) |
185 | 50, 55, 184, 87 | ltadd1dd 11771 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π΄ / (2 Β· Ο)) + (1 / 2)) <
((π¦ / (2 Β· Ο)) +
(1 / 2))) |
186 | 183, 185 | eqbrtrd 5128 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (π / (2 Β· Ο)) < ((π¦ / (2 Β· Ο)) + (1 /
2))) |
187 | 55, 121, 184, 128 | ltadd1dd 11771 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π¦ / (2 Β· Ο)) + (1 / 2)) < ((π΅ / (2 Β· Ο)) + (1 /
2))) |
188 | 129 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (π΅ / (2 Β· Ο)) = ((π + Ο) / (2 Β·
Ο))) |
189 | 188 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β ((π΅ / (2 Β· Ο)) + (1 / 2)) = (((π + Ο) / (2 Β· Ο)) +
(1 / 2))) |
190 | 180 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π β ((π / (2 Β· Ο)) + (Ο / (2 Β·
Ο))) = ((π / (2 Β·
Ο)) + (1 / 2))) |
191 | 131, 190 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β ((π + Ο) / (2 Β· Ο)) = ((π / (2 Β· Ο)) + (1 /
2))) |
192 | 191 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β (((π + Ο) / (2 Β· Ο)) + (1 / 2)) =
(((π / (2 Β· Ο)) +
(1 / 2)) + (1 / 2))) |
193 | 176 | halfcld 12403 |
. . . . . . . . . . . . 13
β’ (π β (1 / 2) β
β) |
194 | 95, 193, 193 | addassd 11182 |
. . . . . . . . . . . 12
β’ (π β (((π / (2 Β· Ο)) + (1 / 2)) + (1 / 2))
= ((π / (2 Β· Ο))
+ ((1 / 2) + (1 / 2)))) |
195 | 176 | 2halvesd 12404 |
. . . . . . . . . . . . 13
β’ (π β ((1 / 2) + (1 / 2)) =
1) |
196 | 195 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π β ((π / (2 Β· Ο)) + ((1 / 2) + (1 / 2)))
= ((π / (2 Β· Ο))
+ 1)) |
197 | 194, 196 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β (((π / (2 Β· Ο)) + (1 / 2)) + (1 / 2))
= ((π / (2 Β· Ο))
+ 1)) |
198 | 189, 192,
197 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π β ((π΅ / (2 Β· Ο)) + (1 / 2)) = ((π / (2 Β· Ο)) +
1)) |
199 | 198 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π΅ / (2 Β· Ο)) + (1 / 2)) = ((π / (2 Β· Ο)) +
1)) |
200 | 187, 199 | breqtrd 5132 |
. . . . . . . 8
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((π¦ / (2 Β· Ο)) + (1 / 2)) < ((π / (2 Β· Ο)) +
1)) |
201 | | btwnnz 12584 |
. . . . . . . 8
β’ (((π / (2 Β· Ο)) β
β€ β§ (π / (2
Β· Ο)) < ((π¦ /
(2 Β· Ο)) + (1 / 2)) β§ ((π¦ / (2 Β· Ο)) + (1 / 2)) < ((π / (2 Β· Ο)) + 1))
β Β¬ ((π¦ / (2
Β· Ο)) + (1 / 2)) β β€) |
202 | 163, 186,
200, 201 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Β¬ ((π¦ / (2 Β· Ο)) + (1 / 2)) β
β€) |
203 | 162, 202 | eqneltrd 2854 |
. . . . . 6
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Β¬ (((π¦ / 2) / Ο) + (1 / 2)) β
β€) |
204 | | coseq0 44191 |
. . . . . . 7
β’ ((π¦ / 2) β β β
((cosβ(π¦ / 2)) = 0
β (((π¦ / 2) / Ο) +
(1 / 2)) β β€)) |
205 | 157, 204 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((cosβ(π¦ / 2)) = 0 β (((π¦ / 2) / Ο) + (1 / 2)) β
β€)) |
206 | 203, 205 | mtbird 325 |
. . . . 5
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β Β¬ (cosβ(π¦ / 2)) = 0) |
207 | 206 | neqned 2947 |
. . . 4
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (cosβ(π¦ / 2)) β 0) |
208 | 161, 207 | jca 513 |
. . 3
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β ((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0)) |
209 | 208 | ralrimiva 3140 |
. 2
β’ (π β βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0)) |
210 | 21, 209 | jca 513 |
1
β’ (π β (π β (π΄(,)π΅) β§ βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β
0))) |