Definition df-fppr 43969

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 43968	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 11631	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1535	. . . . . 6 class 𝑥
6		cprime 16008	. . . . . 6 class ℙ
7	5, 6	wnel 3122	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1535	. . . . . . . 8 class 𝑛
9		c1 10531	. . . . . . . . 9 class 1
10		cmin 10863	. . . . . . . . 9 class −
11	5, 9, 10	co 7149	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13426	. . . . . . . 8 class ↑
13	8, 11, 12	co 7149	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7149	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 15600	. . . . . 6 class ∥
16	5, 14, 15	wbr 5059	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 398	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 11688	. . . . 5 class 4
19		cuz 12237	. . . . 5 class ℤ≥
20	18, 19	cfv 6348	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3141	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5139	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1536	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  43970  fpprbasnn  43973