Metamath Proof Explorer

Theorem modmuladdim

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

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

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2		modelico	$⊢ (A \in ℝ \land M \in ℝ^{+}) \to A \mod M \in [0, M)$
3	1 2	sylan	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \mod M \in [0, M)$
4	3	adantr	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land A \mod M = B) \to A \mod M \in [0, M)$
5		eleq1	$⊢ A \mod M = B \to (A \mod M \in [0, M) \leftrightarrow B \in [0, M))$
6	5	adantl	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land A \mod M = B) \to (A \mod M \in [0, M) \leftrightarrow B \in [0, M))$
7	4 6	mpbid	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land A \mod M = B) \to B \in [0, M)$
8		simpll	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land B \in [0, M)) \to A \in ℤ$
9		simpr	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land B \in [0, M)) \to B \in [0, M)$
10		simpr	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \in ℝ^{+}$
11	10	adantr	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land B \in [0, M)) \to M \in ℝ^{+}$
12		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)$
13	8 9 11 12	syl3anc	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land B \in [0, M)) \to (A \mod M = B \leftrightarrow \exists k \in ℤ A = k \cdot M + B)$
14	13	biimpd	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land B \in [0, M)) \to (A \mod M = B \to \exists k \in ℤ A = k \cdot M + B)$
15	14	impancom	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land A \mod M = B) \to (B \in [0, M) \to \exists k \in ℤ A = k \cdot M + B)$
16	7 15	mpd	$⊢ ((A \in ℤ \land M \in ℝ^{+}) \land A \mod M = B) \to \exists k \in ℤ A = k \cdot M + B$
17	16	ex	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to (A \mod M = B \to \exists k \in ℤ A = k \cdot M + B)$