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		oveq1	$⊢ k = ⌊\frac{A}{M}⌋ \to k \cdot M = ⌊\frac{A}{M}⌋ \cdot M$
2	1	oveq1d	$⊢ k = ⌊\frac{A}{M}⌋ \to k \cdot M + (A \mod M) = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M)$
3	2	eqeq2d	$⊢ k = ⌊\frac{A}{M}⌋ \to (A = k \cdot M + (A \mod M) \leftrightarrow A = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M))$
4		zre	$⊢ A \in ℤ \to A \in ℝ$
5	4	adantr	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \in ℝ$
6		rpre	$⊢ M \in ℝ^{+} \to M \in ℝ$
7	6	adantl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \in ℝ$
8		rpne0	$⊢ M \in ℝ^{+} \to M \neq 0$
9	8	adantl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \neq 0$
10	5 7 9	redivcld	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to \frac{A}{M} \in ℝ$
11	10	flcld	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \in ℤ$
12	11	3adant2	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \in ℤ$
13		flpmodeq	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \cdot M + (A \mod M) = A$
14	4 13	sylan	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to ⌊\frac{A}{M}⌋ \cdot M + (A \mod M) = A$
15	14	eqcomd	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M)$
16	15	3adant2	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to A = ⌊\frac{A}{M}⌋ \cdot M + (A \mod M)$
17	3 12 16	rspcedvdw	$⊢ (A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \to \exists k \in ℤ A = k \cdot M + (A \mod M)$
18		oveq2	$⊢ B = A \mod M \to k \cdot M + B = k \cdot M + (A \mod M)$
19	18	eqeq2d	$⊢ B = A \mod M \to (A = k \cdot M + B \leftrightarrow A = k \cdot M + (A \mod M))$
20	19	eqcoms	$⊢ A \mod M = B \to (A = k \cdot M + B \leftrightarrow A = k \cdot M + (A \mod M))$
21	20	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))$
22	17 21	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)$
23		oveq1	$⊢ A = k \cdot M + B \to A \mod M = (k \cdot M + B) \mod M$
24		simpr	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to k \in ℤ$
25		simpl3	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to M \in ℝ^{+}$
26		simpl2	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to B \in [0, M)$
27		muladdmodid	$⊢ (k \in ℤ \land M \in ℝ^{+} \land B \in [0, M)) \to (k \cdot M + B) \mod M = B$
28	24 25 26 27	syl3anc	$⊢ ((A \in ℤ \land B \in [0, M) \land M \in ℝ^{+}) \land k \in ℤ) \to (k \cdot M + B) \mod M = B$
29	23 28	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$
30	29	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)$
31	22 30	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