Metamath Proof Explorer


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 syl6bi
 |-  ( ( 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 )