Theorem modsub12d

Description: Subtraction 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	modsub12d	|- ( 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	3	renegcld	|- ( ph -> -u C e. RR )
9	4	renegcld	|- ( ph -> -u D e. RR )
10	3 4 5 7	modnegd	|- ( ph -> ( -u C mod E ) = ( -u D mod E ) )
11	1 2 8 9 5 6 10	modadd12d	|- ( ph -> ( ( A + -u C ) mod E ) = ( ( B + -u D ) mod E ) )
12	1	recnd	|- ( ph -> A e. CC )
13	3	recnd	|- ( ph -> C e. CC )
14	12 13	negsubd	|- ( ph -> ( A + -u C ) = ( A - C ) )
15	14	oveq1d	|- ( ph -> ( ( A + -u C ) mod E ) = ( ( A - C ) mod E ) )
16	2	recnd	|- ( ph -> B e. CC )
17	4	recnd	|- ( ph -> D e. CC )
18	16 17	negsubd	|- ( ph -> ( B + -u D ) = ( B - D ) )
19	18	oveq1d	|- ( ph -> ( ( B + -u D ) mod E ) = ( ( B - D ) mod E ) )
20	11 15 19	3eqtr3d	|- ( ph -> ( ( A - C ) mod E ) = ( ( B - D ) mod E ) )