vfermltl

Description: Variant of Fermat's little theorem if A is not a multiple of P , see theorem 5.18 in ApostolNT p. 113. (Contributed by AV, 21-Aug-2020) (Proof shortened by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	vfermltl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} \mod P = 1$

Proof

Step	Hyp	Ref	Expression
1		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
2	1	eqcomd	$⊢ P \in ℙ \to P - 1 = ϕ (P)$
3	2	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - 1 = ϕ (P)$
4	3	oveq2d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} = A^{ϕ (P)}$
5	4	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} \mod P = A^{ϕ (P)} \mod P$
6		prmnn	$⊢ P \in ℙ \to P \in ℕ$
7	6	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℕ$
8		simp2	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \in ℤ$
9		prmz	$⊢ P \in ℙ \to P \in ℤ$
10	9	anim1ci	$⊢ (P \in ℙ \land A \in ℤ) \to (A \in ℤ \land P \in ℤ)$
11	10	3adant3	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (A \in ℤ \land P \in ℤ)$
12		gcdcom	$⊢ (A \in ℤ \land P \in ℤ) \to A \gcd P = P \gcd A$
13	11 12	syl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \gcd P = P \gcd A$
14		coprm	$⊢ (P \in ℙ \land A \in ℤ) \to (\neg P ∥ A \leftrightarrow P \gcd A = 1)$
15	14	biimp3a	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \gcd A = 1$
16	13 15	eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \gcd P = 1$
17		eulerth	$⊢ (P \in ℕ \land A \in ℤ \land A \gcd P = 1) \to A^{ϕ (P)} \mod P = 1 \mod P$
18	7 8 16 17	syl3anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{ϕ (P)} \mod P = 1 \mod P$
19	6	nnred	$⊢ P \in ℙ \to P \in ℝ$
20		prmgt1	$⊢ P \in ℙ \to 1 < P$
21	19 20	jca	$⊢ P \in ℙ \to (P \in ℝ \land 1 < P)$
22	21	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (P \in ℝ \land 1 < P)$
23		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
24	22 23	syl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to 1 \mod P = 1$
25	5 18 24	3eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} \mod P = 1$

Metamath Proof Explorer

Theorem vfermltl

Proof