fpprwppr

Description: A Fermat pseudoprime to the base N is aweak pseudoprime (see Wikipedia "Fermat pseudoprime", 29-May-2023, https://en.wikipedia.org/wiki/Fermat_pseudoprime . (Contributed by AV, 31-May-2023)

		Ref	Expression
	Assertion	fpprwppr	$⊢ X \in FPPr (N) \to N^{X} \mod X = N \mod X$

Proof

Step	Hyp	Ref	Expression
1		fpprbasnn	$⊢ X \in FPPr (N) \to N \in ℕ$
2		fpprel	$⊢ N \in ℕ \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$
3		nnz	$⊢ N \in ℕ \to N \in ℤ$
4		eluz4nn	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$
5		nnm1nn0	$⊢ X \in ℕ \to X - 1 \in ℕ_{0}$
6	4 5	syl	$⊢ X \in ℤ_{\geq 4} \to X - 1 \in ℕ_{0}$
7		zexpcl	$⊢ (N \in ℤ \land X - 1 \in ℕ_{0}) \to N^{X - 1} \in ℤ$
8	3 6 7	syl2an	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N^{X - 1} \in ℤ$
9	8	zred	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N^{X - 1} \in ℝ$
10	4	nnrpd	$⊢ X \in ℤ_{\geq 4} \to X \in ℝ^{+}$
11	10	adantl	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to X \in ℝ^{+}$
12	9 11	modcld	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N^{X - 1} \mod X \in ℝ$
13	12	recnd	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N^{X - 1} \mod X \in ℂ$
14		1cnd	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to 1 \in ℂ$
15		nncn	$⊢ N \in ℕ \to N \in ℂ$
16	15	adantr	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N \in ℂ$
17		nnne0	$⊢ N \in ℕ \to N \neq 0$
18	17	adantr	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N \neq 0$
19	13 14 16 18	mulcand	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N (N^{X - 1} \mod X) = N \cdot 1 \leftrightarrow N^{X - 1} \mod X = 1)$
20		oveq1	$⊢ N (N^{X - 1} \mod X) = N \cdot 1 \to N (N^{X - 1} \mod X) \mod X = N \cdot 1 \mod X$
21	3	adantr	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N \in ℤ$
22		modmulmodr	$⊢ (N \in ℤ \land N^{X - 1} \in ℝ \land X \in ℝ^{+}) \to N (N^{X - 1} \mod X) \mod X = N N^{X - 1} \mod X$
23	21 9 11 22	syl3anc	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N (N^{X - 1} \mod X) \mod X = N N^{X - 1} \mod X$
24	23	eqeq1d	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N (N^{X - 1} \mod X) \mod X = N \cdot 1 \mod X \leftrightarrow N N^{X - 1} \mod X = N \cdot 1 \mod X)$
25	8	zcnd	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N^{X - 1} \in ℂ$
26	16 25	mulcomd	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N N^{X - 1} = N^{X - 1} \cdot N$
27		expm1t	$⊢ (N \in ℂ \land X \in ℕ) \to N^{X} = N^{X - 1} \cdot N$
28	27	eqcomd	$⊢ (N \in ℂ \land X \in ℕ) \to N^{X - 1} \cdot N = N^{X}$
29	15 4 28	syl2an	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N^{X - 1} \cdot N = N^{X}$
30	26 29	eqtrd	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N N^{X - 1} = N^{X}$
31	30	oveq1d	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N N^{X - 1} \mod X = N^{X} \mod X$
32	15	mulridd	$⊢ N \in ℕ \to N \cdot 1 = N$
33	32	adantr	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N \cdot 1 = N$
34	33	oveq1d	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to N \cdot 1 \mod X = N \mod X$
35	31 34	eqeq12d	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N N^{X - 1} \mod X = N \cdot 1 \mod X \leftrightarrow N^{X} \mod X = N \mod X)$
36	35	biimpd	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N N^{X - 1} \mod X = N \cdot 1 \mod X \to N^{X} \mod X = N \mod X)$
37	24 36	sylbid	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N (N^{X - 1} \mod X) \mod X = N \cdot 1 \mod X \to N^{X} \mod X = N \mod X)$
38	20 37	syl5	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N (N^{X - 1} \mod X) = N \cdot 1 \to N^{X} \mod X = N \mod X)$
39	19 38	sylbird	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (N^{X - 1} \mod X = 1 \to N^{X} \mod X = N \mod X)$
40	39	a1d	$⊢ (N \in ℕ \land X \in ℤ_{\geq 4}) \to (X \notin ℙ \to (N^{X - 1} \mod X = 1 \to N^{X} \mod X = N \mod X))$
41	40	ex	$⊢ N \in ℕ \to (X \in ℤ_{\geq 4} \to (X \notin ℙ \to (N^{X - 1} \mod X = 1 \to N^{X} \mod X = N \mod X)))$
42	41	3impd	$⊢ N \in ℕ \to ((X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1) \to N^{X} \mod X = N \mod X)$
43	2 42	sylbid	$⊢ N \in ℕ \to (X \in FPPr (N) \to N^{X} \mod X = N \mod X)$
44	1 43	mpcom	$⊢ X \in FPPr (N) \to N^{X} \mod X = N \mod X$

Metamath Proof Explorer

Theorem fpprwppr

Proof