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	biimtrdi	⊢ ( ( FPPr ‘ 𝑁 ) = ∅ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ ) )
8	3 7	syl	⊢ ( ¬ 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ ) )
9	1 8	pm2.61i	⊢ ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) → 𝑁 ∈ ℕ )