This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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