Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A e. RR ) |
2 |
1
|
flcld |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) e. ZZ ) |
3 |
|
simp2 |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> B e. RR ) |
4 |
3
|
flcld |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` B ) e. ZZ ) |
5 |
|
flwordi |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) <_ ( |_ ` B ) ) |
6 |
|
eluz2 |
|- ( ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) <-> ( ( |_ ` A ) e. ZZ /\ ( |_ ` B ) e. ZZ /\ ( |_ ` A ) <_ ( |_ ` B ) ) ) |
7 |
2 4 5 6
|
syl3anbrc |
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) ) |