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

Metamath Proof Explorer

Theorem modxai

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

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

Proof

Step Hyp Ref Expression
1 modxai.1 ⊢ 𝑁 ∈ ℕ
2 modxai.2 ⊢ 𝐴 ∈ ℕ
3 modxai.3 ⊢ 𝐵 ∈ ℕ0
4 modxai.4 ⊢ 𝐷 ∈ ℤ
5 modxai.5 ⊢ 𝐾 ∈ ℕ0
6 modxai.6 ⊢ 𝑀 ∈ ℕ0
7 modxai.7 ⊢ 𝐶 ∈ ℕ0
8 modxai.8 ⊢ 𝐿 ∈ ℕ0
9 modxai.11 ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 )
10 modxai.12 ⊢ ( ( 𝐴 ↑ 𝐶 ) mod 𝑁 ) = ( 𝐿 mod 𝑁 )
11 modxai.9 ⊢ ( 𝐵 + 𝐶 ) = 𝐸
12 modxai.10 ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐿 )
13 11 oveq2i ⊢ ( 𝐴 ↑ ( 𝐵 + 𝐶 ) ) = ( 𝐴 ↑ 𝐸 )
14 2 nncni ⊢ 𝐴 ∈ ℂ
15 expadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) ) )
16 14 3 7 15 mp3an ⊢ ( 𝐴 ↑ ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) )
17 13 16 eqtr3i ⊢ ( 𝐴 ↑ 𝐸 ) = ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) )
18 17 oveq1i ⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) ) mod 𝑁 )
19 nnexpcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ ℕ )
20 2 3 19 mp2an ⊢ ( 𝐴 ↑ 𝐵 ) ∈ ℕ
21 20 nnzi ⊢ ( 𝐴 ↑ 𝐵 ) ∈ ℤ
22 21 a1i ⊢ ( ⊤ → ( 𝐴 ↑ 𝐵 ) ∈ ℤ )
23 5 nn0zi ⊢ 𝐾 ∈ ℤ
24 23 a1i ⊢ ( ⊤ → 𝐾 ∈ ℤ )
25 nnexpcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐶 ) ∈ ℕ )
26 2 7 25 mp2an ⊢ ( 𝐴 ↑ 𝐶 ) ∈ ℕ
27 26 nnzi ⊢ ( 𝐴 ↑ 𝐶 ) ∈ ℤ
28 27 a1i ⊢ ( ⊤ → ( 𝐴 ↑ 𝐶 ) ∈ ℤ )
29 8 nn0zi ⊢ 𝐿 ∈ ℤ
30 29 a1i ⊢ ( ⊤ → 𝐿 ∈ ℤ )
31 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
32 1 31 ax-mp ⊢ 𝑁 ∈ ℝ+
33 32 a1i ⊢ ( ⊤ → 𝑁 ∈ ℝ+ )
34 9 a1i ⊢ ( ⊤ → ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
35 10 a1i ⊢ ( ⊤ → ( ( 𝐴 ↑ 𝐶 ) mod 𝑁 ) = ( 𝐿 mod 𝑁 ) )
36 22 24 28 30 33 34 35 modmul12d ⊢ ( ⊤ → ( ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) ) mod 𝑁 ) = ( ( 𝐾 · 𝐿 ) mod 𝑁 ) )
37 36 mptru ⊢ ( ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) ) mod 𝑁 ) = ( ( 𝐾 · 𝐿 ) mod 𝑁 )
38 zcn ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
39 4 38 ax-mp ⊢ 𝐷 ∈ ℂ
40 1 nncni ⊢ 𝑁 ∈ ℂ
41 39 40 mulcli ⊢ ( 𝐷 · 𝑁 ) ∈ ℂ
42 6 nn0cni ⊢ 𝑀 ∈ ℂ
43 41 42 addcomi ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝑀 + ( 𝐷 · 𝑁 ) )
44 12 43 eqtr3i ⊢ ( 𝐾 · 𝐿 ) = ( 𝑀 + ( 𝐷 · 𝑁 ) )
45 44 oveq1i ⊢ ( ( 𝐾 · 𝐿 ) mod 𝑁 ) = ( ( 𝑀 + ( 𝐷 · 𝑁 ) ) mod 𝑁 )
46 37 45 eqtri ⊢ ( ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) ) mod 𝑁 ) = ( ( 𝑀 + ( 𝐷 · 𝑁 ) ) mod 𝑁 )
47 6 nn0rei ⊢ 𝑀 ∈ ℝ
48 modcyc ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ∧ 𝐷 ∈ ℤ ) → ( ( 𝑀 + ( 𝐷 · 𝑁 ) ) mod 𝑁 ) = ( 𝑀 mod 𝑁 ) )
49 47 32 4 48 mp3an ⊢ ( ( 𝑀 + ( 𝐷 · 𝑁 ) ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )
50 46 49 eqtri ⊢ ( ( ( 𝐴 ↑ 𝐵 ) · ( 𝐴 ↑ 𝐶 ) ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )
51 18 50 eqtri ⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 )