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