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