dvdsmodexp

Description: If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl ). (Contributed by Mario Carneiro, 28-Feb-2014) (Revised by AV, 19-Mar-2022)

		Ref	Expression
	Assertion	dvdsmodexp	$⊢ (N \in ℕ \land B \in ℕ \land N ∥ A) \to A^{B} \mod N = A \mod N$

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	$⊢ N ∥ A \to (N \in ℤ \land A \in ℤ)$
2		dvdsmod0	$⊢ (N \in ℕ \land N ∥ A) \to A \mod N = 0$
3	2	3ad2antl2	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land N ∥ A) \to A \mod N = 0$
4	3	ex	$⊢ (A \in ℤ \land N \in ℕ \land B \in ℕ) \to (N ∥ A \to A \mod N = 0)$
5		simpl3	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to B \in ℕ$
6	5	0expd	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to 0^{B} = 0$
7	6	oveq1d	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to 0^{B} \mod N = 0 \mod N$
8		simpl1	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to A \in ℤ$
9		0zd	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to 0 \in ℤ$
10		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
11	10	3ad2ant3	$⊢ (A \in ℤ \land N \in ℕ \land B \in ℕ) \to B \in ℕ_{0}$
12	11	adantr	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to B \in ℕ_{0}$
13		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
14	13	3ad2ant2	$⊢ (A \in ℤ \land N \in ℕ \land B \in ℕ) \to N \in ℝ^{+}$
15	14	adantr	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to N \in ℝ^{+}$
16		simpr	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to A \mod N = 0$
17		0mod	$⊢ N \in ℝ^{+} \to 0 \mod N = 0$
18	15 17	syl	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to 0 \mod N = 0$
19	16 18	eqtr4d	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to A \mod N = 0 \mod N$
20		modexp	$⊢ ((A \in ℤ \land 0 \in ℤ) \land (B \in ℕ_{0} \land N \in ℝ^{+}) \land A \mod N = 0 \mod N) \to A^{B} \mod N = 0^{B} \mod N$
21	8 9 12 15 19 20	syl221anc	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to A^{B} \mod N = 0^{B} \mod N$
22	7 21 19	3eqtr4d	$⊢ ((A \in ℤ \land N \in ℕ \land B \in ℕ) \land A \mod N = 0) \to A^{B} \mod N = A \mod N$
23	22	ex	$⊢ (A \in ℤ \land N \in ℕ \land B \in ℕ) \to (A \mod N = 0 \to A^{B} \mod N = A \mod N)$
24	4 23	syld	$⊢ (A \in ℤ \land N \in ℕ \land B \in ℕ) \to (N ∥ A \to A^{B} \mod N = A \mod N)$
25	24	3exp	$⊢ A \in ℤ \to (N \in ℕ \to (B \in ℕ \to (N ∥ A \to A^{B} \mod N = A \mod N)))$
26	25	com24	$⊢ A \in ℤ \to (N ∥ A \to (B \in ℕ \to (N \in ℕ \to A^{B} \mod N = A \mod N)))$
27	26	adantl	$⊢ (N \in ℤ \land A \in ℤ) \to (N ∥ A \to (B \in ℕ \to (N \in ℕ \to A^{B} \mod N = A \mod N)))$
28	1 27	mpcom	$⊢ N ∥ A \to (B \in ℕ \to (N \in ℕ \to A^{B} \mod N = A \mod N))$
29	28	3imp31	$⊢ (N \in ℕ \land B \in ℕ \land N ∥ A) \to A^{B} \mod N = A \mod N$

Metamath Proof Explorer

Theorem dvdsmodexp

Proof