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 ) )