Definition df-fppr 47739

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 47738	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12240	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1539	. . . . . 6 class 𝑥
6		cprime 16690	. . . . . 6 class ℙ
7	5, 6	wnel 3036	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1539	. . . . . . . 8 class 𝑛
9		c1 11130	. . . . . . . . 9 class 1
10		cmin 11466	. . . . . . . . 9 class −
11	5, 9, 10	co 7405	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14079	. . . . . . . 8 class ↑
13	8, 11, 12	co 7405	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7405	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16272	. . . . . 6 class ∥
16	5, 14, 15	wbr 5119	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 395	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12297	. . . . 5 class 4
19		cuz 12852	. . . . 5 class ℤ≥
20	18, 19	cfv 6531	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3415	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5201	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1540	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  47740  fpprbasnn  47743