Metamath Proof Explorer


Theorem flword2

Description: Ordering relation for the floor function. (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Assertion flword2
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) )

Proof

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 ) ) )