# 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\in \mathrm{FPPr}\left(2\right)$

### Proof

Step Hyp Ref Expression
1 4z ${⊢}4\in ℤ$
2 3nn0 ${⊢}3\in {ℕ}_{0}$
3 4nn0 ${⊢}4\in {ℕ}_{0}$
4 2 3 deccl ${⊢}34\in {ℕ}_{0}$
5 1nn ${⊢}1\in ℕ$
6 4 5 decnncl ${⊢}341\in ℕ$
7 6 nnzi ${⊢}341\in ℤ$
8 4nn ${⊢}4\in ℕ$
9 2 8 decnncl ${⊢}34\in ℕ$
10 1nn0 ${⊢}1\in {ℕ}_{0}$
11 4re ${⊢}4\in ℝ$
12 9re ${⊢}9\in ℝ$
13 4lt9 ${⊢}4<9$
14 11 12 13 ltleii ${⊢}4\le 9$
15 9 10 3 14 declei ${⊢}4\le 341$
16 eluz2 ${⊢}341\in {ℤ}_{\ge 4}↔\left(4\in ℤ\wedge 341\in ℤ\wedge 4\le 341\right)$
17 1 7 15 16 mpbir3an ${⊢}341\in {ℤ}_{\ge 4}$
18 2z ${⊢}2\in ℤ$
19 10 5 decnncl ${⊢}11\in ℕ$
20 19 nnzi ${⊢}11\in ℤ$
21 2nn0 ${⊢}2\in {ℕ}_{0}$
22 2re ${⊢}2\in ℝ$
23 2lt9 ${⊢}2<9$
24 22 12 23 ltleii ${⊢}2\le 9$
25 5 10 21 24 declei ${⊢}2\le 11$
26 eluz2 ${⊢}11\in {ℤ}_{\ge 2}↔\left(2\in ℤ\wedge 11\in ℤ\wedge 2\le 11\right)$
27 18 20 25 26 mpbir3an ${⊢}11\in {ℤ}_{\ge 2}$
28 2 5 decnncl ${⊢}31\in ℕ$
29 28 nnzi ${⊢}31\in ℤ$
30 3nn ${⊢}3\in ℕ$
31 30 10 21 24 declei ${⊢}2\le 31$
32 eluz2 ${⊢}31\in {ℤ}_{\ge 2}↔\left(2\in ℤ\wedge 31\in ℤ\wedge 2\le 31\right)$
33 18 29 31 32 mpbir3an ${⊢}31\in {ℤ}_{\ge 2}$
34 nprm ${⊢}\left(11\in {ℤ}_{\ge 2}\wedge 31\in {ℤ}_{\ge 2}\right)\to ¬11\cdot 31\in ℙ$
35 27 33 34 mp2an ${⊢}¬11\cdot 31\in ℙ$
36 df-nel ${⊢}341\notin ℙ↔¬341\in ℙ$
37 11t31e341 ${⊢}11\cdot 31=341$
38 37 eqcomi ${⊢}341=11\cdot 31$
39 38 eleq1i ${⊢}341\in ℙ↔11\cdot 31\in ℙ$
40 36 39 xchbinx ${⊢}341\notin ℙ↔¬11\cdot 31\in ℙ$
41 35 40 mpbir ${⊢}341\notin ℙ$
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}\mathrm{mod}341={2}^{340}\mathrm{mod}341$
48 2exp340mod341 ${⊢}{2}^{340}\mathrm{mod}341=1$
49 47 48 eqtri ${⊢}{2}^{341-1}\mathrm{mod}341=1$
50 2nn ${⊢}2\in ℕ$
51 fpprel ${⊢}2\in ℕ\to \left(341\in \mathrm{FPPr}\left(2\right)↔\left(341\in {ℤ}_{\ge 4}\wedge 341\notin ℙ\wedge {2}^{341-1}\mathrm{mod}341=1\right)\right)$
52 50 51 ax-mp ${⊢}341\in \mathrm{FPPr}\left(2\right)↔\left(341\in {ℤ}_{\ge 4}\wedge 341\notin ℙ\wedge {2}^{341-1}\mathrm{mod}341=1\right)$
53 17 41 49 52 mpbir3an ${⊢}341\in \mathrm{FPPr}\left(2\right)$