Definition df-fppr 47756

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 47755	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12120	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1540	. . . . . 6 class 𝑥
6		cprime 16577	. . . . . 6 class ℙ
7	5, 6	wnel 3032	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1540	. . . . . . . 8 class 𝑛
9		c1 11002	. . . . . . . . 9 class 1
10		cmin 11339	. . . . . . . . 9 class −
11	5, 9, 10	co 7341	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13963	. . . . . . . 8 class ↑
13	8, 11, 12	co 7341	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7341	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16158	. . . . . 6 class ∥
16	5, 14, 15	wbr 5086	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 395	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12177	. . . . 5 class 4
19		cuz 12727	. . . . 5 class ℤ≥
20	18, 19	cfv 6476	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3395	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5167	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1541	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  47757  fpprbasnn  47760