Theorem fldivndvdslt

Description: The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021)

	Ref	Expression
Assertion	fldivndvdslt	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ∧ ¬ 𝐿 ∥ 𝐾 ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝐾 / 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
2	1	adantr	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → 𝐾 ∈ ℝ )
3		zre	⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
4	3	ad2antrl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → 𝐿 ∈ ℝ )
5		simprr	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → 𝐿 ≠ 0 )
6	2 4 5	redivcld	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → ( 𝐾 / 𝐿 ) ∈ ℝ )
7	6	3adant3	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ∧ ¬ 𝐿 ∥ 𝐾 ) → ( 𝐾 / 𝐿 ) ∈ ℝ )
8		simprl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → 𝐿 ∈ ℤ )
9		simpl	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → 𝐾 ∈ ℤ )
10		dvdsval2	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝐿 ∥ 𝐾 ↔ ( 𝐾 / 𝐿 ) ∈ ℤ ) )
11	8 5 9 10	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → ( 𝐿 ∥ 𝐾 ↔ ( 𝐾 / 𝐿 ) ∈ ℤ ) )
12	11	notbid	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ) → ( ¬ 𝐿 ∥ 𝐾 ↔ ¬ ( 𝐾 / 𝐿 ) ∈ ℤ ) )
13	12	biimp3a	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ∧ ¬ 𝐿 ∥ 𝐾 ) → ¬ ( 𝐾 / 𝐿 ) ∈ ℤ )
14		flltnz	⊢ ( ( ( 𝐾 / 𝐿 ) ∈ ℝ ∧ ¬ ( 𝐾 / 𝐿 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝐾 / 𝐿 ) )
15	7 13 14	syl2anc	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝐿 ≠ 0 ) ∧ ¬ 𝐿 ∥ 𝐾 ) → ( ⌊ ‘ ( 𝐾 / 𝐿 ) ) < ( 𝐾 / 𝐿 ) )