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