Theorem fpprmod

Description: The set of Fermat pseudoprimes to the base N , expressed by a modulo operation instead of the divisibility relation. (Contributed by AV, 30-May-2023)

	Ref	Expression
Assertion	fpprmod	⊢ ( 𝑁 ∈ ℕ → ( FPPr ‘ 𝑁 ) = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) } )

Proof

Step	Hyp	Ref	Expression
1		fppr	⊢ ( 𝑁 ∈ ℕ → ( FPPr ‘ 𝑁 ) = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } )
2		uzuzle24	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 4 ) → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
3		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
4		eluz4nn	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 4 ) → 𝑥 ∈ ℕ )
5		nnm1nn0	⊢ ( 𝑥 ∈ ℕ → ( 𝑥 − 1 ) ∈ ℕ0 )
6	4 5	syl	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑥 − 1 ) ∈ ℕ0 )
7		zexpcl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑥 − 1 ) ∈ ℕ0 ) → ( 𝑁 ↑ ( 𝑥 − 1 ) ) ∈ ℤ )
8	3 6 7	syl2an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑁 ↑ ( 𝑥 − 1 ) ) ∈ ℤ )
9		modm1div	⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ↑ ( 𝑥 − 1 ) ) ∈ ℤ ) → ( ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ↔ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) )
10	2 8 9	syl2an2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ↔ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) )
11	10	bicomd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ↔ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) )
12	11	anbi2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) ↔ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) ) )
13	12	rabbidva	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ 𝑥 ∥ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) − 1 ) ) } = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) } )
14	1 13	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( FPPr ‘ 𝑁 ) = { 𝑥 ∈ ( ℤ≥ ‘ 4 ) ∣ ( 𝑥 ∉ ℙ ∧ ( ( 𝑁 ↑ ( 𝑥 − 1 ) ) mod 𝑥 ) = 1 ) } )