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 mulridi ⊢ ( 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 2t3e6 ⊢ ( 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 mulridi ⊢ ( 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 addlidi ⊢ ( 0 + 2 ) = 2
83 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 2 ) = ( 0 + 2 )
84 29 mullidi ⊢ ( 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 addlidi ⊢ ( 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 2t4e8 ⊢ ( 2 · 4 ) = 8
96 95 62 deceq12i ⊢ ( 2 · 4 ) ( 2 · 2 ) = 8 4
97 94 96 eqtri ⊢ ( 2 · 4 2 ) = 8 4
98 21 nn0cni ⊢ 1 6 ∈ ℂ
99 98 addlidi ⊢ ( 0 + 1 6 ) = 1 6
100 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 1 6 ) = ( 0 + 1 6 )
101 4t4e16 ⊢ ( 4 · 4 ) = 1 6
102 99 100 101 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 1 6 ) = ( 4 · 4 )
103 5 6 22 12 2 21 93 97 102 mod2xi ⊢ ( ( 2 ↑ 8 4 ) mod 3 4 1 ) = ( 1 6 mod 3 4 1 )
104 4p1e5 ⊢ ( 4 + 1 ) = 5
105 eqid ⊢ 8 4 = 8 4
106 13 2 104 105 decsuc ⊢ ( 8 4 + 1 ) = 8 5
107 18 nn0cni ⊢ 3 2 ∈ ℂ
108 107 addlidi ⊢ ( 0 + 3 2 ) = 3 2
109 75 oveq1i ⊢ ( ( 0 · 3 4 1 ) + 3 2 ) = ( 0 + 3 2 )
110 eqid ⊢ 1 6 = 1 6
111 84 oveq1i ⊢ ( ( 1 · 2 ) + 1 ) = ( 2 + 1 )
112 2p1e3 ⊢ ( 2 + 1 ) = 3
113 111 112 eqtri ⊢ ( ( 1 · 2 ) + 1 ) = 3
114 6t2e12 ⊢ ( 6 · 2 ) = 1 2
115 17 7 20 110 17 7 113 114 decmul1c ⊢ ( 1 6 · 2 ) = 3 2
116 108 109 115 3eqtr4i ⊢ ( ( 0 · 3 4 1 ) + 3 2 ) = ( 1 6 · 2 )
117 5 6 19 12 21 18 103 106 116 modxp1i ⊢ ( ( 2 ↑ 8 5 ) mod 3 4 1 ) = ( 3 2 mod 3 4 1 )
118 eqid ⊢ 8 5 = 8 5
119 6p1e7 ⊢ ( 6 + 1 ) = 7
120 8cn ⊢ 8 ∈ ℂ
121 8t2e16 ⊢ ( 8 · 2 ) = 1 6
122 120 29 121 mulcomli ⊢ ( 2 · 8 ) = 1 6
123 7 20 119 122 decsuc ⊢ ( ( 2 · 8 ) + 1 ) = 1 7
124 17 13 14 118 10 7 123 31 decmul2c ⊢ ( 2 · 8 5 ) = 1 7 0
125 5 6 15 16 18 7 117 124 66 mod2xi ⊢ ( ( 2 ↑ 1 7 0 ) mod 3 4 1 ) = ( 1 mod 3 4 1 )
126 17 9 10 decmulnc ⊢ ( 2 · 1 7 0 ) = ( 2 · 1 7 ) ( 2 · 0 )
127 eqid ⊢ 1 7 = 1 7
128 69 oveq1i ⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 )
129 128 112 eqtri ⊢ ( ( 2 · 1 ) + 1 ) = 3
130 7cn ⊢ 7 ∈ ℂ
131 7t2e14 ⊢ ( 7 · 2 ) = 1 4
132 130 29 131 mulcomli ⊢ ( 2 · 7 ) = 1 4
133 17 7 8 127 2 7 129 132 decmul2c ⊢ ( 2 · 1 7 ) = 3 4
134 133 70 deceq12i ⊢ ( 2 · 1 7 ) ( 2 · 0 ) = 3 4 0
135 126 134 eqtri ⊢ ( 2 · 1 7 0 ) = 3 4 0
136 5 6 11 12 7 7 125 135 78 mod2xi ⊢ ( ( 2 ↑ 3 4 0 ) mod 3 4 1 ) = ( 1 mod 3 4 1 )
137 1re ⊢ 1 ∈ ℝ
138 nnrp ⊢ ( 3 4 1 ∈ ℕ → 3 4 1 ∈ ℝ+ )
139 5 138 ax-mp ⊢ 3 4 1 ∈ ℝ+
140 0le1 ⊢ 0 ≤ 1
141 4nn ⊢ 4 ∈ ℕ
142 1 141 decnncl ⊢ 3 4 ∈ ℕ
143 9re ⊢ 9 ∈ ℝ
144 1lt9 ⊢ 1 < 9
145 137 143 144 ltleii ⊢ 1 ≤ 9
146 142 7 7 145 decltdi ⊢ 1 < 3 4 1
147 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 3 4 1 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 3 4 1 ) ) → ( 1 mod 3 4 1 ) = 1 )
148 137 139 140 146 147 mp4an ⊢ ( 1 mod 3 4 1 ) = 1
149 136 148 eqtri ⊢ ( ( 2 ↑ 3 4 0 ) mod 3 4 1 ) = 1