vdw

Description: Van der Waerden's theorem. For any finite coloring R and integer K , there is an N such that every coloring function from 1 ... N to R contains a monochromatic arithmetic progression (which written out in full means that there is a color c and base, increment values a , d such that all the numbers a , a + d , ... , a + ( k - 1 ) d lie in the preimage of { c } , i.e. they are all in 1 ... N and f evaluated at each one yields c ). (Contributed by Mario Carneiro, 13-Sep-2014)

		Ref	Expression
	Assertion	vdw	$⊢ (R \in Fin \land K \in ℕ_{0}) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}]$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (R \in Fin \land K \in ℕ_{0}) \to R \in Fin$
2		simpr	$⊢ (R \in Fin \land K \in ℕ_{0}) \to K \in ℕ_{0}$
3	1 2	vdwlem13	$⊢ (R \in Fin \land K \in ℕ_{0}) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f$
4		ovex	$⊢ (1 \dots n) \in V$
5		simpllr	$⊢ (((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to K \in ℕ_{0}$
6		simpll	$⊢ ((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \to R \in Fin$
7		elmapg	$⊢ (R \in Fin \land (1 \dots n) \in V) \to (f \in (R^{(1 \dots n)}) \leftrightarrow f : (1 \dots n) ⟶ R)$
8	6 4 7	sylancl	$⊢ ((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \to (f \in (R^{(1 \dots n)}) \leftrightarrow f : (1 \dots n) ⟶ R)$
9	8	biimpa	$⊢ (((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to f : (1 \dots n) ⟶ R$
10		simplr	$⊢ (((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to n \in ℕ$
11		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
12	10 11	eleqtrdi	$⊢ (((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to n \in ℤ_{\geq 1}$
13		eluzfz1	$⊢ n \in ℤ_{\geq 1} \to 1 \in (1 \dots n)$
14	12 13	syl	$⊢ (((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to 1 \in (1 \dots n)$
15	4 5 9 14	vdwmc2	$⊢ (((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \land f \in (R^{(1 \dots n)})) \to (K MonoAP f \leftrightarrow \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}])$
16	15	ralbidva	$⊢ ((R \in Fin \land K \in ℕ_{0}) \land n \in ℕ) \to (\forall f \in (R^{(1 \dots n)}) K MonoAP f \leftrightarrow \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}])$
17	16	rexbidva	$⊢ (R \in Fin \land K \in ℕ_{0}) \to (\exists n \in ℕ \forall f \in (R^{(1 \dots n)}) K MonoAP f \leftrightarrow \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}])$
18	3 17	mpbid	$⊢ (R \in Fin \land K \in ℕ_{0}) \to \exists n \in ℕ \forall f \in (R^{(1 \dots n)}) \exists c \in R \exists a \in ℕ \exists d \in ℕ \forall m \in (0 \dots K - 1) a + m d \in f^{-1} [\{c\}]$

Metamath Proof Explorer

Theorem vdw

Proof