Definition df-fppr 48308

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 48307	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12204	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1558	. . . . . 6 class 𝑥
6		cprime 16696	. . . . . 6 class ℙ
7	5, 6	wnel 3060	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1558	. . . . . . . 8 class 𝑛
9		c1 11068	. . . . . . . . 9 class 1
10		cmin 11408	. . . . . . . . 9 class −
11	5, 9, 10	co 7391	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14068	. . . . . . . 8 class ↑
13	8, 11, 12	co 7391	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7391	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16277	. . . . . 6 class ∥
16	5, 14, 15	wbr 5097	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 399	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12268	. . . . 5 class 4
19		cuz 12833	. . . . 5 class ℤ≥
20	18, 19	cfv 6516	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3413	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5178	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1559	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  48309  fpprbasnn  48312