Theorem fpprel

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

	Ref	Expression
Assertion	fpprel	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fpprmod	⊢ ( 𝑁 ∈ ℕ → ( FPPr ‘ 𝑁 ) = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) } )
2	1	eleq2d	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ 𝑋 ∈ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) } ) )
3		neleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∉ ℙ ↔ 𝑋 ∉ ℙ ) )
4		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 1 ) = ( 𝑋 − 1 ) )
5	4	oveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑁 ↑ ( 𝑥 − 1 ) ) = ( 𝑁 ↑ ( 𝑋 − 1 ) ) )
6		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7	5 6	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ↔ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) )
9	3 8	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) ↔ ( 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
10	9	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) } ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
11	2 10	bitrdi	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) ) )
12		3anass	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
13	11 12	bitr4di	⊢ ( 𝑁 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 𝑁 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )