fppr2odd

Description: A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023)

		Ref	Expression
	Assertion	fppr2odd	$⊢ X \in FPPr (2) \to X \in Odd$

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	ax-mp	$⊢ X \in FPPr (2) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1)$
4		eluz4nn	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$
5	4	adantr	$⊢ (X \in ℤ_{\geq 4} \land 2^{X - 1} \mod X = 1) \to X \in ℕ$
6		eluzelz	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ$
7		zeo2ALTV	$⊢ X \in ℤ \to (X \in Even \leftrightarrow \neg X \in Odd)$
8	6 7	syl	$⊢ X \in ℤ_{\geq 4} \to (X \in Even \leftrightarrow \neg X \in Odd)$
9	8	adantr	$⊢ (X \in ℤ_{\geq 4} \land 2^{X - 1} \mod X = 1) \to (X \in Even \leftrightarrow \neg X \in Odd)$
10	9	biimprd	$⊢ (X \in ℤ_{\geq 4} \land 2^{X - 1} \mod X = 1) \to (\neg X \in Odd \to X \in Even)$
11		nnennexALTV	$⊢ (X \in ℕ \land X \in Even) \to \exists y \in ℕ X = 2 y$
12	5 10 11	syl6an	$⊢ (X \in ℤ_{\geq 4} \land 2^{X - 1} \mod X = 1) \to (\neg X \in Odd \to \exists y \in ℕ X = 2 y)$
13		oveq1	$⊢ X = 2 y \to X - 1 = 2 y - 1$
14	13	oveq2d	$⊢ X = 2 y \to 2^{X - 1} = 2^{2 y - 1}$
15		id	$⊢ X = 2 y \to X = 2 y$
16	14 15	oveq12d	$⊢ X = 2 y \to 2^{X - 1} \mod X = 2^{2 y - 1} \mod 2 y$
17	16	eqeq1d	$⊢ X = 2 y \to (2^{X - 1} \mod X = 1 \leftrightarrow 2^{2 y - 1} \mod 2 y = 1)$
18	17	adantl	$⊢ ((X \in ℤ_{\geq 4} \land y \in ℕ) \land X = 2 y) \to (2^{X - 1} \mod X = 1 \leftrightarrow 2^{2 y - 1} \mod 2 y = 1)$
19		2z	$⊢ 2 \in ℤ$
20	1	a1i	$⊢ y \in ℕ \to 2 \in ℕ$
21		id	$⊢ y \in ℕ \to y \in ℕ$
22	20 21	nnmulcld	$⊢ y \in ℕ \to 2 y \in ℕ$
23		nnm1nn0	$⊢ 2 y \in ℕ \to 2 y - 1 \in ℕ_{0}$
24	22 23	syl	$⊢ y \in ℕ \to 2 y - 1 \in ℕ_{0}$
25		zexpcl	$⊢ (2 \in ℤ \land 2 y - 1 \in ℕ_{0}) \to 2^{2 y - 1} \in ℤ$
26	19 24 25	sylancr	$⊢ y \in ℕ \to 2^{2 y - 1} \in ℤ$
27	22	nnrpd	$⊢ y \in ℕ \to 2 y \in ℝ^{+}$
28		modmuladdim	$⊢ (2^{2 y - 1} \in ℤ \land 2 y \in ℝ^{+}) \to (2^{2 y - 1} \mod 2 y = 1 \to \exists m \in ℤ 2^{2 y - 1} = m 2 y + 1)$
29	26 27 28	syl2anc	$⊢ y \in ℕ \to (2^{2 y - 1} \mod 2 y = 1 \to \exists m \in ℤ 2^{2 y - 1} = m 2 y + 1)$
30	24	adantr	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y - 1 \in ℕ_{0}$
31	19 30 25	sylancr	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1} \in ℤ$
32	31	zcnd	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1} \in ℂ$
33		zcn	$⊢ m \in ℤ \to m \in ℂ$
34	33	adantl	$⊢ (y \in ℕ \land m \in ℤ) \to m \in ℂ$
35		2cnd	$⊢ (y \in ℕ \land m \in ℤ) \to 2 \in ℂ$
36		nncn	$⊢ y \in ℕ \to y \in ℂ$
37	36	adantr	$⊢ (y \in ℕ \land m \in ℤ) \to y \in ℂ$
38	35 37	mulcld	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y \in ℂ$
39	34 38	mulcld	$⊢ (y \in ℕ \land m \in ℤ) \to m 2 y \in ℂ$
40		1cnd	$⊢ (y \in ℕ \land m \in ℤ) \to 1 \in ℂ$
41		subadd	$⊢ (2^{2 y - 1} \in ℂ \land m 2 y \in ℂ \land 1 \in ℂ) \to (2^{2 y - 1} - m 2 y = 1 \leftrightarrow m 2 y + 1 = 2^{2 y - 1})$
42		eqcom	$⊢ m 2 y + 1 = 2^{2 y - 1} \leftrightarrow 2^{2 y - 1} = m 2 y + 1$
43	41 42	bitrdi	$⊢ (2^{2 y - 1} \in ℂ \land m 2 y \in ℂ \land 1 \in ℂ) \to (2^{2 y - 1} - m 2 y = 1 \leftrightarrow 2^{2 y - 1} = m 2 y + 1)$
44	32 39 40 43	syl3anc	$⊢ (y \in ℕ \land m \in ℤ) \to (2^{2 y - 1} - m 2 y = 1 \leftrightarrow 2^{2 y - 1} = m 2 y + 1)$
45		2cnd	$⊢ y \in ℕ \to 2 \in ℂ$
46	45 36	mulcld	$⊢ y \in ℕ \to 2 y \in ℂ$
47		1cnd	$⊢ y \in ℕ \to 1 \in ℂ$
48	46 47	subcld	$⊢ y \in ℕ \to 2 y - 1 \in ℂ$
49	48	adantr	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y - 1 \in ℂ$
50		npcan1	$⊢ 2 y - 1 \in ℂ \to (2 y - 1) - 1 + 1 = 2 y - 1$
51	49 50	syl	$⊢ (y \in ℕ \land m \in ℤ) \to (2 y - 1) - 1 + 1 = 2 y - 1$
52	51	eqcomd	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y - 1 = (2 y - 1) - 1 + 1$
53	52	oveq2d	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1} = 2^{(2 y - 1) - 1 + 1}$
54		2t1e2	$⊢ 2 \cdot 1 = 2$
55	54	eqcomi	$⊢ 2 = 2 \cdot 1$
56	55	oveq2i	$⊢ 2 y - 2 = 2 y - 2 \cdot 1$
57		sub1m1	$⊢ 2 y \in ℂ \to 2 y - 1 - 1 = 2 y - 2$
58	38 57	syl	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y - 1 - 1 = 2 y - 2$
59	35 37 40	subdid	$⊢ (y \in ℕ \land m \in ℤ) \to 2 (y - 1) = 2 y - 2 \cdot 1$
60	56 58 59	3eqtr4a	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y - 1 - 1 = 2 (y - 1)$
61		2nn0	$⊢ 2 \in ℕ_{0}$
62	61	a1i	$⊢ (y \in ℕ \land m \in ℤ) \to 2 \in ℕ_{0}$
63		nnm1nn0	$⊢ y \in ℕ \to y - 1 \in ℕ_{0}$
64	63	adantr	$⊢ (y \in ℕ \land m \in ℤ) \to y - 1 \in ℕ_{0}$
65	62 64	nn0mulcld	$⊢ (y \in ℕ \land m \in ℤ) \to 2 (y - 1) \in ℕ_{0}$
66	60 65	eqeltrd	$⊢ (y \in ℕ \land m \in ℤ) \to 2 y - 1 - 1 \in ℕ_{0}$
67	35 66	expp1d	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{(2 y - 1) - 1 + 1} = 2^{2 y - 1 - 1} \cdot 2$
68	35 66	expcld	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1 - 1} \in ℂ$
69	68 35	mulcomd	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1 - 1} \cdot 2 = 2 2^{2 y - 1 - 1}$
70	67 69	eqtrd	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{(2 y - 1) - 1 + 1} = 2 2^{2 y - 1 - 1}$
71	53 70	eqtrd	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1} = 2 2^{2 y - 1 - 1}$
72	34 35 37	mul12d	$⊢ (y \in ℕ \land m \in ℤ) \to m 2 y = 2 m y$
73	71 72	oveq12d	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1} - m 2 y = 2 2^{2 y - 1 - 1} - 2 m y$
74	34 37	mulcld	$⊢ (y \in ℕ \land m \in ℤ) \to m y \in ℂ$
75	35 68 74	subdid	$⊢ (y \in ℕ \land m \in ℤ) \to 2 (2^{2 y - 1 - 1} - m y) = 2 2^{2 y - 1 - 1} - 2 m y$
76	75	eqcomd	$⊢ (y \in ℕ \land m \in ℤ) \to 2 2^{2 y - 1 - 1} - 2 m y = 2 (2^{2 y - 1 - 1} - m y)$
77	73 76	eqtrd	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1} - m 2 y = 2 (2^{2 y - 1 - 1} - m y)$
78	77	eqeq1d	$⊢ (y \in ℕ \land m \in ℤ) \to (2^{2 y - 1} - m 2 y = 1 \leftrightarrow 2 (2^{2 y - 1 - 1} - m y) = 1)$
79		zexpcl	$⊢ (2 \in ℤ \land 2 y - 1 - 1 \in ℕ_{0}) \to 2^{2 y - 1 - 1} \in ℤ$
80	19 66 79	sylancr	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1 - 1} \in ℤ$
81		simpr	$⊢ (y \in ℕ \land m \in ℤ) \to m \in ℤ$
82		nnz	$⊢ y \in ℕ \to y \in ℤ$
83	82	adantr	$⊢ (y \in ℕ \land m \in ℤ) \to y \in ℤ$
84	81 83	zmulcld	$⊢ (y \in ℕ \land m \in ℤ) \to m y \in ℤ$
85	80 84	zsubcld	$⊢ (y \in ℕ \land m \in ℤ) \to 2^{2 y - 1 - 1} - m y \in ℤ$
86		m2even	$⊢ 2^{2 y - 1 - 1} - m y \in ℤ \to 2 (2^{2 y - 1 - 1} - m y) \in Even$
87	85 86	syl	$⊢ (y \in ℕ \land m \in ℤ) \to 2 (2^{2 y - 1 - 1} - m y) \in Even$
88		1oddALTV	$⊢ 1 \in Odd$
89		zneoALTV	$⊢ (2 (2^{2 y - 1 - 1} - m y) \in Even \land 1 \in Odd) \to 2 (2^{2 y - 1 - 1} - m y) \neq 1$
90	87 88 89	sylancl	$⊢ (y \in ℕ \land m \in ℤ) \to 2 (2^{2 y - 1 - 1} - m y) \neq 1$
91		eqneqall	$⊢ 2 (2^{2 y - 1 - 1} - m y) = 1 \to (2 (2^{2 y - 1 - 1} - m y) \neq 1 \to X \in Odd)$
92	90 91	syl5com	$⊢ (y \in ℕ \land m \in ℤ) \to (2 (2^{2 y - 1 - 1} - m y) = 1 \to X \in Odd)$
93	78 92	sylbid	$⊢ (y \in ℕ \land m \in ℤ) \to (2^{2 y - 1} - m 2 y = 1 \to X \in Odd)$
94	44 93	sylbird	$⊢ (y \in ℕ \land m \in ℤ) \to (2^{2 y - 1} = m 2 y + 1 \to X \in Odd)$
95	94	rexlimdva	$⊢ y \in ℕ \to (\exists m \in ℤ 2^{2 y - 1} = m 2 y + 1 \to X \in Odd)$
96	29 95	syld	$⊢ y \in ℕ \to (2^{2 y - 1} \mod 2 y = 1 \to X \in Odd)$
97	96	adantl	$⊢ (X \in ℤ_{\geq 4} \land y \in ℕ) \to (2^{2 y - 1} \mod 2 y = 1 \to X \in Odd)$
98	97	adantr	$⊢ ((X \in ℤ_{\geq 4} \land y \in ℕ) \land X = 2 y) \to (2^{2 y - 1} \mod 2 y = 1 \to X \in Odd)$
99	18 98	sylbid	$⊢ ((X \in ℤ_{\geq 4} \land y \in ℕ) \land X = 2 y) \to (2^{X - 1} \mod X = 1 \to X \in Odd)$
100	99	ex	$⊢ (X \in ℤ_{\geq 4} \land y \in ℕ) \to (X = 2 y \to (2^{X - 1} \mod X = 1 \to X \in Odd))$
101	100	rexlimdva	$⊢ X \in ℤ_{\geq 4} \to (\exists y \in ℕ X = 2 y \to (2^{X - 1} \mod X = 1 \to X \in Odd))$
102	101	com23	$⊢ X \in ℤ_{\geq 4} \to (2^{X - 1} \mod X = 1 \to (\exists y \in ℕ X = 2 y \to X \in Odd))$
103	102	imp	$⊢ (X \in ℤ_{\geq 4} \land 2^{X - 1} \mod X = 1) \to (\exists y \in ℕ X = 2 y \to X \in Odd)$
104	12 103	syld	$⊢ (X \in ℤ_{\geq 4} \land 2^{X - 1} \mod X = 1) \to (\neg X \in Odd \to X \in Odd)$
105	104	3adant2	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ \land 2^{X - 1} \mod X = 1) \to (\neg X \in Odd \to X \in Odd)$
106	3 105	sylbi	$⊢ X \in FPPr (2) \to (\neg X \in Odd \to X \in Odd)$
107	106	pm2.18d	$⊢ X \in FPPr (2) \to X \in Odd$

Metamath Proof Explorer

Theorem fppr2odd

Proof