fpprnn

Description: A Fermat pseudoprime to the base N is a positive integer. (Contributed by AV, 30-May-2023)

		Ref	Expression
	Assertion	fpprnn	$⊢ X \in FPPr (N) \to X \in ℕ$

Step	Hyp	Ref	Expression
1		fpprbasnn	$⊢ X \in FPPr (N) \to N \in ℕ$
2		fpprel	$⊢ N \in ℕ \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$
3		eluz4nn	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$
4	3	3ad2ant1	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1) \to X \in ℕ$
5	2 4	syl6bi	$⊢ N \in ℕ \to (X \in FPPr (N) \to X \in ℕ)$
6	1 5	mpcom	$⊢ X \in FPPr (N) \to X \in ℕ$

Metamath Proof Explorer