Theorem muladdmodid

Description: The sum of a positive real number less than an upper bound and the product of an integer and the upper bound is the positive real number modulo the upper bound. (Contributed by AV, 5-Jul-2020)

	Ref	Expression
Assertion	muladdmodid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ∧ 𝐴 ∈ ( 0 [,) 𝑀 ) ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( 𝑀 ∈ ℝ+ → 0 ∈ ℝ )
2		rpxr	⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ∈ ℝ* )
3		elico2	⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ* ) → ( 𝐴 ∈ ( 0 [,) 𝑀 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) )
4	1 2 3	syl2anc	⊢ ( 𝑀 ∈ ℝ+ → ( 𝐴 ∈ ( 0 [,) 𝑀 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) )
5	4	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 ∈ ( 0 [,) 𝑀 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) )
6		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7		rpcn	⊢ ( 𝑀 ∈ ℝ+ → 𝑀 ∈ ℂ )
8		mulcl	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁 · 𝑀 ) ∈ ℂ )
9	6 7 8	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝑁 · 𝑀 ) ∈ ℂ )
10	9	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( 𝑁 · 𝑀 ) ∈ ℂ )
11		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
12	11	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) → 𝐴 ∈ ℂ )
13	12	adantl	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → 𝐴 ∈ ℂ )
14	10 13	addcomd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( ( 𝑁 · 𝑀 ) + 𝐴 ) = ( 𝐴 + ( 𝑁 · 𝑀 ) ) )
15	14	oveq1d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = ( ( 𝐴 + ( 𝑁 · 𝑀 ) ) mod 𝑀 ) )
16		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) → 𝐴 ∈ ℝ )
17	16	adantl	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → 𝐴 ∈ ℝ )
18		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ+ )
19	18	adantr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → 𝑀 ∈ ℝ+ )
20		simpll	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → 𝑁 ∈ ℤ )
21		modcyc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( 𝑁 · 𝑀 ) ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
22	17 19 20 21	syl3anc	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( ( 𝐴 + ( 𝑁 · 𝑀 ) ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
23	18 16	anim12ci	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
24		3simpc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) )
25	24	adantl	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) )
26		modid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( 𝐴 mod 𝑀 ) = 𝐴 )
27	23 25 26	syl2anc	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( 𝐴 mod 𝑀 ) = 𝐴 )
28	15 22 27	3eqtrd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 )
29	28	ex	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 ) )
30	5 29	sylbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 ∈ ( 0 [,) 𝑀 ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 ) )
31	30	3impia	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ∧ 𝐴 ∈ ( 0 [,) 𝑀 ) ) → ( ( ( 𝑁 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 )