fpprel

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

		Ref	Expression
	Assertion	fpprel	$⊢ N \in ℕ \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$

Step	Hyp	Ref	Expression
1		fpprmod	$⊢ N \in ℕ \to FPPr (N) = \{x \in ℤ_{\geq 4} \| (x \notin ℙ \land N^{x - 1} \mod x = 1)\}$
2	1	eleq2d	$⊢ N \in ℕ \to (X \in FPPr (N) \leftrightarrow X \in \{x \in ℤ_{\geq 4} \| (x \notin ℙ \land N^{x - 1} \mod x = 1)\})$
3		neleq1	$⊢ x = X \to (x \notin ℙ \leftrightarrow X \notin ℙ)$
4		oveq1	$⊢ x = X \to x - 1 = X - 1$
5	4	oveq2d	$⊢ x = X \to N^{x - 1} = N^{X - 1}$
6		id	$⊢ x = X \to x = X$
7	5 6	oveq12d	$⊢ x = X \to N^{x - 1} \mod x = N^{X - 1} \mod X$
8	7	eqeq1d	$⊢ x = X \to (N^{x - 1} \mod x = 1 \leftrightarrow N^{X - 1} \mod X = 1)$
9	3 8	anbi12d	$⊢ x = X \to ((x \notin ℙ \land N^{x - 1} \mod x = 1) \leftrightarrow (X \notin ℙ \land N^{X - 1} \mod X = 1))$
10	9	elrab	$⊢ X \in \{x \in ℤ_{\geq 4} \| (x \notin ℙ \land N^{x - 1} \mod x = 1)\} \leftrightarrow (X \in ℤ_{\geq 4} \land (X \notin ℙ \land N^{X - 1} \mod X = 1))$
11	2 10	bitrdi	$⊢ N \in ℕ \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land (X \notin ℙ \land N^{X - 1} \mod X = 1)))$
12		3anass	$⊢ (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1) \leftrightarrow (X \in ℤ_{\geq 4} \land (X \notin ℙ \land N^{X - 1} \mod X = 1))$
13	11 12	bitr4di	$⊢ N \in ℕ \to (X \in FPPr (N) \leftrightarrow (X \in ℤ_{\geq 4} \land X \notin ℙ \land N^{X - 1} \mod X = 1))$

Metamath Proof Explorer