Theorem vdwnn 16168

Description: Van der Waerden's theorem, infinitary version. For any finite coloring 𝐹 of the positive integers, there is a color 𝑐 that contains arbitrarily long arithmetic progressions. (Contributed by Mario Carneiro, 13-Sep-2014.)

Assertion

Ref	Expression
vdwnn	⊢ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) → ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))

Distinct variable groups:   𝑎,𝑐,𝑑,𝑘,𝑚,𝐹   𝑅,𝑐

Allowed substitution hints:   𝑅(𝑘,𝑚,𝑎,𝑑)

Proof of Theorem vdwnn

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

Step	Hyp	Ref	Expression
1		simpll 763	. . 3 ⊢ (((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) → 𝑅 ∈ Fin)
2		simplr 765	. . 3 ⊢ (((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) → 𝐹:ℕ⟶𝑅)
3		oveq1 7028	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑤 → (𝑚 · 𝑑) = (𝑤 · 𝑑))
4	3	oveq2d 7037	. . . . . . . . . 10 ⊢ (𝑚 = 𝑤 → (𝑎 + (𝑚 · 𝑑)) = (𝑎 + (𝑤 · 𝑑)))
5	4	eleq1d 2867	. . . . . . . . 9 ⊢ (𝑚 = 𝑤 → ((𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ (𝑎 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
6	5	cbvralv 3403	. . . . . . . 8 ⊢ (∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ∀𝑤 ∈ (0...(𝑘 − 1))(𝑎 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
7		oveq1 7028	. . . . . . . . . 10 ⊢ (𝑎 = 𝑦 → (𝑎 + (𝑤 · 𝑑)) = (𝑦 + (𝑤 · 𝑑)))
8	7	eleq1d 2867	. . . . . . . . 9 ⊢ (𝑎 = 𝑦 → ((𝑎 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ (𝑦 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
9	8	ralbidv 3164	. . . . . . . 8 ⊢ (𝑎 = 𝑦 → (∀𝑤 ∈ (0...(𝑘 − 1))(𝑎 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
10	6, 9	syl5bb 284	. . . . . . 7 ⊢ (𝑎 = 𝑦 → (∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
11		oveq2 7029	. . . . . . . . . 10 ⊢ (𝑑 = 𝑧 → (𝑤 · 𝑑) = (𝑤 · 𝑧))
12	11	oveq2d 7037	. . . . . . . . 9 ⊢ (𝑑 = 𝑧 → (𝑦 + (𝑤 · 𝑑)) = (𝑦 + (𝑤 · 𝑧)))
13	12	eleq1d 2867	. . . . . . . 8 ⊢ (𝑑 = 𝑧 → ((𝑦 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ (𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})))
14	13	ralbidv 3164	. . . . . . 7 ⊢ (𝑑 = 𝑧 → (∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})))
15	10, 14	cbvrex2v 3413	. . . . . 6 ⊢ (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ∃𝑦 ∈ ℕ ∃𝑧 ∈ ℕ ∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢}))
16		oveq1 7028	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (𝑘 − 1) = (𝑥 − 1))
17	16	oveq2d 7037	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → (0...(𝑘 − 1)) = (0...(𝑥 − 1)))
18	17	raleqdv 3375	. . . . . . 7 ⊢ (𝑘 = 𝑥 → (∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢}) ↔ ∀𝑤 ∈ (0...(𝑥 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})))
19	18	2rexbidv 3263	. . . . . 6 ⊢ (𝑘 = 𝑥 → (∃𝑦 ∈ ℕ ∃𝑧 ∈ ℕ ∀𝑤 ∈ (0...(𝑘 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢}) ↔ ∃𝑦 ∈ ℕ ∃𝑧 ∈ ℕ ∀𝑤 ∈ (0...(𝑥 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})))
20	15, 19	syl5bb 284	. . . . 5 ⊢ (𝑘 = 𝑥 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ∃𝑦 ∈ ℕ ∃𝑧 ∈ ℕ ∀𝑤 ∈ (0...(𝑥 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})))
21	20	notbid 319	. . . 4 ⊢ (𝑘 = 𝑥 → (¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ¬ ∃𝑦 ∈ ℕ ∃𝑧 ∈ ℕ ∀𝑤 ∈ (0...(𝑥 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})))
22	21	cbvrabv 3434	. . 3 ⊢ {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})} = {𝑥 ∈ ℕ ∣ ¬ ∃𝑦 ∈ ℕ ∃𝑧 ∈ ℕ ∀𝑤 ∈ (0...(𝑥 − 1))(𝑦 + (𝑤 · 𝑧)) ∈ (◡𝐹 “ {𝑢})}
23		simpr 485	. . . . 5 ⊢ (((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) → ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))
24		sneq 4486	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑢 → {𝑐} = {𝑢})
25	24	imaeq2d 5811	. . . . . . . . . 10 ⊢ (𝑐 = 𝑢 → (◡𝐹 “ {𝑐}) = (◡𝐹 “ {𝑢}))
26	25	eleq2d 2868	. . . . . . . . 9 ⊢ (𝑐 = 𝑢 → ((𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ (𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
27	26	ralbidv 3164	. . . . . . . 8 ⊢ (𝑐 = 𝑢 → (∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
28	27	2rexbidv 3263	. . . . . . 7 ⊢ (𝑐 = 𝑢 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
29	28	ralbidv 3164	. . . . . 6 ⊢ (𝑐 = 𝑢 → (∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})))
30	29	cbvrexv 3404	. . . . 5 ⊢ (∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∃𝑢 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
31	23, 30	sylnib 329	. . . 4 ⊢ (((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) → ¬ ∃𝑢 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
32		rabn0 4263	. . . . . . 7 ⊢ ({𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})} ≠ ∅ ↔ ∃𝑘 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
33		rexnal 3202	. . . . . . 7 ⊢ (∃𝑘 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ¬ ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
34	32, 33	bitri 276	. . . . . 6 ⊢ ({𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})} ≠ ∅ ↔ ¬ ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
35	34	ralbii 3132	. . . . 5 ⊢ (∀𝑢 ∈ 𝑅 {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})} ≠ ∅ ↔ ∀𝑢 ∈ 𝑅 ¬ ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
36		ralnex 3200	. . . . 5 ⊢ (∀𝑢 ∈ 𝑅 ¬ ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}) ↔ ¬ ∃𝑢 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
37	35, 36	bitri 276	. . . 4 ⊢ (∀𝑢 ∈ 𝑅 {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})} ≠ ∅ ↔ ¬ ∃𝑢 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢}))
38	31, 37	sylibr 235	. . 3 ⊢ (((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) → ∀𝑢 ∈ 𝑅 {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑢})} ≠ ∅)
39	1, 2, 22, 38	vdwnnlem3 16167	. 2 ⊢ ¬ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))
40		iman 402	. 2 ⊢ (((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) → ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) ↔ ¬ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) ∧ ¬ ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})))
41	39, 40	mpbir 232	1 ⊢ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) → ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2081   ≠ wne 2984  ∀wral 3105  ∃wrex 3106  {crab 3109  ∅c0 4215  {csn 4476  ^◡ccnv 5447   “ cima 5451  ⟶wf 6226  (class class class)co 7021  Fincfn 8362  0cc0 10388  1c1 10389   + caddc 10391   · cmul 10393   − cmin 10722  ℕcn 11491  ...cfz 12747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-cnex 10444  ax-resscn 10445  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-mulcom 10452  ax-addass 10453  ax-mulass 10454  ax-distr 10455  ax-i2m1 10456  ax-1ne0 10457  ax-1rid 10458  ax-rnegex 10459  ax-rrecex 10460  ax-cnre 10461  ax-pre-lttri 10462  ax-pre-lttrn 10463  ax-pre-ltadd 10464  ax-pre-mulgt0 10465  ax-pre-sup 10466

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-int 4787  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-riota 6982  df-ov 7024  df-oprab 7025  df-mpo 7026  df-om 7442  df-1st 7550  df-2nd 7551  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-1o 7958  df-2o 7959  df-oadd 7962  df-er 8144  df-map 8263  df-pm 8264  df-en 8363  df-dom 8364  df-sdom 8365  df-fin 8366  df-sup 8757  df-inf 8758  df-dju 9181  df-card 9219  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-sub 10724  df-neg 10725  df-nn 11492  df-2 11553  df-n0 11751  df-xnn0 11821  df-z 11835  df-uz 12099  df-rp 12245  df-fz 12748  df-fl 13017  df-hash 13546  df-vdwap 16138  df-vdwmc 16139  df-vdwpc 16140

This theorem is referenced by: (None)