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 ⊢ 𝑁 ∈ ℕ
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 𝑁 )