powm2modprm

Description: If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to P \in ℙ$
2		simpr	$⊢ (P \in ℙ \land A \in ℤ) \to A \in ℤ$
3	2	adantr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A \in ℤ$
4		m1dvdsndvds	$⊢ (P \in ℙ \land A \in ℤ) \to (P ∥ (A - 1) \to \neg P ∥ A)$
5	4	imp	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to \neg P ∥ A$
6		eqid	$⊢ A^{P - 2} \mod P = A^{P - 2} \mod P$
7	6	modprminv	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (A^{P - 2} \mod P \in (1 \dots P - 1) \land A (A^{P - 2} \mod P) \mod P = 1)$
8		simpr	$⊢ (A^{P - 2} \mod P \in (1 \dots P - 1) \land A (A^{P - 2} \mod P) \mod P = 1) \to A (A^{P - 2} \mod P) \mod P = 1$
9	8	eqcomd	$⊢ (A^{P - 2} \mod P \in (1 \dots P - 1) \land A (A^{P - 2} \mod P) \mod P = 1) \to 1 = A (A^{P - 2} \mod P) \mod P$
10	7 9	syl	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to 1 = A (A^{P - 2} \mod P) \mod P$
11	1 3 5 10	syl3anc	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to 1 = A (A^{P - 2} \mod P) \mod P$
12		modprm1div	$⊢ (P \in ℙ \land A \in ℤ) \to (A \mod P = 1 \leftrightarrow P ∥ (A - 1))$
13	12	biimpar	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A \mod P = 1$
14	13	oveq1d	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to (A \mod P) (A^{P - 2} \mod P) = 1 (A^{P - 2} \mod P)$
15	14	oveq1d	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to (A \mod P) (A^{P - 2} \mod P) \mod P = 1 (A^{P - 2} \mod P) \mod P$
16		zre	$⊢ A \in ℤ \to A \in ℝ$
17	16	ad2antlr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A \in ℝ$
18		prmm2nn0	$⊢ P \in ℙ \to P - 2 \in ℕ_{0}$
19	18	anim1ci	$⊢ (P \in ℙ \land A \in ℤ) \to (A \in ℤ \land P - 2 \in ℕ_{0})$
20	19	adantr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to (A \in ℤ \land P - 2 \in ℕ_{0})$
21		zexpcl	$⊢ (A \in ℤ \land P - 2 \in ℕ_{0}) \to A^{P - 2} \in ℤ$
22	20 21	syl	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A^{P - 2} \in ℤ$
23		prmnn	$⊢ P \in ℙ \to P \in ℕ$
24	23	adantr	$⊢ (P \in ℙ \land A \in ℤ) \to P \in ℕ$
25	24	adantr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to P \in ℕ$
26	22 25	zmodcld	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A^{P - 2} \mod P \in ℕ_{0}$
27	26	nn0zd	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A^{P - 2} \mod P \in ℤ$
28	23	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
29	28	adantr	$⊢ (P \in ℙ \land A \in ℤ) \to P \in ℝ^{+}$
30	29	adantr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to P \in ℝ^{+}$
31		modmulmod	$⊢ (A \in ℝ \land A^{P - 2} \mod P \in ℤ \land P \in ℝ^{+}) \to (A \mod P) (A^{P - 2} \mod P) \mod P = A (A^{P - 2} \mod P) \mod P$
32	17 27 30 31	syl3anc	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to (A \mod P) (A^{P - 2} \mod P) \mod P = A (A^{P - 2} \mod P) \mod P$
33	19 21	syl	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \in ℤ$
34	33 24	zmodcld	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \mod P \in ℕ_{0}$
35	34	nn0cnd	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \mod P \in ℂ$
36	35	mulid2d	$⊢ (P \in ℙ \land A \in ℤ) \to 1 (A^{P - 2} \mod P) = A^{P - 2} \mod P$
37	36	oveq1d	$⊢ (P \in ℙ \land A \in ℤ) \to 1 (A^{P - 2} \mod P) \mod P = (A^{P - 2} \mod P) \mod P$
38	37	adantr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to 1 (A^{P - 2} \mod P) \mod P = (A^{P - 2} \mod P) \mod P$
39		reexpcl	$⊢ (A \in ℝ \land P - 2 \in ℕ_{0}) \to A^{P - 2} \in ℝ$
40	16 18 39	syl2anr	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \in ℝ$
41	40 29	jca	$⊢ (P \in ℙ \land A \in ℤ) \to (A^{P - 2} \in ℝ \land P \in ℝ^{+})$
42	41	adantr	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to (A^{P - 2} \in ℝ \land P \in ℝ^{+})$
43		modabs2	$⊢ (A^{P - 2} \in ℝ \land P \in ℝ^{+}) \to (A^{P - 2} \mod P) \mod P = A^{P - 2} \mod P$
44	42 43	syl	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to (A^{P - 2} \mod P) \mod P = A^{P - 2} \mod P$
45	38 44	eqtrd	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to 1 (A^{P - 2} \mod P) \mod P = A^{P - 2} \mod P$
46	15 32 45	3eqtr3d	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A (A^{P - 2} \mod P) \mod P = A^{P - 2} \mod P$
47	11 46	eqtr2d	$⊢ ((P \in ℙ \land A \in ℤ) \land P ∥ (A - 1)) \to A^{P - 2} \mod P = 1$
48	47	ex	$⊢ (P \in ℙ \land A \in ℤ) \to (P ∥ (A - 1) \to A^{P - 2} \mod P = 1)$

Metamath Proof Explorer

Theorem powm2modprm

Proof