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 e. NN0
2 4nn0 
 |-  4 e. NN0
3 1 2 deccl 
 |-  ; 3 4 e. NN0
4 1nn 
 |-  1 e. NN
5 3 4 decnncl 
 |-  ; ; 3 4 1 e. NN
6 2nn 
 |-  2 e. NN
7 1nn0 
 |-  1 e. NN0
8 7nn0 
 |-  7 e. NN0
9 7 8 deccl 
 |-  ; 1 7 e. NN0
10 0nn0 
 |-  0 e. NN0
11 9 10 deccl 
 |-  ; ; 1 7 0 e. NN0
12 0z 
 |-  0 e. ZZ
13 8nn0 
 |-  8 e. NN0
14 5nn0 
 |-  5 e. NN0
15 13 14 deccl 
 |-  ; 8 5 e. NN0
16 3z 
 |-  3 e. ZZ
17 2nn0 
 |-  2 e. NN0
18 1 17 deccl 
 |-  ; 3 2 e. NN0
19 13 2 deccl 
 |-  ; 8 4 e. NN0
20 6nn0 
 |-  6 e. NN0
21 7 20 deccl 
 |-  ; 1 6 e. NN0
22 2 17 deccl 
 |-  ; 4 2 e. NN0
23 17 7 deccl 
 |-  ; 2 1 e. NN0
24 17 10 deccl 
 |-  ; 2 0 e. NN0
25 7 10 deccl 
 |-  ; 1 0 e. NN0
26 2exp5 
 |-  ( 2 ^ 5 ) = ; 3 2
27 26 oveq1i 
 |-  ( ( 2 ^ 5 ) mod ; ; 3 4 1 ) = ( ; 3 2 mod ; ; 3 4 1 )
28 5cn 
 |-  5 e. CC
29 2cn 
 |-  2 e. CC
30 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
31 28 29 30 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
32 25 17 deccl 
 |-  ; ; 1 0 2 e. NN0
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 x. ; ; 3 4 1 ) = ; ( 3 x. ; 3 4 ) ( 3 x. 1 )
37 eqid 
 |-  ; 3 4 = ; 3 4
38 3t3e9 
 |-  ( 3 x. 3 ) = 9
39 38 oveq1i 
 |-  ( ( 3 x. 3 ) + 1 ) = ( 9 + 1 )
40 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
41 39 40 eqtri 
 |-  ( ( 3 x. 3 ) + 1 ) = ; 1 0
42 4cn 
 |-  4 e. CC
43 3cn 
 |-  3 e. CC
44 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
45 42 43 44 mulcomli 
 |-  ( 3 x. 4 ) = ; 1 2
46 1 1 2 37 17 7 41 45 decmul2c 
 |-  ( 3 x. ; 3 4 ) = ; ; 1 0 2
47 43 mulridi 
 |-  ( 3 x. 1 ) = 3
48 46 47 deceq12i 
 |-  ; ( 3 x. ; 3 4 ) ( 3 x. 1 ) = ; ; ; 1 0 2 3
49 36 48 eqtri 
 |-  ( 3 x. ; ; 3 4 1 ) = ; ; ; 1 0 2 3
50 49 oveq1i 
 |-  ( ( 3 x. ; ; 3 4 1 ) + 1 ) = ( ; ; ; 1 0 2 3 + 1 )
51 eqid 
 |-  ; 3 2 = ; 3 2
52 1 1 17 decmulnc 
 |-  ( 3 x. ; 3 2 ) = ; ( 3 x. 3 ) ( 3 x. 2 )
53 52 oveq1i 
 |-  ( ( 3 x. ; 3 2 ) + 6 ) = ( ; ( 3 x. 3 ) ( 3 x. 2 ) + 6 )
54 9nn0 
 |-  9 e. NN0
55 3t2e6 
 |-  ( 3 x. 2 ) = 6
56 38 55 deceq12i 
 |-  ; ( 3 x. 3 ) ( 3 x. 2 ) = ; 9 6
57 6p6e12 
 |-  ( 6 + 6 ) = ; 1 2
58 54 20 20 56 40 17 57 decaddci 
 |-  ( ; ( 3 x. 3 ) ( 3 x. 2 ) + 6 ) = ; ; 1 0 2
59 53 58 eqtri 
 |-  ( ( 3 x. ; 3 2 ) + 6 ) = ; ; 1 0 2
60 17 1 17 decmulnc 
 |-  ( 2 x. ; 3 2 ) = ; ( 2 x. 3 ) ( 2 x. 2 )
61 2t3e6 
 |-  ( 2 x. 3 ) = 6
62 2t2e4 
 |-  ( 2 x. 2 ) = 4
63 61 62 deceq12i 
 |-  ; ( 2 x. 3 ) ( 2 x. 2 ) = ; 6 4
64 60 63 eqtri 
 |-  ( 2 x. ; 3 2 ) = ; 6 4
65 18 1 17 51 2 20 59 64 decmul1c 
 |-  ( ; 3 2 x. ; 3 2 ) = ; ; ; 1 0 2 4
