This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑀 ) = 𝐴 )