Step |
Hyp |
Ref |
Expression |
1 |
|
dirkercncflem1.a |
โข ๐ด = ( ๐ โ ฯ ) |
2 |
|
dirkercncflem1.b |
โข ๐ต = ( ๐ + ฯ ) |
3 |
|
dirkercncflem1.y |
โข ( ๐ โ ๐ โ โ ) |
4 |
|
dirkercncflem1.ymod0 |
โข ( ๐ โ ( ๐ mod ( 2 ยท ฯ ) ) = 0 ) |
5 |
|
pire |
โข ฯ โ โ |
6 |
5
|
a1i |
โข ( ๐ โ ฯ โ โ ) |
7 |
3 6
|
resubcld |
โข ( ๐ โ ( ๐ โ ฯ ) โ โ ) |
8 |
7
|
rexrd |
โข ( ๐ โ ( ๐ โ ฯ ) โ โ* ) |
9 |
1 8
|
eqeltrid |
โข ( ๐ โ ๐ด โ โ* ) |
10 |
3 6
|
readdcld |
โข ( ๐ โ ( ๐ + ฯ ) โ โ ) |
11 |
10
|
rexrd |
โข ( ๐ โ ( ๐ + ฯ ) โ โ* ) |
12 |
2 11
|
eqeltrid |
โข ( ๐ โ ๐ต โ โ* ) |
13 |
|
pipos |
โข 0 < ฯ |
14 |
|
ltsubpos |
โข ( ( ฯ โ โ โง ๐ โ โ ) โ ( 0 < ฯ โ ( ๐ โ ฯ ) < ๐ ) ) |
15 |
13 14
|
mpbii |
โข ( ( ฯ โ โ โง ๐ โ โ ) โ ( ๐ โ ฯ ) < ๐ ) |
16 |
6 3 15
|
syl2anc |
โข ( ๐ โ ( ๐ โ ฯ ) < ๐ ) |
17 |
1 16
|
eqbrtrid |
โข ( ๐ โ ๐ด < ๐ ) |
18 |
|
ltaddpos |
โข ( ( ฯ โ โ โง ๐ โ โ ) โ ( 0 < ฯ โ ๐ < ( ๐ + ฯ ) ) ) |
19 |
13 18
|
mpbii |
โข ( ( ฯ โ โ โง ๐ โ โ ) โ ๐ < ( ๐ + ฯ ) ) |
20 |
6 3 19
|
syl2anc |
โข ( ๐ โ ๐ < ( ๐ + ฯ ) ) |
21 |
20 2
|
breqtrrdi |
โข ( ๐ โ ๐ < ๐ต ) |
22 |
9 12 3 17 21
|
eliood |
โข ( ๐ โ ๐ โ ( ๐ด (,) ๐ต ) ) |
23 |
|
eldifi |
โข ( ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) โ ๐ฆ โ ( ๐ด (,) ๐ต ) ) |
24 |
23
|
elioored |
โข ( ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) โ ๐ฆ โ โ ) |
25 |
24
|
adantl |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ฆ โ โ ) |
26 |
25
|
recnd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ฆ โ โ ) |
27 |
|
2cnd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ 2 โ โ ) |
28 |
|
picn |
โข ฯ โ โ |
29 |
28
|
a1i |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ฯ โ โ ) |
30 |
|
2ne0 |
โข 2 โ 0 |
31 |
30
|
a1i |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ 2 โ 0 ) |
32 |
5 13
|
gt0ne0ii |
โข ฯ โ 0 |
33 |
32
|
a1i |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ฯ โ 0 ) |
34 |
26 27 29 31 33
|
divdiv1d |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ฆ / 2 ) / ฯ ) = ( ๐ฆ / ( 2 ยท ฯ ) ) ) |
35 |
|
2rp |
โข 2 โ โ+ |
36 |
35
|
a1i |
โข ( ๐ โ 2 โ โ+ ) |
37 |
|
pirp |
โข ฯ โ โ+ |
38 |
37
|
a1i |
โข ( ๐ โ ฯ โ โ+ ) |
39 |
36 38
|
rpmulcld |
โข ( ๐ โ ( 2 ยท ฯ ) โ โ+ ) |
40 |
|
mod0 |
โข ( ( ๐ โ โ โง ( 2 ยท ฯ ) โ โ+ ) โ ( ( ๐ mod ( 2 ยท ฯ ) ) = 0 โ ( ๐ / ( 2 ยท ฯ ) ) โ โค ) ) |
41 |
3 39 40
|
syl2anc |
โข ( ๐ โ ( ( ๐ mod ( 2 ยท ฯ ) ) = 0 โ ( ๐ / ( 2 ยท ฯ ) ) โ โค ) ) |
42 |
4 41
|
mpbid |
โข ( ๐ โ ( ๐ / ( 2 ยท ฯ ) ) โ โค ) |
43 |
|
peano2zm |
โข ( ( ๐ / ( 2 ยท ฯ ) ) โ โค โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) โ โค ) |
44 |
42 43
|
syl |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) โ โค ) |
45 |
44
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) โ โค ) |
46 |
44
|
zred |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) โ โ ) |
47 |
46
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) โ โ ) |
48 |
1 7
|
eqeltrid |
โข ( ๐ โ ๐ด โ โ ) |
49 |
48 39
|
rerpdivcld |
โข ( ๐ โ ( ๐ด / ( 2 ยท ฯ ) ) โ โ ) |
50 |
49
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ด / ( 2 ยท ฯ ) ) โ โ ) |
51 |
39
|
rpred |
โข ( ๐ โ ( 2 ยท ฯ ) โ โ ) |
52 |
51
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( 2 ยท ฯ ) โ โ ) |
53 |
39
|
rpne0d |
โข ( ๐ โ ( 2 ยท ฯ ) โ 0 ) |
54 |
53
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( 2 ยท ฯ ) โ 0 ) |
55 |
25 52 54
|
redivcld |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ฆ / ( 2 ยท ฯ ) ) โ โ ) |
56 |
51
|
recnd |
โข ( ๐ โ ( 2 ยท ฯ ) โ โ ) |
57 |
56 53
|
dividd |
โข ( ๐ โ ( ( 2 ยท ฯ ) / ( 2 ยท ฯ ) ) = 1 ) |
58 |
57
|
eqcomd |
โข ( ๐ โ 1 = ( ( 2 ยท ฯ ) / ( 2 ยท ฯ ) ) ) |
59 |
58
|
oveq2d |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) = ( ( ๐ / ( 2 ยท ฯ ) ) โ ( ( 2 ยท ฯ ) / ( 2 ยท ฯ ) ) ) ) |
60 |
3
|
recnd |
โข ( ๐ โ ๐ โ โ ) |
61 |
60 56 56 53
|
divsubdird |
โข ( ๐ โ ( ( ๐ โ ( 2 ยท ฯ ) ) / ( 2 ยท ฯ ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) โ ( ( 2 ยท ฯ ) / ( 2 ยท ฯ ) ) ) ) |
62 |
59 61
|
eqtr4d |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) = ( ( ๐ โ ( 2 ยท ฯ ) ) / ( 2 ยท ฯ ) ) ) |
63 |
3 51
|
resubcld |
โข ( ๐ โ ( ๐ โ ( 2 ยท ฯ ) ) โ โ ) |
64 |
28
|
mullidi |
โข ( 1 ยท ฯ ) = ฯ |
65 |
64
|
eqcomi |
โข ฯ = ( 1 ยท ฯ ) |
66 |
|
1lt2 |
โข 1 < 2 |
67 |
|
1re |
โข 1 โ โ |
68 |
|
2re |
โข 2 โ โ |
69 |
67 68 5 13
|
ltmul1ii |
โข ( 1 < 2 โ ( 1 ยท ฯ ) < ( 2 ยท ฯ ) ) |
70 |
66 69
|
mpbi |
โข ( 1 ยท ฯ ) < ( 2 ยท ฯ ) |
71 |
65 70
|
eqbrtri |
โข ฯ < ( 2 ยท ฯ ) |
72 |
71
|
a1i |
โข ( ๐ โ ฯ < ( 2 ยท ฯ ) ) |
73 |
6 51 3 72
|
ltsub2dd |
โข ( ๐ โ ( ๐ โ ( 2 ยท ฯ ) ) < ( ๐ โ ฯ ) ) |
74 |
73 1
|
breqtrrdi |
โข ( ๐ โ ( ๐ โ ( 2 ยท ฯ ) ) < ๐ด ) |
75 |
63 48 39 74
|
ltdiv1dd |
โข ( ๐ โ ( ( ๐ โ ( 2 ยท ฯ ) ) / ( 2 ยท ฯ ) ) < ( ๐ด / ( 2 ยท ฯ ) ) ) |
76 |
62 75
|
eqbrtrd |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) < ( ๐ด / ( 2 ยท ฯ ) ) ) |
77 |
76
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) < ( ๐ด / ( 2 ยท ฯ ) ) ) |
78 |
48
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ด โ โ ) |
79 |
39
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( 2 ยท ฯ ) โ โ+ ) |
80 |
23
|
adantl |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ฆ โ ( ๐ด (,) ๐ต ) ) |
81 |
9
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ด โ โ* ) |
82 |
12
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ต โ โ* ) |
83 |
|
elioo2 |
โข ( ( ๐ด โ โ* โง ๐ต โ โ* ) โ ( ๐ฆ โ ( ๐ด (,) ๐ต ) โ ( ๐ฆ โ โ โง ๐ด < ๐ฆ โง ๐ฆ < ๐ต ) ) ) |
84 |
81 82 83
|
syl2anc |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ฆ โ ( ๐ด (,) ๐ต ) โ ( ๐ฆ โ โ โง ๐ด < ๐ฆ โง ๐ฆ < ๐ต ) ) ) |
85 |
80 84
|
mpbid |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ฆ โ โ โง ๐ด < ๐ฆ โง ๐ฆ < ๐ต ) ) |
86 |
85
|
simp2d |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ด < ๐ฆ ) |
87 |
78 25 79 86
|
ltdiv1dd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ด / ( 2 ยท ฯ ) ) < ( ๐ฆ / ( 2 ยท ฯ ) ) ) |
88 |
47 50 55 77 87
|
lttrd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) < ( ๐ฆ / ( 2 ยท ฯ ) ) ) |
89 |
88
|
adantr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) < ( ๐ฆ / ( 2 ยท ฯ ) ) ) |
90 |
24
|
ad2antlr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ๐ฆ โ โ ) |
91 |
3
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ๐ โ โ ) |
92 |
39
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ( 2 ยท ฯ ) โ โ+ ) |
93 |
|
simpr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ๐ฆ < ๐ ) |
94 |
90 91 92 93
|
ltdiv1dd |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ๐ / ( 2 ยท ฯ ) ) ) |
95 |
60 56 53
|
divcld |
โข ( ๐ โ ( ๐ / ( 2 ยท ฯ ) ) โ โ ) |
96 |
95
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ / ( 2 ยท ฯ ) ) โ โ ) |
97 |
|
1cnd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ 1 โ โ ) |
98 |
96 97
|
npcand |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) + 1 ) = ( ๐ / ( 2 ยท ฯ ) ) ) |
99 |
98
|
eqcomd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ / ( 2 ยท ฯ ) ) = ( ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) + 1 ) ) |
100 |
99
|
adantr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ( ๐ / ( 2 ยท ฯ ) ) = ( ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) + 1 ) ) |
101 |
94 100
|
breqtrd |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) + 1 ) ) |
102 |
|
btwnnz |
โข ( ( ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) โ โค โง ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) < ( ๐ฆ / ( 2 ยท ฯ ) ) โง ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ( ( ๐ / ( 2 ยท ฯ ) ) โ 1 ) + 1 ) ) โ ยฌ ( ๐ฆ / ( 2 ยท ฯ ) ) โ โค ) |
103 |
45 89 101 102
|
syl3anc |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ < ๐ ) โ ยฌ ( ๐ฆ / ( 2 ยท ฯ ) ) โ โค ) |
104 |
42
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ( ๐ / ( 2 ยท ฯ ) ) โ โค ) |
105 |
3
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ๐ โ โ ) |
106 |
25
|
adantr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ๐ฆ โ โ ) |
107 |
79
|
adantr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ( 2 ยท ฯ ) โ โ+ ) |
108 |
25
|
adantr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ โค ๐ ) โ ๐ฆ โ โ ) |
109 |
3
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ โค ๐ ) โ ๐ โ โ ) |
110 |
|
simpr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ โค ๐ ) โ ๐ฆ โค ๐ ) |
111 |
|
eldifsni |
โข ( ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) โ ๐ฆ โ ๐ ) |
112 |
111
|
necomd |
โข ( ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) โ ๐ โ ๐ฆ ) |
113 |
112
|
ad2antlr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ โค ๐ ) โ ๐ โ ๐ฆ ) |
114 |
108 109 110 113
|
leneltd |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ๐ฆ โค ๐ ) โ ๐ฆ < ๐ ) |
115 |
114
|
stoic1a |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ยฌ ๐ฆ โค ๐ ) |
116 |
105 106
|
ltnled |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ( ๐ < ๐ฆ โ ยฌ ๐ฆ โค ๐ ) ) |
117 |
115 116
|
mpbird |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ๐ < ๐ฆ ) |
118 |
105 106 107 117
|
ltdiv1dd |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ( ๐ / ( 2 ยท ฯ ) ) < ( ๐ฆ / ( 2 ยท ฯ ) ) ) |
119 |
2 10
|
eqeltrid |
โข ( ๐ โ ๐ต โ โ ) |
120 |
119 39
|
rerpdivcld |
โข ( ๐ โ ( ๐ต / ( 2 ยท ฯ ) ) โ โ ) |
121 |
120
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ต / ( 2 ยท ฯ ) ) โ โ ) |
122 |
3 39
|
rerpdivcld |
โข ( ๐ โ ( ๐ / ( 2 ยท ฯ ) ) โ โ ) |
123 |
122
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ / ( 2 ยท ฯ ) ) โ โ ) |
124 |
|
1red |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ 1 โ โ ) |
125 |
123 124
|
readdcld |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) โ โ ) |
126 |
119
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ต โ โ ) |
127 |
85
|
simp3d |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ๐ฆ < ๐ต ) |
128 |
25 126 79 127
|
ltdiv1dd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ๐ต / ( 2 ยท ฯ ) ) ) |
129 |
2
|
oveq1i |
โข ( ๐ต / ( 2 ยท ฯ ) ) = ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) |
130 |
28
|
a1i |
โข ( ๐ โ ฯ โ โ ) |
131 |
60 130 56 53
|
divdird |
โข ( ๐ โ ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + ( ฯ / ( 2 ยท ฯ ) ) ) ) |
132 |
6 39
|
rerpdivcld |
โข ( ๐ โ ( ฯ / ( 2 ยท ฯ ) ) โ โ ) |
133 |
|
1red |
โข ( ๐ โ 1 โ โ ) |
134 |
|
2cn |
โข 2 โ โ |
135 |
134 28
|
mulcomi |
โข ( 2 ยท ฯ ) = ( ฯ ยท 2 ) |
136 |
135
|
oveq2i |
โข ( ฯ / ( 2 ยท ฯ ) ) = ( ฯ / ( ฯ ยท 2 ) ) |
137 |
28 32
|
pm3.2i |
โข ( ฯ โ โ โง ฯ โ 0 ) |
138 |
|
2cnne0 |
โข ( 2 โ โ โง 2 โ 0 ) |
139 |
|
divdiv1 |
โข ( ( ฯ โ โ โง ( ฯ โ โ โง ฯ โ 0 ) โง ( 2 โ โ โง 2 โ 0 ) ) โ ( ( ฯ / ฯ ) / 2 ) = ( ฯ / ( ฯ ยท 2 ) ) ) |
140 |
28 137 138 139
|
mp3an |
โข ( ( ฯ / ฯ ) / 2 ) = ( ฯ / ( ฯ ยท 2 ) ) |
141 |
28 32
|
dividi |
โข ( ฯ / ฯ ) = 1 |
142 |
141
|
oveq1i |
โข ( ( ฯ / ฯ ) / 2 ) = ( 1 / 2 ) |
143 |
136 140 142
|
3eqtr2i |
โข ( ฯ / ( 2 ยท ฯ ) ) = ( 1 / 2 ) |
144 |
|
halflt1 |
โข ( 1 / 2 ) < 1 |
145 |
143 144
|
eqbrtri |
โข ( ฯ / ( 2 ยท ฯ ) ) < 1 |
146 |
145
|
a1i |
โข ( ๐ โ ( ฯ / ( 2 ยท ฯ ) ) < 1 ) |
147 |
132 133 122 146
|
ltadd2dd |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) + ( ฯ / ( 2 ยท ฯ ) ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
148 |
131 147
|
eqbrtrd |
โข ( ๐ โ ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
149 |
129 148
|
eqbrtrid |
โข ( ๐ โ ( ๐ต / ( 2 ยท ฯ ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
150 |
149
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ต / ( 2 ยท ฯ ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
151 |
55 121 125 128 150
|
lttrd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
152 |
151
|
adantr |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
153 |
|
btwnnz |
โข ( ( ( ๐ / ( 2 ยท ฯ ) ) โ โค โง ( ๐ / ( 2 ยท ฯ ) ) < ( ๐ฆ / ( 2 ยท ฯ ) ) โง ( ๐ฆ / ( 2 ยท ฯ ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) โ ยฌ ( ๐ฆ / ( 2 ยท ฯ ) ) โ โค ) |
154 |
104 118 152 153
|
syl3anc |
โข ( ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โง ยฌ ๐ฆ < ๐ ) โ ยฌ ( ๐ฆ / ( 2 ยท ฯ ) ) โ โค ) |
155 |
103 154
|
pm2.61dan |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ยฌ ( ๐ฆ / ( 2 ยท ฯ ) ) โ โค ) |
156 |
34 155
|
eqneltrd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ยฌ ( ( ๐ฆ / 2 ) / ฯ ) โ โค ) |
157 |
26
|
halfcld |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ฆ / 2 ) โ โ ) |
158 |
|
sineq0 |
โข ( ( ๐ฆ / 2 ) โ โ โ ( ( sin โ ( ๐ฆ / 2 ) ) = 0 โ ( ( ๐ฆ / 2 ) / ฯ ) โ โค ) ) |
159 |
157 158
|
syl |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( sin โ ( ๐ฆ / 2 ) ) = 0 โ ( ( ๐ฆ / 2 ) / ฯ ) โ โค ) ) |
160 |
156 159
|
mtbird |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ยฌ ( sin โ ( ๐ฆ / 2 ) ) = 0 ) |
161 |
160
|
neqned |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( sin โ ( ๐ฆ / 2 ) ) โ 0 ) |
162 |
34
|
oveq1d |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ( ๐ฆ / 2 ) / ฯ ) + ( 1 / 2 ) ) = ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
163 |
42
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ / ( 2 ยท ฯ ) ) โ โค ) |
164 |
1
|
a1i |
โข ( ๐ โ ๐ด = ( ๐ โ ฯ ) ) |
165 |
164
|
oveq1d |
โข ( ๐ โ ( ๐ด + ฯ ) = ( ( ๐ โ ฯ ) + ฯ ) ) |
166 |
60 130
|
npcand |
โข ( ๐ โ ( ( ๐ โ ฯ ) + ฯ ) = ๐ ) |
167 |
165 166
|
eqtr2d |
โข ( ๐ โ ๐ = ( ๐ด + ฯ ) ) |
168 |
167
|
oveq1d |
โข ( ๐ โ ( ๐ / ( 2 ยท ฯ ) ) = ( ( ๐ด + ฯ ) / ( 2 ยท ฯ ) ) ) |
169 |
48
|
recnd |
โข ( ๐ โ ๐ด โ โ ) |
170 |
169 130 56 53
|
divdird |
โข ( ๐ โ ( ( ๐ด + ฯ ) / ( 2 ยท ฯ ) ) = ( ( ๐ด / ( 2 ยท ฯ ) ) + ( ฯ / ( 2 ยท ฯ ) ) ) ) |
171 |
130
|
mulridd |
โข ( ๐ โ ( ฯ ยท 1 ) = ฯ ) |
172 |
171
|
eqcomd |
โข ( ๐ โ ฯ = ( ฯ ยท 1 ) ) |
173 |
|
2cnd |
โข ( ๐ โ 2 โ โ ) |
174 |
173 130
|
mulcomd |
โข ( ๐ โ ( 2 ยท ฯ ) = ( ฯ ยท 2 ) ) |
175 |
172 174
|
oveq12d |
โข ( ๐ โ ( ฯ / ( 2 ยท ฯ ) ) = ( ( ฯ ยท 1 ) / ( ฯ ยท 2 ) ) ) |
176 |
|
1cnd |
โข ( ๐ โ 1 โ โ ) |
177 |
30
|
a1i |
โข ( ๐ โ 2 โ 0 ) |
178 |
32
|
a1i |
โข ( ๐ โ ฯ โ 0 ) |
179 |
176 173 130 177 178
|
divcan5d |
โข ( ๐ โ ( ( ฯ ยท 1 ) / ( ฯ ยท 2 ) ) = ( 1 / 2 ) ) |
180 |
175 179
|
eqtrd |
โข ( ๐ โ ( ฯ / ( 2 ยท ฯ ) ) = ( 1 / 2 ) ) |
181 |
180
|
oveq2d |
โข ( ๐ โ ( ( ๐ด / ( 2 ยท ฯ ) ) + ( ฯ / ( 2 ยท ฯ ) ) ) = ( ( ๐ด / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
182 |
168 170 181
|
3eqtrd |
โข ( ๐ โ ( ๐ / ( 2 ยท ฯ ) ) = ( ( ๐ด / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
183 |
182
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ / ( 2 ยท ฯ ) ) = ( ( ๐ด / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
184 |
124
|
rehalfcld |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( 1 / 2 ) โ โ ) |
185 |
50 55 184 87
|
ltadd1dd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ด / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) < ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
186 |
183 185
|
eqbrtrd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ๐ / ( 2 ยท ฯ ) ) < ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
187 |
55 121 184 128
|
ltadd1dd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) < ( ( ๐ต / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
188 |
129
|
a1i |
โข ( ๐ โ ( ๐ต / ( 2 ยท ฯ ) ) = ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) ) |
189 |
188
|
oveq1d |
โข ( ๐ โ ( ( ๐ต / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) = ( ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
190 |
180
|
oveq2d |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) + ( ฯ / ( 2 ยท ฯ ) ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
191 |
131 190
|
eqtrd |
โข ( ๐ โ ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) ) |
192 |
191
|
oveq1d |
โข ( ๐ โ ( ( ( ๐ + ฯ ) / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) = ( ( ( ๐ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) |
193 |
176
|
halfcld |
โข ( ๐ โ ( 1 / 2 ) โ โ ) |
194 |
95 193 193
|
addassd |
โข ( ๐ โ ( ( ( ๐ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) ) |
195 |
176
|
2halvesd |
โข ( ๐ โ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 ) |
196 |
195
|
oveq2d |
โข ( ๐ โ ( ( ๐ / ( 2 ยท ฯ ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
197 |
194 196
|
eqtrd |
โข ( ๐ โ ( ( ( ๐ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
198 |
189 192 197
|
3eqtrd |
โข ( ๐ โ ( ( ๐ต / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
199 |
198
|
adantr |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ต / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) = ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
200 |
187 199
|
breqtrd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) |
201 |
|
btwnnz |
โข ( ( ( ๐ / ( 2 ยท ฯ ) ) โ โค โง ( ๐ / ( 2 ยท ฯ ) ) < ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) โง ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) < ( ( ๐ / ( 2 ยท ฯ ) ) + 1 ) ) โ ยฌ ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) โ โค ) |
202 |
163 186 200 201
|
syl3anc |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ยฌ ( ( ๐ฆ / ( 2 ยท ฯ ) ) + ( 1 / 2 ) ) โ โค ) |
203 |
162 202
|
eqneltrd |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ยฌ ( ( ( ๐ฆ / 2 ) / ฯ ) + ( 1 / 2 ) ) โ โค ) |
204 |
|
coseq0 |
โข ( ( ๐ฆ / 2 ) โ โ โ ( ( cos โ ( ๐ฆ / 2 ) ) = 0 โ ( ( ( ๐ฆ / 2 ) / ฯ ) + ( 1 / 2 ) ) โ โค ) ) |
205 |
157 204
|
syl |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( cos โ ( ๐ฆ / 2 ) ) = 0 โ ( ( ( ๐ฆ / 2 ) / ฯ ) + ( 1 / 2 ) ) โ โค ) ) |
206 |
203 205
|
mtbird |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ยฌ ( cos โ ( ๐ฆ / 2 ) ) = 0 ) |
207 |
206
|
neqned |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( cos โ ( ๐ฆ / 2 ) ) โ 0 ) |
208 |
161 207
|
jca |
โข ( ( ๐ โง ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ) โ ( ( sin โ ( ๐ฆ / 2 ) ) โ 0 โง ( cos โ ( ๐ฆ / 2 ) ) โ 0 ) ) |
209 |
208
|
ralrimiva |
โข ( ๐ โ โ ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ( ( sin โ ( ๐ฆ / 2 ) ) โ 0 โง ( cos โ ( ๐ฆ / 2 ) ) โ 0 ) ) |
210 |
22 209
|
jca |
โข ( ๐ โ ( ๐ โ ( ๐ด (,) ๐ต ) โง โ ๐ฆ โ ( ( ๐ด (,) ๐ต ) โ { ๐ } ) ( ( sin โ ( ๐ฆ / 2 ) ) โ 0 โง ( cos โ ( ๐ฆ / 2 ) ) โ 0 ) ) ) |