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

Metamath Proof Explorer

Theorem flwordi

Description: Ordering relation for the floor function. (Contributed by NM, 31-Dec-2005) (Proof shortened by Fan Zheng, 14-Jul-2016)

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

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 2 zred 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) e. RR )
4 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> B e. RR )
5 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
6 1 5 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) <_ A )
7 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ B )
8 3 1 4 6 7 letrd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) <_ B )
9 flge 
 |-  ( ( B e. RR /\ ( |_ ` A ) e. ZZ ) -> ( ( |_ ` A ) <_ B <-> ( |_ ` A ) <_ ( |_ ` B ) ) )
10 4 2 9 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( |_ ` A ) <_ B <-> ( |_ ` A ) <_ ( |_ ` B ) ) )
11 8 10 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) <_ ( |_ ` B ) )