Theorem fpprbasnn

Description: The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023)

	Ref	Expression
Assertion	fpprbasnn	$$⊢X\in \mathrm{FPPr}\left(N\right)\to N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$$⊢N\in \mathbb{N}\to \left(X\in \mathrm{FPPr}\left(N\right)\to N\in \mathbb{N}\right)$$
2		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)$$
3	2	fvmptndm	$$⊢\neg N\in \mathbb{N}\to \mathrm{FPPr}\left(N\right)=\varnothing$$
4		eleq2	$$⊢\mathrm{FPPr}\left(N\right)=\varnothing \to \left(X\in \mathrm{FPPr}\left(N\right)\leftrightarrow X\in \varnothing \right)$$
5		noel	$$⊢\neg X\in \varnothing$$
6	5	pm2.21i	$$⊢X\in \varnothing \to N\in \mathbb{N}$$
7	4 6	biimtrdi	$$⊢\mathrm{FPPr}\left(N\right)=\varnothing \to \left(X\in \mathrm{FPPr}\left(N\right)\to N\in \mathbb{N}\right)$$
8	3 7	syl	$$⊢\neg N\in \mathbb{N}\to \left(X\in \mathrm{FPPr}\left(N\right)\to N\in \mathbb{N}\right)$$
9	1 8	pm2.61i	$$⊢X\in \mathrm{FPPr}\left(N\right)\to N\in \mathbb{N}$$