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 e. Fin /\ F : NN --> R ) -> E. c e. R A. k e. NN 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 simpll 
 |-  ( ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) -> R e. Fin )
2 simplr 
 |-  ( ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) -> F : NN --> R )
3 oveq1 
 |-  ( m = w -> ( m x. d ) = ( w x. d ) )
4 3 oveq2d 
 |-  ( m = w -> ( a + ( m x. d ) ) = ( a + ( w x. d ) ) )
5 4 eleq1d 
 |-  ( m = w -> ( ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> ( a + ( w x. d ) ) e. ( `' F " { u } ) ) )
6 5 cbvralvw 
 |-  ( A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> A. w e. ( 0 ... ( k - 1 ) ) ( a + ( w x. d ) ) e. ( `' F " { u } ) )
7 oveq1 
 |-  ( a = y -> ( a + ( w x. d ) ) = ( y + ( w x. d ) ) )
8 7 eleq1d 
 |-  ( a = y -> ( ( a + ( w x. d ) ) e. ( `' F " { u } ) <-> ( y + ( w x. d ) ) e. ( `' F " { u } ) ) )
9 8 ralbidv 
 |-  ( a = y -> ( A. w e. ( 0 ... ( k - 1 ) ) ( a + ( w x. d ) ) e. ( `' F " { u } ) <-> A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. d ) ) e. ( `' F " { u } ) ) )
10 6 9 syl5bb 
 |-  ( a = y -> ( A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. d ) ) e. ( `' F " { u } ) ) )
11 oveq2 
 |-  ( d = z -> ( w x. d ) = ( w x. z ) )
12 11 oveq2d 
 |-  ( d = z -> ( y + ( w x. d ) ) = ( y + ( w x. z ) ) )
13 12 eleq1d 
 |-  ( d = z -> ( ( y + ( w x. d ) ) e. ( `' F " { u } ) <-> ( y + ( w x. z ) ) e. ( `' F " { u } ) ) )
14 13 ralbidv 
 |-  ( d = z -> ( A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. d ) ) e. ( `' F " { u } ) <-> A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) ) )
15 10 14 cbvrex2vw 
 |-  ( E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> E. y e. NN E. z e. NN A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { 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 -> ( A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) <-> A. w e. ( 0 ... ( x - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) ) )
19 18 2rexbidv 
 |-  ( k = x -> ( E. y e. NN E. z e. NN A. w e. ( 0 ... ( k - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) <-> E. y e. NN E. z e. NN A. w e. ( 0 ... ( x - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) ) )
20 15 19 syl5bb 
 |-  ( k = x -> ( E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> E. y e. NN E. z e. NN A. w e. ( 0 ... ( x - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) ) )
21 20 notbid 
 |-  ( k = x -> ( -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> -. E. y e. NN E. z e. NN A. w e. ( 0 ... ( x - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) ) )
22 21 cbvrabv 
 |-  { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) } = { x e. NN | -. E. y e. NN E. z e. NN A. w e. ( 0 ... ( x - 1 ) ) ( y + ( w x. z ) ) e. ( `' F " { u } ) }
23 simpr 
 |-  ( ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) -> -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
24 sneq 
 |-  ( c = u -> { c } = { u } )
25 24 imaeq2d 
 |-  ( c = u -> ( `' F " { c } ) = ( `' F " { u } ) )
26 25 eleq2d 
 |-  ( c = u -> ( ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> ( a + ( m x. d ) ) e. ( `' F " { u } ) ) )
27 26 ralbidv 
 |-  ( c = u -> ( A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) ) )
28 27 2rexbidv 
 |-  ( c = u -> ( E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) ) )
29 28 ralbidv 
 |-  ( c = u -> ( A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) ) )
30 29 cbvrexvw 
 |-  ( E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> E. u e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
31 23 30 sylnib 
 |-  ( ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) -> -. E. u e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
32 rabn0 
 |-  ( { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) } =/= (/) <-> E. k e. NN -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
33 rexnal 
 |-  ( E. k e. NN -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> -. A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
34 32 33 bitri 
 |-  ( { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) } =/= (/) <-> -. A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
35 34 ralbii 
 |-  ( A. u e. R { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) } =/= (/) <-> A. u e. R -. A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
36 ralnex 
 |-  ( A. u e. R -. A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) <-> -. E. u e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
37 35 36 bitri 
 |-  ( A. u e. R { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) } =/= (/) <-> -. E. u e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) )
38 31 37 sylibr 
 |-  ( ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) -> A. u e. R { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { u } ) } =/= (/) )
39 1 2 22 38 vdwnnlem3 
 |-  -. ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
40 iman 
 |-  ( ( ( R e. Fin /\ F : NN --> R ) -> E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) <-> -. ( ( R e. Fin /\ F : NN --> R ) /\ -. E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
41 39 40 mpbir 
 |-  ( ( R e. Fin /\ F : NN --> R ) -> E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )