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 \mathbb{Z}$$
2		3nn0	$$⊢3\in {\mathbb{N}}_0$$
3		4nn0	$$⊢4\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢34\in {\mathbb{N}}_0$$
5		1nn	$$⊢1\in \mathbb{N}$$
6	4 5	decnncl	$$⊢341\in \mathbb{N}$$
7	6	nnzi	$$⊢341\in \mathbb{Z}$$
8		4nn	$$⊢4\in \mathbb{N}$$
9	2 8	decnncl	$$⊢34\in \mathbb{N}$$
10		1nn0	$$⊢1\in {\mathbb{N}}_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 {\mathbb{Z}}_{\ge 4}\leftrightarrow \left(4\in \mathbb{Z}\wedge 341\in \mathbb{Z}\wedge 4\le 341\right)$$
17	1 7 15 16	mpbir3an	$$⊢341\in {\mathbb{Z}}_{\ge 4}$$
18		2z	$$⊢2\in \mathbb{Z}$$
19	10 5	decnncl	$$⊢11\in \mathbb{N}$$
20	19	nnzi	$$⊢11\in \mathbb{Z}$$
21		2nn0	$$⊢2\in {\mathbb{N}}_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 {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 11\in \mathbb{Z}\wedge 2\le 11\right)$$
27	18 20 25 26	mpbir3an	$$⊢11\in {\mathbb{Z}}_{\ge 2}$$
28	2 5	decnncl	$$⊢31\in \mathbb{N}$$
29	28	nnzi	$$⊢31\in \mathbb{Z}$$
30		3nn	$$⊢3\in \mathbb{N}$$
31	30 10 21 24	declei	$$⊢2\le 31$$
32		eluz2	$$⊢31\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 31\in \mathbb{Z}\wedge 2\le 31\right)$$
33	18 29 31 32	mpbir3an	$$⊢31\in {\mathbb{Z}}_{\ge 2}$$
34		nprm	$$⊢\left(11\in {\mathbb{Z}}_{\ge 2}\wedge 31\in {\mathbb{Z}}_{\ge 2}\right)\to \neg 11\cdot 31\in \mathbb{P}$$
35	27 33 34	mp2an	$$⊢\neg 11\cdot 31\in \mathbb{P}$$
36		df-nel	$$⊢341\notin \mathbb{P}\leftrightarrow \neg 341\in \mathbb{P}$$
37		11t31e341	$$⊢11\cdot 31=341$$
38	37	eqcomi	$$⊢341=11\cdot 31$$
39	38	eleq1i	$$⊢341\in \mathbb{P}\leftrightarrow 11\cdot 31\in \mathbb{P}$$
40	36 39	xchbinx	$$⊢341\notin \mathbb{P}\leftrightarrow \neg 11\cdot 31\in \mathbb{P}$$
41	35 40	mpbir	$$⊢341\notin \mathbb{P}$$
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 \mathbb{N}$$
51		fpprel	$$⊢2\in \mathbb{N}\to \left(341\in \mathrm{FPPr}\left(2\right)\leftrightarrow \left(341\in {\mathbb{Z}}_{\ge 4}\wedge 341\notin \mathbb{P}\wedge 2^{341-1}\mathrm{mod}341=1\right)\right)$$
52	50 51	ax-mp	$$⊢341\in \mathrm{FPPr}\left(2\right)\leftrightarrow \left(341\in {\mathbb{Z}}_{\ge 4}\wedge 341\notin \mathbb{P}\wedge 2^{341-1}\mathrm{mod}341=1\right)$$
53	17 41 49 52	mpbir3an	$$⊢341\in \mathrm{FPPr}\left(2\right)$$