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 - π$
	dirkercncflem1.b	$⊢ B = Y + π$
	dirkercncflem1.y	$⊢ φ \to Y \in ℝ$
	dirkercncflem1.ymod0	$⊢ φ \to Y \mod 2 π = 0$
Assertion	dirkercncflem1	$⊢ φ \to (Y \in (A, B) \land \forall y \in ((A, B) ∖ \{Y\}) (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0))$

Proof

Step	Hyp	Ref	Expression
1		dirkercncflem1.a	$⊢ A = Y - π$
2		dirkercncflem1.b	$⊢ B = Y + π$
3		dirkercncflem1.y	$⊢ φ \to Y \in ℝ$
4		dirkercncflem1.ymod0	$⊢ φ \to Y \mod 2 π = 0$
5		pire	$⊢ π \in ℝ$
6	5	a1i	$⊢ φ \to π \in ℝ$
7	3 6	resubcld	$⊢ φ \to Y - π \in ℝ$
8	7	rexrd	$⊢ φ \to Y - π \in ℝ^{*}$
9	1 8	eqeltrid	$⊢ φ \to A \in ℝ^{*}$
10	3 6	readdcld	$⊢ φ \to Y + π \in ℝ$
11	10	rexrd	$⊢ φ \to Y + π \in ℝ^{*}$
12	2 11	eqeltrid	$⊢ φ \to B \in ℝ^{*}$
13		pipos	$⊢ 0 < π$
14		ltsubpos	$⊢ (π \in ℝ \land Y \in ℝ) \to (0 < π \leftrightarrow Y - π < Y)$
15	13 14	mpbii	$⊢ (π \in ℝ \land Y \in ℝ) \to Y - π < Y$
16	6 3 15	syl2anc	$⊢ φ \to Y - π < Y$
17	1 16	eqbrtrid	$⊢ φ \to A < Y$
18		ltaddpos	$⊢ (π \in ℝ \land Y \in ℝ) \to (0 < π \leftrightarrow Y < Y + π)$
19	13 18	mpbii	$⊢ (π \in ℝ \land Y \in ℝ) \to Y < Y + π$
20	6 3 19	syl2anc	$⊢ φ \to Y < Y + π$
21	20 2	breqtrrdi	$⊢ φ \to Y < B$
22	9 12 3 17 21	eliood	$⊢ φ \to Y \in (A, B)$
23		eldifi	$⊢ y \in ((A, B) ∖ \{Y\}) \to y \in (A, B)$
24	23	elioored	$⊢ y \in ((A, B) ∖ \{Y\}) \to y \in ℝ$
25	24	adantl	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to y \in ℝ$
26	25	recnd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to y \in ℂ$
27		2cnd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 2 \in ℂ$
28		picn	$⊢ π \in ℂ$
29	28	a1i	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to π \in ℂ$
30		2ne0	$⊢ 2 \neq 0$
31	30	a1i	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 2 \neq 0$
32	5 13	gt0ne0ii	$⊢ π \neq 0$
33	32	a1i	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to π \neq 0$
34	26 27 29 31 33	divdiv1d	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{\frac{y}{2}}{π} = \frac{y}{2 π}$
35		2rp	$⊢ 2 \in ℝ^{+}$
36	35	a1i	$⊢ φ \to 2 \in ℝ^{+}$
37		pirp	$⊢ π \in ℝ^{+}$
38	37	a1i	$⊢ φ \to π \in ℝ^{+}$
39	36 38	rpmulcld	$⊢ φ \to 2 π \in ℝ^{+}$
40		mod0	$⊢ (Y \in ℝ \land 2 π \in ℝ^{+}) \to (Y \mod 2 π = 0 \leftrightarrow \frac{Y}{2 π} \in ℤ)$
41	3 39 40	syl2anc	$⊢ φ \to (Y \mod 2 π = 0 \leftrightarrow \frac{Y}{2 π} \in ℤ)$
42	4 41	mpbid	$⊢ φ \to \frac{Y}{2 π} \in ℤ$
43		peano2zm	$⊢ \frac{Y}{2 π} \in ℤ \to (\frac{Y}{2 π}) - 1 \in ℤ$
44	42 43	syl	$⊢ φ \to (\frac{Y}{2 π}) - 1 \in ℤ$
45	44	ad2antrr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to (\frac{Y}{2 π}) - 1 \in ℤ$
46	44	zred	$⊢ φ \to (\frac{Y}{2 π}) - 1 \in ℝ$
47	46	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{Y}{2 π}) - 1 \in ℝ$
48	1 7	eqeltrid	$⊢ φ \to A \in ℝ$
49	48 39	rerpdivcld	$⊢ φ \to \frac{A}{2 π} \in ℝ$
50	49	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{A}{2 π} \in ℝ$
51	39	rpred	$⊢ φ \to 2 π \in ℝ$
52	51	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 2 π \in ℝ$
53	39	rpne0d	$⊢ φ \to 2 π \neq 0$
54	53	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 2 π \neq 0$
55	25 52 54	redivcld	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{y}{2 π} \in ℝ$
56	51	recnd	$⊢ φ \to 2 π \in ℂ$
57	56 53	dividd	$⊢ φ \to \frac{2 π}{2 π} = 1$
58	57	eqcomd	$⊢ φ \to 1 = \frac{2 π}{2 π}$
59	58	oveq2d	$⊢ φ \to (\frac{Y}{2 π}) - 1 = (\frac{Y}{2 π}) - (\frac{2 π}{2 π})$
60	3	recnd	$⊢ φ \to Y \in ℂ$
61	60 56 56 53	divsubdird	$⊢ φ \to \frac{Y - 2 π}{2 π} = (\frac{Y}{2 π}) - (\frac{2 π}{2 π})$
62	59 61	eqtr4d	$⊢ φ \to (\frac{Y}{2 π}) - 1 = \frac{Y - 2 π}{2 π}$
63	3 51	resubcld	$⊢ φ \to Y - 2 π \in ℝ$
64	28	mullidi	$⊢ 1 π = π$
65	64	eqcomi	$⊢ π = 1 π$
66		1lt2	$⊢ 1 < 2$
67		1re	$⊢ 1 \in ℝ$
68		2re	$⊢ 2 \in ℝ$
69	67 68 5 13	ltmul1ii	$⊢ 1 < 2 \leftrightarrow 1 π < 2 π$
70	66 69	mpbi	$⊢ 1 π < 2 π$
71	65 70	eqbrtri	$⊢ π < 2 π$
72	71	a1i	$⊢ φ \to π < 2 π$
73	6 51 3 72	ltsub2dd	$⊢ φ \to Y - 2 π < Y - π$
74	73 1	breqtrrdi	$⊢ φ \to Y - 2 π < A$
75	63 48 39 74	ltdiv1dd	$⊢ φ \to \frac{Y - 2 π}{2 π} < \frac{A}{2 π}$
76	62 75	eqbrtrd	$⊢ φ \to (\frac{Y}{2 π}) - 1 < \frac{A}{2 π}$
77	76	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{Y}{2 π}) - 1 < \frac{A}{2 π}$
78	48	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to A \in ℝ$
79	39	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 2 π \in ℝ^{+}$
80	23	adantl	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to y \in (A, B)$
81	9	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to A \in ℝ^{*}$
82	12	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to B \in ℝ^{*}$
83		elioo2	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (y \in (A, B) \leftrightarrow (y \in ℝ \land A < y \land y < B))$
84	81 82 83	syl2anc	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (y \in (A, B) \leftrightarrow (y \in ℝ \land A < y \land y < B))$
85	80 84	mpbid	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (y \in ℝ \land A < y \land y < B)$
86	85	simp2d	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to A < y$
87	78 25 79 86	ltdiv1dd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{A}{2 π} < \frac{y}{2 π}$
88	47 50 55 77 87	lttrd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{Y}{2 π}) - 1 < \frac{y}{2 π}$
89	88	adantr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to (\frac{Y}{2 π}) - 1 < \frac{y}{2 π}$
90	24	ad2antlr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to y \in ℝ$
91	3	ad2antrr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to Y \in ℝ$
92	39	ad2antrr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to 2 π \in ℝ^{+}$
93		simpr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to y < Y$
94	90 91 92 93	ltdiv1dd	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to \frac{y}{2 π} < \frac{Y}{2 π}$
95	60 56 53	divcld	$⊢ φ \to \frac{Y}{2 π} \in ℂ$
96	95	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{Y}{2 π} \in ℂ$
97		1cnd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 1 \in ℂ$
98	96 97	npcand	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{Y}{2 π}) - 1 + 1 = \frac{Y}{2 π}$
99	98	eqcomd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{Y}{2 π} = (\frac{Y}{2 π}) - 1 + 1$
100	99	adantr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to \frac{Y}{2 π} = (\frac{Y}{2 π}) - 1 + 1$
101	94 100	breqtrd	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to \frac{y}{2 π} < (\frac{Y}{2 π}) - 1 + 1$
102		btwnnz	$⊢ ((\frac{Y}{2 π}) - 1 \in ℤ \land (\frac{Y}{2 π}) - 1 < \frac{y}{2 π} \land \frac{y}{2 π} < (\frac{Y}{2 π}) - 1 + 1) \to \neg \frac{y}{2 π} \in ℤ$
103	45 89 101 102	syl3anc	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y < Y) \to \neg \frac{y}{2 π} \in ℤ$
104	42	ad2antrr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to \frac{Y}{2 π} \in ℤ$
105	3	ad2antrr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to Y \in ℝ$
106	25	adantr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to y \in ℝ$
107	79	adantr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to 2 π \in ℝ^{+}$
108	25	adantr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y \leq Y) \to y \in ℝ$
109	3	ad2antrr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y \leq Y) \to Y \in ℝ$
110		simpr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y \leq Y) \to y \leq Y$
111		eldifsni	$⊢ y \in ((A, B) ∖ \{Y\}) \to y \neq Y$
112	111	necomd	$⊢ y \in ((A, B) ∖ \{Y\}) \to Y \neq y$
113	112	ad2antlr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y \leq Y) \to Y \neq y$
114	108 109 110 113	leneltd	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land y \leq Y) \to y < Y$
115	114	stoic1a	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to \neg y \leq Y$
116	105 106	ltnled	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to (Y < y \leftrightarrow \neg y \leq Y)$
117	115 116	mpbird	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to Y < y$
118	105 106 107 117	ltdiv1dd	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to \frac{Y}{2 π} < \frac{y}{2 π}$
119	2 10	eqeltrid	$⊢ φ \to B \in ℝ$
120	119 39	rerpdivcld	$⊢ φ \to \frac{B}{2 π} \in ℝ$
121	120	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{B}{2 π} \in ℝ$
122	3 39	rerpdivcld	$⊢ φ \to \frac{Y}{2 π} \in ℝ$
123	122	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{Y}{2 π} \in ℝ$
124		1red	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to 1 \in ℝ$
125	123 124	readdcld	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{Y}{2 π}) + 1 \in ℝ$
126	119	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to B \in ℝ$
127	85	simp3d	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to y < B$
128	25 126 79 127	ltdiv1dd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{y}{2 π} < \frac{B}{2 π}$
129	2	oveq1i	$⊢ \frac{B}{2 π} = \frac{Y + π}{2 π}$
130	28	a1i	$⊢ φ \to π \in ℂ$
131	60 130 56 53	divdird	$⊢ φ \to \frac{Y + π}{2 π} = (\frac{Y}{2 π}) + (\frac{π}{2 π})$
132	6 39	rerpdivcld	$⊢ φ \to \frac{π}{2 π} \in ℝ$
133		1red	$⊢ φ \to 1 \in ℝ$
134		2cn	$⊢ 2 \in ℂ$
135	134 28	mulcomi	$⊢ 2 π = π \cdot 2$
136	135	oveq2i	$⊢ \frac{π}{2 π} = \frac{π}{π \cdot 2}$
137	28 32	pm3.2i	$⊢ (π \in ℂ \land π \neq 0)$
138		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
139		divdiv1	$⊢ (π \in ℂ \land (π \in ℂ \land π \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{π}{π}}{2} = \frac{π}{π \cdot 2}$
140	28 137 138 139	mp3an	$⊢ \frac{\frac{π}{π}}{2} = \frac{π}{π \cdot 2}$
141	28 32	dividi	$⊢ \frac{π}{π} = 1$
142	141	oveq1i	$⊢ \frac{\frac{π}{π}}{2} = \frac{1}{2}$
143	136 140 142	3eqtr2i	$⊢ \frac{π}{2 π} = \frac{1}{2}$
144		halflt1	$⊢ \frac{1}{2} < 1$
145	143 144	eqbrtri	$⊢ \frac{π}{2 π} < 1$
146	145	a1i	$⊢ φ \to \frac{π}{2 π} < 1$
147	132 133 122 146	ltadd2dd	$⊢ φ \to (\frac{Y}{2 π}) + (\frac{π}{2 π}) < (\frac{Y}{2 π}) + 1$
148	131 147	eqbrtrd	$⊢ φ \to \frac{Y + π}{2 π} < (\frac{Y}{2 π}) + 1$
149	129 148	eqbrtrid	$⊢ φ \to \frac{B}{2 π} < (\frac{Y}{2 π}) + 1$
150	149	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{B}{2 π} < (\frac{Y}{2 π}) + 1$
151	55 121 125 128 150	lttrd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{y}{2 π} < (\frac{Y}{2 π}) + 1$
152	151	adantr	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to \frac{y}{2 π} < (\frac{Y}{2 π}) + 1$
153		btwnnz	$⊢ (\frac{Y}{2 π} \in ℤ \land \frac{Y}{2 π} < \frac{y}{2 π} \land \frac{y}{2 π} < (\frac{Y}{2 π}) + 1) \to \neg \frac{y}{2 π} \in ℤ$
154	104 118 152 153	syl3anc	$⊢ ((φ \land y \in ((A, B) ∖ \{Y\})) \land \neg y < Y) \to \neg \frac{y}{2 π} \in ℤ$
155	103 154	pm2.61dan	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \neg \frac{y}{2 π} \in ℤ$
156	34 155	eqneltrd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \neg \frac{\frac{y}{2}}{π} \in ℤ$
157	26	halfcld	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{y}{2} \in ℂ$
158		sineq0	$⊢ \frac{y}{2} \in ℂ \to (\sin (\frac{y}{2}) = 0 \leftrightarrow \frac{\frac{y}{2}}{π} \in ℤ)$
159	157 158	syl	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\sin (\frac{y}{2}) = 0 \leftrightarrow \frac{\frac{y}{2}}{π} \in ℤ)$
160	156 159	mtbird	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \neg \sin (\frac{y}{2}) = 0$
161	160	neqned	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \sin (\frac{y}{2}) \neq 0$
162	34	oveq1d	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{\frac{y}{2}}{π}) + (\frac{1}{2}) = (\frac{y}{2 π}) + (\frac{1}{2})$
163	42	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{Y}{2 π} \in ℤ$
164	1	a1i	$⊢ φ \to A = Y - π$
165	164	oveq1d	$⊢ φ \to A + π = Y - π + π$
166	60 130	npcand	$⊢ φ \to Y - π + π = Y$
167	165 166	eqtr2d	$⊢ φ \to Y = A + π$
168	167	oveq1d	$⊢ φ \to \frac{Y}{2 π} = \frac{A + π}{2 π}$
169	48	recnd	$⊢ φ \to A \in ℂ$
170	169 130 56 53	divdird	$⊢ φ \to \frac{A + π}{2 π} = (\frac{A}{2 π}) + (\frac{π}{2 π})$
171	130	mulridd	$⊢ φ \to π \cdot 1 = π$
172	171	eqcomd	$⊢ φ \to π = π \cdot 1$
173		2cnd	$⊢ φ \to 2 \in ℂ$
174	173 130	mulcomd	$⊢ φ \to 2 π = π \cdot 2$
175	172 174	oveq12d	$⊢ φ \to \frac{π}{2 π} = \frac{π \cdot 1}{π \cdot 2}$
176		1cnd	$⊢ φ \to 1 \in ℂ$
177	30	a1i	$⊢ φ \to 2 \neq 0$
178	32	a1i	$⊢ φ \to π \neq 0$
179	176 173 130 177 178	divcan5d	$⊢ φ \to \frac{π \cdot 1}{π \cdot 2} = \frac{1}{2}$
180	175 179	eqtrd	$⊢ φ \to \frac{π}{2 π} = \frac{1}{2}$
181	180	oveq2d	$⊢ φ \to (\frac{A}{2 π}) + (\frac{π}{2 π}) = (\frac{A}{2 π}) + (\frac{1}{2})$
182	168 170 181	3eqtrd	$⊢ φ \to \frac{Y}{2 π} = (\frac{A}{2 π}) + (\frac{1}{2})$
183	182	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{Y}{2 π} = (\frac{A}{2 π}) + (\frac{1}{2})$
184	124	rehalfcld	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{1}{2} \in ℝ$
185	50 55 184 87	ltadd1dd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{A}{2 π}) + (\frac{1}{2}) < (\frac{y}{2 π}) + (\frac{1}{2})$
186	183 185	eqbrtrd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \frac{Y}{2 π} < (\frac{y}{2 π}) + (\frac{1}{2})$
187	55 121 184 128	ltadd1dd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{y}{2 π}) + (\frac{1}{2}) < (\frac{B}{2 π}) + (\frac{1}{2})$
188	129	a1i	$⊢ φ \to \frac{B}{2 π} = \frac{Y + π}{2 π}$
189	188	oveq1d	$⊢ φ \to (\frac{B}{2 π}) + (\frac{1}{2}) = (\frac{Y + π}{2 π}) + (\frac{1}{2})$
190	180	oveq2d	$⊢ φ \to (\frac{Y}{2 π}) + (\frac{π}{2 π}) = (\frac{Y}{2 π}) + (\frac{1}{2})$
191	131 190	eqtrd	$⊢ φ \to \frac{Y + π}{2 π} = (\frac{Y}{2 π}) + (\frac{1}{2})$
192	191	oveq1d	$⊢ φ \to (\frac{Y + π}{2 π}) + (\frac{1}{2}) = (\frac{Y}{2 π}) + (\frac{1}{2}) + (\frac{1}{2})$
193	176	halfcld	$⊢ φ \to \frac{1}{2} \in ℂ$
194	95 193 193	addassd	$⊢ φ \to (\frac{Y}{2 π}) + (\frac{1}{2}) + (\frac{1}{2}) = (\frac{Y}{2 π}) + (\frac{1}{2}) + (\frac{1}{2})$
195	176	2halvesd	$⊢ φ \to (\frac{1}{2}) + (\frac{1}{2}) = 1$
196	195	oveq2d	$⊢ φ \to (\frac{Y}{2 π}) + (\frac{1}{2}) + (\frac{1}{2}) = (\frac{Y}{2 π}) + 1$
197	194 196	eqtrd	$⊢ φ \to (\frac{Y}{2 π}) + (\frac{1}{2}) + (\frac{1}{2}) = (\frac{Y}{2 π}) + 1$
198	189 192 197	3eqtrd	$⊢ φ \to (\frac{B}{2 π}) + (\frac{1}{2}) = (\frac{Y}{2 π}) + 1$
199	198	adantr	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{B}{2 π}) + (\frac{1}{2}) = (\frac{Y}{2 π}) + 1$
200	187 199	breqtrd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\frac{y}{2 π}) + (\frac{1}{2}) < (\frac{Y}{2 π}) + 1$
201		btwnnz	$⊢ (\frac{Y}{2 π} \in ℤ \land \frac{Y}{2 π} < (\frac{y}{2 π}) + (\frac{1}{2}) \land (\frac{y}{2 π}) + (\frac{1}{2}) < (\frac{Y}{2 π}) + 1) \to \neg (\frac{y}{2 π}) + (\frac{1}{2}) \in ℤ$
202	163 186 200 201	syl3anc	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \neg (\frac{y}{2 π}) + (\frac{1}{2}) \in ℤ$
203	162 202	eqneltrd	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \neg (\frac{\frac{y}{2}}{π}) + (\frac{1}{2}) \in ℤ$
204		coseq0	$⊢ \frac{y}{2} \in ℂ \to (\cos (\frac{y}{2}) = 0 \leftrightarrow (\frac{\frac{y}{2}}{π}) + (\frac{1}{2}) \in ℤ)$
205	157 204	syl	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\cos (\frac{y}{2}) = 0 \leftrightarrow (\frac{\frac{y}{2}}{π}) + (\frac{1}{2}) \in ℤ)$
206	203 205	mtbird	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \neg \cos (\frac{y}{2}) = 0$
207	206	neqned	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \cos (\frac{y}{2}) \neq 0$
208	161 207	jca	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0)$
209	208	ralrimiva	$⊢ φ \to \forall y \in ((A, B) ∖ \{Y\}) (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0)$
210	22 209	jca	$⊢ φ \to (Y \in (A, B) \land \forall y \in ((A, B) ∖ \{Y\}) (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0))$

Metamath Proof Explorer

Theorem dirkercncflem1

Proof