Description: The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | fpprbasnn | ⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ ) |
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 ‘ 𝑁 ) → 𝑁 ∈ ℕ ) |