fpprel2

Description: An alternate definition for a Fermat pseudoprime to the base 2. (Contributed by AV, 5-Jun-2023)

		Ref	Expression
	Assertion	fpprel2	$⊢ X \in FPPr (2) \leftrightarrow ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2)$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2		fpprel	$⊢ 2 \in ℕ \to (X \in FPPr (2) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1))$
3	1 2	mp1i	$⊢ X \in FPPr (2) \to (X \in FPPr (2) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1))$
4		eluz4eluz2	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 2}$
5	4	3ad2ant1	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1) \to X \in ℤ_{\geq 2}$
6	5	adantl	$⊢ (X \in FPPr (2) \land (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)) \to X \in ℤ_{\geq 2}$
7		fppr2odd	$⊢ X \in FPPr (2) \to X \in Odd$
8	7	adantr	$⊢ (X \in FPPr (2) \land (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)) \to X \in Odd$
9		simpr2	$⊢ (X \in FPPr (2) \land (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)) \to X \notin ℙ$
10	6 8 9	3jca	$⊢ (X \in FPPr (2) \land (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)) \to (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ)$
11		fpprwppr	$⊢ X \in FPPr (2) \to 2^{X} \mod X = 2 \mod X$
12		2re	$⊢ 2 \in ℝ$
13	12	a1i	$⊢ X \in ℤ_{\geq 4} \to 2 \in ℝ$
14		eluz4nn	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$
15	14	nnrpd	$⊢ X \in ℤ_{\geq 4} \to X \in ℝ^{+}$
16		0le2	$⊢ 0 \leq 2$
17	16	a1i	$⊢ X \in ℤ_{\geq 4} \to 0 \leq 2$
18		eluz2	$⊢ X \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land X \in ℤ \land 4 \leq X)$
19		4z	$⊢ 4 \in ℤ$
20		zlem1lt	$⊢ (4 \in ℤ \land X \in ℤ) \to (4 \leq X \leftrightarrow 4 - 1 < X)$
21	19 20	mpan	$⊢ X \in ℤ \to (4 \leq X \leftrightarrow 4 - 1 < X)$
22		4m1e3	$⊢ 4 - 1 = 3$
23	22	breq1i	$⊢ 4 - 1 < X \leftrightarrow 3 < X$
24	12	a1i	$⊢ (X \in ℤ \land 3 < X) \to 2 \in ℝ$
25		3re	$⊢ 3 \in ℝ$
26	25	a1i	$⊢ (X \in ℤ \land 3 < X) \to 3 \in ℝ$
27		zre	$⊢ X \in ℤ \to X \in ℝ$
28	27	adantr	$⊢ (X \in ℤ \land 3 < X) \to X \in ℝ$
29		2lt3	$⊢ 2 < 3$
30	29	a1i	$⊢ (X \in ℤ \land 3 < X) \to 2 < 3$
31		simpr	$⊢ (X \in ℤ \land 3 < X) \to 3 < X$
32	24 26 28 30 31	lttrd	$⊢ (X \in ℤ \land 3 < X) \to 2 < X$
33	32	ex	$⊢ X \in ℤ \to (3 < X \to 2 < X)$
34	23 33	biimtrid	$⊢ X \in ℤ \to (4 - 1 < X \to 2 < X)$
35	21 34	sylbid	$⊢ X \in ℤ \to (4 \leq X \to 2 < X)$
36	35	a1i	$⊢ 4 \in ℤ \to (X \in ℤ \to (4 \leq X \to 2 < X))$
37	36	3imp	$⊢ (4 \in ℤ \land X \in ℤ \land 4 \leq X) \to 2 < X$
38	18 37	sylbi	$⊢ X \in ℤ_{\geq 4} \to 2 < X$
39		modid	$⊢ ((2 \in ℝ \land X \in ℝ^{+}) \land (0 \leq 2 \land 2 < X)) \to 2 \mod X = 2$
40	13 15 17 38 39	syl22anc	$⊢ X \in ℤ_{\geq 4} \to 2 \mod X = 2$
41	40	3ad2ant1	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1) \to 2 \mod X = 2$
42	11 41	sylan9eq	$⊢ (X \in FPPr (2) \land (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)) \to 2^{X} \mod X = 2$
43	10 42	jca	$⊢ (X \in FPPr (2) \land (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)) \to ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2)$
44	43	ex	$⊢ X \in FPPr (2) \to ((X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1) \to ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2))$
45	3 44	sylbid	$⊢ X \in FPPr (2) \to (X \in FPPr (2) \to ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2))$
46	45	pm2.43i	$⊢ X \in FPPr (2) \to ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2)$
47		ge2nprmge4	$⊢ (X \in ℤ_{\geq 2} \land X \notin ℙ) \to X \in ℤ_{\geq 4}$
48	47	3adant2	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to X \in ℤ_{\geq 4}$
49		simp3	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to X \notin ℙ$
50	48 49	jca	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to (X \in ℤ_{\geq 4} \land X \notin ℙ)$
51	50	adantr	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to (X \in ℤ_{\geq 4} \land X \notin ℙ)$
52	1	a1i	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to 2 \in ℕ$
53	12	a1i	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to 2 \in ℝ$
54		eluz2nn	$⊢ X \in ℤ_{\geq 2} \to X \in ℕ$
55	54	nnrpd	$⊢ X \in ℤ_{\geq 2} \to X \in ℝ^{+}$
56	55	3ad2ant1	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to X \in ℝ^{+}$
57	16	a1i	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to 0 \leq 2$
58	48 38	syl	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to 2 < X$
59	53 56 57 58 39	syl22anc	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to 2 \mod X = 2$
60	59	eqcomd	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to 2 = 2 \mod X$
61	60	eqeq2d	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to (2^{X} \mod X = 2 \leftrightarrow 2^{X} \mod X = 2 \mod X)$
62	61	biimpa	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to 2^{X} \mod X = 2 \mod X$
63	52 62	jca	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to (2 \in ℕ \land 2^{X} \mod X = 2 \mod X)$
64		gcd2odd1	$⊢ X \in Odd \to X \gcd 2 = 1$
65	64	3ad2ant2	$⊢ (X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \to X \gcd 2 = 1$
66	65	adantr	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to X \gcd 2 = 1$
67		fpprwpprb	$⊢ X \gcd 2 = 1 \to (X \in FPPr (2) \leftrightarrow ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (2 \in ℕ \land 2^{X} \mod X = 2 \mod X)))$
68	66 67	syl	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to (X \in FPPr (2) \leftrightarrow ((X \in ℤ_{\geq 4} \land X \notin ℙ) \land (2 \in ℕ \land 2^{X} \mod X = 2 \mod X)))$
69	51 63 68	mpbir2and	$⊢ ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2) \to X \in FPPr (2)$
70	46 69	impbii	$⊢ X \in FPPr (2) \leftrightarrow ((X \in ℤ_{\geq 2} \land X \in Odd \land X \notin ℙ) \land 2^{X} \mod X = 2)$

Metamath Proof Explorer

Theorem fpprel2

Proof