This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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