Theorem 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	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → 𝑅 ∈ Fin )
2		simpr	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
3	1 2	vdwlem13	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
4		ovex	⊢ ( 1 ... 𝑛 ) ∈ V
5		simpllr	⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → 𝐾 ∈ ℕ0 )
6		simpll	⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → 𝑅 ∈ Fin )
7		elmapg	⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑛 ) ∈ V ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ↔ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) )
8	6 4 7	sylancl	⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ↔ 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 ) )
9	8	biimpa	⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → 𝑓 : ( 1 ... 𝑛 ) ⟶ 𝑅 )
10		simplr	⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → 𝑛 ∈ ℕ )
11		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
12	10 11	eleqtrdi	⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
13		eluzfz1	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑛 ) )
14	12 13	syl	⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → 1 ∈ ( 1 ... 𝑛 ) )
15	4 5 9 14	vdwmc2	⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ) → ( 𝐾 MonoAP 𝑓 ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ) )
16	15	ralbidva	⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ) )
17	16	rexbidva	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) ) )
18	3 17	mpbid	⊢ ( ( 𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝑓 “ { 𝑐 } ) )