Step |
Hyp |
Ref |
Expression |
1 |
|
zssre |
|- ZZ C_ RR |
2 |
|
ltso |
|- < Or RR |
3 |
|
soss |
|- ( ZZ C_ RR -> ( < Or RR -> < Or ZZ ) ) |
4 |
1 2 3
|
mp2 |
|- < Or ZZ |
5 |
4
|
a1i |
|- ( N e. ( ZZ>= ` M ) -> < Or ZZ ) |
6 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
7 |
|
eluzfz1 |
|- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) ) |
8 |
|
elfzle1 |
|- ( x e. ( M ... N ) -> M <_ x ) |
9 |
8
|
adantl |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> M <_ x ) |
10 |
6
|
zred |
|- ( N e. ( ZZ>= ` M ) -> M e. RR ) |
11 |
|
elfzelz |
|- ( x e. ( M ... N ) -> x e. ZZ ) |
12 |
11
|
zred |
|- ( x e. ( M ... N ) -> x e. RR ) |
13 |
|
lenlt |
|- ( ( M e. RR /\ x e. RR ) -> ( M <_ x <-> -. x < M ) ) |
14 |
10 12 13
|
syl2an |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> ( M <_ x <-> -. x < M ) ) |
15 |
9 14
|
mpbid |
|- ( ( N e. ( ZZ>= ` M ) /\ x e. ( M ... N ) ) -> -. x < M ) |
16 |
5 6 7 15
|
infmin |
|- ( N e. ( ZZ>= ` M ) -> inf ( ( M ... N ) , ZZ , < ) = M ) |