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	biimtrdi	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑋 ∈ ℕ ) )
6	1 5	mpcom	⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑋 ∈ ℕ )