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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
3		rpre	⊢ ( 𝑀 ∈ ℝ⁺ → 𝑀 ∈ ℝ )
4	3	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
5	2 4	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 𝑀 ) ∈ ℝ )
6		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℝ )
7		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ⁺ )
8		modaddmod	⊢ ( ( ( 𝑁 · 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( ( ( 𝑁 · 𝑀 ) mod 𝑀 ) + 𝐴 ) mod 𝑀 ) = ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) )
9	5 6 7 8	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝑁 · 𝑀 ) mod 𝑀 ) + 𝐴 ) mod 𝑀 ) = ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) )
10		pm3.22	⊢ ( ( 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) )
12		mulmod0	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝑁 · 𝑀 ) mod 𝑀 ) = 0 )
13	11 12	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 · 𝑀 ) mod 𝑀 ) = 0 )
14	13	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 · 𝑀 ) mod 𝑀 ) + 𝐴 ) = ( 0 + 𝐴 ) )
15		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
16	15	addlidd	⊢ ( 𝐴 ∈ ℝ → ( 0 + 𝐴 ) = 𝐴 )
17	16	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( 0 + 𝐴 ) = 𝐴 )
18	14 17	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 · 𝑀 ) mod 𝑀 ) + 𝐴 ) = 𝐴 )
19	18	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝑁 · 𝑀 ) mod 𝑀 ) + 𝐴 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
20	9 19	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )

Metamath Proof Explorer

Theorem muladdmod

Proof