Metamath Proof Explorer

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 ⊢N∈ℕ→FPPr⁡N=x∈ℤ≥4|x∉ℙ∧Nx−1modx=1

Proof

Step Hyp Ref Expression
1 fppr ⊢N∈ℕ→FPPr⁡N=x∈ℤ≥4|x∉ℙ∧x∥Nx−1−1
2 eluz4eluz2 ⊢x∈ℤ≥4→x∈ℤ≥2
3 nnz ⊢N∈ℕ→N∈ℤ
4 eluz4nn ⊢x∈ℤ≥4→x∈ℕ
5 nnm1nn0 ⊢x∈ℕ→x−1∈ℕ0
6 4 5 syl ⊢x∈ℤ≥4→x−1∈ℕ0
7 zexpcl ⊢N∈ℤ∧x−1∈ℕ0→Nx−1∈ℤ
8 3 6 7 syl2an ⊢N∈ℕ∧x∈ℤ≥4→Nx−1∈ℤ
9 modm1div ⊢x∈ℤ≥2∧Nx−1∈ℤ→Nx−1modx=1↔x∥Nx−1−1
10 2 8 9 syl2an2 ⊢N∈ℕ∧x∈ℤ≥4→Nx−1modx=1↔x∥Nx−1−1
11 10 bicomd ⊢N∈ℕ∧x∈ℤ≥4→x∥Nx−1−1↔Nx−1modx=1
12 11 anbi2d ⊢N∈ℕ∧x∈ℤ≥4→x∉ℙ∧x∥Nx−1−1↔x∉ℙ∧Nx−1modx=1
13 12 rabbidva ⊢N∈ℕ→x∈ℤ≥4|x∉ℙ∧x∥Nx−1−1=x∈ℤ≥4|x∉ℙ∧Nx−1modx=1
14 1 13 eqtrd ⊢N∈ℕ→FPPr⁡N=x∈ℤ≥4|x∉ℙ∧Nx−1modx=1