2pwp1prm

Description: For ( ( 2 ^ k ) + 1 ) to be prime, k must be a power of 2, see Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number , 5-Aug-2021. (Contributed by AV, 7-Aug-2021)

		Ref	Expression
	Assertion	2pwp1prm	$⊢ (K \in ℕ \land 2^{K} + 1 \in ℙ) \to \exists n \in ℕ_{0} K = 2^{n}$

Proof

Step	Hyp	Ref	Expression
1		oddprmdvds	$⊢ (K \in ℕ \land \neg \exists n \in ℕ_{0} K = 2^{n}) \to \exists p \in (ℙ ∖ \{2\}) p ∥ K$
2	1	adantlr	$⊢ ((K \in ℕ \land 2^{K} + 1 \in ℙ) \land \neg \exists n \in ℕ_{0} K = 2^{n}) \to \exists p \in (ℙ ∖ \{2\}) p ∥ K$
3		eldifi	$⊢ p \in (ℙ ∖ \{2\}) \to p \in ℙ$
4		prmnn	$⊢ p \in ℙ \to p \in ℕ$
5	3 4	syl	$⊢ p \in (ℙ ∖ \{2\}) \to p \in ℕ$
6		simpl	$⊢ (K \in ℕ \land 2^{K} + 1 \in ℙ) \to K \in ℕ$
7		nndivides	$⊢ (p \in ℕ \land K \in ℕ) \to (p ∥ K \leftrightarrow \exists m \in ℕ m p = K)$
8	5 6 7	syl2anr	$⊢ ((K \in ℕ \land 2^{K} + 1 \in ℙ) \land p \in (ℙ ∖ \{2\})) \to (p ∥ K \leftrightarrow \exists m \in ℕ m p = K)$
9		2re	$⊢ 2 \in ℝ$
10	9	a1i	$⊢ m \in ℕ \to 2 \in ℝ$
11		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
12		1le2	$⊢ 1 \leq 2$
13	12	a1i	$⊢ m \in ℕ \to 1 \leq 2$
14	10 11 13	expge1d	$⊢ m \in ℕ \to 1 \leq 2^{m}$
15		1zzd	$⊢ m \in ℕ \to 1 \in ℤ$
16		2nn	$⊢ 2 \in ℕ$
17	16	a1i	$⊢ m \in ℕ \to 2 \in ℕ$
18	17 11	nnexpcld	$⊢ m \in ℕ \to 2^{m} \in ℕ$
19	18	nnzd	$⊢ m \in ℕ \to 2^{m} \in ℤ$
20		zleltp1	$⊢ (1 \in ℤ \land 2^{m} \in ℤ) \to (1 \leq 2^{m} \leftrightarrow 1 < 2^{m} + 1)$
21	15 19 20	syl2anc	$⊢ m \in ℕ \to (1 \leq 2^{m} \leftrightarrow 1 < 2^{m} + 1)$
22	14 21	mpbid	$⊢ m \in ℕ \to 1 < 2^{m} + 1$
23	18	nncnd	$⊢ m \in ℕ \to 2^{m} \in ℂ$
24		1cnd	$⊢ m \in ℕ \to 1 \in ℂ$
25		subneg	$⊢ (2^{m} \in ℂ \land 1 \in ℂ) \to 2^{m} - -1 = 2^{m} + 1$
26	25	breq2d	$⊢ (2^{m} \in ℂ \land 1 \in ℂ) \to (1 < 2^{m} - -1 \leftrightarrow 1 < 2^{m} + 1)$
27	23 24 26	syl2anc	$⊢ m \in ℕ \to (1 < 2^{m} - -1 \leftrightarrow 1 < 2^{m} + 1)$
28	22 27	mpbird	$⊢ m \in ℕ \to 1 < 2^{m} - -1$
29	28	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 1 < 2^{m} - -1$
30	29	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 1 < 2^{m} - -1$
31	18	nnred	$⊢ m \in ℕ \to 2^{m} \in ℝ$
32	31	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} \in ℝ$
33	16	a1i	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2 \in ℕ$
34	11	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to m \in ℕ_{0}$
35	5	nnnn0d	$⊢ p \in (ℙ ∖ \{2\}) \to p \in ℕ_{0}$
36	35	adantr	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to p \in ℕ_{0}$
37	34 36	nn0mulcld	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to m p \in ℕ_{0}$
38	33 37	nnexpcld	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m p} \in ℕ$
39	38	nnred	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m p} \in ℝ$
40		1red	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 1 \in ℝ$
41	9	a1i	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2 \in ℝ$
42		nnz	$⊢ m \in ℕ \to m \in ℤ$
43	42	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to m \in ℤ$
44	5	nnzd	$⊢ p \in (ℙ ∖ \{2\}) \to p \in ℤ$
45	44	adantr	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to p \in ℤ$
46	43 45	zmulcld	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to m p \in ℤ$
47		1lt2	$⊢ 1 < 2$
48	47	a1i	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 1 < 2$
49		prmgt1	$⊢ p \in ℙ \to 1 < p$
50	3 49	syl	$⊢ p \in (ℙ ∖ \{2\}) \to 1 < p$
51	50	adantr	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 1 < p$
52		nnre	$⊢ m \in ℕ \to m \in ℝ$
53	52	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to m \in ℝ$
54	5	nnred	$⊢ p \in (ℙ ∖ \{2\}) \to p \in ℝ$
55	54	adantr	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to p \in ℝ$
56		nngt0	$⊢ m \in ℕ \to 0 < m$
57	56	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 0 < m$
58		ltmulgt11	$⊢ (m \in ℝ \land p \in ℝ \land 0 < m) \to (1 < p \leftrightarrow m < m p)$
59	53 55 57 58	syl3anc	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to (1 < p \leftrightarrow m < m p)$
60	51 59	mpbid	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to m < m p$
61		ltexp2a	$⊢ ((2 \in ℝ \land m \in ℤ \land m p \in ℤ) \land (1 < 2 \land m < m p)) \to 2^{m} < 2^{m p}$
62	41 43 46 48 60 61	syl32anc	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} < 2^{m p}$
63	32 39 40 62	ltadd1dd	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} + 1 < 2^{m p} + 1$
64	63	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{m} + 1 < 2^{m p} + 1$
65	23 24	subnegd	$⊢ m \in ℕ \to 2^{m} - -1 = 2^{m} + 1$
66	65	eqcomd	$⊢ m \in ℕ \to 2^{m} + 1 = 2^{m} - -1$
67	66	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} + 1 = 2^{m} - -1$
68	67	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{m} + 1 = 2^{m} - -1$
69		oveq2	$⊢ m p = K \to 2^{m p} = 2^{K}$
70	69	oveq1d	$⊢ m p = K \to 2^{m p} + 1 = 2^{K} + 1$
71	70	adantl	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{m p} + 1 = 2^{K} + 1$
72	64 68 71	3brtr3d	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{m} - -1 < 2^{K} + 1$
73		neg1z	$⊢ - 1 \in ℤ$
74	73	a1i	$⊢ m \in ℕ \to - 1 \in ℤ$
75	19 74	zsubcld	$⊢ m \in ℕ \to 2^{m} - -1 \in ℤ$
76	75	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} - -1 \in ℤ$
77		fzofi	$⊢ (0 ..^p) \in Fin$
78	77	a1i	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to (0 ..^p) \in Fin$
79	19	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} \in ℤ$
80		elfzonn0	$⊢ k \in (0 ..^p) \to k \in ℕ_{0}$
81		zexpcl	$⊢ (2^{m} \in ℤ \land k \in ℕ_{0}) \to {(2^{m})}^{k} \in ℤ$
82	79 80 81	syl2an	$⊢ ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \land k \in (0 ..^p)) \to {(2^{m})}^{k} \in ℤ$
83	73	a1i	$⊢ ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \land k \in (0 ..^p)) \to - 1 \in ℤ$
84		fzonnsub	$⊢ k \in (0 ..^p) \to p - k \in ℕ$
85	84	adantl	$⊢ ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \land k \in (0 ..^p)) \to p - k \in ℕ$
86		nnm1nn0	$⊢ p - k \in ℕ \to p - k - 1 \in ℕ_{0}$
87	85 86	syl	$⊢ ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \land k \in (0 ..^p)) \to p - k - 1 \in ℕ_{0}$
88		zexpcl	$⊢ (- 1 \in ℤ \land p - k - 1 \in ℕ_{0}) \to {(- 1)}^{p - k - 1} \in ℤ$
89	83 87 88	syl2anc	$⊢ ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \land k \in (0 ..^p)) \to {(- 1)}^{p - k - 1} \in ℤ$
90	82 89	zmulcld	$⊢ ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \land k \in (0 ..^p)) \to {(2^{m})}^{k} {(- 1)}^{p - k - 1} \in ℤ$
91	78 90	fsumzcl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1} \in ℤ$
92		dvdsmul1	$⊢ (2^{m} - -1 \in ℤ \land \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1} \in ℤ) \to (2^{m} - -1) ∥ (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1}$
93	76 91 92	syl2anc	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to (2^{m} - -1) ∥ (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1}$
94	93	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to (2^{m} - -1) ∥ (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1}$
95	23	adantl	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m} \in ℂ$
96		neg1cn	$⊢ - 1 \in ℂ$
97	96	a1i	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to - 1 \in ℂ$
98		pwdif	$⊢ (p \in ℕ_{0} \land 2^{m} \in ℂ \land - 1 \in ℂ) \to {(2^{m})}^{p} - {(- 1)}^{p} = (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1}$
99	36 95 97 98	syl3anc	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to {(2^{m})}^{p} - {(- 1)}^{p} = (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1}$
100	99	breq2d	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to ((2^{m} - -1) ∥ ({(2^{m})}^{p} - {(- 1)}^{p}) \leftrightarrow (2^{m} - -1) ∥ (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1})$
101	100	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to ((2^{m} - -1) ∥ ({(2^{m})}^{p} - {(- 1)}^{p}) \leftrightarrow (2^{m} - -1) ∥ (2^{m} - -1) \sum_{k \in (0 ..^p)} {(2^{m})}^{k} {(- 1)}^{p - k - 1})$
102	94 101	mpbird	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to (2^{m} - -1) ∥ ({(2^{m})}^{p} - {(- 1)}^{p})$
103		2cnd	$⊢ K \in ℕ \to 2 \in ℂ$
104		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
105	103 104	expcld	$⊢ K \in ℕ \to 2^{K} \in ℂ$
106		1cnd	$⊢ K \in ℕ \to 1 \in ℂ$
107	105 106	subnegd	$⊢ K \in ℕ \to 2^{K} - -1 = 2^{K} + 1$
108	107	eqcomd	$⊢ K \in ℕ \to 2^{K} + 1 = 2^{K} - -1$
109	108	adantr	$⊢ (K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \to 2^{K} + 1 = 2^{K} - -1$
110	109	adantr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{K} + 1 = 2^{K} - -1$
111		oveq2	$⊢ K = m p \to 2^{K} = 2^{m p}$
112	111	eqcoms	$⊢ m p = K \to 2^{K} = 2^{m p}$
113	112	adantl	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{K} = 2^{m p}$
114		2cnd	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2 \in ℂ$
115	114 36 34	expmuld	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to 2^{m p} = {(2^{m})}^{p}$
116	115	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{m p} = {(2^{m})}^{p}$
117	113 116	eqtrd	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{K} = {(2^{m})}^{p}$
118		1exp	$⊢ p \in ℤ \to 1^{p} = 1$
119	44 118	syl	$⊢ p \in (ℙ ∖ \{2\}) \to 1^{p} = 1$
120	119	eqcomd	$⊢ p \in (ℙ ∖ \{2\}) \to 1 = 1^{p}$
121	120	negeqd	$⊢ p \in (ℙ ∖ \{2\}) \to - 1 = - 1^{p}$
122		1cnd	$⊢ p \in (ℙ ∖ \{2\}) \to 1 \in ℂ$
123		oddn2prm	$⊢ p \in (ℙ ∖ \{2\}) \to \neg 2 ∥ p$
124		oexpneg	$⊢ (1 \in ℂ \land p \in ℕ \land \neg 2 ∥ p) \to {(- 1)}^{p} = - 1^{p}$
125	122 5 123 124	syl3anc	$⊢ p \in (ℙ ∖ \{2\}) \to {(- 1)}^{p} = - 1^{p}$
126	125	eqcomd	$⊢ p \in (ℙ ∖ \{2\}) \to - 1^{p} = {(- 1)}^{p}$
127	121 126	eqtrd	$⊢ p \in (ℙ ∖ \{2\}) \to - 1 = {(- 1)}^{p}$
128	127	adantr	$⊢ (p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to - 1 = {(- 1)}^{p}$
129	128	ad2antlr	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to - 1 = {(- 1)}^{p}$
130	117 129	oveq12d	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{K} - -1 = {(2^{m})}^{p} - {(- 1)}^{p}$
131	110 130	eqtrd	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to 2^{K} + 1 = {(2^{m})}^{p} - {(- 1)}^{p}$
132	131	breq2d	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to ((2^{m} - -1) ∥ (2^{K} + 1) \leftrightarrow (2^{m} - -1) ∥ ({(2^{m})}^{p} - {(- 1)}^{p}))$
133	102 132	mpbird	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to (2^{m} - -1) ∥ (2^{K} + 1)$
134	30 72 133	dvdsnprmd	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to \neg 2^{K} + 1 \in ℙ$
135	134	pm2.21d	$⊢ ((K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \land m p = K) \to (2^{K} + 1 \in ℙ \to \exists n \in ℕ_{0} K = 2^{n})$
136	135	ex	$⊢ (K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \to (m p = K \to (2^{K} + 1 \in ℙ \to \exists n \in ℕ_{0} K = 2^{n}))$
137	136	com23	$⊢ (K \in ℕ \land (p \in (ℙ ∖ \{2\}) \land m \in ℕ)) \to (2^{K} + 1 \in ℙ \to (m p = K \to \exists n \in ℕ_{0} K = 2^{n}))$
138	137	impancom	$⊢ (K \in ℕ \land 2^{K} + 1 \in ℙ) \to ((p \in (ℙ ∖ \{2\}) \land m \in ℕ) \to (m p = K \to \exists n \in ℕ_{0} K = 2^{n}))$
139	138	impl	$⊢ (((K \in ℕ \land 2^{K} + 1 \in ℙ) \land p \in (ℙ ∖ \{2\})) \land m \in ℕ) \to (m p = K \to \exists n \in ℕ_{0} K = 2^{n})$
140	139	rexlimdva	$⊢ ((K \in ℕ \land 2^{K} + 1 \in ℙ) \land p \in (ℙ ∖ \{2\})) \to (\exists m \in ℕ m p = K \to \exists n \in ℕ_{0} K = 2^{n})$
141	8 140	sylbid	$⊢ ((K \in ℕ \land 2^{K} + 1 \in ℙ) \land p \in (ℙ ∖ \{2\})) \to (p ∥ K \to \exists n \in ℕ_{0} K = 2^{n})$
142	141	rexlimdva	$⊢ (K \in ℕ \land 2^{K} + 1 \in ℙ) \to (\exists p \in (ℙ ∖ \{2\}) p ∥ K \to \exists n \in ℕ_{0} K = 2^{n})$
143	142	adantr	$⊢ ((K \in ℕ \land 2^{K} + 1 \in ℙ) \land \neg \exists n \in ℕ_{0} K = 2^{n}) \to (\exists p \in (ℙ ∖ \{2\}) p ∥ K \to \exists n \in ℕ_{0} K = 2^{n})$
144	2 143	mpd	$⊢ ((K \in ℕ \land 2^{K} + 1 \in ℙ) \land \neg \exists n \in ℕ_{0} K = 2^{n}) \to \exists n \in ℕ_{0} K = 2^{n}$
145	144	pm2.18da	$⊢ (K \in ℕ \land 2^{K} + 1 \in ℙ) \to \exists n \in ℕ_{0} K = 2^{n}$

Metamath Proof Explorer

Theorem 2pwp1prm

Proof