Theorem modsubi

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

	Ref	Expression
Hypotheses	modsubi.1	⊢ 𝑁 ∈ ℕ
	modsubi.2	⊢ 𝐴 ∈ ℕ
	modsubi.3	⊢ 𝐵 ∈ ℕ0
	modsubi.4	⊢ 𝑀 ∈ ℕ0
	modsubi.6	⊢ ( 𝐴 mod 𝑁 ) = ( 𝐾 mod 𝑁 )
	modsubi.5	⊢ ( 𝑀 + 𝐵 ) = 𝐾
Assertion	modsubi	⊢ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		modsubi.1	⊢ 𝑁 ∈ ℕ
2		modsubi.2	⊢ 𝐴 ∈ ℕ
3		modsubi.3	⊢ 𝐵 ∈ ℕ0
4		modsubi.4	⊢ 𝑀 ∈ ℕ0
5		modsubi.6	⊢ ( 𝐴 mod 𝑁 ) = ( 𝐾 mod 𝑁 )
6		modsubi.5	⊢ ( 𝑀 + 𝐵 ) = 𝐾
7	2	nnrei	⊢ 𝐴 ∈ ℝ
8	4 3	nn0addcli	⊢ ( 𝑀 + 𝐵 ) ∈ ℕ0
9	8	nn0rei	⊢ ( 𝑀 + 𝐵 ) ∈ ℝ
10	6 9	eqeltrri	⊢ 𝐾 ∈ ℝ
11	7 10	pm3.2i	⊢ ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℝ )
12	3	nn0rei	⊢ 𝐵 ∈ ℝ
13	12	renegcli	⊢ - 𝐵 ∈ ℝ
14		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
15	1 14	ax-mp	⊢ 𝑁 ∈ ℝ+
16	13 15	pm3.2i	⊢ ( - 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ )
17		modadd1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ∧ ( - 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝑁 ) = ( 𝐾 mod 𝑁 ) ) → ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐾 + - 𝐵 ) mod 𝑁 ) )
18	11 16 5 17	mp3an	⊢ ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐾 + - 𝐵 ) mod 𝑁 )
19	2	nncni	⊢ 𝐴 ∈ ℂ
20	3	nn0cni	⊢ 𝐵 ∈ ℂ
21	19 20	negsubi	⊢ ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 )
22	21	oveq1i	⊢ ( ( 𝐴 + - 𝐵 ) mod 𝑁 ) = ( ( 𝐴 − 𝐵 ) mod 𝑁 )
23	10	recni	⊢ 𝐾 ∈ ℂ
24	23 20	negsubi	⊢ ( 𝐾 + - 𝐵 ) = ( 𝐾 − 𝐵 )
25	4	nn0cni	⊢ 𝑀 ∈ ℂ
26	23 20 25	subadd2i	⊢ ( ( 𝐾 − 𝐵 ) = 𝑀 ↔ ( 𝑀 + 𝐵 ) = 𝐾 )
27	6 26	mpbir	⊢ ( 𝐾 − 𝐵 ) = 𝑀
28	24 27	eqtri	⊢ ( 𝐾 + - 𝐵 ) = 𝑀
29	28	oveq1i	⊢ ( ( 𝐾 + - 𝐵 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )
30	18 22 29	3eqtr3i	⊢ ( ( 𝐴 − 𝐵 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )