Definition df-fppr 48372

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 48371	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12229	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1566	. . . . . 6 class 𝑥
6		cprime 16725	. . . . . 6 class ℙ
7	5, 6	wnel 3070	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1566	. . . . . . . 8 class 𝑛
9		c1 11097	. . . . . . . . 9 class 1
10		cmin 11437	. . . . . . . . 9 class −
11	5, 9, 10	co 7408	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14093	. . . . . . . 8 class ↑
13	8, 11, 12	co 7408	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7408	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16306	. . . . . 6 class ∥
16	5, 14, 15	wbr 5110	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 400	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12293	. . . . 5 class 4
19		cuz 12858	. . . . 5 class ℤ≥
20	18, 19	cfv 6533	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3423	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5193	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1567	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  48373  fpprbasnn  48376