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 e. ( FPPr ` N ) -> X e. NN )

Proof

Step	Hyp	Ref	Expression
1		fpprbasnn	|- ( X e. ( FPPr ` N ) -> N e. NN )
2		fpprel	|- ( N e. NN -> ( X e. ( FPPr ` N ) <-> ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) ) )
3		eluz4nn	|- ( X e. ( ZZ>= ` 4 ) -> X e. NN )
4	3	3ad2ant1	|- ( ( X e. ( ZZ>= ` 4 ) /\ X e/ Prime /\ ( ( N ^ ( X - 1 ) ) mod X ) = 1 ) -> X e. NN )
5	2 4	biimtrdi	|- ( N e. NN -> ( X e. ( FPPr ` N ) -> X e. NN ) )
6	1 5	mpcom	|- ( X e. ( FPPr ` N ) -> X e. NN )