Theorem 8exp8mod9

Description: Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023)

	Ref	Expression
Assertion	8exp8mod9	$$⊢8^8\mathrm{mod}9=1$$

Proof

Step	Hyp	Ref	Expression
1		9nn	$$⊢9\in \mathbb{N}$$
2		8nn	$$⊢8\in \mathbb{N}$$
3		4nn0	$$⊢4\in {\mathbb{N}}_0$$
4		0z	$$⊢0\in \mathbb{Z}$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		7nn	$$⊢7\in \mathbb{N}$$
8	7	nnzi	$$⊢7\in \mathbb{Z}$$
9		8nn0	$$⊢8\in {\mathbb{N}}_0$$
10		8cn	$$⊢8\in ℂ$$
11		exp1	$$⊢8\in ℂ\to 8^1=8$$
12	10 11	ax-mp	$$⊢8^1=8$$
13	12	oveq1i	$$⊢8^1\mathrm{mod}9=8\mathrm{mod}9$$
14		2t1e2	$$⊢2\cdot 1=2$$
15		6nn0	$$⊢6\in {\mathbb{N}}_0$$
16		3nn0	$$⊢3\in {\mathbb{N}}_0$$
17		3p1e4	$$⊢3+1=4$$
18		eqid	$$⊢63=63$$
19	15 16 17 18	decsuc	$$⊢63+1=64$$
20		9cn	$$⊢9\in ℂ$$
21		7cn	$$⊢7\in ℂ$$
22		9t7e63	$$⊢9\cdot 7=63$$
23	20 21 22	mulcomli	$$⊢7\cdot 9=63$$
24	23	oveq1i	$$⊢7\cdot 9+1=63+1$$
25		8t8e64	$$⊢8\cdot 8=64$$
26	19 24 25	3eqtr4i	$$⊢7\cdot 9+1=8\cdot 8$$
27	1 2 5 8 9 5 13 14 26	mod2xi	$$⊢8^2\mathrm{mod}9=1\mathrm{mod}9$$
28		2t2e4	$$⊢2\cdot 2=4$$
29		0p1e1	$$⊢0+1=1$$
30	20	mul02i	$$⊢0\cdot 9=0$$
31	30	oveq1i	$$⊢0\cdot 9+1=0+1$$
32		1t1e1	$$⊢1\cdot 1=1$$
33	29 31 32	3eqtr4i	$$⊢0\cdot 9+1=1\cdot 1$$
34	1 2 6 4 5 5 27 28 33	mod2xi	$$⊢8^4\mathrm{mod}9=1\mathrm{mod}9$$
35		4cn	$$⊢4\in ℂ$$
36		2cn	$$⊢2\in ℂ$$
37		4t2e8	$$⊢4\cdot 2=8$$
38	35 36 37	mulcomli	$$⊢2\cdot 4=8$$
39	1 2 3 4 5 5 34 38 33	mod2xi	$$⊢8^8\mathrm{mod}9=1\mathrm{mod}9$$
40		1re	$$⊢1\in ℝ$$
41		nnrp	$$⊢9\in \mathbb{N}\to 9\in {ℝ}^{+}$$
42	1 41	ax-mp	$$⊢9\in {ℝ}^{+}$$
43		0le1	$$⊢0\le 1$$
44		1lt9	$$⊢1<9$$
45		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$$
46	40 42 43 44 45	mp4an	$$⊢1\mathrm{mod}9=1$$
47	39 46	eqtri	$$⊢8^8\mathrm{mod}9=1$$