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 mulid1i 
 |-  ( 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 43 29 55 mulcomli 
 |-  ( 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 mulid1i 
 |-  ( 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 addid2i 
 |-  ( 0 + 2 ) = 2
83 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + 2 ) = ( 0 + 2 )
84 29 mulid2i 
 |-  ( 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 addid2i 
 |-  ( 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 4t2e8 
 |-  ( 4 x. 2 ) = 8
96 42 29 95 mulcomli 
 |-  ( 2 x. 4 ) = 8
97 96 62 deceq12i 
 |-  ; ( 2 x. 4 ) ( 2 x. 2 ) = ; 8 4
98 94 97 eqtri 
 |-  ( 2 x. ; 4 2 ) = ; 8 4
99 21 nn0cni 
 |-  ; 1 6 e. CC
100 99 addid2i 
 |-  ( 0 + ; 1 6 ) = ; 1 6
101 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 1 6 ) = ( 0 + ; 1 6 )
102 4t4e16 
 |-  ( 4 x. 4 ) = ; 1 6
103 100 101 102 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 1 6 ) = ( 4 x. 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 e. CC
109 108 addid2i 
 |-  ( 0 + ; 3 2 ) = ; 3 2
110 75 oveq1i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 3 2 ) = ( 0 + ; 3 2 )
111 eqid 
 |-  ; 1 6 = ; 1 6
112 84 oveq1i 
 |-  ( ( 1 x. 2 ) + 1 ) = ( 2 + 1 )
113 2p1e3 
 |-  ( 2 + 1 ) = 3
114 112 113 eqtri 
 |-  ( ( 1 x. 2 ) + 1 ) = 3
115 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
116 17 7 20 111 17 7 114 115 decmul1c 
 |-  ( ; 1 6 x. 2 ) = ; 3 2
117 109 110 116 3eqtr4i 
 |-  ( ( 0 x. ; ; 3 4 1 ) + ; 3 2 ) = ( ; 1 6 x. 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 e. CC
122 8t2e16 
 |-  ( 8 x. 2 ) = ; 1 6
123 121 29 122 mulcomli 
 |-  ( 2 x. 8 ) = ; 1 6
124 7 20 120 123 decsuc 
 |-  ( ( 2 x. 8 ) + 1 ) = ; 1 7
125 17 13 14 119 10 7 124 31 decmul2c 
 |-  ( 2 x. ; 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 x. ; ; 1 7 0 ) = ; ( 2 x. ; 1 7 ) ( 2 x. 0 )
128 eqid 
 |-  ; 1 7 = ; 1 7
129 69 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
130 129 113 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
131 7cn 
 |-  7 e. CC
132 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
133 131 29 132 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
134 17 7 8 128 2 7 130 133 decmul2c 
 |-  ( 2 x. ; 1 7 ) = ; 3 4
135 134 70 deceq12i 
 |-  ; ( 2 x. ; 1 7 ) ( 2 x. 0 ) = ; ; 3 4 0
136 127 135 eqtri 
 |-  ( 2 x. ; ; 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 e. RR
139 nnrp 
 |-  ( ; ; 3 4 1 e. NN -> ; ; 3 4 1 e. RR+ )
140 5 139 ax-mp 
 |-  ; ; 3 4 1 e. RR+
141 0le1 
 |-  0 <_ 1
142 4nn 
 |-  4 e. NN
143 1 142 decnncl 
 |-  ; 3 4 e. NN
144 9re 
 |-  9 e. RR
145 1lt9 
 |-  1 < 9
146 138 144 145 ltleii 
 |-  1 <_ 9
147 143 7 7 146 decltdi 
 |-  1 < ; ; 3 4 1
148 modid 
 |-  ( ( ( 1 e. RR /\ ; ; 3 4 1 e. RR+ ) /\ ( 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