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

Metamath Proof Explorer

Theorem divfl0

Description: The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021)

Ref Expression
Assertion divfl0 
|- ( ( A e. NN0 /\ B e. NN ) -> ( A < B <-> ( |_ ` ( A / B ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 nn0nndivcl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) e. RR )
2 1 recnd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) e. CC )
3 addlid 
 |-  ( ( A / B ) e. CC -> ( 0 + ( A / B ) ) = ( A / B ) )
4 3 eqcomd 
 |-  ( ( A / B ) e. CC -> ( A / B ) = ( 0 + ( A / B ) ) )
5 2 4 syl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) = ( 0 + ( A / B ) ) )
6 5 fveqeq2d 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( |_ ` ( A / B ) ) = 0 <-> ( |_ ` ( 0 + ( A / B ) ) ) = 0 ) )
7 0z 
 |-  0 e. ZZ
8 flbi2 
 |-  ( ( 0 e. ZZ /\ ( A / B ) e. RR ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
9 7 1 8 sylancr 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
10 nn0ge0div 
 |-  ( ( A e. NN0 /\ B e. NN ) -> 0 <_ ( A / B ) )
11 10 biantrurd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) < 1 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
12 nn0re 
 |-  ( A e. NN0 -> A e. RR )
13 nnrp 
 |-  ( B e. NN -> B e. RR+ )
14 divlt1lt 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) < 1 <-> A < B ) )
15 12 13 14 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) < 1 <-> A < B ) )
16 11 15 bitr3d 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) <-> A < B ) )
17 6 9 16 3bitrrd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A < B <-> ( |_ ` ( A / B ) ) = 0 ) )