Definition df-fppr 47712

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 47711	. 2 class FPPr
2		vn	. . 3 setvar 𝑛
3		cn 12266	. . 3 class ℕ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1539	. . . . . 6 class 𝑥
6		cprime 16708	. . . . . 6 class ℙ
7	5, 6	wnel 3046	. . . . 5 wff 𝑥 ∉ ℙ
8	2	cv 1539	. . . . . . . 8 class 𝑛
9		c1 11156	. . . . . . . . 9 class 1
10		cmin 11492	. . . . . . . . 9 class −
11	5, 9, 10	co 7431	. . . . . . . 8 class (𝑥 − 1)
12		cexp 14102	. . . . . . . 8 class ↑
13	8, 11, 12	co 7431	. . . . . . 7 class (𝑛↑(𝑥 − 1))
14	13, 9, 10	co 7431	. . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15		cdvds 16290	. . . . . 6 class ∥
16	5, 14, 15	wbr 5143	. . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
17	7, 16	wa 395	. . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18		c4 12323	. . . . 5 class 4
19		cuz 12878	. . . . 5 class ℤ≥
20	18, 19	cfv 6561	. . . 4 class (ℤ≥‘4)
21	17, 4, 20	crab 3436	. . 3 class {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
22	2, 3, 21	cmpt 5225	. 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
23	1, 22	wceq 1540	1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})

This definition is referenced by:  fppr  47713  fpprbasnn  47716