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+BC=A

Proof

Step Hyp Ref Expression
1 simp1 ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→A∈ℤ
2 nn0nndivcl ⊢B∈ℕ0∧C∈ℕ→BC∈ℝ
3 2 3adant1 ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→BC∈ℝ
4 1 3 jca ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→A∈ℤ∧BC∈ℝ
5 flbi2 ⊢A∈ℤ∧BC∈ℝ→A+BC=A↔0≤BC∧BC<1
6 4 5 syl ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→A+BC=A↔0≤BC∧BC<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≤BC
16 14 15 syl ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→0≤BC
17 16 biantrurd ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→BC<1↔0≤BC∧BC<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∈ℝ+→BC<1↔B<C
22 20 21 syl ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→BC<1↔B<C
23 6 17 22 3bitr2rd ⊢A∈ℤ∧B∈ℕ0∧C∈ℕ→B<C↔A+BC=A