Metamath Proof Explorer

Theorem 2exp340mod341

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

Ref Expression
Assertion 2exp340mod341 ( ( 2 ↑ 3 4 0 ) mod 3 4 1 ) = 1

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 4nn0 ⊢ 4 ∈ ℕ0
3 1 2 deccl ⊢ 3 4 ∈ ℕ0
4 1nn ⊢ 1 ∈ ℕ
5 3 4 decnncl ⊢ 3 4 1 ∈ ℕ
6 2nn ⊢ 2 ∈ ℕ
7 1nn0 ⊢ 1 ∈ ℕ0
8 7nn0 ⊢ 7 ∈ ℕ0
9 7 8 deccl ⊢ 1 7 ∈ ℕ0
10 0nn0 ⊢ 0 ∈ ℕ0
11 9 10 deccl ⊢ 1 7 0 ∈ ℕ0
12 0z ⊢ 0 ∈ ℤ
13 8nn0 ⊢ 8 ∈ ℕ0
14 5nn0 ⊢ 5 ∈ ℕ0
15 13 14 deccl ⊢ 8 5 ∈ ℕ0
16 3z ⊢ 3 ∈ ℤ
17 2nn0 ⊢ 2 ∈ ℕ0
18 1 17 deccl ⊢ 3 2 ∈ ℕ0
19 13 2 deccl ⊢ 8 4 ∈ ℕ0
20 6nn0 ⊢ 6 ∈ ℕ0
21 7 20 deccl ⊢ 1 6 ∈ ℕ0
22 2 17 deccl ⊢ 4 2 ∈ ℕ0
23 17 7 deccl ⊢ 2 1 ∈ ℕ0
24 17 10 deccl ⊢ 2 0 ∈ ℕ0
25 7 10 deccl ⊢ 1 0 ∈ ℕ0
26 2exp5 ⊢ ( 2 ↑ 5 ) = 3 2
27 26 oveq1i ⊢ ( ( 2 ↑ 5 ) mod 3 4 1 ) = ( 3 2 mod 3 4 1 )
28 5cn ⊢ 5 ∈ ℂ
29 2cn ⊢ 2 ∈ ℂ
30 5t2e10 ⊢ ( 5 · 2 ) = 1 0
31 28 29 30 mulcomli ⊢ ( 2 · 5 ) = 1 0
32 25 17 deccl ⊢ 1 0 2 ∈ ℕ0
33 3p1e4 ⊢ ( 3 + 1 ) = 4
34 eqid ⊢ 1 0 2 3 = 1 0 2 3
35 32 1 33 34 decsuc ⊢ ( 1 0 2 3 + 1 ) = 1 0 2 4
36 1 3 7 decmulnc ⊢ ( 3 · 3 4 1 ) = ( 3 · 3 4 ) ( 3 · 1 )
37 eqid ⊢ 3 4 = 3 4
38 3t3e9 ⊢ ( 3 · 3 ) = 9
39 38 oveq1i ⊢ ( ( 3 · 3 ) + 1 ) = ( 9 + 1 )
40 9p1e10 ⊢ ( 9 + 1 ) = 1 0
41 39 40 eqtri ⊢ ( ( 3 · 3 ) + 1 ) = 1 0
42 4cn ⊢ 4 ∈ ℂ
43 3cn ⊢ 3 ∈ ℂ
44 4t3e12 ⊢ ( 4 · 3 ) = 1 2
45 42 43 44 mulcomli ⊢ ( 3 · 4 ) = 1 2
46 1 1 2 37 17 7 41 45 decmul2c ⊢ ( 3 · 3 4 ) = 1 0 2
47 43 mulid1i ⊢ ( 3 · 1 ) = 3
48 46 47 deceq12i ⊢ ( 3 · 3 4 ) ( 3 · 1 ) = 1 0 2 3
49 36 48 eqtri ⊢ ( 3 · 3 4 1 ) = 1 0 2 3
50 49 oveq1i ⊢ ( ( 3 · 3 4 1 ) + 1 ) = ( 1 0 2 3 + 1 )
51 eqid ⊢ 3 2 = 3 2
52 1 1 17 decmulnc ⊢ ( 3 · 3 2 ) = ( 3 · 3 ) ( 3 · 2 )
53 52 oveq1i ⊢ ( ( 3 · 3 2 ) + 6 ) = ( ( 3 · 3 ) ( 3 · 2 ) + 6 )
54 9nn0 ⊢ 9 ∈ ℕ0
55 3t2e6 ⊢ ( 3 · 2 ) = 6
56 38 55 deceq12i ⊢ ( 3 · 3 ) ( 3 · 2 ) = 9 6
57 6p6e12 ⊢ ( 6 + 6 ) = 1 2
58 54 20 20 56 40 17 57 decaddci ⊢ ( ( 3 · 3 ) ( 3 · 2 ) + 6 ) = 1 0 2
59 53 58 eqtri ⊢ ( ( 3 · 3 2 ) + 6 ) = 1 0 2
60 17 1 17 decmulnc ⊢ ( 2 · 3 2 ) = ( 2 · 3 ) ( 2 · 2 )
61 43 29 55 mulcomli ⊢ ( 2 · 3 ) = 6
62 2t2e4 ⊢ ( 2 · 2 ) = 4
63 61 62 deceq12i ⊢ ( 2 · 3 ) ( 2 · 2 ) = 6 4
64 60 63 eqtri ⊢ ( 2 · 3 2 ) = 6 4
65 18 1 17 51 2 20 59 64 decmul1c ⊢ ( 3 2 · 3 2 ) = 1 0 2 4
66 35 50 65 3eqtr4i ⊢ ( ( 3 · 3 4 1 ) + 1 ) = ( 3 2 · 3 2 )
67 5 6 14 16 18 7 27 31 66 mod2xi ⊢ ( ( 2 ↑ 1 0 ) mod 3 4 1 ) = ( 1 mod 3 4 1 )
68 17 7 10 decmulnc ⊢ ( 2 · 1 0 ) = ( 2 · 1 ) ( 2 · 0 )
69 29 mulid1i ⊢ ( 2 · 1 ) = 2
70 2t0e0 ⊢ ( 2 · 0 ) = 0
71 69 70 deceq12i ⊢ ( 2 · 1 ) ( 2 · 0 ) = 2 0
72 68 71 eqtri ⊢ ( 2 · 1 0 ) = 2 0
73 0p1e1 ⊢ ( 0 + 1 ) = 1
74 5 nncni ⊢ 3 4 1 ∈ ℂ
75 74 mul02i ⊢ ( 0 · 3 4 1 ) = 0
76 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 1 ) = ( 0 + 1 )
77 1t1e1 ⊢ ( 1 · 1 ) = 1
78 73 76 77 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 1 ) = ( 1 · 1 )
79 5 6 25 12 7 7 67 72 78 mod2xi ⊢ ( ( 2 ↑ 2 0 ) mod 3 4 1 ) = ( 1 mod 3 4 1 )
80 eqid ⊢ 2 0 = 2 0
81 17 10 73 80 decsuc ⊢ ( 2 0 + 1 ) = 2 1
82 29 addid2i ⊢ ( 0 + 2 ) = 2
83 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 2 ) = ( 0 + 2 )
84 29 mulid2i ⊢ ( 1 · 2 ) = 2
85 82 83 84 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 2 ) = ( 1 · 2 )
86 5 6 24 12 7 17 79 81 85 modxp1i ⊢ ( ( 2 ↑ 2 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 )
87 17 17 7 decmulnc ⊢ ( 2 · 2 1 ) = ( 2 · 2 ) ( 2 · 1 )
88 62 69 deceq12i ⊢ ( 2 · 2 ) ( 2 · 1 ) = 4 2
89 87 88 eqtri ⊢ ( 2 · 2 1 ) = 4 2
90 42 addid2i ⊢ ( 0 + 4 ) = 4
91 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 4 ) = ( 0 + 4 )
92 90 91 62 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 4 ) = ( 2 · 2 )
93 5 6 23 12 17 2 86 89 92 mod2xi ⊢ ( ( 2 ↑ 4 2 ) mod 3 4 1 ) = ( 4 mod 3 4 1 )
94 17 2 17 decmulnc ⊢ ( 2 · 4 2 ) = ( 2 · 4 ) ( 2 · 2 )
95 4t2e8 ⊢ ( 4 · 2 ) = 8
96 42 29 95 mulcomli ⊢ ( 2 · 4 ) = 8
97 96 62 deceq12i ⊢ ( 2 · 4 ) ( 2 · 2 ) = 8 4
98 94 97 eqtri ⊢ ( 2 · 4 2 ) = 8 4
99 21 nn0cni ⊢ 1 6 ∈ ℂ
100 99 addid2i ⊢ ( 0 + 1 6 ) = 1 6
101 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 1 6 ) = ( 0 + 1 6 )
102 4t4e16 ⊢ ( 4 · 4 ) = 1 6
103 100 101 102 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 1 6 ) = ( 4 · 4 )
104 5 6 22 12 2 21 93 98 103 mod2xi ⊢ ( ( 2 ↑ 8 4 ) mod 3 4 1 ) = ( 1 6 mod 3 4 1 )
105 4p1e5 ⊢ ( 4 + 1 ) = 5
106 eqid ⊢ 8 4 = 8 4
107 13 2 105 106 decsuc ⊢ ( 8 4 + 1 ) = 8 5
108 18 nn0cni ⊢ 3 2 ∈ ℂ
109 108 addid2i ⊢ ( 0 + 3 2 ) = 3 2
110 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 3 2 ) = ( 0 + 3 2 )
111 eqid ⊢ 1 6 = 1 6
112 84 oveq1i ⊢ ( ( 1 · 2 ) + 1 ) = ( 2 + 1 )
113 2p1e3 ⊢ ( 2 + 1 ) = 3
114 112 113 eqtri ⊢ ( ( 1 · 2 ) + 1 ) = 3
115 6t2e12 ⊢ ( 6 · 2 ) = 1 2
116 17 7 20 111 17 7 114 115 decmul1c ⊢ ( 1 6 · 2 ) = 3 2
117 109 110 116 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 3 2 ) = ( 1 6 · 2 )
118 5 6 19 12 21 18 104 107 117 modxp1i ⊢ ( ( 2 ↑ 8 5 ) mod 3 4 1 ) = ( 3 2 mod 3 4 1 )
119 eqid ⊢ 8 5 = 8 5
120 6p1e7 ⊢ ( 6 + 1 ) = 7
121 8cn ⊢ 8 ∈ ℂ
122 8t2e16 ⊢ ( 8 · 2 ) = 1 6
123 121 29 122 mulcomli ⊢ ( 2 · 8 ) = 1 6
124 7 20 120 123 decsuc ⊢ ( ( 2 · 8 ) + 1 ) = 1 7
125 17 13 14 119 10 7 124 31 decmul2c ⊢ ( 2 · 8 5 ) = 1 7 0
126 5 6 15 16 18 7 118 125 66 mod2xi ⊢ ( ( 2 ↑ 1 7 0 ) mod 3 4 1 ) = ( 1 mod 3 4 1 )
127 17 9 10 decmulnc ⊢ ( 2 · 1 7 0 ) = ( 2 · 1 7 ) ( 2 · 0 )
128 eqid ⊢ 1 7 = 1 7
129 69 oveq1i ⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
130 129 113 eqtri ⊢ ( ( 2 · 1 ) + 1 ) = 3
131 7cn ⊢ 7 ∈ ℂ
132 7t2e14 ⊢ ( 7 · 2 ) = 1 4
133 131 29 132 mulcomli ⊢ ( 2 · 7 ) = 1 4
134 17 7 8 128 2 7 130 133 decmul2c ⊢ ( 2 · 1 7 ) = 3 4
135 134 70 deceq12i ⊢ ( 2 · 1 7 ) ( 2 · 0 ) = 3 4 0
136 127 135 eqtri ⊢ ( 2 · 1 7 0 ) = 3 4 0
137 5 6 11 12 7 7 126 136 78 mod2xi ⊢ ( ( 2 ↑ 3 4 0 ) mod 3 4 1 ) = ( 1 mod 3 4 1 )
138 1re ⊢ 1 ∈ ℝ
139 nnrp ⊢ ( 3 4 1 ∈ ℕ → 3 4 1 ∈ ℝ+ )
140 5 139 ax-mp ⊢ 3 4 1 ∈ ℝ+
141 0le1 ⊢ 0 ≤ 1
142 4nn ⊢ 4 ∈ ℕ
143 1 142 decnncl ⊢ 3 4 ∈ ℕ
144 9re ⊢ 9 ∈ ℝ
145 1lt9 ⊢ 1 < 9
146 138 144 145 ltleii ⊢ 1 ≤ 9
147 143 7 7 146 decltdi ⊢ 1 < 3 4 1
148 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 3 4 1 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 3 4 1 ) ) → ( 1 mod 3 4 1 ) = 1 )
149 138 140 141 147 148 mp4an ⊢ ( 1 mod 3 4 1 ) = 1
150 137 149 eqtri ⊢ ( ( 2 ↑ 3 4 0 ) mod 3 4 1 ) = 1