Theorem fppr

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

	Ref	Expression
Assertion	fppr	$$⊢N\in \mathbb{N}\to \mathrm{FPPr}\left(N\right)=\left\{x\in {\mathbb{Z}}_{\ge 4}|\left(x\notin \mathbb{P}\wedge x\parallel \left(N^{x-1}-1\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢n=N\to n^{x-1}=N^{x-1}$$
2	1	oveq1d	$$⊢n=N\to n^{x-1}-1=N^{x-1}-1$$
3	2	breq2d	$$⊢n=N\to \left(x\parallel \left(n^{x-1}-1\right)\leftrightarrow x\parallel \left(N^{x-1}-1\right)\right)$$
4	3	anbi2d	$$⊢n=N\to \left(\left(x\notin \mathbb{P}\wedge x\parallel \left(n^{x-1}-1\right)\right)\leftrightarrow \left(x\notin \mathbb{P}\wedge x\parallel \left(N^{x-1}-1\right)\right)\right)$$
5	4	rabbidv	$$⊢n=N\to \left\{x\in {\mathbb{Z}}_{\ge 4}|\left(x\notin \mathbb{P}\wedge x\parallel \left(n^{x-1}-1\right)\right)\right\}=\left\{x\in {\mathbb{Z}}_{\ge 4}|\left(x\notin \mathbb{P}\wedge x\parallel \left(N^{x-1}-1\right)\right)\right\}$$
6		df-fppr	$$⊢\mathrm{FPPr}=\left(n\in \mathbb{N}⟼\left\{x\in {\mathbb{Z}}_{\ge 4}|\left(x\notin \mathbb{P}\wedge x\parallel \left(n^{x-1}-1\right)\right)\right\}\right)$$
7		fvex	$$⊢{\mathbb{Z}}_{\ge 4}\in \mathrm{V}$$
8	7	rabex	$$⊢\left\{x\in {\mathbb{Z}}_{\ge 4}|\left(x\notin \mathbb{P}\wedge x\parallel \left(N^{x-1}-1\right)\right)\right\}\in \mathrm{V}$$
9	5 6 8	fvmpt	$$⊢N\in \mathbb{N}\to \mathrm{FPPr}\left(N\right)=\left\{x\in {\mathbb{Z}}_{\ge 4}|\left(x\notin \mathbb{P}\wedge x\parallel \left(N^{x-1}-1\right)\right)\right\}$$