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