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↔AB=0

Proof

Step Hyp Ref Expression
1 nn0nndivcl ⊢A∈ℕ0∧B∈ℕ→AB∈ℝ
2 1 recnd ⊢A∈ℕ0∧B∈ℕ→AB∈ℂ
3 addlid ⊢AB∈ℂ→0+AB=AB
4 3 eqcomd ⊢AB∈ℂ→AB=0+AB
5 2 4 syl ⊢A∈ℕ0∧B∈ℕ→AB=0+AB
6 5 fveqeq2d ⊢A∈ℕ0∧B∈ℕ→AB=0↔0+AB=0
7 0z ⊢0∈ℤ
8 flbi2 ⊢0∈ℤ∧AB∈ℝ→0+AB=0↔0≤AB∧AB<1
9 7 1 8 sylancr ⊢A∈ℕ0∧B∈ℕ→0+AB=0↔0≤AB∧AB<1
10 nn0ge0div ⊢A∈ℕ0∧B∈ℕ→0≤AB
11 10 biantrurd ⊢A∈ℕ0∧B∈ℕ→AB<1↔0≤AB∧AB<1
12 nn0re ⊢A∈ℕ0→A∈ℝ
13 nnrp ⊢B∈ℕ→B∈ℝ+
14 divlt1lt ⊢A∈ℝ∧B∈ℝ+→AB<1↔A<B
15 12 13 14 syl2an ⊢A∈ℕ0∧B∈ℕ→AB<1↔A<B
16 11 15 bitr3d ⊢A∈ℕ0∧B∈ℕ→0≤AB∧AB<1↔A<B
17 6 9 16 3bitrrd ⊢A∈ℕ0∧B∈ℕ→A<B↔AB=0