Step |
Hyp |
Ref |
Expression |
1 |
|
ne0i |
|- ( A e. S -> S =/= (/) ) |
2 |
|
uzwo |
|- ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k ) |
3 |
1 2
|
sylan2 |
|- ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> E. j e. S A. k e. S j <_ k ) |
4 |
|
uzssz |
|- ( ZZ>= ` M ) C_ ZZ |
5 |
|
zssre |
|- ZZ C_ RR |
6 |
4 5
|
sstri |
|- ( ZZ>= ` M ) C_ RR |
7 |
|
sstr |
|- ( ( S C_ ( ZZ>= ` M ) /\ ( ZZ>= ` M ) C_ RR ) -> S C_ RR ) |
8 |
6 7
|
mpan2 |
|- ( S C_ ( ZZ>= ` M ) -> S C_ RR ) |
9 |
|
lbinfle |
|- ( ( S C_ RR /\ E. j e. S A. k e. S j <_ k /\ A e. S ) -> inf ( S , RR , < ) <_ A ) |
10 |
9
|
3com23 |
|- ( ( S C_ RR /\ A e. S /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) <_ A ) |
11 |
8 10
|
syl3an1 |
|- ( ( S C_ ( ZZ>= ` M ) /\ A e. S /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) <_ A ) |
12 |
3 11
|
mpd3an3 |
|- ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> inf ( S , RR , < ) <_ A ) |