lighneallem3

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ N = 1 \to 2^{N} = 2^{1}$
2		2cn	$⊢ 2 \in ℂ$
3		exp1	$⊢ 2 \in ℂ \to 2^{1} = 2$
4	2 3	ax-mp	$⊢ 2^{1} = 2$
5	1 4	syl6eq	$⊢ N = 1 \to 2^{N} = 2$
6	5	oveq1d	$⊢ N = 1 \to 2^{N} - 1 = 2 - 1$
7		2m1e1	$⊢ 2 - 1 = 1$
8	6 7	syl6eq	$⊢ N = 1 \to 2^{N} - 1 = 1$
9	8	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land N = 1) \to 2^{N} - 1 = 1$
10	9	eqeq1d	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land N = 1) \to (2^{N} - 1 = P^{M} \leftrightarrow 1 = P^{M})$
11		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
12		prmnn	$⊢ P \in ℙ \to P \in ℕ$
13		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
14	11 12 13	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ_{0}$
15	14	nn0zd	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ$
16		iddvdsexp	$⊢ (P \in ℤ \land M \in ℕ) \to P ∥ P^{M}$
17	15 16	sylan	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to P ∥ P^{M}$
18		breq2	$⊢ 1 = P^{M} \to (P ∥ 1 \leftrightarrow P ∥ P^{M})$
19	18	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land 1 = P^{M}) \to (P ∥ 1 \leftrightarrow P ∥ P^{M})$
20		dvds1	$⊢ P \in ℕ_{0} \to (P ∥ 1 \leftrightarrow P = 1)$
21	14 20	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (P ∥ 1 \leftrightarrow P = 1)$
22		eleq1	$⊢ P = 1 \to (P \in ℙ \leftrightarrow 1 \in ℙ)$
23		1nprm	$⊢ \neg 1 \in ℙ$
24	23	pm2.21i	$⊢ 1 \in ℙ \to M = 1$
25	22 24	syl6bi	$⊢ P = 1 \to (P \in ℙ \to M = 1)$
26	11 25	syl5com	$⊢ P \in (ℙ ∖ \{2\}) \to (P = 1 \to M = 1)$
27	21 26	sylbid	$⊢ P \in (ℙ ∖ \{2\}) \to (P ∥ 1 \to M = 1)$
28	27	ad2antrr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land 1 = P^{M}) \to (P ∥ 1 \to M = 1)$
29	19 28	sylbird	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land 1 = P^{M}) \to (P ∥ P^{M} \to M = 1)$
30	29	ex	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (1 = P^{M} \to (P ∥ P^{M} \to M = 1))$
31	17 30	mpid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (1 = P^{M} \to M = 1)$
32	31	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land N = 1) \to (1 = P^{M} \to M = 1)$
33	10 32	sylbid	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land N = 1) \to (2^{N} - 1 = P^{M} \to M = 1)$
34	33	ex	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (N = 1 \to (2^{N} - 1 = P^{M} \to M = 1))$
35	34	com23	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (2^{N} - 1 = P^{M} \to (N = 1 \to M = 1))$
36	35	a1d	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to ((\neg 2 ∥ N \land 2 ∥ M) \to (2^{N} - 1 = P^{M} \to (N = 1 \to M = 1)))$
37	36	3adant3	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((\neg 2 ∥ N \land 2 ∥ M) \to (2^{N} - 1 = P^{M} \to (N = 1 \to M = 1)))$
38	37	3imp	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg 2 ∥ N \land 2 ∥ M) \land 2^{N} - 1 = P^{M}) \to (N = 1 \to M = 1)$
39		neqne	$⊢ \neg N = 1 \to N \neq 1$
40	39	anim2i	$⊢ (N \in ℕ \land \neg N = 1) \to (N \in ℕ \land N \neq 1)$
41		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
42	40 41	sylibr	$⊢ (N \in ℕ \land \neg N = 1) \to N \in ℤ_{\geq 2}$
43		oddge22np1	$⊢ N \in ℤ_{\geq 2} \to (\neg 2 ∥ N \leftrightarrow \exists j \in ℕ 2 j + 1 = N)$
44	42 43	syl	$⊢ (N \in ℕ \land \neg N = 1) \to (\neg 2 ∥ N \leftrightarrow \exists j \in ℕ 2 j + 1 = N)$
45	44	3ad2antl3	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg N = 1) \to (\neg 2 ∥ N \leftrightarrow \exists j \in ℕ 2 j + 1 = N)$
46		oveq2	$⊢ N = 2 j + 1 \to 2^{N} = 2^{2 j + 1}$
47	46	oveq1d	$⊢ N = 2 j + 1 \to 2^{N} - 1 = 2^{2 j + 1} - 1$
48	47	eqcoms	$⊢ 2 j + 1 = N \to 2^{N} - 1 = 2^{2 j + 1} - 1$
49	2	a1i	$⊢ j \in ℕ \to 2 \in ℂ$
50		2nn0	$⊢ 2 \in ℕ_{0}$
51	50	a1i	$⊢ j \in ℕ \to 2 \in ℕ_{0}$
52		nnnn0	$⊢ j \in ℕ \to j \in ℕ_{0}$
53	51 52	nn0mulcld	$⊢ j \in ℕ \to 2 j \in ℕ_{0}$
54	49 53	expp1d	$⊢ j \in ℕ \to 2^{2 j + 1} = 2^{2 j} \cdot 2$
55	51 53	nn0expcld	$⊢ j \in ℕ \to 2^{2 j} \in ℕ_{0}$
56	55	nn0cnd	$⊢ j \in ℕ \to 2^{2 j} \in ℂ$
57	56 49	mulcomd	$⊢ j \in ℕ \to 2^{2 j} \cdot 2 = 2 2^{2 j}$
58	54 57	eqtrd	$⊢ j \in ℕ \to 2^{2 j + 1} = 2 2^{2 j}$
59	58	oveq1d	$⊢ j \in ℕ \to 2^{2 j + 1} - 1 = 2 2^{2 j} - 1$
60		npcan1	$⊢ 2^{2 j} \in ℂ \to 2^{2 j} - 1 + 1 = 2^{2 j}$
61	56 60	syl	$⊢ j \in ℕ \to 2^{2 j} - 1 + 1 = 2^{2 j}$
62	61	eqcomd	$⊢ j \in ℕ \to 2^{2 j} = 2^{2 j} - 1 + 1$
63	62	oveq2d	$⊢ j \in ℕ \to 2 2^{2 j} = 2 (2^{2 j} - 1 + 1)$
64		peano2cnm	$⊢ 2^{2 j} \in ℂ \to 2^{2 j} - 1 \in ℂ$
65	56 64	syl	$⊢ j \in ℕ \to 2^{2 j} - 1 \in ℂ$
66		1cnd	$⊢ j \in ℕ \to 1 \in ℂ$
67	49 65 66	adddid	$⊢ j \in ℕ \to 2 (2^{2 j} - 1 + 1) = 2 (2^{2 j} - 1) + 2 \cdot 1$
68	63 67	eqtrd	$⊢ j \in ℕ \to 2 2^{2 j} = 2 (2^{2 j} - 1) + 2 \cdot 1$
69	68	oveq1d	$⊢ j \in ℕ \to 2 2^{2 j} - 1 = 2 (2^{2 j} - 1) + 2 \cdot 1 - 1$
70	49 65	mulcld	$⊢ j \in ℕ \to 2 (2^{2 j} - 1) \in ℂ$
71		ax-1cn	$⊢ 1 \in ℂ$
72	2 71	mulcli	$⊢ 2 \cdot 1 \in ℂ$
73	72	a1i	$⊢ j \in ℕ \to 2 \cdot 1 \in ℂ$
74	70 73 66	addsubassd	$⊢ j \in ℕ \to 2 (2^{2 j} - 1) + 2 \cdot 1 - 1 = 2 (2^{2 j} - 1) + 2 \cdot 1 - 1$
75		2t1e2	$⊢ 2 \cdot 1 = 2$
76	75	oveq1i	$⊢ 2 \cdot 1 - 1 = 2 - 1$
77	76 7	eqtri	$⊢ 2 \cdot 1 - 1 = 1$
78	77	a1i	$⊢ j \in ℕ \to 2 \cdot 1 - 1 = 1$
79	78	oveq2d	$⊢ j \in ℕ \to 2 (2^{2 j} - 1) + 2 \cdot 1 - 1 = 2 (2^{2 j} - 1) + 1$
80	74 79	eqtrd	$⊢ j \in ℕ \to 2 (2^{2 j} - 1) + 2 \cdot 1 - 1 = 2 (2^{2 j} - 1) + 1$
81	59 69 80	3eqtrd	$⊢ j \in ℕ \to 2^{2 j + 1} - 1 = 2 (2^{2 j} - 1) + 1$
82	81	ad2antlr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2^{2 j + 1} - 1 = 2 (2^{2 j} - 1) + 1$
83	48 82	sylan9eqr	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land 2 j + 1 = N) \to 2^{N} - 1 = 2 (2^{2 j} - 1) + 1$
84	83	eqeq1d	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land 2 j + 1 = N) \to (2^{N} - 1 = P^{M} \leftrightarrow 2 (2^{2 j} - 1) + 1 = P^{M})$
85	14	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P \in ℕ_{0}$
86		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
87	86	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℕ_{0}$
88	85 87	nn0expcld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P^{M} \in ℕ_{0}$
89	88	nn0cnd	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P^{M} \in ℂ$
90	89	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to P^{M} \in ℂ$
91		1cnd	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to 1 \in ℂ$
92	70	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to 2 (2^{2 j} - 1) \in ℂ$
93	90 91 92	3jca	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to (P^{M} \in ℂ \land 1 \in ℂ \land 2 (2^{2 j} - 1) \in ℂ)$
94	93	adantr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (P^{M} \in ℂ \land 1 \in ℂ \land 2 (2^{2 j} - 1) \in ℂ)$
95		subadd2	$⊢ (P^{M} \in ℂ \land 1 \in ℂ \land 2 (2^{2 j} - 1) \in ℂ) \to (P^{M} - 1 = 2 (2^{2 j} - 1) \leftrightarrow 2 (2^{2 j} - 1) + 1 = P^{M})$
96	94 95	syl	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (P^{M} - 1 = 2 (2^{2 j} - 1) \leftrightarrow 2 (2^{2 j} - 1) + 1 = P^{M})$
97		nncn	$⊢ P \in ℕ \to P \in ℂ$
98	11 12 97	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℂ$
99	98	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P \in ℂ$
100	99 87	pwm1geoser	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P^{M} - 1 = (P - 1) \sum_{k = 0}^{M - 1} P^{k}$
101	100	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to P^{M} - 1 = (P - 1) \sum_{k = 0}^{M - 1} P^{k}$
102	101	eqeq1d	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to (P^{M} - 1 = 2 (2^{2 j} - 1) \leftrightarrow (P - 1) \sum_{k = 0}^{M - 1} P^{k} = 2 (2^{2 j} - 1))$
103	102	adantr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (P^{M} - 1 = 2 (2^{2 j} - 1) \leftrightarrow (P - 1) \sum_{k = 0}^{M - 1} P^{k} = 2 (2^{2 j} - 1))$
104	99	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to P \in ℂ$
105		1cnd	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 1 \in ℂ$
106	104 105	subcld	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to P - 1 \in ℂ$
107		fzfid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (0 \dots M - 1) \in Fin$
108	85	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to P \in ℕ_{0}$
109		elfznn0	$⊢ k \in (0 \dots M - 1) \to k \in ℕ_{0}$
110	109	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to k \in ℕ_{0}$
111	108 110	nn0expcld	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to P^{k} \in ℕ_{0}$
112	111	nn0zd	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to P^{k} \in ℤ$
113	107 112	fsumzcl	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \sum_{k = 0}^{M - 1} P^{k} \in ℤ$
114	113	zcnd	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \sum_{k = 0}^{M - 1} P^{k} \in ℂ$
115	114	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to \sum_{k = 0}^{M - 1} P^{k} \in ℂ$
116	106 115	mulcld	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (P - 1) \sum_{k = 0}^{M - 1} P^{k} \in ℂ$
117	56	ad2antlr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2^{2 j} \in ℂ$
118	117 105	subcld	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2^{2 j} - 1 \in ℂ$
119		2rp	$⊢ 2 \in ℝ^{+}$
120	119	a1i	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2 \in ℝ^{+}$
121	120	rpcnne0d	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (2 \in ℂ \land 2 \neq 0)$
122		divmul2	$⊢ ((P - 1) \sum_{k = 0}^{M - 1} P^{k} \in ℂ \land 2^{2 j} - 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{(P - 1) \sum_{k = 0}^{M - 1} P^{k}}{2} = 2^{2 j} - 1 \leftrightarrow (P - 1) \sum_{k = 0}^{M - 1} P^{k} = 2 (2^{2 j} - 1))$
123	116 118 121 122	syl3anc	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (\frac{(P - 1) \sum_{k = 0}^{M - 1} P^{k}}{2} = 2^{2 j} - 1 \leftrightarrow (P - 1) \sum_{k = 0}^{M - 1} P^{k} = 2 (2^{2 j} - 1))$
124		div23	$⊢ (P - 1 \in ℂ \land \sum_{k = 0}^{M - 1} P^{k} \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{(P - 1) \sum_{k = 0}^{M - 1} P^{k}}{2} = (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k}$
125	106 115 121 124	syl3anc	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to \frac{(P - 1) \sum_{k = 0}^{M - 1} P^{k}}{2} = (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k}$
126	125	eqeq1d	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (\frac{(P - 1) \sum_{k = 0}^{M - 1} P^{k}}{2} = 2^{2 j} - 1 \leftrightarrow (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1)$
127	51	nn0zd	$⊢ j \in ℕ \to 2 \in ℤ$
128		2nn	$⊢ 2 \in ℕ$
129	128	a1i	$⊢ j \in ℕ \to 2 \in ℕ$
130		id	$⊢ j \in ℕ \to j \in ℕ$
131	129 130	nnmulcld	$⊢ j \in ℕ \to 2 j \in ℕ$
132		iddvdsexp	$⊢ (2 \in ℤ \land 2 j \in ℕ) \to 2 ∥ 2^{2 j}$
133	127 131 132	syl2anc	$⊢ j \in ℕ \to 2 ∥ 2^{2 j}$
134	133	notnotd	$⊢ j \in ℕ \to \neg \neg 2 ∥ 2^{2 j}$
135	55	nn0zd	$⊢ j \in ℕ \to 2^{2 j} \in ℤ$
136		oddm1even	$⊢ 2^{2 j} \in ℤ \to (\neg 2 ∥ 2^{2 j} \leftrightarrow 2 ∥ (2^{2 j} - 1))$
137	135 136	syl	$⊢ j \in ℕ \to (\neg 2 ∥ 2^{2 j} \leftrightarrow 2 ∥ (2^{2 j} - 1))$
138	134 137	mtbid	$⊢ j \in ℕ \to \neg 2 ∥ (2^{2 j} - 1)$
139	138	ad2antlr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to \neg 2 ∥ (2^{2 j} - 1)$
140		breq2	$⊢ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1 \to (2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \leftrightarrow 2 ∥ (2^{2 j} - 1))$
141	140	notbid	$⊢ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1 \to (\neg 2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \leftrightarrow \neg 2 ∥ (2^{2 j} - 1))$
142	141	adantl	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1) \to (\neg 2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \leftrightarrow \neg 2 ∥ (2^{2 j} - 1))$
143		fzfid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (0 \dots M - 1) \in Fin$
144	112	ad4ant14	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land k \in (0 \dots M - 1)) \to P^{k} \in ℤ$
145		elnn0	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℕ \lor k = 0)$
146		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
147		simpr	$⊢ (P \in ℙ \land P \neq 2) \to P \neq 2$
148	147	necomd	$⊢ (P \in ℙ \land P \neq 2) \to 2 \neq P$
149	146 148	sylbi	$⊢ P \in (ℙ ∖ \{2\}) \to 2 \neq P$
150	149	adantl	$⊢ (k \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2 \neq P$
151	150	neneqd	$⊢ (k \in ℕ \land P \in (ℙ ∖ \{2\})) \to \neg 2 = P$
152		2prm	$⊢ 2 \in ℙ$
153	11	adantl	$⊢ (k \in ℕ \land P \in (ℙ ∖ \{2\})) \to P \in ℙ$
154		simpl	$⊢ (k \in ℕ \land P \in (ℙ ∖ \{2\})) \to k \in ℕ$
155		prmdvdsexpb	$⊢ (2 \in ℙ \land P \in ℙ \land k \in ℕ) \to (2 ∥ P^{k} \leftrightarrow 2 = P)$
156	152 153 154 155	mp3an2i	$⊢ (k \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2 ∥ P^{k} \leftrightarrow 2 = P)$
157	151 156	mtbird	$⊢ (k \in ℕ \land P \in (ℙ ∖ \{2\})) \to \neg 2 ∥ P^{k}$
158	157	ex	$⊢ k \in ℕ \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
159		n2dvds1	$⊢ \neg 2 ∥ 1$
160		oveq2	$⊢ k = 0 \to P^{k} = P^{0}$
161	98	exp0d	$⊢ P \in (ℙ ∖ \{2\}) \to P^{0} = 1$
162	160 161	sylan9eq	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to P^{k} = 1$
163	162	breq2d	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to (2 ∥ P^{k} \leftrightarrow 2 ∥ 1)$
164	159 163	mtbiri	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to \neg 2 ∥ P^{k}$
165	164	ex	$⊢ k = 0 \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
166	158 165	jaoi	$⊢ (k \in ℕ \lor k = 0) \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
167	145 166	sylbi	$⊢ k \in ℕ_{0} \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
168	167 109	syl11	$⊢ P \in (ℙ ∖ \{2\}) \to (k \in (0 \dots M - 1) \to \neg 2 ∥ P^{k})$
169	168	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (k \in (0 \dots M - 1) \to \neg 2 ∥ P^{k})$
170	169	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (k \in (0 \dots M - 1) \to \neg 2 ∥ P^{k})$
171	170	imp	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land k \in (0 \dots M - 1)) \to \neg 2 ∥ P^{k}$
172		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
173		hashfz0	$⊢ M - 1 \in ℕ_{0} \to \|(0 \dots M - 1)\| = M - 1 + 1$
174	172 173	syl	$⊢ M \in ℕ \to \|(0 \dots M - 1)\| = M - 1 + 1$
175		nncn	$⊢ M \in ℕ \to M \in ℂ$
176		1cnd	$⊢ M \in ℕ \to 1 \in ℂ$
177	175 176	npcand	$⊢ M \in ℕ \to M - 1 + 1 = M$
178	174 177	eqtr2d	$⊢ M \in ℕ \to M = \|(0 \dots M - 1)\|$
179	178	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M = \|(0 \dots M - 1)\|$
180	179	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to M = \|(0 \dots M - 1)\|$
181	180	breq2d	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to (2 ∥ M \leftrightarrow 2 ∥ \|(0 \dots M - 1)\|)$
182	181	biimpa	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2 ∥ \|(0 \dots M - 1)\|$
183	143 144 171 182	evensumodd	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2 ∥ \sum_{k = 0}^{M - 1} P^{k}$
184	183	olcd	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (2 ∥ (\frac{P - 1}{2}) \lor 2 ∥ \sum_{k = 0}^{M - 1} P^{k})$
185	152	a1i	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to 2 \in ℙ$
186		oddn2prm	$⊢ P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P$
187		oddm1d2	$⊢ P \in ℤ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
188	15 187	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
189	186 188	mpbid	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℤ$
190	189	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to \frac{P - 1}{2} \in ℤ$
191		fzfid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (0 \dots M - 1) \in Fin$
192	14	ad2antrr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land k \in (0 \dots M - 1)) \to P \in ℕ_{0}$
193	109	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land k \in (0 \dots M - 1)) \to k \in ℕ_{0}$
194	192 193	nn0expcld	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land k \in (0 \dots M - 1)) \to P^{k} \in ℕ_{0}$
195	194	nn0zd	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ) \land k \in (0 \dots M - 1)) \to P^{k} \in ℤ$
196	191 195	fsumzcl	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to \sum_{k = 0}^{M - 1} P^{k} \in ℤ$
197	185 190 196	3jca	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ) \to (2 \in ℙ \land \frac{P - 1}{2} \in ℤ \land \sum_{k = 0}^{M - 1} P^{k} \in ℤ)$
198	197	3adant3	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (2 \in ℙ \land \frac{P - 1}{2} \in ℤ \land \sum_{k = 0}^{M - 1} P^{k} \in ℤ)$
199		euclemma	$⊢ (2 \in ℙ \land \frac{P - 1}{2} \in ℤ \land \sum_{k = 0}^{M - 1} P^{k} \in ℤ) \to (2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \leftrightarrow (2 ∥ (\frac{P - 1}{2}) \lor 2 ∥ \sum_{k = 0}^{M - 1} P^{k}))$
200	198 199	syl	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \leftrightarrow (2 ∥ (\frac{P - 1}{2}) \lor 2 ∥ \sum_{k = 0}^{M - 1} P^{k}))$
201	200	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \leftrightarrow (2 ∥ (\frac{P - 1}{2}) \lor 2 ∥ \sum_{k = 0}^{M - 1} P^{k}))$
202	184 201	mpbird	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to 2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k}$
203	202	pm2.24d	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (\neg 2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \to M = 1)$
204	203	adantr	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1) \to (\neg 2 ∥ (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} \to M = 1)$
205	142 204	sylbird	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land (\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1) \to (\neg 2 ∥ (2^{2 j} - 1) \to M = 1)$
206	205	ex	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to ((\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1 \to (\neg 2 ∥ (2^{2 j} - 1) \to M = 1))$
207	139 206	mpid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to ((\frac{P - 1}{2}) \sum_{k = 0}^{M - 1} P^{k} = 2^{2 j} - 1 \to M = 1)$
208	126 207	sylbid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (\frac{(P - 1) \sum_{k = 0}^{M - 1} P^{k}}{2} = 2^{2 j} - 1 \to M = 1)$
209	123 208	sylbird	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to ((P - 1) \sum_{k = 0}^{M - 1} P^{k} = 2 (2^{2 j} - 1) \to M = 1)$
210	103 209	sylbid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (P^{M} - 1 = 2 (2^{2 j} - 1) \to M = 1)$
211	96 210	sylbird	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \to (2 (2^{2 j} - 1) + 1 = P^{M} \to M = 1)$
212	211	adantr	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land 2 j + 1 = N) \to (2 (2^{2 j} - 1) + 1 = P^{M} \to M = 1)$
213	84 212	sylbid	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \land 2 ∥ M) \land 2 j + 1 = N) \to (2^{N} - 1 = P^{M} \to M = 1)$
214	213	exp31	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to (2 ∥ M \to (2 j + 1 = N \to (2^{N} - 1 = P^{M} \to M = 1)))$
215	214	com23	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land j \in ℕ) \to (2 j + 1 = N \to (2 ∥ M \to (2^{N} - 1 = P^{M} \to M = 1)))$
216	215	rexlimdva	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\exists j \in ℕ 2 j + 1 = N \to (2 ∥ M \to (2^{N} - 1 = P^{M} \to M = 1)))$
217	216	com34	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\exists j \in ℕ 2 j + 1 = N \to (2^{N} - 1 = P^{M} \to (2 ∥ M \to M = 1)))$
218	217	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg N = 1) \to (\exists j \in ℕ 2 j + 1 = N \to (2^{N} - 1 = P^{M} \to (2 ∥ M \to M = 1)))$
219	45 218	sylbid	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg N = 1) \to (\neg 2 ∥ N \to (2^{N} - 1 = P^{M} \to (2 ∥ M \to M = 1)))$
220	219	com24	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg N = 1) \to (2 ∥ M \to (2^{N} - 1 = P^{M} \to (\neg 2 ∥ N \to M = 1)))$
221	220	ex	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\neg N = 1 \to (2 ∥ M \to (2^{N} - 1 = P^{M} \to (\neg 2 ∥ N \to M = 1))))$
222	221	com25	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\neg 2 ∥ N \to (2 ∥ M \to (2^{N} - 1 = P^{M} \to (\neg N = 1 \to M = 1))))$
223	222	impd	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((\neg 2 ∥ N \land 2 ∥ M) \to (2^{N} - 1 = P^{M} \to (\neg N = 1 \to M = 1)))$
224	223	3imp	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg 2 ∥ N \land 2 ∥ M) \land 2^{N} - 1 = P^{M}) \to (\neg N = 1 \to M = 1)$
225	38 224	pm2.61d	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg 2 ∥ N \land 2 ∥ M) \land 2^{N} - 1 = P^{M}) \to M = 1$

Metamath Proof Explorer

Theorem lighneallem3

Proof