Description: Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | modxai.1 | ⊢ 𝑁 ∈ ℕ | |
| modxai.2 | ⊢ 𝐴 ∈ ℕ | ||
| modxai.3 | ⊢ 𝐵 ∈ ℕ0 | ||
| modxai.4 | ⊢ 𝐷 ∈ ℤ | ||
| modxai.5 | ⊢ 𝐾 ∈ ℕ0 | ||
| modxai.6 | ⊢ 𝑀 ∈ ℕ0 | ||
| mod2xi.9 | ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 ) | ||
| mod2xi.7 | ⊢ ( 2 · 𝐵 ) = 𝐸 | ||
| mod2xi.8 | ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 ) | ||
| Assertion | mod2xi | ⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 ) |
| 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 | mod2xi.9 | ⊢ ( ( 𝐴 ↑ 𝐵 ) mod 𝑁 ) = ( 𝐾 mod 𝑁 ) | |
| 8 | mod2xi.7 | ⊢ ( 2 · 𝐵 ) = 𝐸 | |
| 9 | mod2xi.8 | ⊢ ( ( 𝐷 · 𝑁 ) + 𝑀 ) = ( 𝐾 · 𝐾 ) | |
| 10 | 3 | nn0cni | ⊢ 𝐵 ∈ ℂ |
| 11 | 10 | 2timesi | ⊢ ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) |
| 12 | 11 8 | eqtr3i | ⊢ ( 𝐵 + 𝐵 ) = 𝐸 |
| 13 | 1 2 3 4 5 6 3 5 7 7 12 9 | modxai | ⊢ ( ( 𝐴 ↑ 𝐸 ) mod 𝑁 ) = ( 𝑀 mod 𝑁 ) |