Metamath Proof Explorer

Theorem dirkercncflem1

Description: If Y is a multiple of _pi then it belongs to an open inerval ( A (,) B ) such that for any other point y in the interval, cos y/2 and sin y/2 are nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkercncflem1.a 
|- A = ( Y - _pi )
dirkercncflem1.b 
|- B = ( Y + _pi )
dirkercncflem1.y 
|- ( ph -> Y e. RR )
dirkercncflem1.ymod0 
|- ( ph -> ( Y mod ( 2 x. _pi ) ) = 0 )
Assertion dirkercncflem1 
|- ( ph -> ( Y e. ( A (,) B ) /\ A. y e. ( ( A (,) B ) \ { Y } ) ( ( sin ` ( y / 2 ) ) =/= 0 /\ ( cos ` ( y / 2 ) ) =/= 0 ) ) )

Proof

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 mullidi 
 |-  ( 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 mulridd 
 |-  ( 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 ) ) )