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 addlid ⊢ 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