modmuladd

Description: Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021)

		Ref	Expression
	Assertion	modmuladd	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to (A \mod M = B \leftrightarrow \exists k \in ℤ A = k \cdot M + B)$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2	1	adantr	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \in ℝ$
3		rpre	$⊢ M \in ℝ^{+} \to M \in ℝ$
4	3	adantl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \in ℝ$
5		rpne0	$⊢ M \in ℝ^{+} \to M \neq 0$
6	5	adantl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \neq 0$
7	2 4 6	redivcld	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to \frac{A}{M} \in ℝ$
8	7	flcld	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \in ℤ$
9	8	3adant2	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \in ℤ$
10		oveq1	$⊢ k = ⌊\frac{A}{M}⌋ \to k \cdot M = ⌊\frac{A}{M}⌋ \cdot M$
11	10	oveq1d	$⊢ k = ⌊\frac{A}{M}⌋ \to k \cdot M + (A \mod M) = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M)$
12	11	eqeq2d	$⊢ k = ⌊\frac{A}{M}⌋ \to (A = k \cdot M + (A \mod M) \leftrightarrow A = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M))$
13	12	adantl	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k = ⌊\frac{A}{M}⌋) \to (A = k \cdot M + (A \mod M) \leftrightarrow A = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M))$
14	1	anim1i	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to (A \in ℝ \land M \in ℝ^{+})$
15	14	3adant2	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to (A \in ℝ \land M \in ℝ^{+})$
16		flpmodeq	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \cdot M + (A \mod M) = A$
17	15 16	syl	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \cdot M + (A \mod M) = A$
18	17	eqcomd	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to A = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M)$
19	9 13 18	rspcedvd	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to \exists k \in ℤ A = k \cdot M + (A \mod M)$
20		oveq2	$⊢ B = A \mod M \to k \cdot M + B = k \cdot M + (A \mod M)$
21	20	eqeq2d	$⊢ B = A \mod M \to (A = k \cdot M + B \leftrightarrow A = k \cdot M + (A \mod M))$
22	21	eqcoms	$⊢ A \mod M = B \to (A = k \cdot M + B \leftrightarrow A = k \cdot M + (A \mod M))$
23	22	rexbidv	$⊢ A \mod M = B \to (\exists k \in ℤ A = k \cdot M + B \leftrightarrow \exists k \in ℤ A = k \cdot M + (A \mod M))$
24	19 23	syl5ibrcom	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to (A \mod M = B \to \exists k \in ℤ A = k \cdot M + B)$
25		oveq1	$⊢ A = k \cdot M + B \to A \mod M = (k \cdot M + B) \mod M$
26		simpr	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to k \in ℤ$
27		simpl3	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to M \in ℝ^{+}$
28		simpl2	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to B \in [0, M)$
29		muladdmodid	$⊢ (k \in ℤ \land M \in ℝ^{+} \land B \in [0, M)) \to (k \cdot M + B) \mod M = B$
30	26 27 28 29	syl3anc	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to (k \cdot M + B) \mod M = B$
31	25 30	sylan9eqr	$⊢ (((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \land A = k \cdot M + B) \to A \mod M = B$
32	31	rexlimdva2	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to (\exists k \in ℤ A = k \cdot M + B \to A \mod M = B)$
33	24 32	impbid	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to (A \mod M = B \leftrightarrow \exists k \in ℤ A = k \cdot M + B)$

Metamath Proof Explorer

Theorem modmuladd

Proof