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 𝐷 ) )