fermltl

Description: Fermat's little theorem. When P is prime, A ^ P == A (mod P ) for any A , see theorem 5.19 in ApostolNT p. 114. (Contributed by Mario Carneiro, 28-Feb-2014) (Proof shortened by AV, 19-Mar-2022)

		Ref	Expression
	Assertion	fermltl	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P} \mod P = A \mod P$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2		dvdsmodexp	$⊢ (P \in ℕ \land P \in ℕ \land P ∥ A) \to A^{P} \mod P = A \mod P$
3	2	3exp	$⊢ P \in ℕ \to (P \in ℕ \to (P ∥ A \to A^{P} \mod P = A \mod P))$
4	1 1 3	sylc	$⊢ P \in ℙ \to (P ∥ A \to A^{P} \mod P = A \mod P)$
5	4	adantr	$⊢ (P \in ℙ \land A \in ℤ) \to (P ∥ A \to A^{P} \mod P = A \mod P)$
6		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
7		prmz	$⊢ P \in ℙ \to P \in ℤ$
8		gcdcom	$⊢ (P \in ℤ \land A \in ℤ) \to P \gcd A = A \gcd P$
9	7 8	sylan	$⊢ (P \in ℙ \land A \in ℤ) \to P \gcd A = A \gcd P$
10	9	eqeq1d	$⊢ (P \in ℙ \land A \in ℤ) \to (P \gcd A = 1 \leftrightarrow A \gcd P = 1)$
11	6 10	bitrd	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow A \gcd P = 1)$
12		simp2	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A \in ℤ$
13	1	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to P \in ℕ$
14	13	phicld	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to ϕ (P) \in ℕ$
15	14	nnnn0d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to ϕ (P) \in ℕ_{0}$
16		zexpcl	$⊢ (A \in ℤ \land ϕ (P) \in ℕ_{0}) \to A^{ϕ (P)} \in ℤ$
17	12 15 16	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \in ℤ$
18	17	zred	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \in ℝ$
19		1red	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to 1 \in ℝ$
20	13	nnrpd	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to P \in ℝ^{+}$
21		eulerth	$⊢ (P \in ℕ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \mod P = 1 \mod P$
22	1 21	syl3an1	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \mod P = 1 \mod P$
23		modmul1	$⊢ ((A^{ϕ (P)} \in ℝ \land 1 \in ℝ) \land (A \in ℤ \land P \in ℝ^{+}) \land A^{ϕ (P)} \mod P = 1 \mod P) \to A^{ϕ (P)} A \mod P = 1 A \mod P$
24	18 19 12 20 22 23	syl221anc	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} A \mod P = 1 A \mod P$
25		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
26	25	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to ϕ (P) = P - 1$
27	26	oveq2d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} = A^{P - 1}$
28	27	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} A = A^{P - 1} A$
29	12	zcnd	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A \in ℂ$
30		expm1t	$⊢ (A \in ℂ \land P \in ℕ) \to A^{P} = A^{P - 1} A$
31	29 13 30	syl2anc	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{P} = A^{P - 1} A$
32	28 31	eqtr4d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} A = A^{P}$
33	32	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} A \mod P = A^{P} \mod P$
34	29	mulid2d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to 1 A = A$
35	34	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to 1 A \mod P = A \mod P$
36	24 33 35	3eqtr3d	$⊢ (P \in ℙ \land A \in ℤ \land A \gcd P = 1) \to A^{P} \mod P = A \mod P$
37	36	3expia	$⊢ (P \in ℙ \land A \in ℤ) \to (A \gcd P = 1 \to A^{P} \mod P = A \mod P)$
38	11 37	sylbid	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \to A^{P} \mod P = A \mod P)$
39	5 38	pm2.61d	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P} \mod P = A \mod P$

Metamath Proof Explorer

Theorem fermltl

Proof