Definition df-fppr

Description: Define the function that maps a positive integer to the set ofFermat 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 x e. NN /\ x e/ Prime because x = 1 would fulfil this requirement, but should not be regarded as "composite" integer). (Contributed by AV, 29-May-2023)

	Ref	Expression
Assertion	df-fppr	⊢ FPPr = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfppr	⊢ FPPr
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		vx	⊢ 𝑥
4		cuz	⊢ ℤ≥
5		c4	⊢ 4
6	5 4	cfv	⊢ ( ℤ≥ ‘ 4 )
7	3	cv	⊢ 𝑥
8		cprime	⊢ ℙ
9	7 8	wnel	⊢ 𝑥 ∉ ℙ
10		cdvds	⊢ ∥
11	1	cv	⊢ 𝑛
12		cexp	⊢ ↑
13		cmin	⊢ −
14		c1	⊢ 1
15	7 14 13	co	⊢ ( 𝑥 − 1 )
16	11 15 12	co	⊢ ( 𝑛 ↑ ( 𝑥 − 1 ) )
17	16 14 13	co	⊢ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 )
18	7 17 10	wbr	⊢ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 )
19	9 18	wa	⊢ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) )
20	19 3 6	crab	⊢ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) }
21	1 2 20	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )
22	0 21	wceq	⊢ FPPr = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )