Metamath Proof Explorer

Theorem fldivmod

Description: Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020)

		Ref	Expression
	Assertion	fldivmod	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ = \frac{A - (A \mod B)}{B}$

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
2	1	flcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℤ$
3	2	zcnd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℂ$
4		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
5	4	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℂ$
6	3 5	mulcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B \in ℂ$
7		modcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$
8	7	recnd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℂ$
9	6 8	pncand	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B) = ⌊\frac{A}{B}⌋ B$
10	6 8	addcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B + (A \mod B) \in ℂ$
11	10 8	subcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B) \in ℂ$
12		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
13	12	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \neq 0$
14	11 3 5 13	divmul3d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B)}{B} = ⌊\frac{A}{B}⌋ \leftrightarrow ⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B) = ⌊\frac{A}{B}⌋ B)$
15	9 14	mpbird	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B)}{B} = ⌊\frac{A}{B}⌋$
16		flpmodeq	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B + (A \mod B) = A$
17	16	oveq1d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B) = A - (A \mod B)$
18	17	oveq1d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{⌊\frac{A}{B}⌋ B + (A \mod B) - (A \mod B)}{B} = \frac{A - (A \mod B)}{B}$
19	15 18	eqtr3d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ = \frac{A - (A \mod B)}{B}$