lighneallem2

		Ref	Expression
	Assertion	lighneallem2	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land 2 ∥ N \land 2^{N} - 1 = P^{M}) \to M = 1$

Proof

Step	Hyp	Ref	Expression
1		evennn2n	$⊢ N \in ℕ \to (2 ∥ N \leftrightarrow \exists k \in ℕ 2 k = N)$
2	1	3ad2ant3	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (2 ∥ N \leftrightarrow \exists k \in ℕ 2 k = N)$
3		oveq2	$⊢ N = 2 k \to 2^{N} = 2^{2 k}$
4	3	eqcoms	$⊢ 2 k = N \to 2^{N} = 2^{2 k}$
5		2cnd	$⊢ k \in ℕ \to 2 \in ℂ$
6		nncn	$⊢ k \in ℕ \to k \in ℂ$
7	5 6	mulcomd	$⊢ k \in ℕ \to 2 k = k \cdot 2$
8	7	oveq2d	$⊢ k \in ℕ \to 2^{2 k} = 2^{k \cdot 2}$
9		2nn0	$⊢ 2 \in ℕ_{0}$
10	9	a1i	$⊢ k \in ℕ \to 2 \in ℕ_{0}$
11		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
12	5 10 11	expmuld	$⊢ k \in ℕ \to 2^{k \cdot 2} = {(2^{k})}^{2}$
13	8 12	eqtrd	$⊢ k \in ℕ \to 2^{2 k} = {(2^{k})}^{2}$
14	13	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \to 2^{2 k} = {(2^{k})}^{2}$
15	4 14	sylan9eqr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \land 2 k = N) \to 2^{N} = {(2^{k})}^{2}$
16	15	oveq1d	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \land 2 k = N) \to 2^{N} - 1 = {(2^{k})}^{2} - 1$
17	16	eqeq1d	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \land 2 k = N) \to (2^{N} - 1 = P^{M} \leftrightarrow {(2^{k})}^{2} - 1 = P^{M})$
18		elnn1uz2	$⊢ k \in ℕ \leftrightarrow (k = 1 \lor k \in ℤ_{\geq 2})$
19		oveq2	$⊢ k = 1 \to 2^{k} = 2^{1}$
20		2cn	$⊢ 2 \in ℂ$
21		exp1	$⊢ 2 \in ℂ \to 2^{1} = 2$
22	20 21	ax-mp	$⊢ 2^{1} = 2$
23	19 22	eqtrdi	$⊢ k = 1 \to 2^{k} = 2$
24	23	oveq1d	$⊢ k = 1 \to {(2^{k})}^{2} = 2^{2}$
25	24	oveq1d	$⊢ k = 1 \to {(2^{k})}^{2} - 1 = 2^{2} - 1$
26		sq2	$⊢ 2^{2} = 4$
27	26	oveq1i	$⊢ 2^{2} - 1 = 4 - 1$
28		4m1e3	$⊢ 4 - 1 = 3$
29	27 28	eqtri	$⊢ 2^{2} - 1 = 3$
30	25 29	eqtrdi	$⊢ k = 1 \to {(2^{k})}^{2} - 1 = 3$
31	30	eqeq1d	$⊢ k = 1 \to ({(2^{k})}^{2} - 1 = P^{M} \leftrightarrow 3 = P^{M})$
32	31	adantr	$⊢ (k = 1 \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to ({(2^{k})}^{2} - 1 = P^{M} \leftrightarrow 3 = P^{M})$
33		eqcom	$⊢ 3 = P^{M} \leftrightarrow P^{M} = 3$
34		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
35		prmnn	$⊢ P \in ℙ \to P \in ℕ$
36		nnre	$⊢ P \in ℕ \to P \in ℝ$
37	34 35 36	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℝ$
38	37	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P \in ℝ$
39		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
40	39	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℕ_{0}$
41	38 40	reexpcld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P^{M} \in ℝ$
42	41	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land P^{M} = 3) \to P^{M} \in ℝ$
43		simpr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land P^{M} = 3) \to P^{M} = 3$
44	42 43	eqled	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land P^{M} = 3) \to P^{M} \leq 3$
45	44	ex	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P^{M} = 3 \to P^{M} \leq 3)$
46	33 45	syl5bi	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (3 = P^{M} \to P^{M} \leq 3)$
47	35	nnred	$⊢ P \in ℙ \to P \in ℝ$
48		prmgt1	$⊢ P \in ℙ \to 1 < P$
49	47 48	jca	$⊢ P \in ℙ \to (P \in ℝ \land 1 < P)$
50	34 49	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℝ \land 1 < P)$
51	50	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P \in ℝ \land 1 < P)$
52		nnz	$⊢ M \in ℕ \to M \in ℤ$
53	52	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℤ$
54		3rp	$⊢ 3 \in ℝ^{+}$
55	54	a1i	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to 3 \in ℝ^{+}$
56		efexple	$⊢ ((P \in ℝ \land 1 < P) \land M \in ℤ \land 3 \in ℝ^{+}) \to (P^{M} \leq 3 \leftrightarrow M \leq ⌊\frac{\log 3}{\log P}⌋)$
57	51 53 55 56	syl3anc	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P^{M} \leq 3 \leftrightarrow M \leq ⌊\frac{\log 3}{\log P}⌋)$
58		oddprmge3	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 3}$
59		eluzle	$⊢ P \in ℤ_{\geq 3} \to 3 \leq P$
60	58 59	syl	$⊢ P \in (ℙ ∖ \{2\}) \to 3 \leq P$
61	54	a1i	$⊢ P \in (ℙ ∖ \{2\}) \to 3 \in ℝ^{+}$
62		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
63	34 35 62	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℝ^{+}$
64	61 63	logled	$⊢ P \in (ℙ ∖ \{2\}) \to (3 \leq P \leftrightarrow \log 3 \leq \log P)$
65	60 64	mpbid	$⊢ P \in (ℙ ∖ \{2\}) \to \log 3 \leq \log P$
66	65	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \log 3 \leq \log P$
67		relogcl	$⊢ 3 \in ℝ^{+} \to \log 3 \in ℝ$
68	54 67	ax-mp	$⊢ \log 3 \in ℝ$
69		rplogcl	$⊢ (P \in ℝ \land 1 < P) \to \log P \in ℝ^{+}$
70	34 49 69	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to \log P \in ℝ^{+}$
71	70	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \log P \in ℝ^{+}$
72		divle1le	$⊢ (\log 3 \in ℝ \land \log P \in ℝ^{+}) \to (\frac{\log 3}{\log P} \leq 1 \leftrightarrow \log 3 \leq \log P)$
73	68 71 72	sylancr	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\frac{\log 3}{\log P} \leq 1 \leftrightarrow \log 3 \leq \log P)$
74	66 73	mpbird	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \frac{\log 3}{\log P} \leq 1$
75		fldivle	$⊢ (\log 3 \in ℝ \land \log P \in ℝ^{+}) \to ⌊\frac{\log 3}{\log P}⌋ \leq \frac{\log 3}{\log P}$
76	68 71 75	sylancr	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ⌊\frac{\log 3}{\log P}⌋ \leq \frac{\log 3}{\log P}$
77		nnre	$⊢ M \in ℕ \to M \in ℝ$
78	77	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℝ$
79	68	a1i	$⊢ P \in (ℙ ∖ \{2\}) \to \log 3 \in ℝ$
80	62	relogcld	$⊢ P \in ℕ \to \log P \in ℝ$
81	34 35 80	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to \log P \in ℝ$
82	35	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
83		1red	$⊢ P \in ℙ \to 1 \in ℝ$
84	83 48	gtned	$⊢ P \in ℙ \to P \neq 1$
85	82 84	jca	$⊢ P \in ℙ \to (P \in ℝ^{+} \land P \neq 1)$
86		logne0	$⊢ (P \in ℝ^{+} \land P \neq 1) \to \log P \neq 0$
87	34 85 86	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to \log P \neq 0$
88	79 81 87	redivcld	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{\log 3}{\log P} \in ℝ$
89	88	flcld	$⊢ P \in (ℙ ∖ \{2\}) \to ⌊\frac{\log 3}{\log P}⌋ \in ℤ$
90	89	zred	$⊢ P \in (ℙ ∖ \{2\}) \to ⌊\frac{\log 3}{\log P}⌋ \in ℝ$
91	90	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ⌊\frac{\log 3}{\log P}⌋ \in ℝ$
92	88	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \frac{\log 3}{\log P} \in ℝ$
93		letr	$⊢ (M \in ℝ \land ⌊\frac{\log 3}{\log P}⌋ \in ℝ \land \frac{\log 3}{\log P} \in ℝ) \to ((M \leq ⌊\frac{\log 3}{\log P}⌋ \land ⌊\frac{\log 3}{\log P}⌋ \leq \frac{\log 3}{\log P}) \to M \leq \frac{\log 3}{\log P})$
94	78 91 92 93	syl3anc	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((M \leq ⌊\frac{\log 3}{\log P}⌋ \land ⌊\frac{\log 3}{\log P}⌋ \leq \frac{\log 3}{\log P}) \to M \leq \frac{\log 3}{\log P})$
95		1red	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to 1 \in ℝ$
96		letr	$⊢ (M \in ℝ \land \frac{\log 3}{\log P} \in ℝ \land 1 \in ℝ) \to ((M \leq \frac{\log 3}{\log P} \land \frac{\log 3}{\log P} \leq 1) \to M \leq 1)$
97	78 92 95 96	syl3anc	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((M \leq \frac{\log 3}{\log P} \land \frac{\log 3}{\log P} \leq 1) \to M \leq 1)$
98		nnge1	$⊢ M \in ℕ \to 1 \leq M$
99		eqcom	$⊢ M = 1 \leftrightarrow 1 = M$
100		1red	$⊢ M \in ℕ \to 1 \in ℝ$
101	100 77	letri3d	$⊢ M \in ℕ \to (1 = M \leftrightarrow (1 \leq M \land M \leq 1))$
102	99 101	syl5rbb	$⊢ M \in ℕ \to ((1 \leq M \land M \leq 1) \leftrightarrow M = 1)$
103	102	biimpd	$⊢ M \in ℕ \to ((1 \leq M \land M \leq 1) \to M = 1)$
104	98 103	mpand	$⊢ M \in ℕ \to (M \leq 1 \to M = 1)$
105	104	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (M \leq 1 \to M = 1)$
106	97 105	syld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((M \leq \frac{\log 3}{\log P} \land \frac{\log 3}{\log P} \leq 1) \to M = 1)$
107	106	expd	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (M \leq \frac{\log 3}{\log P} \to (\frac{\log 3}{\log P} \leq 1 \to M = 1))$
108	94 107	syld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((M \leq ⌊\frac{\log 3}{\log P}⌋ \land ⌊\frac{\log 3}{\log P}⌋ \leq \frac{\log 3}{\log P}) \to (\frac{\log 3}{\log P} \leq 1 \to M = 1))$
109	76 108	mpan2d	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (M \leq ⌊\frac{\log 3}{\log P}⌋ \to (\frac{\log 3}{\log P} \leq 1 \to M = 1))$
110	74 109	mpid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (M \leq ⌊\frac{\log 3}{\log P}⌋ \to M = 1)$
111	57 110	sylbid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P^{M} \leq 3 \to M = 1)$
112	46 111	syld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (3 = P^{M} \to M = 1)$
113	112	adantl	$⊢ (k = 1 \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to (3 = P^{M} \to M = 1)$
114	32 113	sylbid	$⊢ (k = 1 \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1)$
115	114	ex	$⊢ k = 1 \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1))$
116		sq1	$⊢ 1^{2} = 1$
117	116	eqcomi	$⊢ 1 = 1^{2}$
118	117	oveq2i	$⊢ {(2^{k})}^{2} - 1 = {(2^{k})}^{2} - 1^{2}$
119	118	eqeq1i	$⊢ {(2^{k})}^{2} - 1 = P^{M} \leftrightarrow {(2^{k})}^{2} - 1^{2} = P^{M}$
120		eqcom	$⊢ {(2^{k})}^{2} - 1^{2} = P^{M} \leftrightarrow P^{M} = {(2^{k})}^{2} - 1^{2}$
121	9	a1i	$⊢ k \in ℤ_{\geq 2} \to 2 \in ℕ_{0}$
122		eluzge2nn0	$⊢ k \in ℤ_{\geq 2} \to k \in ℕ_{0}$
123	121 122	nn0expcld	$⊢ k \in ℤ_{\geq 2} \to 2^{k} \in ℕ_{0}$
124	123	adantr	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to 2^{k} \in ℕ_{0}$
125		1nn0	$⊢ 1 \in ℕ_{0}$
126	125	a1i	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to 1 \in ℕ_{0}$
127		1p1e2	$⊢ 1 + 1 = 2$
128	22	eqcomi	$⊢ 2 = 2^{1}$
129	127 128	eqtri	$⊢ 1 + 1 = 2^{1}$
130		eluz2gt1	$⊢ k \in ℤ_{\geq 2} \to 1 < k$
131		2re	$⊢ 2 \in ℝ$
132	131	a1i	$⊢ k \in ℤ_{\geq 2} \to 2 \in ℝ$
133		1zzd	$⊢ k \in ℤ_{\geq 2} \to 1 \in ℤ$
134		eluzelz	$⊢ k \in ℤ_{\geq 2} \to k \in ℤ$
135		1lt2	$⊢ 1 < 2$
136	135	a1i	$⊢ k \in ℤ_{\geq 2} \to 1 < 2$
137	132 133 134 136	ltexp2d	$⊢ k \in ℤ_{\geq 2} \to (1 < k \leftrightarrow 2^{1} < 2^{k})$
138	130 137	mpbid	$⊢ k \in ℤ_{\geq 2} \to 2^{1} < 2^{k}$
139	129 138	eqbrtrid	$⊢ k \in ℤ_{\geq 2} \to 1 + 1 < 2^{k}$
140	139	adantr	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to 1 + 1 < 2^{k}$
141	34 39	anim12i	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (P \in ℙ \land M \in ℕ_{0})$
142	141	3adant3	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P \in ℙ \land M \in ℕ_{0})$
143	142	adantl	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to (P \in ℙ \land M \in ℕ_{0})$
144		difsqpwdvds	$⊢ ((2^{k} \in ℕ_{0} \land 1 \in ℕ_{0} \land 1 + 1 < 2^{k}) \land (P \in ℙ \land M \in ℕ_{0})) \to (P^{M} = {(2^{k})}^{2} - 1^{2} \to P ∥ 2 \cdot 1)$
145	124 126 140 143 144	syl31anc	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to (P^{M} = {(2^{k})}^{2} - 1^{2} \to P ∥ 2 \cdot 1)$
146		2t1e2	$⊢ 2 \cdot 1 = 2$
147	146	breq2i	$⊢ P ∥ 2 \cdot 1 \leftrightarrow P ∥ 2$
148		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
149	34 148	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 2}$
150		2prm	$⊢ 2 \in ℙ$
151		dvdsprm	$⊢ (P \in ℤ_{\geq 2} \land 2 \in ℙ) \to (P ∥ 2 \leftrightarrow P = 2)$
152	149 150 151	sylancl	$⊢ P \in (ℙ ∖ \{2\}) \to (P ∥ 2 \leftrightarrow P = 2)$
153	147 152	syl5bb	$⊢ P \in (ℙ ∖ \{2\}) \to (P ∥ 2 \cdot 1 \leftrightarrow P = 2)$
154		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
155		eqneqall	$⊢ P = 2 \to (P \neq 2 \to M = 1)$
156	155	com12	$⊢ P \neq 2 \to (P = 2 \to M = 1)$
157	154 156	simplbiim	$⊢ P \in (ℙ ∖ \{2\}) \to (P = 2 \to M = 1)$
158	153 157	sylbid	$⊢ P \in (ℙ ∖ \{2\}) \to (P ∥ 2 \cdot 1 \to M = 1)$
159	158	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P ∥ 2 \cdot 1 \to M = 1)$
160	159	adantl	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to (P ∥ 2 \cdot 1 \to M = 1)$
161	145 160	syld	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to (P^{M} = {(2^{k})}^{2} - 1^{2} \to M = 1)$
162	120 161	syl5bi	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to ({(2^{k})}^{2} - 1^{2} = P^{M} \to M = 1)$
163	119 162	syl5bi	$⊢ (k \in ℤ_{\geq 2} \land (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ)) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1)$
164	163	ex	$⊢ k \in ℤ_{\geq 2} \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1))$
165	115 164	jaoi	$⊢ (k = 1 \lor k \in ℤ_{\geq 2}) \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1))$
166	18 165	sylbi	$⊢ k \in ℕ \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1))$
167	166	impcom	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1)$
168	167	adantr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \land 2 k = N) \to ({(2^{k})}^{2} - 1 = P^{M} \to M = 1)$
169	17 168	sylbid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in ℕ) \land 2 k = N) \to (2^{N} - 1 = P^{M} \to M = 1)$
170	169	rexlimdva2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\exists k \in ℕ 2 k = N \to (2^{N} - 1 = P^{M} \to M = 1))$
171	2 170	sylbid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (2 ∥ N \to (2^{N} - 1 = P^{M} \to M = 1))$
172	171	3imp	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land 2 ∥ N \land 2^{N} - 1 = P^{M}) \to M = 1$

Metamath Proof Explorer

Theorem lighneallem2

Proof