Definition df-fppr 44850

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 44849	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 11830	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1542	. . . . . 6 class 𝑥
6		cprime 16228	. . . . . 6 class ℙ
7	5, 6	wnel 3046	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1542	. . . . . . . 8 class 𝑛
9		c1 10730	. . . . . . . . 9 class 1
10		cmin 11062	. . . . . . . . 9 class −
11	5, 9, 10	co 7213	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13635	. . . . . . . 8 class ↑
13	8, 11, 12	co 7213	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7213	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 15815	. . . . . 6 class ∥
16	5, 14, 15	wbr 5053	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 399	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 11887	. . . . 5 class 4
19		cuz 12438	. . . . 5 class ℤ≥
20	18, 19	cfv 6380	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3065	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5135	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1543	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  44851  fpprbasnn  44854