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 0 B A < B A B = 0

Proof

Step Hyp Ref Expression
1 nn0nndivcl A 0 B A B
2 1 recnd A 0 B A B
3 addid2 A B 0 + A B = A B
4 3 eqcomd A B A B = 0 + A B
5 2 4 syl A 0 B A B = 0 + A B
6 5 fveqeq2d A 0 B A B = 0 0 + A B = 0
7 0z 0
8 flbi2 0 A B 0 + A B = 0 0 A B A B < 1
9 7 1 8 sylancr A 0 B 0 + A B = 0 0 A B A B < 1
10 nn0ge0div A 0 B 0 A B
11 10 biantrurd A 0 B A B < 1 0 A B A B < 1
12 nn0re A 0 A
13 nnrp B B +
14 divlt1lt A B + A B < 1 A < B
15 12 13 14 syl2an A 0 B A B < 1 A < B
16 11 15 bitr3d A 0 B 0 A B A B < 1 A < B
17 6 9 16 3bitrrd A 0 B A < B A B = 0