Theorem fpprnn

Description: A Fermat pseudoprime to the base N is a positive integer. (Contributed by AV, 30-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fpprbasnn	$$⊢X\in \mathrm{FPPr}\left(N\right)\to N\in \mathbb{N}$$
2		fpprel	$$⊢N\in \mathbb{N}\to \left(X\in \mathrm{FPPr}\left(N\right)\leftrightarrow \left(X\in {\mathbb{Z}}_{\ge 4}\wedge X\notin \mathbb{P}\wedge N^{X-1}\mathrm{mod}X=1\right)\right)$$
3		eluz4nn	$$⊢X\in {\mathbb{Z}}_{\ge 4}\to X\in \mathbb{N}$$
4	3	3ad2ant1	$$⊢\left(X\in {\mathbb{Z}}_{\ge 4}\wedge X\notin \mathbb{P}\wedge N^{X-1}\mathrm{mod}X=1\right)\to X\in \mathbb{N}$$
5	2 4	syl6bi	$$⊢N\in \mathbb{N}\to \left(X\in \mathrm{FPPr}\left(N\right)\to X\in \mathbb{N}\right)$$
6	1 5	mpcom	$$⊢X\in \mathrm{FPPr}\left(N\right)\to X\in \mathbb{N}$$