66 35 50 65 3eqtr4i 
 |-  ( ( 3 x. ; ; 3 4 1 ) + 1 ) = ( ; 3 2 x. ; 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 x. ; 1 0 ) = ; ( 2 x. 1 ) ( 2 x. 0 )
69 29 mulridi 
 |-  ( 2 x. 1 ) = 2
70 2t0e0 
 |-  ( 2 x. 0 ) = 0
71 69 70 deceq12i 
 |-  ; ( 2 x. 1 ) ( 2 x. 0 ) = ; 2 0
72 68 71 eqtri 
 |-  ( 2 x. ; 1 0 ) = ; 2 0
73 0p1e1 
 |-  ( 0 + 1 ) = 1
74 5 nncni 
 |-  ; ; 3 4 1 e. CC
75 74 mul02i 
 |-  ( 0 x. ; ; 3 4 1 ) = 0
76 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + 1 ) = ( 0 + 1 )
77 1t1e1 
 |-  ( 1 x. 1 ) = 1
78 73 76 77 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + 1 ) = ( 1 x. 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 x. ; ; 3 4 1 ) + 2 ) = ( 0 + 2 )
84 29 mullidi 
 |-  ( 1 x. 2 ) = 2
85 82 83 84 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + 2 ) = ( 1 x. 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 x. ; 2 1 ) = ; ( 2 x. 2 ) ( 2 x. 1 )
88 62 69 deceq12i 
 |-  ; ( 2 x. 2 ) ( 2 x. 1 ) = ; 4 2
89 87 88 eqtri 
 |-  ( 2 x. ; 2 1 ) = ; 4 2
90 42 addlidi 
 |-  ( 0 + 4 ) = 4
91 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + 4 ) = ( 0 + 4 )
92 90 91 62 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + 4 ) = ( 2 x. 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 x. ; 4 2 ) = ; ( 2 x. 4 ) ( 2 x. 2 )
95 2t4e8 
 |-  ( 2 x. 4 ) = 8
96 95 62 deceq12i 
 |-  ; ( 2 x. 4 ) ( 2 x. 2 ) = ; 8 4
97 94 96 eqtri 
 |-  ( 2 x. ; 4 2 ) = ; 8 4
98 21 nn0cni 
 |-  ; 1 6 e. CC
99 98 addlidi 
 |-  ( 0 + ; 1 6 ) = ; 1 6
100 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 1 6 ) = ( 0 + ; 1 6 )
101 4t4e16 
 |-  ( 4 x. 4 ) = ; 1 6
102 99 100 101 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 1 6 ) = ( 4 x. 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 e. CC
108 107 addlidi 
 |-  ( 0 + ; 3 2 ) = ; 3 2
109 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 3 2 ) = ( 0 + ; 3 2 )
110 eqid 
 |-  ; 1 6 = ; 1 6
111 84 oveq1i 
 |-  ( ( 1 x. 2 ) + 1 ) = ( 2 + 1 )
112 2p1e3 
 |-  ( 2 + 1 ) = 3
113 111 112 eqtri 
 |-  ( ( 1 x. 2 ) + 1 ) = 3
114 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
115 17 7 20 110 17 7 113 114 decmul1c 
 |-  ( ; 1 6 x. 2 ) = ; 3 2
116 108 109 115 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 3 2 ) = ( ; 1 6 x. 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 e. CC
121 8t2e16 
 |-  ( 8 x. 2 ) = ; 1 6
122 120 29 121 mulcomli 
 |-  ( 2 x. 8 ) = ; 1 6
123 7 20 119 122 decsuc 
 |-  ( ( 2 x. 8 ) + 1 ) = ; 1 7
124 17 13 14 118 10 7 123 31 decmul2c 
 |-  ( 2 x. ; 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 x. ; ; 1 7 0 ) = ; ( 2 x. ; 1 7 ) ( 2 x. 0 )
127 eqid 
 |-  ; 1 7 = ; 1 7
128 69 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
129 128 112 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
130 7cn 
 |-  7 e. CC
131 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
132 130 29 131 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
133 17 7 8 127 2 7 129 132 decmul2c 
 |-  ( 2 x. ; 1 7 ) = ; 3 4
134 133 70 deceq12i 
 |-  ; ( 2 x. ; 1 7 ) ( 2 x. 0 ) = ; ; 3 4 0
135 126 134 eqtri 
 |-  ( 2 x. ; ; 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 e. RR
138 nnrp 
 |-  ( ; ; 3 4 1 e. NN -> ; ; 3 4 1 e. RR+ )
139 5 138 ax-mp 
 |-  ; ; 3 4 1 e. RR+
140 0le1 
 |-  0 <_ 1
141 4nn 
 |-  4 e. NN
142 1 141 decnncl 
 |-  ; 3 4 e. NN
143 9re 
 |-  9 e. RR
144 1lt9 
 |-  1 < 9
145 137 143 144 ltleii 
 |-  1 <_ 9
146 142 7 7 145 decltdi 
 |-  1 < ; ; 3 4 1
147 modid 
 |-  ( ( ( 1 e. RR /\ ; ; 3 4 1 e. RR+ ) /\ ( 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