muladdmod

Description: A real number is the sum of the number and a multiple of a positive real number modulo the positive real number. (Contributed by AV, 7-Sep-2025)

		Ref	Expression
	Assertion	muladdmod	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to (N \cdot M + A) \mod M = A \mod M$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ N \in ℤ \to N \in ℝ$
2	1	3ad2ant3	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to N \in ℝ$
3		rpre	$⊢ M \in ℝ^{+} \to M \in ℝ$
4	3	3ad2ant2	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to M \in ℝ$
5	2 4	remulcld	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to N \cdot M \in ℝ$
6		simp1	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to A \in ℝ$
7		simp2	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to M \in ℝ^{+}$
8		modaddmod	$⊢ (N \cdot M \in ℝ \land A \in ℝ \land M \in ℝ^{+}) \to ((N \cdot M \mod M) + A) \mod M = (N \cdot M + A) \mod M$
9	5 6 7 8	syl3anc	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to ((N \cdot M \mod M) + A) \mod M = (N \cdot M + A) \mod M$
10		pm3.22	$⊢ (M \in ℝ^{+} \land N \in ℤ) \to (N \in ℤ \land M \in ℝ^{+})$
11	10	3adant1	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to (N \in ℤ \land M \in ℝ^{+})$
12		mulmod0	$⊢ (N \in ℤ \land M \in ℝ^{+}) \to N \cdot M \mod M = 0$
13	11 12	syl	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to N \cdot M \mod M = 0$
14	13	oveq1d	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to (N \cdot M \mod M) + A = 0 + A$
15		recn	$⊢ A \in ℝ \to A \in ℂ$
16	15	addlidd	$⊢ A \in ℝ \to 0 + A = A$
17	16	3ad2ant1	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to 0 + A = A$
18	14 17	eqtrd	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to (N \cdot M \mod M) + A = A$
19	18	oveq1d	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to ((N \cdot M \mod M) + A) \mod M = A \mod M$
20	9 19	eqtr3d	$⊢ (A \in ℝ \land M \in ℝ^{+} \land N \in ℤ) \to (N \cdot M + A) \mod M = A \mod M$

Metamath Proof Explorer

Theorem muladdmod

Proof