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