Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension)
Fermat numbers
fmtnoprmfac2lem1
Next ⟩
fmtnoprmfac2
Metamath Proof Explorer
Ascii
Unicode
Theorem
fmtnoprmfac2lem1
Description:
Lemma for
fmtnoprmfac2
.
(Contributed by
AV
, 26-Jul-2021)
Ref
Expression
Assertion
fmtnoprmfac2lem1
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
2
P
−
1
2
mod
P
=
1
Proof
Step
Hyp
Ref
Expression
1
eluz2nn
⊢
N
∈
ℤ
≥
2
→
N
∈
ℕ
2
eldifi
⊢
P
∈
ℙ
∖
2
→
P
∈
ℙ
3
id
⊢
P
∥
FermatNo
N
→
P
∥
FermatNo
N
4
fmtnoprmfac1
⊢
N
∈
ℕ
∧
P
∈
ℙ
∧
P
∥
FermatNo
N
→
∃
n
∈
ℕ
P
=
n
2
N
+
1
+
1
5
1
2
3
4
syl3an
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
∃
n
∈
ℕ
P
=
n
2
N
+
1
+
1
6
2z
⊢
2
∈
ℤ
7
simp2
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
P
∈
ℙ
∖
2
8
lgsvalmod
⊢
2
∈
ℤ
∧
P
∈
ℙ
∖
2
→
2
/
L
P
mod
P
=
2
P
−
1
2
mod
P
9
8
eqcomd
⊢
2
∈
ℤ
∧
P
∈
ℙ
∖
2
→
2
P
−
1
2
mod
P
=
2
/
L
P
mod
P
10
6
7
9
sylancr
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
2
P
−
1
2
mod
P
=
2
/
L
P
mod
P
11
10
ad2antrr
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
2
P
−
1
2
mod
P
=
2
/
L
P
mod
P
12
nncn
⊢
n
∈
ℕ
→
n
∈
ℂ
13
12
adantl
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
n
∈
ℂ
14
2nn
⊢
2
∈
ℕ
15
14
a1i
⊢
N
∈
ℤ
≥
2
→
2
∈
ℕ
16
eluzge2nn0
⊢
N
∈
ℤ
≥
2
→
N
∈
ℕ
0
17
peano2nn0
⊢
N
∈
ℕ
0
→
N
+
1
∈
ℕ
0
18
16
17
syl
⊢
N
∈
ℤ
≥
2
→
N
+
1
∈
ℕ
0
19
15
18
nnexpcld
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
∈
ℕ
20
19
nncnd
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
∈
ℂ
21
20
adantr
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
2
N
+
1
∈
ℂ
22
13
21
mulcomd
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
n
2
N
+
1
=
2
N
+
1
n
23
8cn
⊢
8
∈
ℂ
24
23
a1i
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
8
∈
ℂ
25
0re
⊢
0
∈
ℝ
26
8pos
⊢
0
<
8
27
25
26
gtneii
⊢
8
≠
0
28
27
a1i
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
8
≠
0
29
21
24
28
divcan2d
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
8
2
N
+
1
8
=
2
N
+
1
30
29
eqcomd
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
2
N
+
1
=
8
2
N
+
1
8
31
30
oveq1d
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
2
N
+
1
n
=
8
2
N
+
1
8
n
32
23
a1i
⊢
N
∈
ℤ
≥
2
→
8
∈
ℂ
33
27
a1i
⊢
N
∈
ℤ
≥
2
→
8
≠
0
34
20
32
33
divcld
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
8
∈
ℂ
35
34
adantr
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
2
N
+
1
8
∈
ℂ
36
24
35
13
mulassd
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
8
2
N
+
1
8
n
=
8
2
N
+
1
8
n
37
22
31
36
3eqtrd
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
n
2
N
+
1
=
8
2
N
+
1
8
n
38
37
oveq1d
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
n
2
N
+
1
+
1
=
8
2
N
+
1
8
n
+
1
39
38
eqeq2d
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
P
=
n
2
N
+
1
+
1
↔
P
=
8
2
N
+
1
8
n
+
1
40
oveq1
⊢
P
=
8
2
N
+
1
8
n
+
1
→
P
mod
8
=
8
2
N
+
1
8
n
+
1
mod
8
41
40
adantl
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
∧
P
=
8
2
N
+
1
8
n
+
1
→
P
mod
8
=
8
2
N
+
1
8
n
+
1
mod
8
42
3m1e2
⊢
3
−
1
=
2
43
eluzle
⊢
N
∈
ℤ
≥
2
→
2
≤
N
44
42
43
eqbrtrid
⊢
N
∈
ℤ
≥
2
→
3
−
1
≤
N
45
3re
⊢
3
∈
ℝ
46
45
a1i
⊢
N
∈
ℤ
≥
2
→
3
∈
ℝ
47
1red
⊢
N
∈
ℤ
≥
2
→
1
∈
ℝ
48
eluzelre
⊢
N
∈
ℤ
≥
2
→
N
∈
ℝ
49
46
47
48
lesubaddd
⊢
N
∈
ℤ
≥
2
→
3
−
1
≤
N
↔
3
≤
N
+
1
50
44
49
mpbid
⊢
N
∈
ℤ
≥
2
→
3
≤
N
+
1
51
3nn0
⊢
3
∈
ℕ
0
52
nn0sub
⊢
3
∈
ℕ
0
∧
N
+
1
∈
ℕ
0
→
3
≤
N
+
1
↔
N
+
1
-
3
∈
ℕ
0
53
51
18
52
sylancr
⊢
N
∈
ℤ
≥
2
→
3
≤
N
+
1
↔
N
+
1
-
3
∈
ℕ
0
54
50
53
mpbid
⊢
N
∈
ℤ
≥
2
→
N
+
1
-
3
∈
ℕ
0
55
15
54
nnexpcld
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
-
3
∈
ℕ
56
55
nnzd
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
-
3
∈
ℤ
57
oveq2
⊢
k
=
2
N
+
1
-
3
→
8
k
=
8
2
N
+
1
-
3
58
57
eqeq1d
⊢
k
=
2
N
+
1
-
3
→
8
k
=
2
N
+
1
↔
8
2
N
+
1
-
3
=
2
N
+
1
59
58
adantl
⊢
N
∈
ℤ
≥
2
∧
k
=
2
N
+
1
-
3
→
8
k
=
2
N
+
1
↔
8
2
N
+
1
-
3
=
2
N
+
1
60
cu2
⊢
2
3
=
8
61
60
eqcomi
⊢
8
=
2
3
62
61
a1i
⊢
N
∈
ℤ
≥
2
→
8
=
2
3
63
2cnne0
⊢
2
∈
ℂ
∧
2
≠
0
64
63
a1i
⊢
N
∈
ℤ
≥
2
→
2
∈
ℂ
∧
2
≠
0
65
eluzelz
⊢
N
∈
ℤ
≥
2
→
N
∈
ℤ
66
65
peano2zd
⊢
N
∈
ℤ
≥
2
→
N
+
1
∈
ℤ
67
3z
⊢
3
∈
ℤ
68
67
a1i
⊢
N
∈
ℤ
≥
2
→
3
∈
ℤ
69
expsub
⊢
2
∈
ℂ
∧
2
≠
0
∧
N
+
1
∈
ℤ
∧
3
∈
ℤ
→
2
N
+
1
-
3
=
2
N
+
1
2
3
70
64
66
68
69
syl12anc
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
-
3
=
2
N
+
1
2
3
71
62
70
oveq12d
⊢
N
∈
ℤ
≥
2
→
8
2
N
+
1
-
3
=
2
3
2
N
+
1
2
3
72
nnexpcl
⊢
2
∈
ℕ
∧
3
∈
ℕ
0
→
2
3
∈
ℕ
73
14
51
72
mp2an
⊢
2
3
∈
ℕ
74
73
nncni
⊢
2
3
∈
ℂ
75
74
a1i
⊢
N
∈
ℤ
≥
2
→
2
3
∈
ℂ
76
2cn
⊢
2
∈
ℂ
77
2ne0
⊢
2
≠
0
78
expne0i
⊢
2
∈
ℂ
∧
2
≠
0
∧
3
∈
ℤ
→
2
3
≠
0
79
76
77
67
78
mp3an
⊢
2
3
≠
0
80
79
a1i
⊢
N
∈
ℤ
≥
2
→
2
3
≠
0
81
20
75
80
divcan2d
⊢
N
∈
ℤ
≥
2
→
2
3
2
N
+
1
2
3
=
2
N
+
1
82
71
81
eqtrd
⊢
N
∈
ℤ
≥
2
→
8
2
N
+
1
-
3
=
2
N
+
1
83
56
59
82
rspcedvd
⊢
N
∈
ℤ
≥
2
→
∃
k
∈
ℤ
8
k
=
2
N
+
1
84
8nn
⊢
8
∈
ℕ
85
2nn0
⊢
2
∈
ℕ
0
86
85
a1i
⊢
N
∈
ℤ
≥
2
→
2
∈
ℕ
0
87
86
18
nn0expcld
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
∈
ℕ
0
88
87
nn0zd
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
∈
ℤ
89
zdiv
⊢
8
∈
ℕ
∧
2
N
+
1
∈
ℤ
→
∃
k
∈
ℤ
8
k
=
2
N
+
1
↔
2
N
+
1
8
∈
ℤ
90
84
88
89
sylancr
⊢
N
∈
ℤ
≥
2
→
∃
k
∈
ℤ
8
k
=
2
N
+
1
↔
2
N
+
1
8
∈
ℤ
91
83
90
mpbid
⊢
N
∈
ℤ
≥
2
→
2
N
+
1
8
∈
ℤ
92
91
adantr
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
2
N
+
1
8
∈
ℤ
93
nnz
⊢
n
∈
ℕ
→
n
∈
ℤ
94
93
adantl
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
n
∈
ℤ
95
92
94
zmulcld
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
2
N
+
1
8
n
∈
ℤ
96
84
nnzi
⊢
8
∈
ℤ
97
2re
⊢
2
∈
ℝ
98
8re
⊢
8
∈
ℝ
99
2lt8
⊢
2
<
8
100
97
98
99
ltleii
⊢
2
≤
8
101
eluz2
⊢
8
∈
ℤ
≥
2
↔
2
∈
ℤ
∧
8
∈
ℤ
∧
2
≤
8
102
6
96
100
101
mpbir3an
⊢
8
∈
ℤ
≥
2
103
mulp1mod1
⊢
2
N
+
1
8
n
∈
ℤ
∧
8
∈
ℤ
≥
2
→
8
2
N
+
1
8
n
+
1
mod
8
=
1
104
95
102
103
sylancl
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
8
2
N
+
1
8
n
+
1
mod
8
=
1
105
1nn
⊢
1
∈
ℕ
106
prid1g
⊢
1
∈
ℕ
→
1
∈
1
7
107
105
106
mp1i
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
1
∈
1
7
108
104
107
eqeltrd
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
8
2
N
+
1
8
n
+
1
mod
8
∈
1
7
109
108
adantr
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
∧
P
=
8
2
N
+
1
8
n
+
1
→
8
2
N
+
1
8
n
+
1
mod
8
∈
1
7
110
41
109
eqeltrd
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
∧
P
=
8
2
N
+
1
8
n
+
1
→
P
mod
8
∈
1
7
111
110
ex
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
P
=
8
2
N
+
1
8
n
+
1
→
P
mod
8
∈
1
7
112
39
111
sylbid
⊢
N
∈
ℤ
≥
2
∧
n
∈
ℕ
→
P
=
n
2
N
+
1
+
1
→
P
mod
8
∈
1
7
113
112
3ad2antl1
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
→
P
=
n
2
N
+
1
+
1
→
P
mod
8
∈
1
7
114
113
imp
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
P
mod
8
∈
1
7
115
2lgs
⊢
P
∈
ℙ
→
2
/
L
P
=
1
↔
P
mod
8
∈
1
7
116
2
115
syl
⊢
P
∈
ℙ
∖
2
→
2
/
L
P
=
1
↔
P
mod
8
∈
1
7
117
116
3ad2ant2
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
2
/
L
P
=
1
↔
P
mod
8
∈
1
7
118
117
ad2antrr
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
2
/
L
P
=
1
↔
P
mod
8
∈
1
7
119
114
118
mpbird
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
2
/
L
P
=
1
120
119
oveq1d
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
2
/
L
P
mod
P
=
1
mod
P
121
prmuz2
⊢
P
∈
ℙ
→
P
∈
ℤ
≥
2
122
eluzelre
⊢
P
∈
ℤ
≥
2
→
P
∈
ℝ
123
eluz2gt1
⊢
P
∈
ℤ
≥
2
→
1
<
P
124
122
123
jca
⊢
P
∈
ℤ
≥
2
→
P
∈
ℝ
∧
1
<
P
125
121
124
syl
⊢
P
∈
ℙ
→
P
∈
ℝ
∧
1
<
P
126
1mod
⊢
P
∈
ℝ
∧
1
<
P
→
1
mod
P
=
1
127
2
125
126
3syl
⊢
P
∈
ℙ
∖
2
→
1
mod
P
=
1
128
127
3ad2ant2
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
1
mod
P
=
1
129
128
ad2antrr
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
1
mod
P
=
1
130
11
120
129
3eqtrd
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
∧
n
∈
ℕ
∧
P
=
n
2
N
+
1
+
1
→
2
P
−
1
2
mod
P
=
1
131
130
rexlimdva2
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
∃
n
∈
ℕ
P
=
n
2
N
+
1
+
1
→
2
P
−
1
2
mod
P
=
1
132
5
131
mpd
⊢
N
∈
ℤ
≥
2
∧
P
∈
ℙ
∖
2
∧
P
∥
FermatNo
N
→
2
P
−
1
2
mod
P
=
1