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		addid2	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( 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 ) )