Theorem modsubi

Description: Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	modsubi.1	|- N e. NN
	modsubi.2	|- A e. NN
	modsubi.3	|- B e. NN0
	modsubi.4	|- M e. NN0
	modsubi.6	|- ( A mod N ) = ( K mod N )
	modsubi.5	|- ( M + B ) = K
Assertion	modsubi	|- ( ( A - B ) mod N ) = ( M mod N )

Proof

Step	Hyp	Ref	Expression
1		modsubi.1	|- N e. NN
2		modsubi.2	|- A e. NN
3		modsubi.3	|- B e. NN0
4		modsubi.4	|- M e. NN0
5		modsubi.6	|- ( A mod N ) = ( K mod N )
6		modsubi.5	|- ( M + B ) = K
7	2	nnrei	|- A e. RR
8	4 3	nn0addcli	|- ( M + B ) e. NN0
9	8	nn0rei	|- ( M + B ) e. RR
10	6 9	eqeltrri	|- K e. RR
11	7 10	pm3.2i	|- ( A e. RR /\ K e. RR )
12	3	nn0rei	|- B e. RR
13	12	renegcli	|- -u B e. RR
14		nnrp	|- ( N e. NN -> N e. RR+ )
15	1 14	ax-mp	|- N e. RR+
16	13 15	pm3.2i	|- ( -u B e. RR /\ N e. RR+ )
17		modadd1	|- ( ( ( A e. RR /\ K e. RR ) /\ ( -u B e. RR /\ N e. RR+ ) /\ ( A mod N ) = ( K mod N ) ) -> ( ( A + -u B ) mod N ) = ( ( K + -u B ) mod N ) )
18	11 16 5 17	mp3an	|- ( ( A + -u B ) mod N ) = ( ( K + -u B ) mod N )
19	2	nncni	|- A e. CC
20	3	nn0cni	|- B e. CC
21	19 20	negsubi	|- ( A + -u B ) = ( A - B )
22	21	oveq1i	|- ( ( A + -u B ) mod N ) = ( ( A - B ) mod N )
23	10	recni	|- K e. CC
24	23 20	negsubi	|- ( K + -u B ) = ( K - B )
25	4	nn0cni	|- M e. CC
26	23 20 25	subadd2i	|- ( ( K - B ) = M <-> ( M + B ) = K )
27	6 26	mpbir	|- ( K - B ) = M
28	24 27	eqtri	|- ( K + -u B ) = M
29	28	oveq1i	|- ( ( K + -u B ) mod N ) = ( M mod N )
30	18 22 29	3eqtr3i	|- ( ( A - B ) mod N ) = ( M mod N )