lighneallem4

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

Proof

Step	Hyp	Ref	Expression
1		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3	1 2	expcld	$⊢ N \in ℕ \to 2^{N} \in ℂ$
4	3	3ad2ant3	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to 2^{N} \in ℂ$
5		1cnd	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to 1 \in ℂ$
6		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
7		prmnn	$⊢ P \in ℙ \to P \in ℕ$
8		nncn	$⊢ P \in ℕ \to P \in ℂ$
9	6 7 8	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℂ$
10	9	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P \in ℂ$
11		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
12	11	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℕ_{0}$
13	10 12	expcld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P^{M} \in ℂ$
14	4 5 13	3jca	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (2^{N} \in ℂ \land 1 \in ℂ \land P^{M} \in ℂ)$
15	14	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (2^{N} \in ℂ \land 1 \in ℂ \land P^{M} \in ℂ)$
16		subadd2	$⊢ (2^{N} \in ℂ \land 1 \in ℂ \land P^{M} \in ℂ) \to (2^{N} - 1 = P^{M} \leftrightarrow P^{M} + 1 = 2^{N})$
17	15 16	syl	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (2^{N} - 1 = P^{M} \leftrightarrow P^{M} + 1 = 2^{N})$
18	10	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to P \in ℂ$
19		simpl2	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to M \in ℕ$
20		simpr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to \neg 2 ∥ M$
21	18 19 20	oddpwp1fsum	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to P^{M} + 1 = (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k}$
22	21	eqeq1d	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (P^{M} + 1 = 2^{N} \leftrightarrow (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N})$
23		peano2nn	$⊢ P \in ℕ \to P + 1 \in ℕ$
24	23	nnzd	$⊢ P \in ℕ \to P + 1 \in ℤ$
25	6 7 24	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P + 1 \in ℤ$
26	25	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P + 1 \in ℤ$
27		fzfid	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (0 \dots M - 1) \in Fin$
28		neg1z	$⊢ - 1 \in ℤ$
29	28	a1i	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to - 1 \in ℤ$
30		elfznn0	$⊢ k \in (0 \dots M - 1) \to k \in ℕ_{0}$
31		zexpcl	$⊢ (- 1 \in ℤ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℤ$
32	29 30 31	syl2an	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to {(- 1)}^{k} \in ℤ$
33		nnz	$⊢ P \in ℕ \to P \in ℤ$
34	6 7 33	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ$
35	34	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P \in ℤ$
36		zexpcl	$⊢ (P \in ℤ \land k \in ℕ_{0}) \to P^{k} \in ℤ$
37	35 30 36	syl2an	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to P^{k} \in ℤ$
38	32 37	zmulcld	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land k \in (0 \dots M - 1)) \to {(- 1)}^{k} P^{k} \in ℤ$
39	27 38	fsumzcl	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ$
40	26 39	jca	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (P + 1 \in ℤ \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ)$
41	40	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \land (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N}) \to (P + 1 \in ℤ \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ)$
42		dvdsmul2	$⊢ (P + 1 \in ℤ \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k}$
43	41 42	syl	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \land (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N}) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k}$
44		breq2	$⊢ (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N} \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \leftrightarrow \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N})$
45	44	adantl	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \land (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N}) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \leftrightarrow \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N})$
46		2a1	$⊢ M = 1 \to (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1))$
47		2prm	$⊢ 2 \in ℙ$
48		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
49	6 48	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 2}$
50	49	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to P \in ℤ_{\geq 2}$
51	50	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to P \in ℤ_{\geq 2}$
52		df-ne	$⊢ M \neq 1 \leftrightarrow \neg M = 1$
53		eluz2b3	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℕ \land M \neq 1)$
54	53	simplbi2	$⊢ M \in ℕ \to (M \neq 1 \to M \in ℤ_{\geq 2})$
55	52 54	biimtrrid	$⊢ M \in ℕ \to (\neg M = 1 \to M \in ℤ_{\geq 2})$
56	55	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\neg M = 1 \to M \in ℤ_{\geq 2})$
57	56	com12	$⊢ \neg M = 1 \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℤ_{\geq 2})$
58	57	adantr	$⊢ (\neg M = 1 \land \neg 2 ∥ M) \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M \in ℤ_{\geq 2})$
59	58	impcom	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to M \in ℤ_{\geq 2}$
60		simprr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to \neg 2 ∥ M$
61		lighneallem4b	$⊢ (P \in ℤ_{\geq 2} \land M \in ℤ_{\geq 2} \land \neg 2 ∥ M) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ_{\geq 2}$
62	51 59 60 61	syl3anc	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ_{\geq 2}$
63	2	3ad2ant3	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to N \in ℕ_{0}$
64	63	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to N \in ℕ_{0}$
65		dvdsprmpweqnn	$⊢ (2 \in ℙ \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to \exists n \in ℕ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n})$
66	47 62 64 65	mp3an2i	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to \exists n \in ℕ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n})$
67		2z	$⊢ 2 \in ℤ$
68	67	a1i	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to 2 \in ℤ$
69		iddvdsexp	$⊢ (2 \in ℤ \land n \in ℕ) \to 2 ∥ 2^{n}$
70	68 69	sylan	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to 2 ∥ 2^{n}$
71		breq2	$⊢ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n} \to (2 ∥ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \leftrightarrow 2 ∥ 2^{n})$
72	71	adantl	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n}) \to (2 ∥ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \leftrightarrow 2 ∥ 2^{n})$
73		fzfid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to (0 \dots M - 1) \in Fin$
74	28	a1i	$⊢ P \in ℕ \to - 1 \in ℤ$
75	74 31	sylan	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℤ$
76		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
77	76	adantr	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to P \in ℕ_{0}$
78		simpr	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
79	77 78	nn0expcld	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to P^{k} \in ℕ_{0}$
80	79	nn0zd	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to P^{k} \in ℤ$
81	75 80	zmulcld	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to {(- 1)}^{k} P^{k} \in ℤ$
82	81	ex	$⊢ P \in ℕ \to (k \in ℕ_{0} \to {(- 1)}^{k} P^{k} \in ℤ)$
83	6 7 82	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to (k \in ℕ_{0} \to {(- 1)}^{k} P^{k} \in ℤ)$
84	83	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (k \in ℕ_{0} \to {(- 1)}^{k} P^{k} \in ℤ)$
85	84	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to (k \in ℕ_{0} \to {(- 1)}^{k} P^{k} \in ℤ)$
86	85 30	impel	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \land k \in (0 \dots M - 1)) \to {(- 1)}^{k} P^{k} \in ℤ$
87		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
88		m1expcl2	$⊢ k \in ℤ \to {(- 1)}^{k} \in \{- 1, 1\}$
89	87 88	syl	$⊢ k \in ℕ_{0} \to {(- 1)}^{k} \in \{- 1, 1\}$
90		ovex	$⊢ {(- 1)}^{k} \in V$
91	90	elpr	$⊢ {(- 1)}^{k} \in \{- 1, 1\} \leftrightarrow ({(- 1)}^{k} = - 1 \lor {(- 1)}^{k} = 1)$
92		n2dvdsm1	$⊢ \neg 2 ∥ -1$
93		breq2	$⊢ {(- 1)}^{k} = - 1 \to (2 ∥ {(- 1)}^{k} \leftrightarrow 2 ∥ -1)$
94	92 93	mtbiri	$⊢ {(- 1)}^{k} = - 1 \to \neg 2 ∥ {(- 1)}^{k}$
95		n2dvds1	$⊢ \neg 2 ∥ 1$
96		breq2	$⊢ {(- 1)}^{k} = 1 \to (2 ∥ {(- 1)}^{k} \leftrightarrow 2 ∥ 1)$
97	95 96	mtbiri	$⊢ {(- 1)}^{k} = 1 \to \neg 2 ∥ {(- 1)}^{k}$
98	94 97	jaoi	$⊢ ({(- 1)}^{k} = - 1 \lor {(- 1)}^{k} = 1) \to \neg 2 ∥ {(- 1)}^{k}$
99	98	a1d	$⊢ ({(- 1)}^{k} = - 1 \lor {(- 1)}^{k} = 1) \to (k \in ℕ_{0} \to \neg 2 ∥ {(- 1)}^{k})$
100	91 99	sylbi	$⊢ {(- 1)}^{k} \in \{- 1, 1\} \to (k \in ℕ_{0} \to \neg 2 ∥ {(- 1)}^{k})$
101	89 100	mpcom	$⊢ k \in ℕ_{0} \to \neg 2 ∥ {(- 1)}^{k}$
102	101	adantl	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to \neg 2 ∥ {(- 1)}^{k}$
103		elnn0	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℕ \lor k = 0)$
104		oddn2prm	$⊢ P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P$
105	104	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ) \to \neg 2 ∥ P$
106		simpr	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ) \to k \in ℕ$
107		prmdvdsexp	$⊢ (2 \in ℙ \land P \in ℤ \land k \in ℕ) \to (2 ∥ P^{k} \leftrightarrow 2 ∥ P)$
108	47 34 106 107	mp3an2ani	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ) \to (2 ∥ P^{k} \leftrightarrow 2 ∥ P)$
109	105 108	mtbird	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ) \to \neg 2 ∥ P^{k}$
110	109	expcom	$⊢ k \in ℕ \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
111		oveq2	$⊢ k = 0 \to P^{k} = P^{0}$
112	111	adantr	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to P^{k} = P^{0}$
113	9	adantl	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to P \in ℂ$
114	113	exp0d	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to P^{0} = 1$
115	112 114	eqtrd	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to P^{k} = 1$
116	115	breq2d	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to (2 ∥ P^{k} \leftrightarrow 2 ∥ 1)$
117	95 116	mtbiri	$⊢ (k = 0 \land P \in (ℙ ∖ \{2\})) \to \neg 2 ∥ P^{k}$
118	117	ex	$⊢ k = 0 \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
119	110 118	jaoi	$⊢ (k \in ℕ \lor k = 0) \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
120	103 119	sylbi	$⊢ k \in ℕ_{0} \to (P \in (ℙ ∖ \{2\}) \to \neg 2 ∥ P^{k})$
121	120	impcom	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to \neg 2 ∥ P^{k}$
122		ioran	$⊢ \neg (2 ∥ {(- 1)}^{k} \lor 2 ∥ P^{k}) \leftrightarrow (\neg 2 ∥ {(- 1)}^{k} \land \neg 2 ∥ P^{k})$
123	102 121 122	sylanbrc	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to \neg (2 ∥ {(- 1)}^{k} \lor 2 ∥ P^{k})$
124	28 31	mpan	$⊢ k \in ℕ_{0} \to {(- 1)}^{k} \in ℤ$
125	124	adantl	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℤ$
126	6 7 76	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ_{0}$
127	126	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to P \in ℕ_{0}$
128		simpr	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
129	127 128	nn0expcld	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to P^{k} \in ℕ_{0}$
130	129	nn0zd	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to P^{k} \in ℤ$
131		euclemma	$⊢ (2 \in ℙ \land {(- 1)}^{k} \in ℤ \land P^{k} \in ℤ) \to (2 ∥ {(- 1)}^{k} P^{k} \leftrightarrow (2 ∥ {(- 1)}^{k} \lor 2 ∥ P^{k}))$
132	47 125 130 131	mp3an2i	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to (2 ∥ {(- 1)}^{k} P^{k} \leftrightarrow (2 ∥ {(- 1)}^{k} \lor 2 ∥ P^{k}))$
133	123 132	mtbird	$⊢ (P \in (ℙ ∖ \{2\}) \land k \in ℕ_{0}) \to \neg 2 ∥ {(- 1)}^{k} P^{k}$
134	133	ex	$⊢ P \in (ℙ ∖ \{2\}) \to (k \in ℕ_{0} \to \neg 2 ∥ {(- 1)}^{k} P^{k})$
135	134	3ad2ant1	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (k \in ℕ_{0} \to \neg 2 ∥ {(- 1)}^{k} P^{k})$
136	135	ad2antrr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to (k \in ℕ_{0} \to \neg 2 ∥ {(- 1)}^{k} P^{k})$
137	136 30	impel	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \land k \in (0 \dots M - 1)) \to \neg 2 ∥ {(- 1)}^{k} P^{k}$
138		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
139		hashfz0	$⊢ M - 1 \in ℕ_{0} \to \|(0 \dots M - 1)\| = M - 1 + 1$
140	138 139	syl	$⊢ M \in ℕ \to \|(0 \dots M - 1)\| = M - 1 + 1$
141		nncn	$⊢ M \in ℕ \to M \in ℂ$
142		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
143	141 142	syl	$⊢ M \in ℕ \to M - 1 + 1 = M$
144	140 143	eqtr2d	$⊢ M \in ℕ \to M = \|(0 \dots M - 1)\|$
145	144	3ad2ant2	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to M = \|(0 \dots M - 1)\|$
146	145	adantr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg M = 1) \to M = \|(0 \dots M - 1)\|$
147	146	breq2d	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg M = 1) \to (2 ∥ M \leftrightarrow 2 ∥ \|(0 \dots M - 1)\|)$
148	147	notbid	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg M = 1) \to (\neg 2 ∥ M \leftrightarrow \neg 2 ∥ \|(0 \dots M - 1)\|)$
149	148	biimpd	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg M = 1) \to (\neg 2 ∥ M \to \neg 2 ∥ \|(0 \dots M - 1)\|)$
150	149	impr	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to \neg 2 ∥ \|(0 \dots M - 1)\|$
151	150	adantr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to \neg 2 ∥ \|(0 \dots M - 1)\|$
152	73 86 137 151	oddsumodd	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to \neg 2 ∥ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k}$
153	152	pm2.21d	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to (2 ∥ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \to M = 1)$
154	153	adantr	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n}) \to (2 ∥ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \to M = 1)$
155	72 154	sylbird	$⊢ ((((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \land \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n}) \to (2 ∥ 2^{n} \to M = 1)$
156	155	ex	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n} \to (2 ∥ 2^{n} \to M = 1))$
157	70 156	mpid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \land n \in ℕ) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n} \to M = 1)$
158	157	rexlimdva	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to (\exists n \in ℕ \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{n} \to M = 1)$
159	66 158	syld	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg M = 1 \land \neg 2 ∥ M)) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1)$
160	159	exp32	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\neg M = 1 \to (\neg 2 ∥ M \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1)))$
161	160	com12	$⊢ \neg M = 1 \to ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\neg 2 ∥ M \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1)))$
162	161	impd	$⊢ \neg M = 1 \to (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1))$
163	46 162	pm2.61i	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1)$
164	163	adantr	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \land (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N}) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ 2^{N} \to M = 1)$
165	45 164	sylbid	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \land (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N}) \to (\sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} ∥ (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} \to M = 1)$
166	43 165	mpd	$⊢ (((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \land (P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N}) \to M = 1$
167	166	ex	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to ((P + 1) \sum_{k = 0}^{M - 1} {(- 1)}^{k} P^{k} = 2^{N} \to M = 1)$
168	22 167	sylbid	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (P^{M} + 1 = 2^{N} \to M = 1)$
169	17 168	sylbid	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land \neg 2 ∥ M) \to (2^{N} - 1 = P^{M} \to M = 1)$
170	169	ex	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (\neg 2 ∥ M \to (2^{N} - 1 = P^{M} \to M = 1))$
171	170	adantld	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((\neg 2 ∥ N \land \neg 2 ∥ M) \to (2^{N} - 1 = P^{M} \to M = 1))$
172	171	3imp	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg 2 ∥ N \land \neg 2 ∥ M) \land 2^{N} - 1 = P^{M}) \to M = 1$

Metamath Proof Explorer

Theorem lighneallem4

Proof