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	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to A^{C} \mod D = B^{C} \mod D$

Proof

Step	Hyp	Ref	Expression
1		simp2l	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to C \in ℕ_{0}$
2		id	$⊢ ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D)$
3	2	3adant2l	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D)$
4		oveq2	$⊢ x = 0 \to A^{x} = A^{0}$
5	4	oveq1d	$⊢ x = 0 \to A^{x} \mod D = A^{0} \mod D$
6		oveq2	$⊢ x = 0 \to B^{x} = B^{0}$
7	6	oveq1d	$⊢ x = 0 \to B^{x} \mod D = B^{0} \mod D$
8	5 7	eqeq12d	$⊢ x = 0 \to (A^{x} \mod D = B^{x} \mod D \leftrightarrow A^{0} \mod D = B^{0} \mod D)$
9	8	imbi2d	$⊢ x = 0 \to ((((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{x} \mod D = B^{x} \mod D) \leftrightarrow (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{0} \mod D = B^{0} \mod D))$
10		oveq2	$⊢ x = k \to A^{x} = A^{k}$
11	10	oveq1d	$⊢ x = k \to A^{x} \mod D = A^{k} \mod D$
12		oveq2	$⊢ x = k \to B^{x} = B^{k}$
13	12	oveq1d	$⊢ x = k \to B^{x} \mod D = B^{k} \mod D$
14	11 13	eqeq12d	$⊢ x = k \to (A^{x} \mod D = B^{x} \mod D \leftrightarrow A^{k} \mod D = B^{k} \mod D)$
15	14	imbi2d	$⊢ x = k \to ((((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{x} \mod D = B^{x} \mod D) \leftrightarrow (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{k} \mod D = B^{k} \mod D))$
16		oveq2	$⊢ x = k + 1 \to A^{x} = A^{k + 1}$
17	16	oveq1d	$⊢ x = k + 1 \to A^{x} \mod D = A^{k + 1} \mod D$
18		oveq2	$⊢ x = k + 1 \to B^{x} = B^{k + 1}$
19	18	oveq1d	$⊢ x = k + 1 \to B^{x} \mod D = B^{k + 1} \mod D$
20	17 19	eqeq12d	$⊢ x = k + 1 \to (A^{x} \mod D = B^{x} \mod D \leftrightarrow A^{k + 1} \mod D = B^{k + 1} \mod D)$
21	20	imbi2d	$⊢ x = k + 1 \to ((((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{x} \mod D = B^{x} \mod D) \leftrightarrow (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{k + 1} \mod D = B^{k + 1} \mod D))$
22		oveq2	$⊢ x = C \to A^{x} = A^{C}$
23	22	oveq1d	$⊢ x = C \to A^{x} \mod D = A^{C} \mod D$
24		oveq2	$⊢ x = C \to B^{x} = B^{C}$
25	24	oveq1d	$⊢ x = C \to B^{x} \mod D = B^{C} \mod D$
26	23 25	eqeq12d	$⊢ x = C \to (A^{x} \mod D = B^{x} \mod D \leftrightarrow A^{C} \mod D = B^{C} \mod D)$
27	26	imbi2d	$⊢ x = C \to ((((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{x} \mod D = B^{x} \mod D) \leftrightarrow (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{C} \mod D = B^{C} \mod D))$
28		zcn	$⊢ A \in ℤ \to A \in ℂ$
29		exp0	$⊢ A \in ℂ \to A^{0} = 1$
30	28 29	syl	$⊢ A \in ℤ \to A^{0} = 1$
31		zcn	$⊢ B \in ℤ \to B \in ℂ$
32		exp0	$⊢ B \in ℂ \to B^{0} = 1$
33	31 32	syl	$⊢ B \in ℤ \to B^{0} = 1$
34	33	eqcomd	$⊢ B \in ℤ \to 1 = B^{0}$
35	30 34	sylan9eq	$⊢ (A \in ℤ \land B \in ℤ) \to A^{0} = B^{0}$
36	35	oveq1d	$⊢ (A \in ℤ \land B \in ℤ) \to A^{0} \mod D = B^{0} \mod D$
37	36	3ad2ant1	$⊢ ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{0} \mod D = B^{0} \mod D$
38		simp21l	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A \in ℤ$
39		simp1	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to k \in ℕ_{0}$
40		zexpcl	$⊢ (A \in ℤ \land k \in ℕ_{0}) \to A^{k} \in ℤ$
41	38 39 40	syl2anc	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A^{k} \in ℤ$
42		simp21r	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to B \in ℤ$
43		zexpcl	$⊢ (B \in ℤ \land k \in ℕ_{0}) \to B^{k} \in ℤ$
44	42 39 43	syl2anc	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to B^{k} \in ℤ$
45		simp22	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to D \in ℝ^{+}$
46		simp3	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A^{k} \mod D = B^{k} \mod D$
47		simp23	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A \mod D = B \mod D$
48	41 44 38 42 45 46 47	modmul12d	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A^{k} A \mod D = B^{k} B \mod D$
49	38	zcnd	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A \in ℂ$
50		expp1	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k + 1} = A^{k} A$
51	49 39 50	syl2anc	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A^{k + 1} = A^{k} A$
52	51	oveq1d	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A^{k + 1} \mod D = A^{k} A \mod D$
53	42	zcnd	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to B \in ℂ$
54		expp1	$⊢ (B \in ℂ \land k \in ℕ_{0}) \to B^{k + 1} = B^{k} B$
55	53 39 54	syl2anc	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to B^{k + 1} = B^{k} B$
56	55	oveq1d	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to B^{k + 1} \mod D = B^{k} B \mod D$
57	48 52 56	3eqtr4d	$⊢ (k \in ℕ_{0} \land ((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \land A^{k} \mod D = B^{k} \mod D) \to A^{k + 1} \mod D = B^{k + 1} \mod D$
58	57	3exp	$⊢ k \in ℕ_{0} \to (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to (A^{k} \mod D = B^{k} \mod D \to A^{k + 1} \mod D = B^{k + 1} \mod D))$
59	58	a2d	$⊢ k \in ℕ_{0} \to ((((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{k} \mod D = B^{k} \mod D) \to (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{k + 1} \mod D = B^{k + 1} \mod D))$
60	9 15 21 27 37 59	nn0ind	$⊢ C \in ℕ_{0} \to (((A \in ℤ \land B \in ℤ) \land D \in ℝ^{+} \land A \mod D = B \mod D) \to A^{C} \mod D = B^{C} \mod D)$
61	1 3 60	sylc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℝ^{+}) \land A \mod D = B \mod D) \to A^{C} \mod D = B^{C} \mod D$

Metamath Proof Explorer

Theorem modexp

Proof