Metamath Proof Explorer

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	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0) \land \neg L ∥ K) \to ⌊\frac{K}{L}⌋ < \frac{K}{L}$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ K \in ℤ \to K \in ℝ$
2	1	adantr	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to K \in ℝ$
3		zre	$⊢ L \in ℤ \to L \in ℝ$
4	3	ad2antrl	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to L \in ℝ$
5		simprr	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to L \neq 0$
6	2 4 5	redivcld	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to \frac{K}{L} \in ℝ$
7	6	3adant3	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0) \land \neg L ∥ K) \to \frac{K}{L} \in ℝ$
8		simprl	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to L \in ℤ$
9		simpl	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to K \in ℤ$
10		dvdsval2	$⊢ (L \in ℤ \land L \neq 0 \land K \in ℤ) \to (L ∥ K \leftrightarrow \frac{K}{L} \in ℤ)$
11	8 5 9 10	syl3anc	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to (L ∥ K \leftrightarrow \frac{K}{L} \in ℤ)$
12	11	notbid	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0)) \to (\neg L ∥ K \leftrightarrow \neg \frac{K}{L} \in ℤ)$
13	12	biimp3a	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0) \land \neg L ∥ K) \to \neg \frac{K}{L} \in ℤ$
14		flltnz	$⊢ (\frac{K}{L} \in ℝ \land \neg \frac{K}{L} \in ℤ) \to ⌊\frac{K}{L}⌋ < \frac{K}{L}$
15	7 13 14	syl2anc	$⊢ (K \in ℤ \land (L \in ℤ \land L \neq 0) \land \neg L ∥ K) \to ⌊\frac{K}{L}⌋ < \frac{K}{L}$