Theorem fppr

Description: The set of Fermat pseudoprimes to the base N . (Contributed by AV, 29-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ↑ ( 𝑥 − 1 ) ) = ( 𝑁 ↑ ( 𝑥 − 1 ) ) )
2	1	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) = ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) )
3	2	breq2d	⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ↔ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) )
4	3	anbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) ↔ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) ) )
5	4	rabbidv	⊢ ( 𝑛 = 𝑁 → { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )
6		df-fppr	⊢ FPPr = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )
7		fvex	⊢ ( ℤ≥ ‘ 4 ) ∈ V
8	7	rabex	⊢ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } ∈ V
9	5 6 8	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( FPPr ‘ 𝑁 ) = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )