Definition df-fppr 48216

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 48215	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12165	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1546	. . . . . 6 class 𝑥
6		cprime 16631	. . . . . 6 class ℙ
7	5, 6	wnel 3038	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1546	. . . . . . . 8 class 𝑛
9		c1 11030	. . . . . . . . 9 class 1
10		cmin 11368	. . . . . . . . 9 class −
11	5, 9, 10	co 7356	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14014	. . . . . . . 8 class ↑
13	8, 11, 12	co 7356	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7356	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16212	. . . . . 6 class ∥
16	5, 14, 15	wbr 5072	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 396	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12229	. . . . 5 class 4
19		cuz 12779	. . . . 5 class ℤ≥
20	18, 19	cfv 6485	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3391	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5153	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1547	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  48217  fpprbasnn  48220