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 โŠข ๐ด = ( ๐‘Œ โˆ’ ฯ€ )
dirkercncflem1.b โŠข ๐ต = ( ๐‘Œ + ฯ€ )
dirkercncflem1.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ โ„ )
dirkercncflem1.ymod0 โŠข ( ๐œ‘ โ†’ ( ๐‘Œ mod ( 2 ยท ฯ€ ) ) = 0 )
Assertion dirkercncflem1 ( ๐œ‘ โ†’ ( ๐‘Œ โˆˆ ( ๐ด (,) ๐ต ) โˆง โˆ€ ๐‘ฆ โˆˆ ( ( ๐ด (,) ๐ต ) โˆ– { ๐‘Œ } ) ( ( sin โ€˜ ( ๐‘ฆ / 2 ) ) โ‰  0 โˆง ( cos โ€˜ ( ๐‘ฆ / 2 ) ) โ‰  0 ) ) )

Proof

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