Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension 2)
Fermat pseudoprimes
fppr
Next ⟩
fpprmod
Metamath Proof Explorer
Ascii
Unicode
Theorem
fppr
Description:
The set of Fermat pseudoprimes to the base
N
.
(Contributed by
AV
, 29-May-2023)
Ref
Expression
Assertion
fppr
⊢
N
∈
ℕ
→
FPPr
⁡
N
=
x
∈
ℤ
≥
4
|
x
∉
ℙ
∧
x
∥
N
x
−
1
−
1
Proof
Step
Hyp
Ref
Expression
1
oveq1
⊢
n
=
N
→
n
x
−
1
=
N
x
−
1
2
1
oveq1d
⊢
n
=
N
→
n
x
−
1
−
1
=
N
x
−
1
−
1
3
2
breq2d
⊢
n
=
N
→
x
∥
n
x
−
1
−
1
↔
x
∥
N
x
−
1
−
1
4
3
anbi2d
⊢
n
=
N
→
x
∉
ℙ
∧
x
∥
n
x
−
1
−
1
↔
x
∉
ℙ
∧
x
∥
N
x
−
1
−
1
5
4
rabbidv
⊢
n
=
N
→
x
∈
ℤ
≥
4
|
x
∉
ℙ
∧
x
∥
n
x
−
1
−
1
=
x
∈
ℤ
≥
4
|
x
∉
ℙ
∧
x
∥
N
x
−
1
−
1
6
df-fppr
⊢
FPPr
=
n
∈
ℕ
⟼
x
∈
ℤ
≥
4
|
x
∉
ℙ
∧
x
∥
n
x
−
1
−
1
7
fvex
⊢
ℤ
≥
4
∈
V
8
7
rabex
⊢
x
∈
ℤ
≥
4
|
x
∉
ℙ
∧
x
∥
N
x
−
1
−
1
∈
V
9
5
6
8
fvmpt
⊢
N
∈
ℕ
→
FPPr
⁡
N
=
x
∈
ℤ
≥
4
|
x
∉
ℙ
∧
x
∥
N
x
−
1
−
1