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

Metamath Proof Explorer

Theorem modsubi

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

Ref Expression
Hypotheses modsubi.1 ⊢ N ∈ ℕ
modsubi.2 ⊢ A ∈ ℕ
modsubi.3 ⊢ B ∈ ℕ 0
modsubi.4 ⊢ M ∈ ℕ 0
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 ∈ ℕ
2 modsubi.2 ⊢ A ∈ ℕ
3 modsubi.3 ⊢ B ∈ ℕ 0
4 modsubi.4 ⊢ M ∈ ℕ 0
5 modsubi.6 ⊢ A mod N = K mod N
6 modsubi.5 ⊢ M + B = K
7 2 nnrei ⊢ A ∈ ℝ
8 4 3 nn0addcli ⊢ M + B ∈ ℕ 0
9 8 nn0rei ⊢ M + B ∈ ℝ
10 6 9 eqeltrri ⊢ K ∈ ℝ
11 7 10 pm3.2i ⊢ A ∈ ℝ ∧ K ∈ ℝ
12 3 nn0rei ⊢ B ∈ ℝ
13 12 renegcli ⊢ − B ∈ ℝ
14 nnrp ⊢ N ∈ ℕ → N ∈ ℝ +
15 1 14 ax-mp ⊢ N ∈ ℝ +
16 13 15 pm3.2i ⊢ − B ∈ ℝ ∧ N ∈ ℝ +
17 modadd1 ⊢ A ∈ ℝ ∧ K ∈ ℝ ∧ − B ∈ ℝ ∧ N ∈ ℝ + ∧ A mod N = K mod N → A + − B mod N = K + − B mod N
18 11 16 5 17 mp3an ⊢ A + − B mod N = K + − B mod N
19 2 nncni ⊢ A ∈ ℂ
20 3 nn0cni ⊢ B ∈ ℂ
21 19 20 negsubi ⊢ A + − B = A − B
22 21 oveq1i ⊢ A + − B mod N = A − B mod N
23 10 recni ⊢ K ∈ ℂ
24 23 20 negsubi ⊢ K + − B = K − B
25 4 nn0cni ⊢ M ∈ ℂ
26 23 20 25 subadd2i ⊢ K − B = M ↔ M + B = K
27 6 26 mpbir ⊢ K − B = M
28 24 27 eqtri ⊢ K + − B = M
29 28 oveq1i ⊢ K + − B mod N = M mod N
30 18 22 29 3eqtr3i ⊢ A − B mod N = M mod N