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 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 ) ) )