Metamath Proof Explorer

Theorem 341fppr2

Description: 341 is the (smallest)Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023)

Ref Expression
Assertion 341fppr2 ⊢ 341 ∈ FPPr ⁡ 2

Proof

Step Hyp Ref Expression
1 4z ⊢ 4 ∈ ℤ
2 3nn0 ⊢ 3 ∈ ℕ 0
3 4nn0 ⊢ 4 ∈ ℕ 0
4 2 3 deccl ⊢ 34 ∈ ℕ 0
5 1nn ⊢ 1 ∈ ℕ
6 4 5 decnncl ⊢ 341 ∈ ℕ
7 6 nnzi ⊢ 341 ∈ ℤ
8 4nn ⊢ 4 ∈ ℕ
9 2 8 decnncl ⊢ 34 ∈ ℕ
10 1nn0 ⊢ 1 ∈ ℕ 0
11 4re ⊢ 4 ∈ ℝ
12 9re ⊢ 9 ∈ ℝ
13 4lt9 ⊢ 4 < 9
14 11 12 13 ltleii ⊢ 4 ≤ 9
15 9 10 3 14 declei ⊢ 4 ≤ 341
16 eluz2 ⊢ 341 ∈ ℤ ≥ 4 ↔ 4 ∈ ℤ ∧ 341 ∈ ℤ ∧ 4 ≤ 341
17 1 7 15 16 mpbir3an ⊢ 341 ∈ ℤ ≥ 4
18 2z ⊢ 2 ∈ ℤ
19 10 5 decnncl ⊢ 11 ∈ ℕ
20 19 nnzi ⊢ 11 ∈ ℤ
21 2nn0 ⊢ 2 ∈ ℕ 0
22 2re ⊢ 2 ∈ ℝ
23 2lt9 ⊢ 2 < 9
24 22 12 23 ltleii ⊢ 2 ≤ 9
25 5 10 21 24 declei ⊢ 2 ≤ 11
26 eluz2 ⊢ 11 ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ 11 ∈ ℤ ∧ 2 ≤ 11
27 18 20 25 26 mpbir3an ⊢ 11 ∈ ℤ ≥ 2
28 2 5 decnncl ⊢ 31 ∈ ℕ
29 28 nnzi ⊢ 31 ∈ ℤ
30 3nn ⊢ 3 ∈ ℕ
31 30 10 21 24 declei ⊢ 2 ≤ 31
32 eluz2 ⊢ 31 ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ 31 ∈ ℤ ∧ 2 ≤ 31
33 18 29 31 32 mpbir3an ⊢ 31 ∈ ℤ ≥ 2
34 nprm ⊢ 11 ∈ ℤ ≥ 2 ∧ 31 ∈ ℤ ≥ 2 → ¬ 11 ⋅ 31 ∈ ℙ
35 27 33 34 mp2an ⊢ ¬ 11 ⋅ 31 ∈ ℙ
36 df-nel ⊢ 341 ∉ ℙ ↔ ¬ 341 ∈ ℙ
37 11t31e341 ⊢ 11 ⋅ 31 = 341
38 37 eqcomi ⊢ 341 = 11 ⋅ 31
39 38 eleq1i ⊢ 341 ∈ ℙ ↔ 11 ⋅ 31 ∈ ℙ
40 36 39 xchbinx ⊢ 341 ∉ ℙ ↔ ¬ 11 ⋅ 31 ∈ ℙ
41 35 40 mpbir ⊢ 341 ∉ ℙ
42 eqid ⊢ 341 = 341
43 eqid ⊢ 34 + 1 = 34 + 1
44 1m1e0 ⊢ 1 − 1 = 0
45 4 10 10 42 43 44 decsubi ⊢ 341 − 1 = 340
46 45 oveq2i ⊢ 2 341 − 1 = 2 340
47 46 oveq1i ⊢ 2 341 − 1 mod 341 = 2 340 mod 341
48 2exp340mod341 ⊢ 2 340 mod 341 = 1
49 47 48 eqtri ⊢ 2 341 − 1 mod 341 = 1
50 2nn ⊢ 2 ∈ ℕ
51 fpprel ⊢ 2 ∈ ℕ → 341 ∈ FPPr ⁡ 2 ↔ 341 ∈ ℤ ≥ 4 ∧ 341 ∉ ℙ ∧ 2 341 − 1 mod 341 = 1
52 50 51 ax-mp ⊢ 341 ∈ FPPr ⁡ 2 ↔ 341 ∈ ℤ ≥ 4 ∧ 341 ∉ ℙ ∧ 2 341 − 1 mod 341 = 1
53 17 41 49 52 mpbir3an ⊢ 341 ∈ FPPr ⁡ 2