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

Proof

Step Hyp Ref Expression
1 ax-1 ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ ) )
2 df-fppr FPPr = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ( ℤ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑛 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )
3 2 fvmptndm ( ¬ 𝑁 ∈ ℕ → ( FPPr ‘ 𝑁 ) = ∅ )
4 eleq2 ( ( FPPr ‘ 𝑁 ) = ∅ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ 𝑋 ∈ ∅ ) )
5 noel ¬ 𝑋 ∈ ∅
6 5 pm2.21i ( 𝑋 ∈ ∅ → 𝑁 ∈ ℕ )
7 4 6 syl6bi ( ( FPPr ‘ 𝑁 ) = ∅ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ ) )
8 3 7 syl ( ¬ 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ ) )
9 1 8 pm2.61i ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ )