Definition df-fppr 43975

Description: Define the function that maps a positive integer to the set of Fermat pseudoprimes to the base of this positive integer. Since Fermat pseudoprimes shall be composite (positive) integers, they must be nonprime integers greater than or equal to 4 (we cannot use 𝑥 ∈ ℕ ∧ 𝑥 ∉ ℙ because 𝑥 = 1 would fulfil this requirement, but should not be regarded as "composite" integer). (Contributed by AV, 29-May-2023.)

Assertion

Ref	Expression
df-fppr	⊢ FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-fppr

Step	Hyp	Ref	Expression
1		cfppr 43974	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 11624	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1536	. . . . . 6 class 𝑥
6		cprime 15998	. . . . . 6 class ℙ
7	5, 6	wnel 3123	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1536	. . . . . . . 8 class 𝑛
9		c1 10524	. . . . . . . . 9 class 1
10		cmin 10856	. . . . . . . . 9 class −
11	5, 9, 10	co 7142	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13419	. . . . . . . 8 class ↑
13	8, 11, 12	co 7142	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7142	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 15592	. . . . . 6 class ∥
16	5, 14, 15	wbr 5052	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 398	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 11681	. . . . 5 class 4
19		cuz 12230	. . . . 5 class ℤ≥
20	18, 19	cfv 6341	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3142	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5132	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1537	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  43976  fpprbasnn  43979