Theorem 8exp8mod9

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

	Ref	Expression
Assertion	8exp8mod9	|- ( ( 8 ^ 8 ) mod 9 ) = 1

Proof

Step	Hyp	Ref	Expression
1		9nn	|- 9 e. NN
2		8nn	|- 8 e. NN
3		4nn0	|- 4 e. NN0
4		0z	|- 0 e. ZZ
5		1nn0	|- 1 e. NN0
6		2nn0	|- 2 e. NN0
7		7nn	|- 7 e. NN
8	7	nnzi	|- 7 e. ZZ
9		8nn0	|- 8 e. NN0
10		8cn	|- 8 e. CC
11		exp1	|- ( 8 e. CC -> ( 8 ^ 1 ) = 8 )
12	10 11	ax-mp	|- ( 8 ^ 1 ) = 8
13	12	oveq1i	|- ( ( 8 ^ 1 ) mod 9 ) = ( 8 mod 9 )
14		2t1e2	|- ( 2 x. 1 ) = 2
15		6nn0	|- 6 e. NN0
16		3nn0	|- 3 e. NN0
17		3p1e4	|- ( 3 + 1 ) = 4
18		eqid	|- ; 6 3 = ; 6 3
19	15 16 17 18	decsuc	|- ( ; 6 3 + 1 ) = ; 6 4
20		9cn	|- 9 e. CC
21		7cn	|- 7 e. CC
22		9t7e63	|- ( 9 x. 7 ) = ; 6 3
23	20 21 22	mulcomli	|- ( 7 x. 9 ) = ; 6 3
24	23	oveq1i	|- ( ( 7 x. 9 ) + 1 ) = ( ; 6 3 + 1 )
25		8t8e64	|- ( 8 x. 8 ) = ; 6 4
26	19 24 25	3eqtr4i	|- ( ( 7 x. 9 ) + 1 ) = ( 8 x. 8 )
27	1 2 5 8 9 5 13 14 26	mod2xi	|- ( ( 8 ^ 2 ) mod 9 ) = ( 1 mod 9 )
28		2t2e4	|- ( 2 x. 2 ) = 4
29		0p1e1	|- ( 0 + 1 ) = 1
30	20	mul02i	|- ( 0 x. 9 ) = 0
31	30	oveq1i	|- ( ( 0 x. 9 ) + 1 ) = ( 0 + 1 )
32		1t1e1	|- ( 1 x. 1 ) = 1
33	29 31 32	3eqtr4i	|- ( ( 0 x. 9 ) + 1 ) = ( 1 x. 1 )
34	1 2 6 4 5 5 27 28 33	mod2xi	|- ( ( 8 ^ 4 ) mod 9 ) = ( 1 mod 9 )
35		4cn	|- 4 e. CC
36		2cn	|- 2 e. CC
37		4t2e8	|- ( 4 x. 2 ) = 8
38	35 36 37	mulcomli	|- ( 2 x. 4 ) = 8
39	1 2 3 4 5 5 34 38 33	mod2xi	|- ( ( 8 ^ 8 ) mod 9 ) = ( 1 mod 9 )
40		1re	|- 1 e. RR
41		nnrp	|- ( 9 e. NN -> 9 e. RR+ )
42	1 41	ax-mp	|- 9 e. RR+
43		0le1	|- 0 <_ 1
44		1lt9	|- 1 < 9
45		modid	|- ( ( ( 1 e. RR /\ 9 e. RR+ ) /\ ( 0 <_ 1 /\ 1 < 9 ) ) -> ( 1 mod 9 ) = 1 )
46	40 42 43 44 45	mp4an	|- ( 1 mod 9 ) = 1
47	39 46	eqtri	|- ( ( 8 ^ 8 ) mod 9 ) = 1