Definition df-fppr 48917

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 48916	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12339	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1568	. . . . . 6 class 𝑥
6		cprime 16852	. . . . . 6 class ℙ
7	5, 6	wnel 3061	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1568	. . . . . . . 8 class 𝑛
9		c1 11205	. . . . . . . . 9 class 1
10		cmin 11545	. . . . . . . . 9 class −
11	5, 9, 10	co 7421	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14208	. . . . . . . 8 class ↑
13	8, 11, 12	co 7421	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7421	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16428	. . . . . 6 class ∥
16	5, 14, 15	wbr 5102	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 401	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12403	. . . . 5 class 4
19		cuz 12969	. . . . 5 class ℤ≥
20	18, 19	cfv 6539	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3412	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5185	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1569	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is used by:  fppr  48918  fpprbasnn  48921