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

Metamath Proof Explorer

Theorem modexp

Description: Exponentiation property of the modulo operation, see theorem 5.2(c) in ApostolNT p. 107. (Contributed by Mario Carneiro, 28-Feb-2014)

Ref Expression
Assertion modexp ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝐶 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝐶 ) mod 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simp2l ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → 𝐶 ∈ ℕ0 )
2 id ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) )
3 2 3adant2l ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) )
4 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 0 ) )
5 4 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐴 ↑ 0 ) mod 𝐷 ) )
6 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐵 ↑ 𝑥 ) = ( 𝐵 ↑ 0 ) )
7 6 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 0 ) mod 𝐷 ) )
8 5 7 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ↔ ( ( 𝐴 ↑ 0 ) mod 𝐷 ) = ( ( 𝐵 ↑ 0 ) mod 𝐷 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ) ↔ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 0 ) mod 𝐷 ) = ( ( 𝐵 ↑ 0 ) mod 𝐷 ) ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑘 ) )
11 10 oveq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) )
12 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ↑ 𝑥 ) = ( 𝐵 ↑ 𝑘 ) )
13 12 oveq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) )
14 11 13 eqeq12d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ↔ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) )
15 14 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ) ↔ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) ) )
16 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
17 16 oveq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) )
18 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐵 ↑ 𝑥 ) = ( 𝐵 ↑ ( 𝑘 + 1 ) ) )
19 18 oveq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) )
20 17 19 eqeq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ↔ ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) ) )
21 20 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ) ↔ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) ) ) )
22 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝐶 ) )
23 22 oveq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐴 ↑ 𝐶 ) mod 𝐷 ) )
24 oveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 ↑ 𝑥 ) = ( 𝐵 ↑ 𝐶 ) )
25 24 oveq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝐶 ) mod 𝐷 ) )
26 23 25 eqeq12d ⊢ ( 𝑥 = 𝐶 → ( ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ↔ ( ( 𝐴 ↑ 𝐶 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝐶 ) mod 𝐷 ) ) )
27 26 imbi2d ⊢ ( 𝑥 = 𝐶 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑥 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑥 ) mod 𝐷 ) ) ↔ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝐶 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝐶 ) mod 𝐷 ) ) ) )
28 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
29 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
30 28 29 syl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 0 ) = 1 )
31 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
32 exp0 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 0 ) = 1 )
33 31 32 syl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 0 ) = 1 )
34 33 eqcomd ⊢ ( 𝐵 ∈ ℤ → 1 = ( 𝐵 ↑ 0 ) )
35 30 34 sylan9eq ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 0 ) = ( 𝐵 ↑ 0 ) )
36 35 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ↑ 0 ) mod 𝐷 ) = ( ( 𝐵 ↑ 0 ) mod 𝐷 ) )
37 36 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 0 ) mod 𝐷 ) = ( ( 𝐵 ↑ 0 ) mod 𝐷 ) )
38 simp21l ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → 𝐴 ∈ ℤ )
39 simp1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → 𝑘 ∈ ℕ0 )
40 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℤ )
41 38 39 40 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℤ )
42 simp21r ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → 𝐵 ∈ ℤ )
43 zexpcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑘 ) ∈ ℤ )
44 42 39 43 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( 𝐵 ↑ 𝑘 ) ∈ ℤ )
45 simp22 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → 𝐷 ∈ ℝ+ )
46 simp3 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) )
47 simp23 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) )
48 41 44 38 42 45 46 47 modmul12d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) mod 𝐷 ) = ( ( ( 𝐵 ↑ 𝑘 ) · 𝐵 ) mod 𝐷 ) )
49 38 zcnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → 𝐴 ∈ ℂ )
50 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
51 49 39 50 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
52 51 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) mod 𝐷 ) )
53 42 zcnd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → 𝐵 ∈ ℂ )
54 expp1 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐵 ↑ 𝑘 ) · 𝐵 ) )
55 53 39 54 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( 𝐵 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐵 ↑ 𝑘 ) · 𝐵 ) )
56 55 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( ( 𝐵 ↑ 𝑘 ) · 𝐵 ) mod 𝐷 ) )
57 48 52 56 3eqtr4d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) ∧ ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) )
58 57 3exp ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) ) ) )
59 58 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝑘 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝑘 ) mod 𝐷 ) ) → ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) = ( ( 𝐵 ↑ ( 𝑘 + 1 ) ) mod 𝐷 ) ) ) )
60 9 15 21 27 37 59 nn0ind ⊢ ( 𝐶 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐷 ∈ ℝ+ ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝐶 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝐶 ) mod 𝐷 ) ) )
61 1 3 60 sylc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 ↑ 𝐶 ) mod 𝐷 ) = ( ( 𝐵 ↑ 𝐶 ) mod 𝐷 ) )