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