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 ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑋 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 fpprbasnn ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ )
2 fpprel ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
3 eluz4nn ( 𝑋 ∈ ( ℤ ‘ 4 ) → 𝑋 ∈ ℕ )
4 3 3ad2ant1 ( ( 𝑋 ∈ ( ℤ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → 𝑋 ∈ ℕ )
5 2 4 syl6bi ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑋 ∈ ℕ ) )
6 1 5 mpcom ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑋 ∈ ℕ )