flpmodeq

Description: Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018)

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

Step	Hyp	Ref	Expression
1		modvalr	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - ⌊\frac{A}{B}⌋ B$
2	1	eqcomd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A - ⌊\frac{A}{B}⌋ B = A \mod B$
3		recn	$⊢ A \in ℝ \to A \in ℂ$
4	3	adantr	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \in ℂ$
5		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
6		flcl	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℤ$
7	6	zcnd	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℂ$
8	5 7	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℂ$
9		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
10	9	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℂ$
11	8 10	mulcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B \in ℂ$
12		modcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℝ$
13	12	recnd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B \in ℂ$
14	4 11 13	subaddd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A - ⌊\frac{A}{B}⌋ B = A \mod B \leftrightarrow ⌊\frac{A}{B}⌋ B + (A \mod B) = A)$
15	2 14	mpbid	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ B + (A \mod B) = A$

Metamath Proof Explorer