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

Metamath Proof Explorer

Theorem modadd12d

Description: Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses modadd12d.1 
|- ( ph -> A e. RR )
modadd12d.2 
|- ( ph -> B e. RR )
modadd12d.3 
|- ( ph -> C e. RR )
modadd12d.4 
|- ( ph -> D e. RR )
modadd12d.5 
|- ( ph -> E e. RR+ )
modadd12d.6 
|- ( ph -> ( A mod E ) = ( B mod E ) )
modadd12d.7 
|- ( ph -> ( C mod E ) = ( D mod E ) )
Assertion modadd12d 
|- ( ph -> ( ( A + C ) mod E ) = ( ( B + D ) mod E ) )

Proof

Step Hyp Ref Expression
1 modadd12d.1 
 |-  ( ph -> A e. RR )
2 modadd12d.2 
 |-  ( ph -> B e. RR )
3 modadd12d.3 
 |-  ( ph -> C e. RR )
4 modadd12d.4 
 |-  ( ph -> D e. RR )
5 modadd12d.5 
 |-  ( ph -> E e. RR+ )
6 modadd12d.6 
 |-  ( ph -> ( A mod E ) = ( B mod E ) )
7 modadd12d.7 
 |-  ( ph -> ( C mod E ) = ( D mod E ) )
8 modadd1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ E e. RR+ ) /\ ( A mod E ) = ( B mod E ) ) -> ( ( A + C ) mod E ) = ( ( B + C ) mod E ) )
9 1 2 3 5 6 8 syl221anc 
 |-  ( ph -> ( ( A + C ) mod E ) = ( ( B + C ) mod E ) )
10 2 recnd 
 |-  ( ph -> B e. CC )
11 3 recnd 
 |-  ( ph -> C e. CC )
12 10 11 addcomd 
 |-  ( ph -> ( B + C ) = ( C + B ) )
13 12 oveq1d 
 |-  ( ph -> ( ( B + C ) mod E ) = ( ( C + B ) mod E ) )
14 modadd1 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( B e. RR /\ E e. RR+ ) /\ ( C mod E ) = ( D mod E ) ) -> ( ( C + B ) mod E ) = ( ( D + B ) mod E ) )
15 3 4 2 5 7 14 syl221anc 
 |-  ( ph -> ( ( C + B ) mod E ) = ( ( D + B ) mod E ) )
16 4 recnd 
 |-  ( ph -> D e. CC )
17 16 10 addcomd 
 |-  ( ph -> ( D + B ) = ( B + D ) )
18 17 oveq1d 
 |-  ( ph -> ( ( D + B ) mod E ) = ( ( B + D ) mod E ) )
19 13 15 18 3eqtrd 
 |-  ( ph -> ( ( B + C ) mod E ) = ( ( B + D ) mod E ) )
20 9 19 eqtrd 
 |-  ( ph -> ( ( A + C ) mod E ) = ( ( B + D ) mod E ) )