Theorem nfermltl8rev

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

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

Proof

Step	Hyp	Ref	Expression
1		9nn	$$⊢9\in \mathbb{N}$$
2	1	elexi	$$⊢9\in \mathrm{V}$$
3		eleq1	$$⊢p=9\to \left(p\in {\mathbb{Z}}_{\ge 3}\leftrightarrow 9\in {\mathbb{Z}}_{\ge 3}\right)$$
4		oveq2	$$⊢p=9\to 8^p=8^9$$
5		id	$$⊢p=9\to p=9$$
6	4 5	oveq12d	$$⊢p=9\to 8^p\mathrm{mod}p=8^9\mathrm{mod}9$$
7		oveq2	$$⊢p=9\to 8\mathrm{mod}p=8\mathrm{mod}9$$
8	6 7	eqeq12d	$$⊢p=9\to \left(8^p\mathrm{mod}p=8\mathrm{mod}p\leftrightarrow 8^9\mathrm{mod}9=8\mathrm{mod}9\right)$$
9		eleq1	$$⊢p=9\to \left(p\in \mathbb{P}\leftrightarrow 9\in \mathbb{P}\right)$$
10	8 9	imbi12d	$$⊢p=9\to \left(\left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)\leftrightarrow \left(8^9\mathrm{mod}9=8\mathrm{mod}9\to 9\in \mathbb{P}\right)\right)$$
11	10	notbid	$$⊢p=9\to \left(\neg \left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)\leftrightarrow \neg \left(8^9\mathrm{mod}9=8\mathrm{mod}9\to 9\in \mathbb{P}\right)\right)$$
12	3 11	anbi12d	$$⊢p=9\to \left(\left(p\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)\right)\leftrightarrow \left(9\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(8^9\mathrm{mod}9=8\mathrm{mod}9\to 9\in \mathbb{P}\right)\right)\right)$$
13		3z	$$⊢3\in \mathbb{Z}$$
14	1	nnzi	$$⊢9\in \mathbb{Z}$$
15		3re	$$⊢3\in ℝ$$
16		9re	$$⊢9\in ℝ$$
17		3lt9	$$⊢3<9$$
18	15 16 17	ltleii	$$⊢3\le 9$$
19		eluz2	$$⊢9\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(3\in \mathbb{Z}\wedge 9\in \mathbb{Z}\wedge 3\le 9\right)$$
20	13 14 18 19	mpbir3an	$$⊢9\in {\mathbb{Z}}_{\ge 3}$$
21		8nn	$$⊢8\in \mathbb{N}$$
22		8nn0	$$⊢8\in {\mathbb{N}}_0$$
23		0z	$$⊢0\in \mathbb{Z}$$
24		1nn0	$$⊢1\in {\mathbb{N}}_0$$
25		8exp8mod9	$$⊢8^8\mathrm{mod}9=1$$
26		1re	$$⊢1\in ℝ$$
27		nnrp	$$⊢9\in \mathbb{N}\to 9\in {ℝ}^{+}$$
28	1 27	ax-mp	$$⊢9\in {ℝ}^{+}$$
29		0le1	$$⊢0\le 1$$
30		1lt9	$$⊢1<9$$
31		modid	$$⊢\left(\left(1\in ℝ\wedge 9\in {ℝ}^{+}\right)\wedge \left(0\le 1\wedge 1<9\right)\right)\to 1\mathrm{mod}9=1$$
32	26 28 29 30 31	mp4an	$$⊢1\mathrm{mod}9=1$$
33	25 32	eqtr4i	$$⊢8^8\mathrm{mod}9=1\mathrm{mod}9$$
34		8p1e9	$$⊢8+1=9$$
35		8cn	$$⊢8\in ℂ$$
36	35	addlidi	$$⊢0+8=8$$
37		9cn	$$⊢9\in ℂ$$
38	37	mul02i	$$⊢0\cdot 9=0$$
39	38	oveq1i	$$⊢0\cdot 9+8=0+8$$
40	35	mullidi	$$⊢1\cdot 8=8$$
41	36 39 40	3eqtr4i	$$⊢0\cdot 9+8=1\cdot 8$$
42	1 21 22 23 24 22 33 34 41	modxp1i	$$⊢8^9\mathrm{mod}9=8\mathrm{mod}9$$
43		9nprm	$$⊢\neg 9\in \mathbb{P}$$
44	42 43	pm3.2i	$$⊢\left(8^9\mathrm{mod}9=8\mathrm{mod}9\wedge \neg 9\in \mathbb{P}\right)$$
45		annim	$$⊢\left(8^9\mathrm{mod}9=8\mathrm{mod}9\wedge \neg 9\in \mathbb{P}\right)\leftrightarrow \neg \left(8^9\mathrm{mod}9=8\mathrm{mod}9\to 9\in \mathbb{P}\right)$$
46	44 45	mpbi	$$⊢\neg \left(8^9\mathrm{mod}9=8\mathrm{mod}9\to 9\in \mathbb{P}\right)$$
47	20 46	pm3.2i	$$⊢\left(9\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(8^9\mathrm{mod}9=8\mathrm{mod}9\to 9\in \mathbb{P}\right)\right)$$
48	2 12 47	ceqsexv2d	$$⊢\exists p\left(p\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)\right)$$
49		df-rex	$$⊢\exists p\in {\mathbb{Z}}_{\ge 3}\neg \left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)\leftrightarrow \exists p\left(p\in {\mathbb{Z}}_{\ge 3}\wedge \neg \left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)\right)$$
50	48 49	mpbir	$$⊢\exists p\in {\mathbb{Z}}_{\ge 3}\neg \left(8^p\mathrm{mod}p=8\mathrm{mod}p\to p\in \mathbb{P}\right)$$