Theorem fpprbasnn

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

	Ref	Expression
Assertion	fpprbasnn	|- ( X e. ( FPPr ` N ) -> N e. NN )

Proof

Step	Hyp	Ref	Expression
1		ax-1	|- ( N e. NN -> ( X e. ( FPPr ` N ) -> N e. NN ) )
2		df-fppr	|- FPPr = ( n e. NN |-> { x e. ( ZZ>= ` 4 ) | ( x e/ Prime /\ x || ( ( n ^ ( x - 1 ) ) - 1 ) ) } )
3	2	fvmptndm	|- ( -. N e. NN -> ( FPPr ` N ) = (/) )
4		eleq2	|- ( ( FPPr ` N ) = (/) -> ( X e. ( FPPr ` N ) <-> X e. (/) ) )
5		noel	|- -. X e. (/)
6	5	pm2.21i	|- ( X e. (/) -> N e. NN )
7	4 6	biimtrdi	|- ( ( FPPr ` N ) = (/) -> ( X e. ( FPPr ` N ) -> N e. NN ) )
8	3 7	syl	|- ( -. N e. NN -> ( X e. ( FPPr ` N ) -> N e. NN ) )
9	1 8	pm2.61i	|- ( X e. ( FPPr ` N ) -> N e. NN )