Metamath Proof Explorer

Theorem vdwnnlem3

Description: Lemma for vdwnn . (Contributed by Mario Carneiro, 13-Sep-2014) (Proof shortened by AV, 27-Sep-2020)

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 } ) }
vdwnn.4 
|- ( ph -> A. c e. R S =/= (/) )
Assertion vdwnnlem3 
|- -. ph

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 vdwnn.4 
 |-  ( ph -> A. c e. R S =/= (/) )
5 3 ssrab3 
 |-  S C_ NN
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 5 6 sseqtri 
 |-  S C_ ( ZZ>= ` 1 )
8 4 r19.21bi 
 |-  ( ( ph /\ c e. R ) -> S =/= (/) )
9 infssuzcl 
 |-  ( ( S C_ ( ZZ>= ` 1 ) /\ S =/= (/) ) -> inf ( S , RR , < ) e. S )
10 7 8 9 sylancr 
 |-  ( ( ph /\ c e. R ) -> inf ( S , RR , < ) e. S )
11 5 10 sselid 
 |-  ( ( ph /\ c e. R ) -> inf ( S , RR , < ) e. NN )
12 11 nnred 
 |-  ( ( ph /\ c e. R ) -> inf ( S , RR , < ) e. RR )
13 12 ralrimiva 
 |-  ( ph -> A. c e. R inf ( S , RR , < ) e. RR )
14 fimaxre3 
 |-  ( ( R e. Fin /\ A. c e. R inf ( S , RR , < ) e. RR ) -> E. x e. RR A. c e. R inf ( S , RR , < ) <_ x )
15 1 13 14 syl2anc 
 |-  ( ph -> E. x e. RR A. c e. R inf ( S , RR , < ) <_ x )
16 1nn 
 |-  1 e. NN
17 ffvelrn 
 |-  ( ( F : NN --> R /\ 1 e. NN ) -> ( F ` 1 ) e. R )
18 2 16 17 sylancl 
 |-  ( ph -> ( F ` 1 ) e. R )
19 18 ne0d 
 |-  ( ph -> R =/= (/) )
20 19 adantr 
 |-  ( ( ph /\ x e. RR ) -> R =/= (/) )
21 r19.2z 
 |-  ( ( R =/= (/) /\ A. c e. R inf ( S , RR , < ) <_ x ) -> E. c e. R inf ( S , RR , < ) <_ x )
22 21 ex 
 |-  ( R =/= (/) -> ( A. c e. R inf ( S , RR , < ) <_ x -> E. c e. R inf ( S , RR , < ) <_ x ) )
23 20 22 syl 
 |-  ( ( ph /\ x e. RR ) -> ( A. c e. R inf ( S , RR , < ) <_ x -> E. c e. R inf ( S , RR , < ) <_ x ) )
24 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> x e. RR )
25 fllep1 
 |-  ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) )
