fpprwpprb

Description: An integer X which is coprime with an integer N is a Fermat pseudoprime to the base N iff it is a weak pseudoprime to the base N . (Contributed by AV, 2-Jun-2023)

		Ref	Expression
	Assertion	fpprwpprb	$⊢ X \gcd N = 1 \to (X \in FPPr (N) \leftrightarrow ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land 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		3simpa	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1) \to (X \in ℤ_{\geq 4} \land X \notin ℙ)$
4	3	a1i	$⊢ N \in ℕ \to ((X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1) \to (X \in ℤ_{\geq 4} \land X \notin ℙ))$
5	2 4	sylbid	$⊢ N \in ℕ \to (X \in FPPr (N) \to (X \in ℤ_{\geq 4} \land X \notin ℙ))$
6	1 5	mpcom	$⊢ X \in FPPr (N) \to (X \in ℤ_{\geq 4} \land X \notin ℙ)$
7		fpprwppr	$⊢ X \in FPPr (N) \to N^{X} \mod X = N \mod X$
8	1 7	jca	$⊢ X \in FPPr (N) \to (N \in ℕ \land N^{X} \mod X = N \mod X)$
9	6 8	jca	$⊢ X \in FPPr (N) \to ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))$
10		simprll	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to X \in ℤ_{\geq 4}$
11		simprlr	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to X \notin ℙ$
12		eluz4nn	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$
13	12	adantr	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to X \in ℕ$
14		nnz	$⊢ N \in ℕ \to N \in ℤ$
15	12	nnnn0d	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ_{0}$
16		zexpcl	$⊢ (N \in ℤ \land X \in ℕ_{0}) \to N^{X} \in ℤ$
17	14 15 16	syl2anr	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X} \in ℤ$
18	14	adantl	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N \in ℤ$
19		moddvds	$⊢ (X \in ℕ \land N^{X} \in ℤ \land N \in ℤ) \to (N^{X} \mod X = N \mod X \leftrightarrow X ∥ (N^{X} - N))$
20	13 17 18 19	syl3anc	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (N^{X} \mod X = N \mod X \leftrightarrow X ∥ (N^{X} - N))$
21		nncn	$⊢ N \in ℕ \to N \in ℂ$
22		expm1t	$⊢ (N \in ℂ \land X \in ℕ) \to N^{X} = N^{X - 1} \cdot N$
23	21 12 22	syl2anr	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X} = N^{X - 1} \cdot N$
24	23	oveq1d	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X} - N = N^{X - 1} \cdot N - N$
25		nnm1nn0	$⊢ X \in ℕ \to X - 1 \in ℕ_{0}$
26	12 25	syl	$⊢ X \in ℤ_{\geq 4} \to X - 1 \in ℕ_{0}$
27		zexpcl	$⊢ (N \in ℤ \land X - 1 \in ℕ_{0}) \to N^{X - 1} \in ℤ$
28	14 26 27	syl2anr	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X - 1} \in ℤ$
29	28	zcnd	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X - 1} \in ℂ$
30	21	adantl	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N \in ℂ$
31	29 30	mulsubfacd	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X - 1} \cdot N - N = (N^{X - 1} - 1) \cdot N$
32	24 31	eqtrd	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X} - N = (N^{X - 1} - 1) \cdot N$
33	32	breq2d	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X ∥ (N^{X} - N) \leftrightarrow X ∥ (N^{X - 1} - 1) \cdot N)$
34		1zzd	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to 1 \in ℤ$
35	28 34	zsubcld	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X - 1} - 1 \in ℤ$
36		dvdsmulgcd	$⊢ (N^{X - 1} - 1 \in ℤ \land N \in ℤ) \to (X ∥ (N^{X - 1} - 1) \cdot N \leftrightarrow X ∥ (N^{X - 1} - 1) (N \gcd X))$
37	35 18 36	syl2anc	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X ∥ (N^{X - 1} - 1) \cdot N \leftrightarrow X ∥ (N^{X - 1} - 1) (N \gcd X))$
38		eluzelz	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ$
39		gcdcom	$⊢ (X \in ℤ \land N \in ℤ) \to X \gcd N = N \gcd X$
40	38 14 39	syl2an	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to X \gcd N = N \gcd X$
41	40	eqeq1d	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X \gcd N = 1 \leftrightarrow N \gcd X = 1)$
42	41	biimpd	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X \gcd N = 1 \to N \gcd X = 1)$
43	42	imp	$⊢ ((X \in ℤ_{\geq 4} \land N \in ℕ) \land X \gcd N = 1) \to N \gcd X = 1$
44	43	oveq2d	$⊢ ((X \in ℤ_{\geq 4} \land N \in ℕ) \land X \gcd N = 1) \to (N^{X - 1} - 1) (N \gcd X) = (N^{X - 1} - 1) \cdot 1$
45	35	zcnd	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to N^{X - 1} - 1 \in ℂ$
46	45	mulid1d	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (N^{X - 1} - 1) \cdot 1 = N^{X - 1} - 1$
47	46	adantr	$⊢ ((X \in ℤ_{\geq 4} \land N \in ℕ) \land X \gcd N = 1) \to (N^{X - 1} - 1) \cdot 1 = N^{X - 1} - 1$
48	44 47	eqtrd	$⊢ ((X \in ℤ_{\geq 4} \land N \in ℕ) \land X \gcd N = 1) \to (N^{X - 1} - 1) (N \gcd X) = N^{X - 1} - 1$
49	48	breq2d	$⊢ ((X \in ℤ_{\geq 4} \land N \in ℕ) \land X \gcd N = 1) \to (X ∥ (N^{X - 1} - 1) (N \gcd X) \leftrightarrow X ∥ (N^{X - 1} - 1))$
50	49	biimpd	$⊢ ((X \in ℤ_{\geq 4} \land N \in ℕ) \land X \gcd N = 1) \to (X ∥ (N^{X - 1} - 1) (N \gcd X) \to X ∥ (N^{X - 1} - 1))$
51	50	ex	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X \gcd N = 1 \to (X ∥ (N^{X - 1} - 1) (N \gcd X) \to X ∥ (N^{X - 1} - 1)))$
52	51	com23	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X ∥ (N^{X - 1} - 1) (N \gcd X) \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1)))$
53	37 52	sylbid	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X ∥ (N^{X - 1} - 1) \cdot N \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1)))$
54	33 53	sylbid	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (X ∥ (N^{X} - N) \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1)))$
55	20 54	sylbid	$⊢ (X \in ℤ_{\geq 4} \land N \in ℕ) \to (N^{X} \mod X = N \mod X \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1)))$
56	55	expimpd	$⊢ X \in ℤ_{\geq 4} \to ((N \in ℕ \land N^{X} \mod X = N \mod X) \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1)))$
57	56	adantr	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ) \to ((N \in ℕ \land N^{X} \mod X = N \mod X) \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1)))$
58	57	imp	$⊢ ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)) \to (X \gcd N = 1 \to X ∥ (N^{X - 1} - 1))$
59	58	impcom	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to X ∥ (N^{X - 1} - 1)$
60		eluz4eluz2	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 2}$
61	60	adantr	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ) \to X \in ℤ_{\geq 2}$
62	61	adantr	$⊢ ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)) \to X \in ℤ_{\geq 2}$
63	14	adantr	$⊢ (N \in ℕ \land N^{X} \mod X = N \mod X) \to N \in ℤ$
64	26	adantr	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ) \to X - 1 \in ℕ_{0}$
65	63 64 27	syl2anr	$⊢ ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)) \to N^{X - 1} \in ℤ$
66	62 65	jca	$⊢ ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)) \to (X \in ℤ_{\geq 2} \land N^{X - 1} \in ℤ)$
67	66	adantl	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to (X \in ℤ_{\geq 2} \land N^{X - 1} \in ℤ)$
68		modm1div	$⊢ (X \in ℤ_{\geq 2} \land N^{X - 1} \in ℤ) \to (N^{X - 1} \mod X = 1 \leftrightarrow X ∥ (N^{X - 1} - 1))$
69	67 68	syl	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to (N^{X - 1} \mod X = 1 \leftrightarrow X ∥ (N^{X - 1} - 1))$
70	59 69	mpbird	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to N^{X - 1} \mod X = 1$
71	2	adantr	$⊢ (N \in ℕ \land N^{X} \mod X = N \mod X) \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$
72	71	adantl	$⊢ ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)) \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$
73	72	adantl	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$
74	10 11 70 73	mpbir3and	$⊢ (X \gcd N = 1 \land ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X))) \to X \in FPPr (N)$
75	74	ex	$⊢ X \gcd N = 1 \to (((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)) \to X \in FPPr (N))$
76	9 75	impbid2	$⊢ X \gcd N = 1 \to (X \in FPPr (N) \leftrightarrow ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (N \in ℕ \land N^{X} \mod X = N \mod X)))$

Metamath Proof Explorer

Theorem fpprwpprb

Proof