Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension)
Mersenne primes
lighneallem4b
Next ⟩
lighneallem4
Metamath Proof Explorer
Ascii
Unicode
Theorem
lighneallem4b
Description:
Lemma 2 for
lighneallem4
.
(Contributed by
AV
, 16-Aug-2021)
Ref
Expression
Assertion
lighneallem4b
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℤ
≥
2
Proof
Step
Hyp
Ref
Expression
1
2z
⊢
2
∈
ℤ
2
1
a1i
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
2
∈
ℤ
3
fzfid
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
0
…
M
−
1
∈
Fin
4
neg1z
⊢
−
1
∈
ℤ
5
elfznn0
⊢
k
∈
0
…
M
−
1
→
k
∈
ℕ
0
6
zexpcl
⊢
−
1
∈
ℤ
∧
k
∈
ℕ
0
→
−
1
k
∈
ℤ
7
4
5
6
sylancr
⊢
k
∈
0
…
M
−
1
→
−
1
k
∈
ℤ
8
7
adantl
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
k
∈
0
…
M
−
1
→
−
1
k
∈
ℤ
9
eluzge2nn0
⊢
A
∈
ℤ
≥
2
→
A
∈
ℕ
0
10
9
adantr
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
A
∈
ℕ
0
11
10
adantr
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
k
∈
0
…
M
−
1
→
A
∈
ℕ
0
12
5
adantl
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
k
∈
0
…
M
−
1
→
k
∈
ℕ
0
13
11
12
nn0expcld
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
k
∈
0
…
M
−
1
→
A
k
∈
ℕ
0
14
13
nn0zd
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
k
∈
0
…
M
−
1
→
A
k
∈
ℤ
15
8
14
zmulcld
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
k
∈
0
…
M
−
1
→
−
1
k
A
k
∈
ℤ
16
3
15
fsumzcl
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℤ
17
16
3adant3
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℤ
18
simp1
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
∈
ℤ
≥
2
19
3z
⊢
3
∈
ℤ
20
19
a1i
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
3
∈
ℤ
21
eluzelz
⊢
M
∈
ℤ
≥
2
→
M
∈
ℤ
22
21
3ad2ant2
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
M
∈
ℤ
23
eluz2
⊢
M
∈
ℤ
≥
2
↔
2
∈
ℤ
∧
M
∈
ℤ
∧
2
≤
M
24
2re
⊢
2
∈
ℝ
25
24
a1i
⊢
M
∈
ℤ
→
2
∈
ℝ
26
zre
⊢
M
∈
ℤ
→
M
∈
ℝ
27
25
26
leloed
⊢
M
∈
ℤ
→
2
≤
M
↔
2
<
M
∨
2
=
M
28
zltp1le
⊢
2
∈
ℤ
∧
M
∈
ℤ
→
2
<
M
↔
2
+
1
≤
M
29
1
28
mpan
⊢
M
∈
ℤ
→
2
<
M
↔
2
+
1
≤
M
30
29
biimpd
⊢
M
∈
ℤ
→
2
<
M
→
2
+
1
≤
M
31
df-3
⊢
3
=
2
+
1
32
31
breq1i
⊢
3
≤
M
↔
2
+
1
≤
M
33
30
32
syl6ibr
⊢
M
∈
ℤ
→
2
<
M
→
3
≤
M
34
33
a1i
⊢
¬
2
∥
M
→
M
∈
ℤ
→
2
<
M
→
3
≤
M
35
34
com13
⊢
2
<
M
→
M
∈
ℤ
→
¬
2
∥
M
→
3
≤
M
36
z2even
⊢
2
∥
2
37
breq2
⊢
2
=
M
→
2
∥
2
↔
2
∥
M
38
36
37
mpbii
⊢
2
=
M
→
2
∥
M
39
38
pm2.24d
⊢
2
=
M
→
¬
2
∥
M
→
3
≤
M
40
39
a1d
⊢
2
=
M
→
M
∈
ℤ
→
¬
2
∥
M
→
3
≤
M
41
35
40
jaoi
⊢
2
<
M
∨
2
=
M
→
M
∈
ℤ
→
¬
2
∥
M
→
3
≤
M
42
41
com12
⊢
M
∈
ℤ
→
2
<
M
∨
2
=
M
→
¬
2
∥
M
→
3
≤
M
43
27
42
sylbid
⊢
M
∈
ℤ
→
2
≤
M
→
¬
2
∥
M
→
3
≤
M
44
43
imp
⊢
M
∈
ℤ
∧
2
≤
M
→
¬
2
∥
M
→
3
≤
M
45
44
3adant1
⊢
2
∈
ℤ
∧
M
∈
ℤ
∧
2
≤
M
→
¬
2
∥
M
→
3
≤
M
46
23
45
sylbi
⊢
M
∈
ℤ
≥
2
→
¬
2
∥
M
→
3
≤
M
47
46
imp
⊢
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
3
≤
M
48
47
3adant1
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
3
≤
M
49
eluz2
⊢
M
∈
ℤ
≥
3
↔
3
∈
ℤ
∧
M
∈
ℤ
∧
3
≤
M
50
20
22
48
49
syl3anbrc
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
M
∈
ℤ
≥
3
51
eluzelcn
⊢
A
∈
ℤ
≥
2
→
A
∈
ℂ
52
51
3ad2ant1
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
∈
ℂ
53
eluz2nn
⊢
M
∈
ℤ
≥
2
→
M
∈
ℕ
54
53
3ad2ant2
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
M
∈
ℕ
55
simp3
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
¬
2
∥
M
56
52
54
55
oddpwp1fsum
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
M
+
1
=
A
+
1
∑
k
=
0
M
−
1
−
1
k
A
k
57
56
eqcomd
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
+
1
∑
k
=
0
M
−
1
−
1
k
A
k
=
A
M
+
1
58
eluzge2nn0
⊢
M
∈
ℤ
≥
2
→
M
∈
ℕ
0
59
58
adantl
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
M
∈
ℕ
0
60
10
59
nn0expcld
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
A
M
∈
ℕ
0
61
60
nn0cnd
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
A
M
∈
ℂ
62
peano2cn
⊢
A
M
∈
ℂ
→
A
M
+
1
∈
ℂ
63
61
62
syl
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
→
A
M
+
1
∈
ℂ
64
63
3adant3
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
M
+
1
∈
ℂ
65
17
zcnd
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℂ
66
eluz2nn
⊢
A
∈
ℤ
≥
2
→
A
∈
ℕ
67
66
peano2nnd
⊢
A
∈
ℤ
≥
2
→
A
+
1
∈
ℕ
68
67
nncnd
⊢
A
∈
ℤ
≥
2
→
A
+
1
∈
ℂ
69
67
nnne0d
⊢
A
∈
ℤ
≥
2
→
A
+
1
≠
0
70
68
69
jca
⊢
A
∈
ℤ
≥
2
→
A
+
1
∈
ℂ
∧
A
+
1
≠
0
71
70
3ad2ant1
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
+
1
∈
ℂ
∧
A
+
1
≠
0
72
divmul
⊢
A
M
+
1
∈
ℂ
∧
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℂ
∧
A
+
1
∈
ℂ
∧
A
+
1
≠
0
→
A
M
+
1
A
+
1
=
∑
k
=
0
M
−
1
−
1
k
A
k
↔
A
+
1
∑
k
=
0
M
−
1
−
1
k
A
k
=
A
M
+
1
73
64
65
71
72
syl3anc
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
M
+
1
A
+
1
=
∑
k
=
0
M
−
1
−
1
k
A
k
↔
A
+
1
∑
k
=
0
M
−
1
−
1
k
A
k
=
A
M
+
1
74
57
73
mpbird
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
A
M
+
1
A
+
1
=
∑
k
=
0
M
−
1
−
1
k
A
k
75
74
eqcomd
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
∑
k
=
0
M
−
1
−
1
k
A
k
=
A
M
+
1
A
+
1
76
lighneallem4a
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
3
∧
∑
k
=
0
M
−
1
−
1
k
A
k
=
A
M
+
1
A
+
1
→
2
≤
∑
k
=
0
M
−
1
−
1
k
A
k
77
18
50
75
76
syl3anc
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
2
≤
∑
k
=
0
M
−
1
−
1
k
A
k
78
eluz2
⊢
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℤ
≥
2
↔
2
∈
ℤ
∧
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℤ
∧
2
≤
∑
k
=
0
M
−
1
−
1
k
A
k
79
2
17
77
78
syl3anbrc
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
≥
2
∧
¬
2
∥
M
→
∑
k
=
0
M
−
1
−
1
k
A
k
∈
ℤ
≥
2