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
|
sseldi |
|- ( ( 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 |