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 ∈ ℕ
2		8nn	⊢ 8 ∈ ℕ
3		4nn0	⊢ 4 ∈ ℕ0
4		0z	⊢ 0 ∈ ℤ
5		1nn0	⊢ 1 ∈ ℕ0
6		2nn0	⊢ 2 ∈ ℕ0
7		7nn	⊢ 7 ∈ ℕ
8	7	nnzi	⊢ 7 ∈ ℤ
9		8nn0	⊢ 8 ∈ ℕ0
10		8cn	⊢ 8 ∈ ℂ
11		exp1	⊢ ( 8 ∈ ℂ → ( 8 ↑ 1 ) = 8 )
12	10 11	ax-mp	⊢ ( 8 ↑ 1 ) = 8
13	12	oveq1i	⊢ ( ( 8 ↑ 1 ) mod 9 ) = ( 8 mod 9 )
14		2t1e2	⊢ ( 2 · 1 ) = 2
15		6nn0	⊢ 6 ∈ ℕ0
16		3nn0	⊢ 3 ∈ ℕ0
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 ∈ ℂ
21		7cn	⊢ 7 ∈ ℂ
22		9t7e63	⊢ ( 9 · 7 ) = ; 6 3
23	20 21 22	mulcomli	⊢ ( 7 · 9 ) = ; 6 3
24	23	oveq1i	⊢ ( ( 7 · 9 ) + 1 ) = ( ; 6 3 + 1 )
25		8t8e64	⊢ ( 8 · 8 ) = ; 6 4
26	19 24 25	3eqtr4i	⊢ ( ( 7 · 9 ) + 1 ) = ( 8 · 8 )
27	1 2 5 8 9 5 13 14 26	mod2xi	⊢ ( ( 8 ↑ 2 ) mod 9 ) = ( 1 mod 9 )
28		2t2e4	⊢ ( 2 · 2 ) = 4
29		0p1e1	⊢ ( 0 + 1 ) = 1
30	20	mul02i	⊢ ( 0 · 9 ) = 0
31	30	oveq1i	⊢ ( ( 0 · 9 ) + 1 ) = ( 0 + 1 )
32		1t1e1	⊢ ( 1 · 1 ) = 1
33	29 31 32	3eqtr4i	⊢ ( ( 0 · 9 ) + 1 ) = ( 1 · 1 )
34	1 2 6 4 5 5 27 28 33	mod2xi	⊢ ( ( 8 ↑ 4 ) mod 9 ) = ( 1 mod 9 )
35		4cn	⊢ 4 ∈ ℂ
36		2cn	⊢ 2 ∈ ℂ
37		4t2e8	⊢ ( 4 · 2 ) = 8
38	35 36 37	mulcomli	⊢ ( 2 · 4 ) = 8
39	1 2 3 4 5 5 34 38 33	mod2xi	⊢ ( ( 8 ↑ 8 ) mod 9 ) = ( 1 mod 9 )
40		1re	⊢ 1 ∈ ℝ
41		nnrp	⊢ ( 9 ∈ ℕ → 9 ∈ ℝ+ )
42	1 41	ax-mp	⊢ 9 ∈ ℝ+
43		0le1	⊢ 0 ≤ 1
44		1lt9	⊢ 1 < 9
45		modid	⊢ ( ( ( 1 ∈ ℝ ∧ 9 ∈ ℝ+ ) ∧ ( 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