Theorem dirkercncflem1 46075

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 26436	. . . . . . 7 ⊢ π ∈ ℝ
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → π ∈ ℝ)
5	2, 4	resubcld 11673	. . . . 5 ⊢ (𝜑 → (𝑌 − π) ∈ ℝ)
6	5	rexrd 11293	. . . 4 ⊢ (𝜑 → (𝑌 − π) ∈ ℝ*)
7	1, 6	eqeltrid 2837	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
8		dirkercncflem1.b	. . . 4 ⊢ 𝐵 = (𝑌 + π)
9	2, 4	readdcld 11272	. . . . 5 ⊢ (𝜑 → (𝑌 + π) ∈ ℝ)
10	9	rexrd 11293	. . . 4 ⊢ (𝜑 → (𝑌 + π) ∈ ℝ*)
11	8, 10	eqeltrid 2837	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
12		pipos 26438	. . . . . 6 ⊢ 0 < π
13		ltsubpos 11737	. . . . . 6 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (0 < π ↔ (𝑌 − π) < 𝑌))
14	12, 13	mpbii 233	. . . . 5 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌 − π) < 𝑌)
15	4, 2, 14	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑌 − π) < 𝑌)
16	1, 15	eqbrtrid 5158	. . 3 ⊢ (𝜑 → 𝐴 < 𝑌)
17		ltaddpos 11735	. . . . . 6 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → (0 < π ↔ 𝑌 < (𝑌 + π)))
18	12, 17	mpbii 233	. . . . 5 ⊢ ((π ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 < (𝑌 + π))
19	4, 2, 18	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝑌 < (𝑌 + π))
20	19, 8	breqtrrdi 5165	. . 3 ⊢ (𝜑 → 𝑌 < 𝐵)
21	7, 11, 2, 16, 20	eliood 45468	. 2 ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))
22		eldifi 4111	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
23	22	elioored 45519	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℝ)
24	23	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
25	24	recnd 11271	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
26		2cnd 12326	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
27		picn 26437	. . . . . . . . 9 ⊢ π ∈ ℂ
28	27	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
29		2ne0 12352	. . . . . . . . 9 ⊢ 2 ≠ 0
30	29	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
31	3, 12	gt0ne0ii 11781	. . . . . . . . 9 ⊢ π ≠ 0
32	31	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
33	25, 26, 28, 30, 32	divdiv1d 12056	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem1.ymod0	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)
35		2rp 13021	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
36	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ+)
37		pirp 26439	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ+
38	37	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → π ∈ ℝ+)
39	36, 38	rpmulcld 13075	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ+)
40		mod0 13898	. . . . . . . . . . . . 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 12643	. . . . . . . . . . 11 ⊢ ((𝑌 / (2 · π)) ∈ ℤ → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
44	42, 43	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
45	44	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → ((𝑌 / (2 · π)) − 1) ∈ ℤ)
46	44	zred 12705	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) ∈ ℝ)
47	46	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) − 1) ∈ ℝ)
48	1, 5	eqeltrid 2837	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ)
49	48, 39	rerpdivcld 13090	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 / (2 · π)) ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) ∈ ℝ)
51	39	rpred 13059	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ)
52	51	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
53	39	rpne0d 13064	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ≠ 0)
54	53	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ≠ 0)
55	24, 52, 54	redivcld 12077	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) ∈ ℝ)
56	51	recnd 11271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · π) ∈ ℂ)
57	56, 53	dividd 12023	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · π) / (2 · π)) = 1)
58	57	eqcomd 2740	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 = ((2 · π) / (2 · π)))
59	58	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 / (2 · π)) − ((2 · π) / (2 · π))))
60	2	recnd 11271	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ ℂ)
61	60, 56, 56, 53	divsubdird 12064	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 · π)) = ((𝑌 / (2 · π)) − ((2 · π) / (2 · π))))
62	59, 61	eqtr4d 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 / (2 · π)) − 1) = ((𝑌 − (2 · π)) / (2 · π)))
63	2, 51	resubcld 11673	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 − (2 · π)) ∈ ℝ)
64	27	mullidi 11248	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 · π) = π
65	64	eqcomi 2743	. . . . . . . . . . . . . . . . . 18 ⊢ π = (1 · π)
66		1lt2 12419	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
67		1re 11243	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ
68		2re 12322	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
69	67, 68, 3, 12	ltmul1ii 12178	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 < 2 ↔ (1 · π) < (2 · π))
70	66, 69	mpbi 230	. . . . . . . . . . . . . . . . . 18 ⊢ (1 · π) < (2 · π)
71	65, 70	eqbrtri 5144	. . . . . . . . . . . . . . . . 17 ⊢ π < (2 · π)
72	71	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π < (2 · π))
73	4, 51, 2, 72	ltsub2dd 11858	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 − (2 · π)) < (𝑌 − π))
74	73, 1	breqtrrdi 5165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 − (2 · π)) < 𝐴)
75	63, 48, 39, 74	ltdiv1dd 13116	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 − (2 · π)) / (2 · π)) < (𝐴 / (2 · π)))
76	62, 75	eqbrtrd 5145	. . . . . . . . . . . 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 13410	. . . . . . . . . . . . . . 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 13116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐴 / (2 · π)) < (𝑦 / (2 · π)))
88	47, 50, 55, 77, 87	lttrd 11404	. . . . . . . . . 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 13116	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (𝑌 / (2 · π)))
95	60, 56, 53	divcld 12025	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
96	95	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℂ)
97		1cnd 11238	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
98	96, 97	npcand 11606	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑌 / (2 · π)) − 1) + 1) = (𝑌 / (2 · π)))
99	98	eqcomd 2740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) + 1))
100	99	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑌 / (2 · π)) = (((𝑌 / (2 · π)) − 1) + 1))
101	94, 100	breqtrd 5149	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1) + 1))
102		btwnnz 12677	. . . . . . . . 9 ⊢ ((((𝑌 / (2 · π)) − 1) ∈ ℤ ∧ ((𝑌 / (2 · π)) − 1) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < (((𝑌 / (2 · π)) − 1) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
103	45, 89, 101, 102	syl3anc 1372	. . . . . . . 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 4770	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ≠ 𝑌)
112	111	necomd 2986	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑌 ≠ 𝑦)
113	112	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑌 ≠ 𝑦)
114	108, 109, 110, 113	leneltd 11397	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 ≤ 𝑌) → 𝑦 < 𝑌)
115	114	stoic1a 1771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ 𝑦 ≤ 𝑌)
116	105, 106	ltnled 11390	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑌))
117	115, 116	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → 𝑌 < 𝑦)
118	105, 106, 107, 117	ltdiv1dd 13116	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑌 / (2 · π)) < (𝑦 / (2 · π)))
119	8, 9	eqeltrid 2837	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ)
120	119, 39	rerpdivcld 13090	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / (2 · π)) ∈ ℝ)
121	120	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) ∈ ℝ)
122	2, 39	rerpdivcld 13090	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
123	122	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℝ)
124		1red 11244	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℝ)
125	123, 124	readdcld 11272	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑌 / (2 · π)) + 1) ∈ ℝ)
126	119	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐵 ∈ ℝ)
127	85	simp3d 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 < 𝐵)
128	24, 126, 79, 127	ltdiv1dd 13116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < (𝐵 / (2 · π)))
129	8	oveq1i 7423	. . . . . . . . . . . . 13 ⊢ (𝐵 / (2 · π)) = ((𝑌 + π) / (2 · π))
130	27	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
131	60, 130, 56, 53	divdird 12063	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (π / (2 · π))))
132	4, 39	rerpdivcld 13090	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π / (2 · π)) ∈ ℝ)
133		1red 11244	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℝ)
134		2cn 12323	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
135	134, 27	mulcomi 11251	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · π) = (π · 2)
136	135	oveq2i 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (π / (2 · π)) = (π / (π · 2))
137	27, 31	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (π ∈ ℂ ∧ π ≠ 0)
138		2cnne0 12458	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
139		divdiv1 11960	. . . . . . . . . . . . . . . . . . 19 ⊢ ((π ∈ ℂ ∧ (π ∈ ℂ ∧ π ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((π / π) / 2) = (π / (π · 2)))
140	27, 137, 138, 139	mp3an 1462	. . . . . . . . . . . . . . . . . 18 ⊢ ((π / π) / 2) = (π / (π · 2))
141	27, 31	dividi 11982	. . . . . . . . . . . . . . . . . . 19 ⊢ (π / π) = 1
142	141	oveq1i 7423	. . . . . . . . . . . . . . . . . 18 ⊢ ((π / π) / 2) = (1 / 2)
143	136, 140, 142	3eqtr2i 2763	. . . . . . . . . . . . . . . . 17 ⊢ (π / (2 · π)) = (1 / 2)
144		halflt1 12466	. . . . . . . . . . . . . . . . 17 ⊢ (1 / 2) < 1
145	143, 144	eqbrtri 5144	. . . . . . . . . . . . . . . 16 ⊢ (π / (2 · π)) < 1
146	145	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π / (2 · π)) < 1)
147	132, 133, 122, 146	ltadd2dd 11402	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 · π))) < ((𝑌 / (2 · π)) + 1))
148	131, 147	eqbrtrd 5145	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 + π) / (2 · π)) < ((𝑌 / (2 · π)) + 1))
149	129, 148	eqbrtrid 5158	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
150	149	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐵 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
151	55, 121, 125, 128, 150	lttrd 11404	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
152	151	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1))
153		btwnnz 12677	. . . . . . . . 9 ⊢ (((𝑌 / (2 · π)) ∈ ℤ ∧ (𝑌 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝑌 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
154	104, 118, 152, 153	syl3anc 1372	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ¬ 𝑦 < 𝑌) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
155	103, 154	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
156	33, 155	eqneltrd 2853	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
157	25	halfcld 12494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
158		sineq0 26502	. . . . . . 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 2938	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
162	33	oveq1d 7428	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑦 / 2) / π) + (1 / 2)) = ((𝑦 / (2 · π)) + (1 / 2)))
163	42	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) ∈ ℤ)
164	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 = (𝑌 − π))
165	164	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + π) = ((𝑌 − π) + π))
166	60, 130	npcand 11606	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 − π) + π) = 𝑌)
167	165, 166	eqtr2d 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 = (𝐴 + π))
168	167	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 + π) / (2 · π)))
169	48	recnd 11271	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
170	169, 130, 56, 53	divdird 12063	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 + π) / (2 · π)) = ((𝐴 / (2 · π)) + (π / (2 · π))))
171	130	mulridd 11260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π · 1) = π)
172	171	eqcomd 2740	. . . . . . . . . . . . . 14 ⊢ (𝜑 → π = (π · 1))
173		2cnd 12326	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
174	173, 130	mulcomd 11264	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · π) = (π · 2))
175	172, 174	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → (π / (2 · π)) = ((π · 1) / (π · 2)))
176		1cnd 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
177	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ≠ 0)
178	31	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → π ≠ 0)
179	176, 173, 130, 177, 178	divcan5d 12051	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((π · 1) / (π · 2)) = (1 / 2))
180	175, 179	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → (π / (2 · π)) = (1 / 2))
181	180	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 / (2 · π)) + (π / (2 · π))) = ((𝐴 / (2 · π)) + (1 / 2)))
182	168, 170, 181	3eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 / 2)))
183	182	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) = ((𝐴 / (2 · π)) + (1 / 2)))
184	124	rehalfcld 12496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
185	50, 55, 184, 87	ltadd1dd 11856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐴 / (2 · π)) + (1 / 2)) < ((𝑦 / (2 · π)) + (1 / 2)))
186	183, 185	eqbrtrd 5145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 / 2)))
187	55, 121, 184, 128	ltadd1dd 11856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝐵 / (2 · π)) + (1 / 2)))
188	129	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / (2 · π)) = ((𝑌 + π) / (2 · π)))
189	188	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = (((𝑌 + π) / (2 · π)) + (1 / 2)))
190	180	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑌 / (2 · π)) + (π / (2 · π))) = ((𝑌 / (2 · π)) + (1 / 2)))
191	131, 190	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 + π) / (2 · π)) = ((𝑌 / (2 · π)) + (1 / 2)))
192	191	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑌 + π) / (2 · π)) + (1 / 2)) = (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)))
193	176	halfcld 12494	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
194	95, 193, 193	addassd 11265	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)) = ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2))))
195	176	2halvesd 12495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1 / 2) + (1 / 2)) = 1)
196	195	oveq2d 7429	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑌 / (2 · π)) + ((1 / 2) + (1 / 2))) = ((𝑌 / (2 · π)) + 1))
197	194, 196	eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑌 / (2 · π)) + (1 / 2)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
198	189, 192, 197	3eqtrd 2773	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
199	198	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐵 / (2 · π)) + (1 / 2)) = ((𝑌 / (2 · π)) + 1))
200	187, 199	breqtrd 5149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1))
201		btwnnz 12677	. . . . . . . 8 ⊢ (((𝑌 / (2 · π)) ∈ ℤ ∧ (𝑌 / (2 · π)) < ((𝑦 / (2 · π)) + (1 / 2)) ∧ ((𝑦 / (2 · π)) + (1 / 2)) < ((𝑌 / (2 · π)) + 1)) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈ ℤ)
202	163, 186, 200, 201	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / (2 · π)) + (1 / 2)) ∈ ℤ)
203	162, 202	eqneltrd 2853	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (((𝑦 / 2) / π) + (1 / 2)) ∈ ℤ)
204		coseq0 45836	. . . . . . 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 2938	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
208	161, 207	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0))
209	208	ralrimiva 3133	. 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 1539   ∈ wcel 2107   ≠ wne 2931  ∀wral 3050   ∖ cdif 3928  {csn 4606   class class class wbr 5123  ‘cfv 6541  (class class class)co 7413  ℂcc 11135  ℝcr 11136  0cc0 11137  1c1 11138   + caddc 11140   · cmul 11142  ℝ^*cxr 11276   < clt 11277   ≤ cle 11278   − cmin 11474   / cdiv 11902  2c2 12303  ℤcz 12596  ℝ⁺crp 13016  (,)cioo 13369   mod cmo 13891  sincsin 16081  cosccos 16082  πcpi 16084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-inf2 9663  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214  ax-pre-sup 11215  ax-addf 11216

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4888  df-int 4927  df-iun 4973  df-iin 4974  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7870  df-1st 7996  df-2nd 7997  df-supp 8168  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8727  df-map 8850  df-pm 8851  df-ixp 8920  df-en 8968  df-dom 8969  df-sdom 8970  df-fin 8971  df-fsupp 9384  df-fi 9433  df-sup 9464  df-inf 9465  df-oi 9532  df-card 9961  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-div 11903  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12510  df-z 12597  df-dec 12717  df-uz 12861  df-q 12973  df-rp 13017  df-xneg 13136  df-xadd 13137  df-xmul 13138  df-ioo 13373  df-ioc 13374  df-ico 13375  df-icc 13376  df-fz 13530  df-fzo 13677  df-fl 13814  df-mod 13892  df-seq 14025  df-exp 14085  df-fac 14295  df-bc 14324  df-hash 14352  df-shft 15088  df-cj 15120  df-re 15121  df-im 15122  df-sqrt 15256  df-abs 15257  df-limsup 15489  df-clim 15506  df-rlim 15507  df-sum 15705  df-ef 16085  df-sin 16087  df-cos 16088  df-pi 16090  df-struct 17166  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17230  df-ress 17253  df-plusg 17286  df-mulr 17287  df-starv 17288  df-sca 17289  df-vsca 17290  df-ip 17291  df-tset 17292  df-ple 17293  df-ds 17295  df-unif 17296  df-hom 17297  df-cco 17298  df-rest 17438  df-topn 17439  df-0g 17457  df-gsum 17458  df-topgen 17459  df-pt 17460  df-prds 17463  df-xrs 17518  df-qtop 17523  df-imas 17524  df-xps 17526  df-mre 17600  df-mrc 17601  df-acs 17603  df-mgm 18622  df-sgrp 18701  df-mnd 18717  df-submnd 18766  df-mulg 19055  df-cntz 19304  df-cmn 19768  df-psmet 21318  df-xmet 21319  df-met 21320  df-bl 21321  df-mopn 21322  df-fbas 21323  df-fg 21324  df-cnfld 21327  df-top 22848  df-topon 22865  df-topsp 22887  df-bases 22900  df-cld 22973  df-ntr 22974  df-cls 22975  df-nei 23052  df-lp 23090  df-perf 23091  df-cn 23181  df-cnp 23182  df-haus 23269  df-tx 23516  df-hmeo 23709  df-fil 23800  df-fm 23892  df-flim 23893  df-flf 23894  df-xms 24275  df-ms 24276  df-tms 24277  df-cncf 24840  df-limc 25837  df-dv 25838

This theorem is referenced by:  dirkercncflem3  46077