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

Metamath Proof Explorer

Theorem mod2xnegi

Description: Version of mod2xi with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014)

Ref Expression
Hypotheses mod2xnegi.1 ⊢ 𝐴 ∈ ℕ
mod2xnegi.2 ⊢ 𝐵 ∈ ℕ0
mod2xnegi.3 ⊢ 𝐷 ∈ ℤ
mod2xnegi.4 ⊢ 𝐾 ∈ ℕ
mod2xnegi.5 ⊢ 𝑀 ∈ ℕ0
mod2xnegi.6 ⊢ 𝐿 ∈ ℕ0
mod2xnegi.10 ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐿 mod 𝑁 )
mod2xnegi.7 ⊢ ( 2 · 𝐵 ) = 𝐸
mod2xnegi.8 ⊢ ( 𝐿 + 𝐾 ) = 𝑁
mod2xnegi.9 ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 )
Assertion mod2xnegi ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )

Proof

Step Hyp Ref Expression
1 mod2xnegi.1 ⊢ 𝐴 ∈ ℕ
2 mod2xnegi.2 ⊢ 𝐵 ∈ ℕ0
3 mod2xnegi.3 ⊢ 𝐷 ∈ ℤ
4 mod2xnegi.4 ⊢ 𝐾 ∈ ℕ
5 mod2xnegi.5 ⊢ 𝑀 ∈ ℕ0
6 mod2xnegi.6 ⊢ 𝐿 ∈ ℕ0
7 mod2xnegi.10 ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐿 mod 𝑁 )
8 mod2xnegi.7 ⊢ ( 2 · 𝐵 ) = 𝐸
9 mod2xnegi.8 ⊢ ( 𝐿 + 𝐾 ) = 𝑁
10 mod2xnegi.9 ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 )
11 nn0nnaddcl ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝐿 + 𝐾 ) ∈ ℕ )
12 6 4 11 mp2an ⊢ ( 𝐿 + 𝐾 ) ∈ ℕ
13 9 12 eqeltrri ⊢ 𝑁 ∈ ℕ
14 13 nnzi ⊢ 𝑁 ∈ ℤ
15 zaddcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝑁 + 𝐷 ) ∈ ℤ )
16 14 3 15 mp2an ⊢ ( 𝑁 + 𝐷 ) ∈ ℤ
17 4 nnnn0i ⊢ 𝐾 ∈ ℕ0
18 17 17 nn0addcli ⊢ ( 𝐾 + 𝐾 ) ∈ ℕ0
19 18 nn0zi ⊢ ( 𝐾 + 𝐾 ) ∈ ℤ
20 zsubcl ⊢ ( ( ( 𝑁 + 𝐷 ) ∈ ℤ ∧ ( 𝐾 + 𝐾 ) ∈ ℤ ) → ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) ∈ ℤ )
21 16 19 20 mp2an ⊢ ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) ∈ ℤ
22 13 nncni ⊢ 𝑁 ∈ ℂ
23 zcn ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
24 3 23 ax-mp ⊢ 𝐷 ∈ ℂ
25 22 24 addcli ⊢ ( 𝑁 + 𝐷 ) ∈ ℂ
26 4 nncni ⊢ 𝐾 ∈ ℂ
27 26 26 addcli ⊢ ( 𝐾 + 𝐾 ) ∈ ℂ
28 25 27 22 subdiri ⊢ ( ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) · 𝑁 ) = ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) )
29 28 oveq1i ⊢ ( ( ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) · 𝑁 ) + 𝑀 ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) + 𝑀 )
30 25 22 mulcli ⊢ ( ( 𝑁 + 𝐷 ) · 𝑁 ) ∈ ℂ
31 5 nn0cni ⊢ 𝑀 ∈ ℂ
32 27 22 mulcli ⊢ ( ( 𝐾 + 𝐾 ) · 𝑁 ) ∈ ℂ
33 30 31 32 addsubi ⊢ ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) + 𝑀 )
34 10 oveq2i ⊢ ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) = ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) )
35 22 26 26 adddii ⊢ ( 𝑁 · ( 𝐾 + 𝐾 ) ) = ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) )
36 34 35 oveq12i ⊢ ( ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) − ( 𝑁 · ( 𝐾 + 𝐾 ) ) ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) )
37 22 24 22 adddiri ⊢ ( ( 𝑁 + 𝐷 ) · 𝑁 ) = ( ( 𝑁 · 𝑁 ) + ( 𝐷 · 𝑁 ) )
38 37 oveq1i ⊢ ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐷 · 𝑁 ) ) + 𝑀 )
39 22 22 mulcli ⊢ ( 𝑁 · 𝑁 ) ∈ ℂ
40 24 22 mulcli ⊢ ( 𝐷 · 𝑁 ) ∈ ℂ
41 39 40 31 addassi ⊢ ( ( ( 𝑁 · 𝑁 ) + ( 𝐷 · 𝑁 ) ) + 𝑀 ) = ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) )
42 38 41 eqtr2i ⊢ ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) = ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 )
43 22 27 mulcomi ⊢ ( 𝑁 · ( 𝐾 + 𝐾 ) ) = ( ( 𝐾 + 𝐾 ) · 𝑁 )
44 42 43 oveq12i ⊢ ( ( ( 𝑁 · 𝑁 ) + ( ( 𝐷 · 𝑁 ) + 𝑀 ) ) − ( 𝑁 · ( 𝐾 + 𝐾 ) ) ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) )
45 36 44 eqtr3i ⊢ ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) ) = ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) )
46 mulsub ⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ∧ ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ) → ( ( 𝑁 − 𝐾 ) · ( 𝑁 − 𝐾 ) ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) ) )
47 22 26 22 26 46 mp4an ⊢ ( ( 𝑁 − 𝐾 ) · ( 𝑁 − 𝐾 ) ) = ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) )
48 6 nn0cni ⊢ 𝐿 ∈ ℂ
49 22 26 48 subadd2i ⊢ ( ( 𝑁 − 𝐾 ) = 𝐿 ↔ ( 𝐿 + 𝐾 ) = 𝑁 )
50 9 49 mpbir ⊢ ( 𝑁 − 𝐾 ) = 𝐿
51 50 50 oveq12i ⊢ ( ( 𝑁 − 𝐾 ) · ( 𝑁 − 𝐾 ) ) = ( 𝐿 · 𝐿 )
52 47 51 eqtr3i ⊢ ( ( ( 𝑁 · 𝑁 ) + ( 𝐾 · 𝐾 ) ) − ( ( 𝑁 · 𝐾 ) + ( 𝑁 · 𝐾 ) ) ) = ( 𝐿 · 𝐿 )
53 45 52 eqtr3i ⊢ ( ( ( ( 𝑁 + 𝐷 ) · 𝑁 ) + 𝑀 ) − ( ( 𝐾 + 𝐾 ) · 𝑁 ) ) = ( 𝐿 · 𝐿 )
54 29 33 53 3eqtr2i ⊢ ( ( ( ( 𝑁 + 𝐷 ) − ( 𝐾 + 𝐾 ) ) · 𝑁 ) + 𝑀 ) = ( 𝐿 · 𝐿 )
55 13 1 2 21 6 5 7 8 54 mod2xi ⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )