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 FPPr N X

Proof

Step Hyp Ref Expression
1 fpprbasnn X FPPr N N
2 fpprel N X FPPr N X 4 X N X 1 mod X = 1
3 eluz4nn X 4 X
4 3 3ad2ant1 X 4 X N X 1 mod X = 1 X
5 2 4 syl6bi N X FPPr N X
6 1 5 mpcom X FPPr N X