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 ∉ ℙ ∧ N x − 1 mod x = 1

Proof

Step Hyp Ref Expression
1 fppr ⊢ N ∈ ℕ → FPPr ⁡ N = x ∈ ℤ ≥ 4 | x ∉ ℙ ∧ x ∥ N x − 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 → N x − 1 ∈ ℤ
8 3 6 7 syl2an ⊢ N ∈ ℕ ∧ x ∈ ℤ ≥ 4 → N x − 1 ∈ ℤ
9 modm1div ⊢ x ∈ ℤ ≥ 2 ∧ N x − 1 ∈ ℤ → N x − 1 mod x = 1 ↔ x ∥ N x − 1 − 1
10 2 8 9 syl2an2 ⊢ N ∈ ℕ ∧ x ∈ ℤ ≥ 4 → N x − 1 mod x = 1 ↔ x ∥ N x − 1 − 1
11 10 bicomd ⊢ N ∈ ℕ ∧ x ∈ ℤ ≥ 4 → x ∥ N x − 1 − 1 ↔ N x − 1 mod x = 1
12 11 anbi2d ⊢ N ∈ ℕ ∧ x ∈ ℤ ≥ 4 → x ∉ ℙ ∧ x ∥ N x − 1 − 1 ↔ x ∉ ℙ ∧ N x − 1 mod x = 1
13 12 rabbidva ⊢ N ∈ ℕ → x ∈ ℤ ≥ 4 | x ∉ ℙ ∧ x ∥ N x − 1 − 1 = x ∈ ℤ ≥ 4 | x ∉ ℙ ∧ N x − 1 mod x = 1
14 1 13 eqtrd ⊢ N ∈ ℕ → FPPr ⁡ N = x ∈ ℤ ≥ 4 | x ∉ ℙ ∧ N x − 1 mod x = 1