Definition df-fppr 46037

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 46036	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12162	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1540	. . . . . 6 class 𝑥
6		cprime 16558	. . . . . 6 class ℙ
7	5, 6	wnel 3045	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1540	. . . . . . . 8 class 𝑛
9		c1 11061	. . . . . . . . 9 class 1
10		cmin 11394	. . . . . . . . 9 class −
11	5, 9, 10	co 7362	. . . . . . . 8 class (𝑥 − 1)
12		cexp 13977	. . . . . . . 8 class ↑
13	8, 11, 12	co 7362	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7362	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16147	. . . . . 6 class ∥
16	5, 14, 15	wbr 5110	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 396	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12219	. . . . 5 class 4
19		cuz 12772	. . . . 5 class ℤ≥
20	18, 19	cfv 6501	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3405	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5193	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1541	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  46038  fpprbasnn  46041