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

Metamath Proof Explorer

Theorem modadd2mod

Description: The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Assertion modadd2mod ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
2 1 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
3 modcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
4 3 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
5 4 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
6 2 5 addcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) = ( ( 𝐴 mod 𝑀 ) + 𝐵 ) )
7 6 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( ( 𝐴 mod 𝑀 ) + 𝐵 ) mod 𝑀 ) )
8 modaddmod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 𝐵 ) mod 𝑀 ) = ( ( 𝐴 + 𝐵 ) mod 𝑀 ) )
9 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
10 addcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
11 9 1 10 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
12 11 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
13 12 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
14 7 8 13 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )