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