Metamath Proof Explorer

Theorem vdwnn

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

Ref Expression
Assertion vdwnn ⊢ R ∈ Fin ∧ F : ℕ ⟶ R → ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c

Proof

Step Hyp Ref Expression
1 simpll ⊢ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c → R ∈ Fin
2 simplr ⊢ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c → F : ℕ ⟶ R
3 oveq1 ⊢ m = w → m ⁢ d = w ⁢ d
4 3 oveq2d ⊢ m = w → a + m ⁢ d = a + w ⁢ d
5 4 eleq1d ⊢ m = w → a + m ⁢ d ∈ F -1 u ↔ a + w ⁢ d ∈ F -1 u
6 5 cbvralvw ⊢ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ∀ w ∈ 0 … k − 1 a + w ⁢ d ∈ F -1 u
7 oveq1 ⊢ a = y → a + w ⁢ d = y + w ⁢ d
8 7 eleq1d ⊢ a = y → a + w ⁢ d ∈ F -1 u ↔ y + w ⁢ d ∈ F -1 u
9 8 ralbidv ⊢ a = y → ∀ w ∈ 0 … k − 1 a + w ⁢ d ∈ F -1 u ↔ ∀ w ∈ 0 … k − 1 y + w ⁢ d ∈ F -1 u
10 6 9 bitrid ⊢ a = y → ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ∀ w ∈ 0 … k − 1 y + w ⁢ d ∈ F -1 u
11 oveq2 ⊢ d = z → w ⁢ d = w ⁢ z
12 11 oveq2d ⊢ d = z → y + w ⁢ d = y + w ⁢ z
13 12 eleq1d ⊢ d = z → y + w ⁢ d ∈ F -1 u ↔ y + w ⁢ z ∈ F -1 u
14 13 ralbidv ⊢ d = z → ∀ w ∈ 0 … k − 1 y + w ⁢ d ∈ F -1 u ↔ ∀ w ∈ 0 … k − 1 y + w ⁢ z ∈ F -1 u
15 10 14 cbvrex2vw ⊢ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ∃ y ∈ ℕ ∃ z ∈ ℕ ∀ w ∈ 0 … k − 1 y + w ⁢ z ∈ F -1 u
16 oveq1 ⊢ k = x → k − 1 = x − 1
17 16 oveq2d ⊢ k = x → 0 … k − 1 = 0 … x − 1
18 17 raleqdv ⊢ k = x → ∀ w ∈ 0 … k − 1 y + w ⁢ z ∈ F -1 u ↔ ∀ w ∈ 0 … x − 1 y + w ⁢ z ∈ F -1 u
19 18 2rexbidv ⊢ k = x → ∃ y ∈ ℕ ∃ z ∈ ℕ ∀ w ∈ 0 … k − 1 y + w ⁢ z ∈ F -1 u ↔ ∃ y ∈ ℕ ∃ z ∈ ℕ ∀ w ∈ 0 … x − 1 y + w ⁢ z ∈ F -1 u
20 15 19 bitrid ⊢ k = x → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ∃ y ∈ ℕ ∃ z ∈ ℕ ∀ w ∈ 0 … x − 1 y + w ⁢ z ∈ F -1 u
21 20 notbid ⊢ k = x → ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ¬ ∃ y ∈ ℕ ∃ z ∈ ℕ ∀ w ∈ 0 … x − 1 y + w ⁢ z ∈ F -1 u
22 21 cbvrabv ⊢ k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u = x ∈ ℕ | ¬ ∃ y ∈ ℕ ∃ z ∈ ℕ ∀ w ∈ 0 … x − 1 y + w ⁢ z ∈ F -1 u
23 simpr ⊢ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c → ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c
24 sneq ⊢ c = u → c = u
25 24 imaeq2d ⊢ c = u → F -1 c = F -1 u
26 25 eleq2d ⊢ c = u → a + m ⁢ d ∈ F -1 c ↔ a + m ⁢ d ∈ F -1 u
27 26 ralbidv ⊢ c = u → ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
28 27 2rexbidv ⊢ c = u → ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
29 28 ralbidv ⊢ c = u → ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
30 29 cbvrexvw ⊢ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ∃ u ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
31 23 30 sylnib ⊢ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c → ¬ ∃ u ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
32 rabn0 ⊢ k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ≠ ∅ ↔ ∃ k ∈ ℕ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
33 rexnal ⊢ ∃ k ∈ ℕ ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ¬ ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
34 32 33 bitri ⊢ k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ≠ ∅ ↔ ¬ ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
35 34 ralbii ⊢ ∀ u ∈ R k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ≠ ∅ ↔ ∀ u ∈ R ¬ ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
36 ralnex ⊢ ∀ u ∈ R ¬ ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ↔ ¬ ∃ u ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
37 35 36 bitri ⊢ ∀ u ∈ R k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ≠ ∅ ↔ ¬ ∃ u ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u
38 31 37 sylibr ⊢ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c → ∀ u ∈ R k ∈ ℕ | ¬ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 u ≠ ∅
39 1 2 22 38 vdwnnlem3 ⊢ ¬ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c
40 iman ⊢ R ∈ Fin ∧ F : ℕ ⟶ R → ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c ↔ ¬ R ∈ Fin ∧ F : ℕ ⟶ R ∧ ¬ ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c
41 39 40 mpbir ⊢ R ∈ Fin ∧ F : ℕ ⟶ R → ∃ c ∈ R ∀ k ∈ ℕ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … k − 1 a + m ⁢ d ∈ F -1 c