Metamath Proof Explorer


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 syl6bi
 |-  ( N e. NN -> ( X e. ( FPPr ` N ) -> X e. NN ) )
6 1 5 mpcom
 |-  ( X e. ( FPPr ` N ) -> X e. NN )