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

Metamath Proof Explorer

Theorem modaddabs

Description: Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion modaddabs ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )

Proof

Step Hyp Ref Expression
1 modcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℝ )
2 1 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℂ )
3 2 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℂ )
4 modcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℝ )
5 4 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℂ )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℂ )
7 3 6 addcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) = ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) )
8 7 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
9 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
10 4 9 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
11 10 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
12 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ+ )
13 1 12 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
14 13 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
15 modabs2 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) mod 𝐶 ) = ( 𝐵 mod 𝐶 ) )
16 15 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) mod 𝐶 ) = ( 𝐵 mod 𝐶 ) )
17 modadd1 ⊢ ( ( ( ( 𝐵 mod 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐵 mod 𝐶 ) mod 𝐶 ) = ( 𝐵 mod 𝐶 ) ) → ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐵 + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
18 11 14 16 17 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐵 + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
19 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
20 19 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
21 3 20 addcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) + 𝐵 ) = ( 𝐵 + ( 𝐴 mod 𝐶 ) ) )
22 21 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) = ( ( 𝐵 + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
23 18 22 eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) = ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) )
24 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
25 1 24 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
26 25 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
27 3simpc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
28 modabs2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) mod 𝐶 ) = ( 𝐴 mod 𝐶 ) )
29 28 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) mod 𝐶 ) = ( 𝐴 mod 𝐶 ) )
30 modadd1 ⊢ ( ( ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐴 mod 𝐶 ) mod 𝐶 ) = ( 𝐴 mod 𝐶 ) ) → ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )
31 26 27 29 30 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )
32 8 23 31 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )