Theorem pilem3OLD 24656

Description: Obsolete proof of pilem3 24655 as of 30-Jun-2022. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
pilem3OLD	⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)

Proof of Theorem pilem3OLD

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 11454	. . . . 5 ⊢ 2 ∈ ℝ
2	1	a1i 11	. . . 4 ⊢ (⊤ → 2 ∈ ℝ)
3		4re 11465	. . . . 5 ⊢ 4 ∈ ℝ
4	3	a1i 11	. . . 4 ⊢ (⊤ → 4 ∈ ℝ)
5		0re 10380	. . . . 5 ⊢ 0 ∈ ℝ
6	5	a1i 11	. . . 4 ⊢ (⊤ → 0 ∈ ℝ)
7		2lt4 11562	. . . . 5 ⊢ 2 < 4
8	7	a1i 11	. . . 4 ⊢ (⊤ → 2 < 4)
9		iccssre 12572	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ 4 ∈ ℝ) → (2[,]4) ⊆ ℝ)
10	1, 3, 9	mp2an 682	. . . . . 6 ⊢ (2[,]4) ⊆ ℝ
11		ax-resscn 10331	. . . . . 6 ⊢ ℝ ⊆ ℂ
12	10, 11	sstri 3830	. . . . 5 ⊢ (2[,]4) ⊆ ℂ
13	12	a1i 11	. . . 4 ⊢ (⊤ → (2[,]4) ⊆ ℂ)
14		sincn 24646	. . . . 5 ⊢ sin ∈ (ℂ–cn→ℂ)
15	14	a1i 11	. . . 4 ⊢ (⊤ → sin ∈ (ℂ–cn→ℂ))
16	10	sseli 3817	. . . . . 6 ⊢ (𝑦 ∈ (2[,]4) → 𝑦 ∈ ℝ)
17	16	resincld 15284	. . . . 5 ⊢ (𝑦 ∈ (2[,]4) → (sin‘𝑦) ∈ ℝ)
18	17	adantl 475	. . . 4 ⊢ ((⊤ ∧ 𝑦 ∈ (2[,]4)) → (sin‘𝑦) ∈ ℝ)
19		sin4lt0 15336	. . . . . 6 ⊢ (sin‘4) < 0
20		sincos2sgn 15335	. . . . . . 7 ⊢ (0 < (sin‘2) ∧ (cos‘2) < 0)
21	20	simpli 478	. . . . . 6 ⊢ 0 < (sin‘2)
22	19, 21	pm3.2i 464	. . . . 5 ⊢ ((sin‘4) < 0 ∧ 0 < (sin‘2))
23	22	a1i 11	. . . 4 ⊢ (⊤ → ((sin‘4) < 0 ∧ 0 < (sin‘2)))
24	2, 4, 6, 8, 13, 15, 18, 23	ivth2 23670	. . 3 ⊢ (⊤ → ∃𝑥 ∈ (2(,)4)(sin‘𝑥) = 0)
25	24	mptru 1609	. 2 ⊢ ∃𝑥 ∈ (2(,)4)(sin‘𝑥) = 0
26		df-pi 15214	. . . . . . 7 ⊢ π = inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < )
27		elioore 12522	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (2(,)4) → 𝑥 ∈ ℝ)
28	27	adantr 474	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 𝑥 ∈ ℝ)
29	5	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 0 ∈ ℝ)
30	1	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 2 ∈ ℝ)
31		2pos 11490	. . . . . . . . . . . 12 ⊢ 0 < 2
32	31	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 0 < 2)
33		eliooord 12550	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (2(,)4) → (2 < 𝑥 ∧ 𝑥 < 4))
34	33	simpld 490	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (2(,)4) → 2 < 𝑥)
35	34	adantr 474	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 2 < 𝑥)
36	29, 30, 28, 32, 35	lttrd 10539	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 0 < 𝑥)
37	28, 36	elrpd 12183	. . . . . . . . 9 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 𝑥 ∈ ℝ+)
38		simpr 479	. . . . . . . . 9 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (sin‘𝑥) = 0)
39		pilem1 24653	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝑥 ∈ ℝ+ ∧ (sin‘𝑥) = 0))
40	37, 38, 39	sylanbrc 578	. . . . . . . 8 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 𝑥 ∈ (ℝ+ ∩ (◡sin “ {0})))
41		inss1 4053	. . . . . . . . . 10 ⊢ (ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ+
42		rpssre 12149	. . . . . . . . . 10 ⊢ ℝ+ ⊆ ℝ
43	41, 42	sstri 3830	. . . . . . . . 9 ⊢ (ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ
44	41	sseli 3817	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (ℝ+ ∩ (◡sin “ {0})) → 𝑧 ∈ ℝ+)
45	44	rpge0d 12190	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (ℝ+ ∩ (◡sin “ {0})) → 0 ≤ 𝑧)
46	45	rgen 3104	. . . . . . . . . 10 ⊢ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))0 ≤ 𝑧
47		breq1 4891	. . . . . . . . . . . 12 ⊢ (𝑦 = 0 → (𝑦 ≤ 𝑧 ↔ 0 ≤ 𝑧))
48	47	ralbidv 3168	. . . . . . . . . . 11 ⊢ (𝑦 = 0 → (∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧 ↔ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))0 ≤ 𝑧))
49	48	rspcev 3511	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))0 ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧)
50	5, 46, 49	mp2an 682	. . . . . . . . 9 ⊢ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧
51		infrelb 11367	. . . . . . . . 9 ⊢ (((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧 ∧ 𝑥 ∈ (ℝ+ ∩ (◡sin “ {0}))) → inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ≤ 𝑥)
52	43, 50, 51	mp3an12 1524	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡sin “ {0})) → inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ≤ 𝑥)
53	40, 52	syl 17	. . . . . . 7 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ≤ 𝑥)
54	26, 53	syl5eqbr 4923	. . . . . 6 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → π ≤ 𝑥)
55		simplll 765	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → 𝑥 ∈ (2(,)4))
56		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0})))
57		pilem1 24653	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝑦 ∈ ℝ+ ∧ (sin‘𝑦) = 0))
58	56, 57	sylib 210	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → (𝑦 ∈ ℝ+ ∧ (sin‘𝑦) = 0))
59	58	simpld 490	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → 𝑦 ∈ ℝ+)
60		simpllr 766	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → (sin‘𝑥) = 0)
61	58	simprd 491	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → (sin‘𝑦) = 0)
62	55, 59, 60, 61	pilem2 24654	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) ∧ 𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))) → ((π + 𝑥) / 2) ≤ 𝑦)
63	62	ralrimiva 3148	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))((π + 𝑥) / 2) ≤ 𝑦)
64	43	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → (ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ)
65		ne0i 4149	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡sin “ {0})) → (ℝ+ ∩ (◡sin “ {0})) ≠ ∅)
66	40, 65	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (ℝ+ ∩ (◡sin “ {0})) ≠ ∅)
67	66	adantr 474	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → (ℝ+ ∩ (◡sin “ {0})) ≠ ∅)
68	50	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧)
69		infrecl 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧ (ℝ+ ∩ (◡sin “ {0})) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧) → inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ∈ ℝ)
70	43, 50, 69	mp3an13 1525	. . . . . . . . . . . . . . . . 17 ⊢ ((ℝ+ ∩ (◡sin “ {0})) ≠ ∅ → inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ∈ ℝ)
71	66, 70	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ∈ ℝ)
72	26, 71	syl5eqel 2863	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → π ∈ ℝ)
73	72, 28	readdcld 10408	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (π + 𝑥) ∈ ℝ)
74	73	adantr 474	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → (π + 𝑥) ∈ ℝ)
75	74	rehalfcld 11634	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → ((π + 𝑥) / 2) ∈ ℝ)
76		infregelb 11366	. . . . . . . . . . . 12 ⊢ ((((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧ (ℝ+ ∩ (◡sin “ {0})) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑦 ≤ 𝑧) ∧ ((π + 𝑥) / 2) ∈ ℝ) → (((π + 𝑥) / 2) ≤ inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ↔ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))((π + 𝑥) / 2) ≤ 𝑦))
77	64, 67, 68, 75, 76	syl31anc 1441	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → (((π + 𝑥) / 2) ≤ inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ) ↔ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))((π + 𝑥) / 2) ≤ 𝑦))
78	63, 77	mpbird 249	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → ((π + 𝑥) / 2) ≤ inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < ))
79	78, 26	syl6breqr 4930	. . . . . . . . 9 ⊢ (((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) ∧ π < 𝑥) → ((π + 𝑥) / 2) ≤ π)
80	79	ex 403	. . . . . . . 8 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (π < 𝑥 → ((π + 𝑥) / 2) ≤ π))
81	72, 28	ltnled 10525	. . . . . . . 8 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (π < 𝑥 ↔ ¬ 𝑥 ≤ π))
82	72	recnd 10407	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → π ∈ ℂ)
83	28	recnd 10407	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 𝑥 ∈ ℂ)
84	82, 83	addcomd 10580	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (π + 𝑥) = (𝑥 + π))
85	84	oveq1d 6939	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → ((π + 𝑥) / 2) = ((𝑥 + π) / 2))
86	85	breq1d 4898	. . . . . . . . 9 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (((π + 𝑥) / 2) ≤ π ↔ ((𝑥 + π) / 2) ≤ π))
87		avgle2 11628	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ π ∈ ℝ) → (𝑥 ≤ π ↔ ((𝑥 + π) / 2) ≤ π))
88	28, 72, 87	syl2anc 579	. . . . . . . . 9 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (𝑥 ≤ π ↔ ((𝑥 + π) / 2) ≤ π))
89	86, 88	bitr4d 274	. . . . . . . 8 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (((π + 𝑥) / 2) ≤ π ↔ 𝑥 ≤ π))
90	80, 81, 89	3imtr3d 285	. . . . . . 7 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (¬ 𝑥 ≤ π → 𝑥 ≤ π))
91	90	pm2.18d 127	. . . . . 6 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 𝑥 ≤ π)
92	72, 28	letri3d 10520	. . . . . 6 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (π = 𝑥 ↔ (π ≤ 𝑥 ∧ 𝑥 ≤ π)))
93	54, 91, 92	mpbir2and 703	. . . . 5 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → π = 𝑥)
94		simpl 476	. . . . 5 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → 𝑥 ∈ (2(,)4))
95	93, 94	eqeltrd 2859	. . . 4 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → π ∈ (2(,)4))
96	93	fveq2d 6452	. . . . 5 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (sin‘π) = (sin‘𝑥))
97	96, 38	eqtrd 2814	. . . 4 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (sin‘π) = 0)
98	95, 97	jca 507	. . 3 ⊢ ((𝑥 ∈ (2(,)4) ∧ (sin‘𝑥) = 0) → (π ∈ (2(,)4) ∧ (sin‘π) = 0))
99	98	rexlimiva 3210	. 2 ⊢ (∃𝑥 ∈ (2(,)4)(sin‘𝑥) = 0 → (π ∈ (2(,)4) ∧ (sin‘π) = 0))
100	25, 99	ax-mp 5	1 ⊢ (π ∈ (2(,)4) ∧ (sin‘π) = 0)

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386   = wceq 1601  ⊤wtru 1602   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  {csn 4398   class class class wbr 4888  ^◡ccnv 5356   “ cima 5360  ‘cfv 6137  (class class class)co 6924  infcinf 8637  ℂcc 10272  ℝcr 10273  0cc0 10274   + caddc 10277   < clt 10413   ≤ cle 10414   / cdiv 11035  2c2 11435  4c4 11437  ℝ⁺crp 12142  (,)cioo 12492  [,]cicc 12495  sincsin 15205  cosccos 15206  πcpi 15208  –cn→ccncf 23098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11036  df-nn 11380  df-2 11443  df-3 11444  df-4 11445  df-5 11446  df-6 11447  df-7 11448  df-8 11449  df-9 11450  df-n0 11648  df-z 11734  df-dec 11851  df-uz 11998  df-q 12101  df-rp 12143  df-xneg 12262  df-xadd 12263  df-xmul 12264  df-ioo 12496  df-ioc 12497  df-ico 12498  df-icc 12499  df-fz 12649  df-fzo 12790  df-fl 12917  df-seq 13125  df-exp 13184  df-fac 13385  df-bc 13414  df-hash 13442  df-shft 14220  df-cj 14252  df-re 14253  df-im 14254  df-sqrt 14388  df-abs 14389  df-limsup 14619  df-clim 14636  df-rlim 14637  df-sum 14834  df-ef 15209  df-sin 15211  df-cos 15212  df-pi 15214  df-struct 16268  df-ndx 16269  df-slot 16270  df-base 16272  df-sets 16273  df-ress 16274  df-plusg 16362  df-mulr 16363  df-starv 16364  df-sca 16365  df-vsca 16366  df-ip 16367  df-tset 16368  df-ple 16369  df-ds 16371  df-unif 16372  df-hom 16373  df-cco 16374  df-rest 16480  df-topn 16481  df-0g 16499  df-gsum 16500  df-topgen 16501  df-pt 16502  df-prds 16505  df-xrs 16559  df-qtop 16564  df-imas 16565  df-xps 16567  df-mre 16643  df-mrc 16644  df-acs 16646  df-mgm 17639  df-sgrp 17681  df-mnd 17692  df-submnd 17733  df-mulg 17939  df-cntz 18144  df-cmn 18592  df-psmet 20145  df-xmet 20146  df-met 20147  df-bl 20148  df-mopn 20149  df-fbas 20150  df-fg 20151  df-cnfld 20154  df-top 21117  df-topon 21134  df-topsp 21156  df-bases 21169  df-cld 21242  df-ntr 21243  df-cls 21244  df-nei 21321  df-lp 21359  df-perf 21360  df-cn 21450  df-cnp 21451  df-haus 21538  df-tx 21785  df-hmeo 21978  df-fil 22069  df-fm 22161  df-flim 22162  df-flf 22163  df-xms 22544  df-ms 22545  df-tms 22546  df-cncf 23100  df-limc 24078  df-dv 24079

This theorem is referenced by: (None)