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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 ↔ ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = 0 ) )

Proof

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