vfermltlALT

Description: Alternate proof of vfermltl , not using Euler's theorem. (Contributed by AV, 21-Aug-2020) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		2m1e1	$⊢ 2 - 1 = 1$
2	1	a1i	$⊢ P \in ℙ \to 2 - 1 = 1$
3	2	eqcomd	$⊢ P \in ℙ \to 1 = 2 - 1$
4	3	oveq2d	$⊢ P \in ℙ \to P - 1 = P - (2 - 1)$
5		prmz	$⊢ P \in ℙ \to P \in ℤ$
6	5	zcnd	$⊢ P \in ℙ \to P \in ℂ$
7		2cnd	$⊢ P \in ℙ \to 2 \in ℂ$
8		1cnd	$⊢ P \in ℙ \to 1 \in ℂ$
9	6 7 8	subsubd	$⊢ P \in ℙ \to P - (2 - 1) = P - 2 + 1$
10	4 9	eqtrd	$⊢ P \in ℙ \to P - 1 = P - 2 + 1$
11	10	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - 1 = P - 2 + 1$
12	11	oveq2d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} = A^{P - 2 + 1}$
13		zcn	$⊢ A \in ℤ \to A \in ℂ$
14	13	3ad2ant2	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \in ℂ$
15		prmm2nn0	$⊢ P \in ℙ \to P - 2 \in ℕ_{0}$
16	15	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P - 2 \in ℕ_{0}$
17	14 16	expp1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2 + 1} = A^{P - 2} A$
18	12 17	eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} = A^{P - 2} A$
19	18	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} \mod P = A^{P - 2} A \mod P$
20	15	anim1i	$⊢ (P \in ℙ \land A \in ℤ) \to (P - 2 \in ℕ_{0} \land A \in ℤ)$
21	20	ancomd	$⊢ (P \in ℙ \land A \in ℤ) \to (A \in ℤ \land P - 2 \in ℕ_{0})$
22		zexpcl	$⊢ (A \in ℤ \land P - 2 \in ℕ_{0}) \to A^{P - 2} \in ℤ$
23	21 22	syl	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \in ℤ$
24	23	zred	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \in ℝ$
25	24	3adant3	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 2} \in ℝ$
26		simp2	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A \in ℤ$
27		prmnn	$⊢ P \in ℙ \to P \in ℕ$
28	27	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
29	28	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to P \in ℝ^{+}$
30		modmulmod	$⊢ (A^{P - 2} \in ℝ \land A \in ℤ \land P \in ℝ^{+}) \to (A^{P - 2} \mod P) A \mod P = A^{P - 2} A \mod P$
31	25 26 29 30	syl3anc	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (A^{P - 2} \mod P) A \mod P = A^{P - 2} A \mod P$
32		zre	$⊢ A \in ℤ \to A \in ℝ$
33	32	adantl	$⊢ (P \in ℙ \land A \in ℤ) \to A \in ℝ$
34	15	adantr	$⊢ (P \in ℙ \land A \in ℤ) \to P - 2 \in ℕ_{0}$
35	33 34	reexpcld	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \in ℝ$
36	28	adantr	$⊢ (P \in ℙ \land A \in ℤ) \to P \in ℝ^{+}$
37	35 36	modcld	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \mod P \in ℝ$
38	37	recnd	$⊢ (P \in ℙ \land A \in ℤ) \to A^{P - 2} \mod P \in ℂ$
39	13	adantl	$⊢ (P \in ℙ \land A \in ℤ) \to A \in ℂ$
40	38 39	mulcomd	$⊢ (P \in ℙ \land A \in ℤ) \to (A^{P - 2} \mod P) A = A (A^{P - 2} \mod P)$
41	40	3adant3	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (A^{P - 2} \mod P) A = A (A^{P - 2} \mod P)$
42	41	oveq1d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to (A^{P - 2} \mod P) A \mod P = A (A^{P - 2} \mod P) \mod P$
43	19 31 42	3eqtr2d	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} \mod P = A (A^{P - 2} \mod P) \mod P$
44		eqid	$⊢ A^{P - 2} \mod P = A^{P - 2} \mod P$
45	44	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)$
46	45	simprd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A (A^{P - 2} \mod P) \mod P = 1$
47	43 46	eqtrd	$⊢ (P \in ℙ \land A \in ℤ \land \neg P ∥ A) \to A^{P - 1} \mod P = 1$

Metamath Proof Explorer

Theorem vfermltlALT

Proof