Definition df-fppr 45144

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 45143	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 11971	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1538	. . . . . 6 class 𝑥
6		cprime 16374	. . . . . 6 class ℙ
7	5, 6	wnel 3049	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1538	. . . . . . . 8 class 𝑛
9		c1 10870	. . . . . . . . 9 class 1
10		cmin 11203	. . . . . . . . 9 class −
11	5, 9, 10	co 7277	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13780	. . . . . . . 8 class ↑
13	8, 11, 12	co 7277	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7277	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 15961	. . . . . 6 class ∥
16	5, 14, 15	wbr 5076	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 396	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12028	. . . . 5 class 4
19		cuz 12580	. . . . 5 class ℤ≥
20	18, 19	cfv 6435	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3068	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5159	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1539	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  45145  fpprbasnn  45148