Metamath Proof Explorer

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 
|- ( ( R e. Fin /\ K e. NN0 ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( R e. Fin /\ K e. NN0 ) -> R e. Fin )
2 simpr 
 |-  ( ( R e. Fin /\ K e. NN0 ) -> K e. NN0 )
3 1 2 vdwlem13 
 |-  ( ( R e. Fin /\ K e. NN0 ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f )
4 ovex 
 |-  ( 1 ... n ) e. _V
5 simpllr 
 |-  ( ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> K e. NN0 )
6 simpll 
 |-  ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) -> R e. Fin )
7 elmapg 
 |-  ( ( R e. Fin /\ ( 1 ... n ) e. _V ) -> ( f e. ( R ^m ( 1 ... n ) ) <-> f : ( 1 ... n ) --> R ) )
8 6 4 7 sylancl 
 |-  ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) -> ( f e. ( R ^m ( 1 ... n ) ) <-> f : ( 1 ... n ) --> R ) )
9 8 biimpa 
 |-  ( ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> f : ( 1 ... n ) --> R )
10 simplr 
 |-  ( ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> n e. NN )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 10 11 eleqtrdi 
 |-  ( ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> n e. ( ZZ>= ` 1 ) )
13 eluzfz1 
 |-  ( n e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... n ) )
14 12 13 syl 
 |-  ( ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> 1 e. ( 1 ... n ) )
15 4 5 9 14 vdwmc2 
 |-  ( ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) /\ f e. ( R ^m ( 1 ... n ) ) ) -> ( K MonoAP f <-> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) ) )
16 15 ralbidva 
 |-  ( ( ( R e. Fin /\ K e. NN0 ) /\ n e. NN ) -> ( A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f <-> A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) ) )
17 16 rexbidva 
 |-  ( ( R e. Fin /\ K e. NN0 ) -> ( E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f <-> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) ) )
18 3 17 mpbid 
 |-  ( ( R e. Fin /\ K e. NN0 ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) )