Metamath Proof Explorer

Theorem vdwnnlem2

Description: Lemma for vdwnn . The set of all "bad" k for the theorem is upwards-closed, because a long AP implies a short AP. (Contributed by Mario Carneiro, 13-Sep-2014)

Ref Expression
Hypotheses vdwnn.1 
|- ( ph -> R e. Fin )
vdwnn.2 
|- ( ph -> F : NN --> R )
vdwnn.3 
|- S = { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) }
Assertion vdwnnlem2 
|- ( ( ph /\ B e. ( ZZ>= ` A ) ) -> ( A e. S -> B e. S ) )

Proof

Step Hyp Ref Expression
1 vdwnn.1 
 |-  ( ph -> R e. Fin )
2 vdwnn.2 
 |-  ( ph -> F : NN --> R )
3 vdwnn.3 
 |-  S = { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) }
4 eluzel2 
 |-  ( B e. ( ZZ>= ` A ) -> A e. ZZ )
5 peano2zm 
 |-  ( A e. ZZ -> ( A - 1 ) e. ZZ )
6 4 5 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( A - 1 ) e. ZZ )
7 id 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ( ZZ>= ` A ) )
8 4 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> A e. CC )
9 ax-1cn 
 |-  1 e. CC
10 npcan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) + 1 ) = A )
11 8 9 10 sylancl 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A - 1 ) + 1 ) = A )
12 11 fveq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ZZ>= ` ( ( A - 1 ) + 1 ) ) = ( ZZ>= ` A ) )
13 7 12 eleqtrrd 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ( ZZ>= ` ( ( A - 1 ) + 1 ) ) )
14 eluzp1m1 
 |-  ( ( ( A - 1 ) e. ZZ /\ B e. ( ZZ>= ` ( ( A - 1 ) + 1 ) ) ) -> ( B - 1 ) e. ( ZZ>= ` ( A - 1 ) ) )
15 6 13 14 syl2anc 
 |-  ( B e. ( ZZ>= ` A ) -> ( B - 1 ) e. ( ZZ>= ` ( A - 1 ) ) )
16 15 ad2antlr 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> ( B - 1 ) e. ( ZZ>= ` ( A - 1 ) ) )
17 fzss2 
 |-  ( ( B - 1 ) e. ( ZZ>= ` ( A - 1 ) ) -> ( 0 ... ( A - 1 ) ) C_ ( 0 ... ( B - 1 ) ) )
18 ssralv 
 |-  ( ( 0 ... ( A - 1 ) ) C_ ( 0 ... ( B - 1 ) ) -> ( A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) -> A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
19 16 17 18 3syl 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> ( A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) -> A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
20 19 reximdv 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> ( E. d e. NN A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) -> E. d e. NN A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
21 20 reximdv 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> ( E. a e. NN E. d e. NN A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) -> E. a e. NN E. d e. NN A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
22 21 con3d 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> ( -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) -> -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
23 id 
 |-  ( A e. NN -> A e. NN )
24 simpr 
 |-  ( ( ph /\ B e. ( ZZ>= ` A ) ) -> B e. ( ZZ>= ` A ) )
25 eluznn 
 |-  ( ( A e. NN /\ B e. ( ZZ>= ` A ) ) -> B e. NN )
26 23 24 25 syl2anr 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> B e. NN )
27 22 26 jctild 
 |-  ( ( ( ph /\ B e. ( ZZ>= ` A ) ) /\ A e. NN ) -> ( -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) -> ( B e. NN /\ -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) ) )
28 27 expimpd 
 |-  ( ( ph /\ B e. ( ZZ>= ` A ) ) -> ( ( A e. NN /\ -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) -> ( B e. NN /\ -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) ) )
29 oveq1 
 |-  ( k = A -> ( k - 1 ) = ( A - 1 ) )
30 29 oveq2d 
 |-  ( k = A -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( A - 1 ) ) )
31 30 raleqdv 
 |-  ( k = A -> ( A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
32 31 2rexbidv 
 |-  ( k = A -> ( 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 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
33 32 notbid 
 |-  ( k = A -> ( -. 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 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
34 33 3 elrab2 
 |-  ( A e. S <-> ( A e. NN /\ -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( A - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
35 oveq1 
 |-  ( k = B -> ( k - 1 ) = ( B - 1 ) )
36 35 oveq2d 
 |-  ( k = B -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( B - 1 ) ) )
37 36 raleqdv 
 |-  ( k = B -> ( A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
38 37 2rexbidv 
 |-  ( k = B -> ( 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 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
39 38 notbid 
 |-  ( k = B -> ( -. 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 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
40 39 3 elrab2 
 |-  ( B e. S <-> ( B e. NN /\ -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( B - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
41 28 34 40 3imtr4g 
 |-  ( ( ph /\ B e. ( ZZ>= ` A ) ) -> ( A e. S -> B e. S ) )