Theorem nfermltl2rev

Description: Fermat's little theorem with base 2 reversed is not generally true: There is an integer p (for example 341, see 341fppr2 ) so that " p is prime" does not follow from 2 ^ p == 2 (mod p ). (Contributed by AV, 3-Jun-2023)

	Ref	Expression
Assertion	nfermltl2rev	$$⊢\exists p\in {\mathbb{Z}}_{\ge 3}\neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)$$

Proof

Step	Hyp	Ref	Expression
1		decex	$$⊢341\in \mathrm{V}$$
2		eleq1	$$⊢p=341\to \left(p\in {\mathbb{Z}}_{\ge 3}\leftrightarrow 341\in {\mathbb{Z}}_{\ge 3}\right)$$
3		oveq2	$$⊢p=341\to 2^p=2^{341}$$
4		id	$$⊢p=341\to p=341$$
5	3 4	oveq12d	$$⊢p=341\to 2^p\mathrm{mod}p=2^{341}\mathrm{mod}341$$
6		oveq2	$$⊢p=341\to 2\mathrm{mod}p=2\mathrm{mod}341$$
7	5 6	eqeq12d	$$⊢p=341\to \left(2^p\mathrm{mod}p=2\mathrm{mod}p\leftrightarrow 2^{341}\mathrm{mod}341=2\mathrm{mod}341\right)$$
8		eleq1	$$⊢p=341\to \left(p\in \mathbb{P}\leftrightarrow 341\in \mathbb{P}\right)$$
9	7 8	imbi12d	$$⊢p=341\to \left(\left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)\leftrightarrow \left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\to 341\in \mathbb{P}\right)\right)$$
10	9	notbid	$$⊢p=341\to \left(\neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)\leftrightarrow \neg \left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\to 341\in \mathbb{P}\right)\right)$$
11	2 10	anbi12d	$$⊢p=341\to \left(\left(p\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)\right)\leftrightarrow \left(341\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\to 341\in \mathbb{P}\right)\right)\right)$$
12		3z	$$⊢3\in \mathbb{Z}$$
13		3nn0	$$⊢3\in {\mathbb{N}}_0$$
14		4nn0	$$⊢4\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢34\in {\mathbb{N}}_0$$
16		1nn0	$$⊢1\in {\mathbb{N}}_0$$
17	15 16	deccl	$$⊢341\in {\mathbb{N}}_0$$
18	17	nn0zi	$$⊢341\in \mathbb{Z}$$
19	13	dec0h	$$⊢3=03$$
20		0nn0	$$⊢0\in {\mathbb{N}}_0$$
21		3re	$$⊢3\in ℝ$$
22		9re	$$⊢9\in ℝ$$
23		3lt9	$$⊢3<9$$
24	21 22 23	ltleii	$$⊢3\le 9$$
25		3nn	$$⊢3\in \mathbb{N}$$
26		0re	$$⊢0\in ℝ$$
27		9pos	$$⊢0<9$$
28	26 22 27	ltleii	$$⊢0\le 9$$
29	25 14 20 28	decltdi	$$⊢0<34$$
30	20 15 13 16 24 29	decleh	$$⊢03\le 341$$
31	19 30	eqbrtri	$$⊢3\le 341$$
32		eluz2	$$⊢341\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(3\in \mathbb{Z}\wedge 341\in \mathbb{Z}\wedge 3\le 341\right)$$
33	12 18 31 32	mpbir3an	$$⊢341\in {\mathbb{Z}}_{\ge 3}$$
34		341fppr2	$$⊢341\in \mathrm{FPPr}\left(2\right)$$
35		fpprwppr	$$⊢341\in \mathrm{FPPr}\left(2\right)\to 2^{341}\mathrm{mod}341=2\mathrm{mod}341$$
36	34 35	ax-mp	$$⊢2^{341}\mathrm{mod}341=2\mathrm{mod}341$$
37		11t31e341	$$⊢11\cdot 31=341$$
38	37	eqcomi	$$⊢341=11\cdot 31$$
39		2z	$$⊢2\in \mathbb{Z}$$
40	16 16	deccl	$$⊢11\in {\mathbb{N}}_0$$
41	40	nn0zi	$$⊢11\in \mathbb{Z}$$
42		2nn0	$$⊢2\in {\mathbb{N}}_0$$
43	42	dec0h	$$⊢2=02$$
44		2re	$$⊢2\in ℝ$$
45		2lt9	$$⊢2<9$$
46	44 22 45	ltleii	$$⊢2\le 9$$
47		0lt1	$$⊢0<1$$
48	20 16 42 16 46 47	decleh	$$⊢02\le 11$$
49	43 48	eqbrtri	$$⊢2\le 11$$
50		eluz2	$$⊢11\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 11\in \mathbb{Z}\wedge 2\le 11\right)$$
51	39 41 49 50	mpbir3an	$$⊢11\in {\mathbb{Z}}_{\ge 2}$$
52	13 16	deccl	$$⊢31\in {\mathbb{N}}_0$$
53	52	nn0zi	$$⊢31\in \mathbb{Z}$$
54		3pos	$$⊢0<3$$
55	20 13 42 16 46 54	decleh	$$⊢02\le 31$$
56	43 55	eqbrtri	$$⊢2\le 31$$
57		eluz2	$$⊢31\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 31\in \mathbb{Z}\wedge 2\le 31\right)$$
58	39 53 56 57	mpbir3an	$$⊢31\in {\mathbb{Z}}_{\ge 2}$$
59		nprm	$$⊢\left(11\in {\mathbb{Z}}_{\ge 2}\wedge 31\in {\mathbb{Z}}_{\ge 2}\right)\to \neg 11\cdot 31\in \mathbb{P}$$
60	51 58 59	mp2an	$$⊢\neg 11\cdot 31\in \mathbb{P}$$
61	38 60	eqneltri	$$⊢\neg 341\in \mathbb{P}$$
62	36 61	pm3.2i	$$⊢\left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\wedge \neg 341\in \mathbb{P}\right)$$
63		annim	$$⊢\left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\wedge \neg 341\in \mathbb{P}\right)\leftrightarrow \neg \left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\to 341\in \mathbb{P}\right)$$
64	62 63	mpbi	$$⊢\neg \left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\to 341\in \mathbb{P}\right)$$
65	33 64	pm3.2i	$$⊢\left(341\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(2^{341}\mathrm{mod}341=2\mathrm{mod}341\to 341\in \mathbb{P}\right)\right)$$
66	1 11 65	ceqsexv2d	$$⊢\exists p\left(p\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)\right)$$
67		df-rex	$$⊢\exists p\in {\mathbb{Z}}_{\ge 3}\neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)\leftrightarrow \exists p\left(p\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)\right)$$
68	66 67	mpbir	$$⊢\exists p\in {\mathbb{Z}}_{\ge 3}\neg \left(2^p\mathrm{mod}p=2\mathrm{mod}p\to p\in \mathbb{P}\right)$$