Metamath Proof Explorer

Theorem moddifz

Description: The modulo operation differs from A by an integer multiple of B . (Contributed by Mario Carneiro, 15-Jul-2014)

		Ref	Expression
	Assertion	moddifz	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A - (A \mod B)}{B} \in ℤ$

Step	Hyp	Ref	Expression
1		moddiffl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A - (A \mod B)}{B} = ⌊\frac{A}{B}⌋$
2		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
3	2	flcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℤ$
4	1 3	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A - (A \mod B)}{B} \in ℤ$