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−1a+m⁢d∈F-1c

Proof

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