26 24 25 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> x <_ ( ( |_ ` x ) + 1 ) )
27 12 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> inf ( S , RR , < ) e. RR )
28 24 flcld 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( |_ ` x ) e. ZZ )
29 28 peano2zd 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( ( |_ ` x ) + 1 ) e. ZZ )
30 29 zred 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( ( |_ ` x ) + 1 ) e. RR )
31 letr 
 |-  ( ( inf ( S , RR , < ) e. RR /\ x e. RR /\ ( ( |_ ` x ) + 1 ) e. RR ) -> ( ( inf ( S , RR , < ) <_ x /\ x <_ ( ( |_ ` x ) + 1 ) ) -> inf ( S , RR , < ) <_ ( ( |_ ` x ) + 1 ) ) )
32 27 24 30 31 syl3anc 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( ( inf ( S , RR , < ) <_ x /\ x <_ ( ( |_ ` x ) + 1 ) ) -> inf ( S , RR , < ) <_ ( ( |_ ` x ) + 1 ) ) )
33 26 32 mpan2d 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( inf ( S , RR , < ) <_ x -> inf ( S , RR , < ) <_ ( ( |_ ` x ) + 1 ) ) )
34 11 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> inf ( S , RR , < ) e. NN )
35 34 nnzd 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> inf ( S , RR , < ) e. ZZ )
36 eluz 
 |-  ( ( inf ( S , RR , < ) e. ZZ /\ ( ( |_ ` x ) + 1 ) e. ZZ ) -> ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` inf ( S , RR , < ) ) <-> inf ( S , RR , < ) <_ ( ( |_ ` x ) + 1 ) ) )
37 35 29 36 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` inf ( S , RR , < ) ) <-> inf ( S , RR , < ) <_ ( ( |_ ` x ) + 1 ) ) )
38 simpll 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ph )
39 10 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> inf ( S , RR , < ) e. S )
40 1 2 3 vdwnnlem2 
 |-  ( ( ph /\ ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` inf ( S , RR , < ) ) ) -> ( inf ( S , RR , < ) e. S -> ( ( |_ ` x ) + 1 ) e. S ) )
41 40 impancom 
 |-  ( ( ph /\ inf ( S , RR , < ) e. S ) -> ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` inf ( S , RR , < ) ) -> ( ( |_ ` x ) + 1 ) e. S ) )
42 38 39 41 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` inf ( S , RR , < ) ) -> ( ( |_ ` x ) + 1 ) e. S ) )
43 37 42 sylbird 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( inf ( S , RR , < ) <_ ( ( |_ ` x ) + 1 ) -> ( ( |_ ` x ) + 1 ) e. S ) )
44 33 43 syld 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( inf ( S , RR , < ) <_ x -> ( ( |_ ` x ) + 1 ) e. S ) )
45 5 sseli 
 |-  ( ( ( |_ ` x ) + 1 ) e. S -> ( ( |_ ` x ) + 1 ) e. NN )
46 45 nnnn0d 
 |-  ( ( ( |_ ` x ) + 1 ) e. S -> ( ( |_ ` x ) + 1 ) e. NN0 )
47 44 46 syl6 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( inf ( S , RR , < ) <_ x -> ( ( |_ ` x ) + 1 ) e. NN0 ) )
48 47 rexlimdva 
 |-  ( ( ph /\ x e. RR ) -> ( E. c e. R inf ( S , RR , < ) <_ x -> ( ( |_ ` x ) + 1 ) e. NN0 ) )
49 1 adantr 
 |-  ( ( ph /\ ( ( |_ ` x ) + 1 ) e. NN0 ) -> R e. Fin )
50 2 adantr 
 |-  ( ( ph /\ ( ( |_ ` x ) + 1 ) e. NN0 ) -> F : NN --> R )
51 simpr 
 |-  ( ( ph /\ ( ( |_ ` x ) + 1 ) e. NN0 ) -> ( ( |_ ` x ) + 1 ) e. NN0 )
52 vdwnnlem1 
 |-  ( ( R e. Fin /\ F : NN --> R /\ ( ( |_ ` x ) + 1 ) e. NN0 ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
53 49 50 51 52 syl3anc 
 |-  ( ( ph /\ ( ( |_ ` x ) + 1 ) e. NN0 ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
54 53 ex 
 |-  ( ph -> ( ( ( |_ ` x ) + 1 ) e. NN0 -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
55 54 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( ( ( |_ ` x ) + 1 ) e. NN0 -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
56 23 48 55 3syld 
 |-  ( ( ph /\ x e. RR ) -> ( A. c e. R inf ( S , RR , < ) <_ x -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
57 oveq1 
 |-  ( k = ( ( |_ ` x ) + 1 ) -> ( k - 1 ) = ( ( ( |_ ` x ) + 1 ) - 1 ) )
58 57 oveq2d 
 |-  ( k = ( ( |_ ` x ) + 1 ) -> ( 0 ... ( k - 1 ) ) = ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
59 58 raleqdv 
 |-  ( k = ( ( |_ ` x ) + 1 ) -> ( A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
60 59 2rexbidv 
 |-  ( k = ( ( |_ ` x ) + 1 ) -> ( 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 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
61 60 notbid 
 |-  ( k = ( ( |_ ` x ) + 1 ) -> ( -. 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 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
62 61 3 elrab2 
 |-  ( ( ( |_ ` x ) + 1 ) e. S <-> ( ( ( |_ ` x ) + 1 ) e. NN /\ -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
63 62 simprbi 
 |-  ( ( ( |_ ` x ) + 1 ) e. S -> -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
64 44 63 syl6 
 |-  ( ( ( ph /\ x e. RR ) /\ c e. R ) -> ( inf ( S , RR , < ) <_ x -> -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
65 64 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. c e. R inf ( S , RR , < ) <_ x -> A. c e. R -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
66 ralnex 
 |-  ( A. c e. R -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) <-> -. E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
67 65 66 syl6ib 
 |-  ( ( ph /\ x e. RR ) -> ( A. c e. R inf ( S , RR , < ) <_ x -> -. E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( ( ( |_ ` x ) + 1 ) - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
68 56 67 pm2.65d 
 |-  ( ( ph /\ x e. RR ) -> -. A. c e. R inf ( S , RR , < ) <_ x )
69 68 nrexdv 
 |-  ( ph -> -. E. x e. RR A. c e. R inf ( S , RR , < ) <_ x )
70 15 69 pm2.65i 
 |-  -. ph