Theorem dirkercncflem1 46088

Description: If 𝑌 is a multiple of π then it belongs to an open inerval (𝐴(,)𝐵) such that for any other point 𝑦 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.)

Hypotheses

Ref	Expression
dirkercncflem1.a	⊢ 𝐴 = (𝑌 − π)
dirkercncflem1.b	⊢ 𝐵 = (𝑌 + π)
dirkercncflem1.y	⊢ (𝜑 → 𝑌 ∈ ℝ)
dirkercncflem1.ymod0	⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)

Assertion

Ref	Expression
dirkercncflem1	⊢ (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)))

Distinct variable groups:   𝑦,𝑌   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑦)

Proof of Theorem dirkercncflem1

Step	Hyp	Ref	Expression
1		dirkercncflem1.a	. . . 4 ⊢ 𝐴 = (𝑌 − π)
2		dirkercncflem1.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
3		pire 26382	. . . . . . 7 ⊢ π ∈ ℝ
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → π ∈ ℝ)
5	2, 4	resubcld 11566	. . . . 5 ⊢ (𝜑 → (𝑌 − π) ∈ ℝ)
6	5	rexrd 11184	. . . 4 ⊢ (𝜑 → (𝑌 − π) ∈ ℝ*)
7	1, 6	eqeltrid 2832	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
8		dirkercncflem1.b	. . . 4 ⊢ 𝐵 = (𝑌 + π)
9	2, 4	readdcld 11163	. . . . 5 ⊢ (𝜑 → (𝑌 + π) ∈ ℝ)
10	9	rexrd 11184	. . . 4 ⊢ (𝜑 → (𝑌 + π) ∈ ℝ*)
11	8, 10	eqeltrid 2832	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
12		pipos 26384	. . . . . 6 ⊢ 0 < π
13		ltsubpos 11630	. . . . . 6 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (0 < π ↔ (𝑌 − π) < 𝑌))
14	12, 13	mpbii 233	. . . . 5 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌 − π) < 𝑌)
15	4, 2, 14	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑌 − π) < 𝑌)
16	1, 15	eqbrtrid 5130	. . 3 ⊢ (𝜑 → 𝐴 < 𝑌)
17		ltaddpos 11628	. . . . . 6 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (0 < π ↔ 𝑌 < (𝑌 + π)))
18	12, 17	mpbii 233	. . . . 5 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 < (𝑌 + π))
19	4, 2, 18	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝑌 < (𝑌 + π))
20	19, 8	breqtrrdi 5137	. . 3 ⊢ (𝜑 → 𝑌 < 𝐵)
21	7, 11, 2, 16, 20	eliood 45483	. 2 ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))
22		eldifi 4084	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
23	22	elioored 45534	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℝ)
24	23	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
25	24	recnd 11162	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
26		2cnd 12224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
27		picn 26383	. . . . . . . . 9 ⊢ π ∈ ℂ
28	27	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
29		2ne0 12250	. . . . . . . . 9 ⊢ 2 ≠ 0
30	29	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
31	3, 12	gt0ne0ii 11674	. . . . . . . . 9 ⊢ π ≠ 0
32	31	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
33	25, 26, 28, 30, 32	divdiv1d 11949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem1.ymod0	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)
35		2rp 12916	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
36	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ+)
37		pirp 26386	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ+
38	37	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → π ∈ ℝ+)
39	36, 38	rpmulcld 12971	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ+)
40		mod0 13798	. . . . . . . . . . . . 13 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
41	2, 39, 40	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
42	34, 41	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
43		peano2zm 12536	. . . . . . . . . . 11 ⊢ ((𝑌 / (2 · π)) ∈ ℤ → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
44	42, 43	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
45	44	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
46	44	zred 12598	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈ ℝ)
47	46	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) ∈ ℝ)
48	1, 5	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ)
49	48, 39	rerpdivcld 12986	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 / (2 · π)) ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) ∈ ℝ)
51	39	rpred 12955	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ)
52	51	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
53	39	rpne0d 12960	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ≠ 0)
54	53	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ≠ 0)
55	24, 52, 54	redivcld 11970	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) ∈ ℝ)
56	51	recnd 11162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · π) ∈ ℂ)
57	56, 53	dividd 11916	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · π) / (2 · π)) = 1)
58	57	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 = ((2 · π) / (2 · π)))
59	58	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 / (2 · π)) − ((2 · π) / (2 · π))))
60	2	recnd 11162	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ ℂ)
61	60, 56, 56, 53	divsubdird 11957	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 · π)) = ((𝑌 / (2 · π)) − ((2 · π) / (2 · π))))
62	59, 61	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 − (2 · π)) / (2 · π)))
63	2, 51	resubcld 11566	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 − (2 · π)) ∈ ℝ)
64	27	mullidi 11139	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 · π) = π
65	64	eqcomi 2738	. . . . . . . . . . . . . . . . . 18 ⊢ π = (1 · π)
66		1lt2 12312	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
67		1re 11134	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ
68		2re 12220	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
69	67, 68, 3, 12	ltmul1ii 12071	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 < 2 ↔ (1 · π) < (2 · π))
70	66, 69	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ (1 · π) < (2 · π)
71	65, 70	eqbrtri 5116	. . . . . . . . . . . . . . . . 17 ⊢ π < (2 · π)
72	71	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π < (2 · π))
73	4, 51, 2, 72	ltsub2dd 11751	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 − (2 · π)) < (𝑌 − π))
74	73, 1	breqtrrdi 5137	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 − (2 · π)) < 𝐴)
75	63, 48, 39, 74	ltdiv1dd 13012	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 · π)) < (𝐴 / (2 · π)))
76	62, 75	eqbrtrd 5117	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 · π)))
77	76	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝐴 / (2 · π)))
78	48	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈ ℝ)
79	39	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ+)
80	22	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ (𝐴(,)𝐵))
81	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 ∈ ℝ*)
82	11	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ*)
83		elioo2 13307	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵)))
84	81, 82, 83	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ (𝐴(,)𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵)))
85	80, 84	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ℝ ∧ 𝐴 < 𝑦 ∧ 𝑦 < 𝐵))
86	85	simp2d 1143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐴 < 𝑦)
87	78, 24, 79, 86	ltdiv1dd 13012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) < (𝑦 / (2 · π)))
88	47, 50, 55, 77, 87	lttrd 11295	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)))
89	88	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)))
90	23	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 ∈ ℝ)
91	2	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑌 ∈ ℝ)
92	39	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (2 · π) ∈ ℝ+)
93		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → 𝑦 < 𝑌)
94	90, 91, 92, 93	ltdiv1dd 13012	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (𝑌 / (2 · π)))
95	60, 56, 53	divcld 11918	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
96	95	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℂ)
97		1cnd 11129	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
98	96, 97	npcand 11497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑌 / (2 · π)) − 1) + 1) = (𝑌 / (2 · π)))
99	98	eqcomd 2735	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) + 1))
100	99	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) + 1))
101	94, 100	breqtrd 5121	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1) + 1))
102		btwnnz 12570	. . . . . . . . 9 ⊢ ((((𝑌 / (2 · π)) − 1) ∈ ℤ ∧ ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
103	45, 89, 101, 102	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
104	42	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) ∈ ℤ)
105	2	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 ∈ ℝ)
106	24	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑦 ∈ ℝ)
107	79	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (2 · π) ∈ ℝ+)
108	24	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 ∈ ℝ)
109	2	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ∈ ℝ)
110		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 ≤ 𝑌)
111		eldifsni 4744	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ≠ 𝑌)
112	111	necomd 2980	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑌 ≠ 𝑦)
113	112	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ≠ 𝑦)
114	108, 109, 110, 113	leneltd 11288	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 < 𝑌)
115	114	stoic1a 1772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ 𝑦 ≤ 𝑌)
116	105, 106	ltnled 11281	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑌))
117	115, 116	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 < 𝑦)
118	105, 106, 107, 117	ltdiv1dd 13012	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) < (𝑦 / (2 · π)))
119	8, 9	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ)
120	119, 39	rerpdivcld 12986	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / (2 · π)) ∈ ℝ)
121	120	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) ∈ ℝ)
122	2, 39	rerpdivcld 12986	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
123	122	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℝ)
124		1red 11135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℝ)
125	123, 124	readdcld 11163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) + 1) ∈ ℝ)
126	119	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ)
127	85	simp3d 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 < 𝐵)
128	24, 126, 79, 127	ltdiv1dd 13012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < (𝐵 / (2 · π)))
129	8	oveq1i 7363	. . . . . . . . . . . . 13 ⊢ (𝐵 / (2 · π)) = ((𝑌 + π) / (2 · π))
130	27	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
131	60, 130, 56, 53	divdird 11956	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (π / (2 · π))))
132	4, 39	rerpdivcld 12986	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π / (2 · π)) ∈ ℝ)
133		1red 11135	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
134		2cn 12221	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
135	134, 27	mulcomi 11142	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · π) = (π · 2)
136	135	oveq2i 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (π / (2 · π)) = (π / (π · 2))
137	27, 31	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (π ∈ ℂ ∧ π ≠ 0)
138		2cnne0 12351	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
139		divdiv1 11853	. . . . . . . . . . . . . . . . . . 19 ⊢ ((π ∈ ℂ ∧ (π ∈ ℂ ∧ π ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((π / π) / 2) = (π / (π · 2)))
140	27, 137, 138, 139	mp3an 1463	. . . . . . . . . . . . . . . . . 18 ⊢ ((π / π) / 2) = (π / (π · 2))
141	27, 31	dividi 11875	. . . . . . . . . . . . . . . . . . 19 ⊢ (π / π) = 1
142	141	oveq1i 7363	. . . . . . . . . . . . . . . . . 18 ⊢ ((π / π) / 2) = (1 / 2)
143	136, 140, 142	3eqtr2i 2758	. . . . . . . . . . . . . . . . 17 ⊢ (π / (2 · π)) = (1 / 2)
144		halflt1 12359	. . . . . . . . . . . . . . . . 17 ⊢ (1 / 2) < 1
145	143, 144	eqbrtri 5116	. . . . . . . . . . . . . . . 16 ⊢ (π / (2 · π)) < 1
146	145	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π / (2 · π)) < 1)
147	132, 133, 122, 146	ltadd2dd 11293	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 · π))) < ((𝑌 / (2 · π)) + 1))
148	131, 147	eqbrtrd 5117	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 + π) / (2 · π)) < ((𝑌 / (2 · π)) + 1))
149	129, 148	eqbrtrid 5130	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
150	149	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
151	55, 121, 125, 128, 150	lttrd 11295	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
152	151	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
153		btwnnz 12570	. . . . . . . . 9 ⊢ (((𝑌 / (2 · π)) ∈ ℤ ∧ (𝑌 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
154	104, 118, 152, 153	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
155	103, 154	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
156	33, 155	eqneltrd 2848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
157	25	halfcld 12387	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
158		sineq0 26449	. . . . . . 7 ⊢ ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
159	157, 158	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
160	156, 159	mtbird 325	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
161	160	neqned 2932	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
162	33	oveq1d 7368	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑦 / 2) / π) + (1 / 2)) = ((𝑦 / (2 · π)) + (1 / 2)))
163	42	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℤ)
164	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = (𝑌 − π))
165	164	oveq1d 7368	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + π) = ((𝑌 − π) + π))
166	60, 130	npcand 11497	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 − π) + π) = 𝑌)
167	165, 166	eqtr2d 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 = (𝐴 + π))
168	167	oveq1d 7368	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 + π) / (2 · π)))
169	48	recnd 11162	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
170	169, 130, 56, 53	divdird 11956	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 + π) / (2 · π)) = ((𝐴 / (2 · π)) + (π / (2 · π))))
171	130	mulridd 11151	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π · 1) = π)
172	171	eqcomd 2735	. . . . . . . . . . . . . 14 ⊢ (𝜑 → π = (π · 1))
173		2cnd 12224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
174	173, 130	mulcomd 11155	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · π) = (π · 2))
175	172, 174	oveq12d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (π / (2 · π)) = ((π · 1) / (π · 2)))
176		1cnd 11129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
177	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
178	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → π ≠ 0)
179	176, 173, 130, 177, 178	divcan5d 11944	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((π · 1) / (π · 2)) = (1 / 2))
180	175, 179	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝜑 → (π / (2 · π)) = (1 / 2))
181	180	oveq2d 7369	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / (2 · π)) + (π / (2 · π))) = ((𝐴 / (2 · π)) + (1 / 2)))
182	168, 170, 181	3eqtrd 2768	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 / 2)))
183	182	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 / 2)))
184	124	rehalfcld 12389	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
185	50, 55, 184, 87	ltadd1dd 11749	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐴 / (2 · π)) + (1 / 2)) < ((𝑦 / (2 · π)) + (1 / 2)))
186	183, 185	eqbrtrd 5117	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 / 2)))
187	55, 121, 184, 128	ltadd1dd 11749	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝐵 / (2 · π)) + (1 / 2)))
188	129	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / (2 · π)) = ((𝑌 + π) / (2 · π)))
189	188	oveq1d 7368	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = (((𝑌 + π) / (2 · π)) + (1 / 2)))
190	180	oveq2d 7369	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 · π))) = ((𝑌 / (2 · π)) + (1 / 2)))
191	131, 190	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (1 / 2)))
192	191	oveq1d 7368	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑌 + π) / (2 · π)) + (1 / 2)) = (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)))
193	176	halfcld 12387	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
194	95, 193, 193	addassd 11156	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)) = ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2))))
195	176	2halvesd 12388	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1 / 2) + (1 / 2)) = 1)
196	195	oveq2d 7369	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2))) = ((𝑌 / (2 · π)) + 1))
197	194, 196	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
198	189, 192, 197	3eqtrd 2768	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
199	198	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
200	187, 199	breqtrd 5121	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1))
201		btwnnz 12570	. . . . . . . 8 ⊢ (((𝑌 / (2 · π)) ∈ ℤ ∧ (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 / 2)) ∧ ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1)) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈ ℤ)
202	163, 186, 200, 201	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈ ℤ)
203	162, 202	eqneltrd 2848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ)
204		coseq0 45849	. . . . . . 7 ⊢ ((𝑦 / 2) ∈ ℂ → ((cos‘(𝑦 / 2)) = 0 ↔ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ))
205	157, 204	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((cos‘(𝑦 / 2)) = 0 ↔ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ))
206	203, 205	mtbird 325	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (cos‘(𝑦 / 2)) = 0)
207	206	neqned 2932	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
208	161, 207	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0))
209	208	ralrimiva 3121	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0))
210	21, 209	jca 511	1 ⊢ (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044   ∖ cdif 3902  {csn 4579   class class class wbr 5095  ‘cfv 6486  (class class class)co 7353  ℂcc 11026  ℝcr 11027  0cc0 11028  1c1 11029   + caddc 11031   · cmul 11033  ℝ^*cxr 11167   < clt 11168   ≤ cle 11169   − cmin 11365   / cdiv 11795  2c2 12201  ℤcz 12489  ℝ⁺crp 12911  (,)cioo 13266   mod cmo 13791  sincsin 15988  cosccos 15989  πcpi 15991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-inf2 9556  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106  ax-addf 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8632  df-map 8762  df-pm 8763  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-fi 9320  df-sup 9351  df-inf 9352  df-oi 9421  df-card 9854  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-div 11796  df-nn 12147  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214  df-8 12215  df-9 12216  df-n0 12403  df-z 12490  df-dec 12610  df-uz 12754  df-q 12868  df-rp 12912  df-xneg 13032  df-xadd 13033  df-xmul 13034  df-ioo 13270  df-ioc 13271  df-ico 13272  df-icc 13273  df-fz 13429  df-fzo 13576  df-fl 13714  df-mod 13792  df-seq 13927  df-exp 13987  df-fac 14199  df-bc 14228  df-hash 14256  df-shft 14992  df-cj 15024  df-re 15025  df-im 15026  df-sqrt 15160  df-abs 15161  df-limsup 15396  df-clim 15413  df-rlim 15414  df-sum 15612  df-ef 15992  df-sin 15994  df-cos 15995  df-pi 15997  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-ress 17160  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-hom 17203  df-cco 17204  df-rest 17344  df-topn 17345  df-0g 17363  df-gsum 17364  df-topgen 17365  df-pt 17366  df-prds 17369  df-xrs 17424  df-qtop 17429  df-imas 17430  df-xps 17432  df-mre 17506  df-mrc 17507  df-acs 17509  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-submnd 18676  df-mulg 18965  df-cntz 19214  df-cmn 19679  df-psmet 21271  df-xmet 21272  df-met 21273  df-bl 21274  df-mopn 21275  df-fbas 21276  df-fg 21277  df-cnfld 21280  df-top 22797  df-topon 22814  df-topsp 22836  df-bases 22849  df-cld 22922  df-ntr 22923  df-cls 22924  df-nei 23001  df-lp 23039  df-perf 23040  df-cn 23130  df-cnp 23131  df-haus 23218  df-tx 23465  df-hmeo 23658  df-fil 23749  df-fm 23841  df-flim 23842  df-flf 23843  df-xms 24224  df-ms 24225  df-tms 24226  df-cncf 24787  df-limc 25783  df-dv 25784

This theorem is referenced by:  dirkercncflem3  46090