Metamath Proof Explorer

Theorem adddivflid

Description: The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion adddivflid ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B < C ↔ A + B C = A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → A ∈ ℤ
2 nn0nndivcl ⊢ B ∈ ℕ 0 ∧ C ∈ ℕ → B C ∈ ℝ
3 2 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B C ∈ ℝ
4 1 3 jca ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → A ∈ ℤ ∧ B C ∈ ℝ
5 flbi2 ⊢ A ∈ ℤ ∧ B C ∈ ℝ → A + B C = A ↔ 0 ≤ B C ∧ B C < 1
6 4 5 syl ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → A + B C = A ↔ 0 ≤ B C ∧ B C < 1
7 nn0re ⊢ B ∈ ℕ 0 → B ∈ ℝ
8 nn0ge0 ⊢ B ∈ ℕ 0 → 0 ≤ B
9 7 8 jca ⊢ B ∈ ℕ 0 → B ∈ ℝ ∧ 0 ≤ B
10 nnre ⊢ C ∈ ℕ → C ∈ ℝ
11 nngt0 ⊢ C ∈ ℕ → 0 < C
12 10 11 jca ⊢ C ∈ ℕ → C ∈ ℝ ∧ 0 < C
13 9 12 anim12i ⊢ B ∈ ℕ 0 ∧ C ∈ ℕ → B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ ∧ 0 < C
14 13 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ ∧ 0 < C
15 divge0 ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ ∧ 0 < C → 0 ≤ B C
16 14 15 syl ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → 0 ≤ B C
17 16 biantrurd ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B C < 1 ↔ 0 ≤ B C ∧ B C < 1
18 nnrp ⊢ C ∈ ℕ → C ∈ ℝ +
19 7 18 anim12i ⊢ B ∈ ℕ 0 ∧ C ∈ ℕ → B ∈ ℝ ∧ C ∈ ℝ +
20 19 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B ∈ ℝ ∧ C ∈ ℝ +
21 divlt1lt ⊢ B ∈ ℝ ∧ C ∈ ℝ + → B C < 1 ↔ B < C
22 20 21 syl ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B C < 1 ↔ B < C
23 6 17 22 3bitr2rd ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ → B < C ↔ A + B C = A