Metamath Proof Explorer

Theorem fpprel

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

Ref Expression
Assertion fpprel ⊢N∈ℕ→X∈FPPr⁡N↔X∈ℤ≥4∧X∉ℙ∧NX−1modX=1

Proof

Step Hyp Ref Expression
1 fpprmod ⊢N∈ℕ→FPPr⁡N=x∈ℤ≥4|x∉ℙ∧Nx−1modx=1
2 1 eleq2d ⊢N∈ℕ→X∈FPPr⁡N↔X∈x∈ℤ≥4|x∉ℙ∧Nx−1modx=1
3 neleq1 ⊢x=X→x∉ℙ↔X∉ℙ
4 oveq1 ⊢x=X→x−1=X−1
5 4 oveq2d ⊢x=X→Nx−1=NX−1
6 id ⊢x=X→x=X
7 5 6 oveq12d ⊢x=X→Nx−1modx=NX−1modX
8 7 eqeq1d ⊢x=X→Nx−1modx=1↔NX−1modX=1
9 3 8 anbi12d ⊢x=X→x∉ℙ∧Nx−1modx=1↔X∉ℙ∧NX−1modX=1
10 9 elrab ⊢X∈x∈ℤ≥4|x∉ℙ∧Nx−1modx=1↔X∈ℤ≥4∧X∉ℙ∧NX−1modX=1
11 2 10 bitrdi ⊢N∈ℕ→X∈FPPr⁡N↔X∈ℤ≥4∧X∉ℙ∧NX−1modX=1
12 3anass ⊢X∈ℤ≥4∧X∉ℙ∧NX−1modX=1↔X∈ℤ≥4∧X∉ℙ∧NX−1modX=1
13 11 12 bitr4di ⊢N∈ℕ→X∈FPPr⁡N↔X∈ℤ≥4∧X∉ℙ∧NX−1modX=1