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

Metamath Proof Explorer

Theorem mod2xi

Description: Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014)

Ref Expression
Hypotheses modxai.1 ⊢ N ∈ ℕ
modxai.2 ⊢ A ∈ ℕ
modxai.3 ⊢ B ∈ ℕ 0
modxai.4 ⊢ D ∈ ℤ
modxai.5 ⊢ K ∈ ℕ 0
modxai.6 ⊢ M ∈ ℕ 0
mod2xi.9 ⊢ A B mod N = K mod N
mod2xi.7 ⊢ 2 ⁢ B = E
mod2xi.8 ⊢ D ⋅ N + M = K ⁢ K
Assertion mod2xi ⊢ A E mod N = M mod N

Proof

Step Hyp Ref Expression
1 modxai.1 ⊢ N ∈ ℕ
2 modxai.2 ⊢ A ∈ ℕ
3 modxai.3 ⊢ B ∈ ℕ 0
4 modxai.4 ⊢ D ∈ ℤ
5 modxai.5 ⊢ K ∈ ℕ 0
6 modxai.6 ⊢ M ∈ ℕ 0
7 mod2xi.9 ⊢ A B mod N = K mod N
8 mod2xi.7 ⊢ 2 ⁢ B = E
9 mod2xi.8 ⊢ D ⋅ N + M = K ⁢ K
10 3 nn0cni ⊢ B ∈ ℂ
11 10 2timesi ⊢ 2 ⁢ B = B + B
12 11 8 eqtr3i ⊢ B + B = E
13 1 2 3 4 5 6 3 5 7 7 12 9 modxai ⊢ A E mod N = M mod N