# Metamath Proof Explorer

## Theorem 2503lem1

Description: Lemma for 2503prm . Calculate a power mod. In decimal, we calculate 2 ^ 1 8 = 5 1 2 ^ 2 = 1 0 4 N + 1 8 3 2 == 1 8 3 2 . (Contributed by Mario Carneiro, 3-Mar-2014) (Revised by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Hypothesis 2503prm.1 $⊢ N = 2503$
Assertion 2503lem1 $⊢ 2 18 mod N = 1832 mod N$

### Proof

Step Hyp Ref Expression
1 2503prm.1 $⊢ N = 2503$
2 2nn0 $⊢ 2 ∈ ℕ 0$
3 5nn0 $⊢ 5 ∈ ℕ 0$
4 2 3 deccl $⊢ 25 ∈ ℕ 0$
5 0nn0 $⊢ 0 ∈ ℕ 0$
6 4 5 deccl $⊢ 250 ∈ ℕ 0$
7 3nn $⊢ 3 ∈ ℕ$
8 6 7 decnncl $⊢ 2503 ∈ ℕ$
9 1 8 eqeltri $⊢ N ∈ ℕ$
10 2nn $⊢ 2 ∈ ℕ$
11 9nn0 $⊢ 9 ∈ ℕ 0$
12 10nn0 $⊢ 10 ∈ ℕ 0$
13 4nn0 $⊢ 4 ∈ ℕ 0$
14 12 13 deccl $⊢ 104 ∈ ℕ 0$
15 14 nn0zi $⊢ 104 ∈ ℤ$
16 1nn0 $⊢ 1 ∈ ℕ 0$
17 3 16 deccl $⊢ 51 ∈ ℕ 0$
18 17 2 deccl $⊢ 512 ∈ ℕ 0$
19 8nn0 $⊢ 8 ∈ ℕ 0$
20 16 19 deccl $⊢ 18 ∈ ℕ 0$
21 3nn0 $⊢ 3 ∈ ℕ 0$
22 20 21 deccl $⊢ 183 ∈ ℕ 0$
23 22 2 deccl $⊢ 1832 ∈ ℕ 0$
24 8p1e9 $⊢ 8 + 1 = 9$
25 6nn0 $⊢ 6 ∈ ℕ 0$
26 2exp8 $⊢ 2 8 = 256$
27 eqid $⊢ 25 = 25$
28 16 dec0h $⊢ 1 = 01$
29 2t2e4 $⊢ 2 ⋅ 2 = 4$
30 ax-1cn $⊢ 1 ∈ ℂ$
31 30 addid2i $⊢ 0 + 1 = 1$
32 29 31 oveq12i $⊢ 2 ⋅ 2 + 0 + 1 = 4 + 1$
33 4p1e5 $⊢ 4 + 1 = 5$
34 32 33 eqtri $⊢ 2 ⋅ 2 + 0 + 1 = 5$
35 5t2e10 $⊢ 5 ⋅ 2 = 10$
36 16 5 31 35 decsuc $⊢ 5 ⋅ 2 + 1 = 11$
37 2 3 5 16 27 28 2 16 16 34 36 decmac $⊢ 25 ⋅ 2 + 1 = 51$
38 6t2e12 $⊢ 6 ⋅ 2 = 12$
39 2 4 25 26 2 16 37 38 decmul1c $⊢ 2 8 ⋅ 2 = 512$
40 2 19 24 39 numexpp1 $⊢ 2 9 = 512$
41 40 oveq1i $⊢ 2 9 mod N = 512 mod N$
42 9cn $⊢ 9 ∈ ℂ$
43 2cn $⊢ 2 ∈ ℂ$
44 9t2e18 $⊢ 9 ⋅ 2 = 18$
45 42 43 44 mulcomli $⊢ 2 ⋅ 9 = 18$
46 eqid $⊢ 1832 = 1832$
47 21 16 deccl $⊢ 31 ∈ ℕ 0$
48 2 16 deccl $⊢ 21 ∈ ℕ 0$
49 eqid $⊢ 250 = 250$
50 eqid $⊢ 183 = 183$
51 eqid $⊢ 31 = 31$
52 eqid $⊢ 18 = 18$
53 1p1e2 $⊢ 1 + 1 = 2$
54 8p3e11 $⊢ 8 + 3 = 11$
55 16 19 21 52 53 16 54 decaddci $⊢ 18 + 3 = 21$
56 3p1e4 $⊢ 3 + 1 = 4$
57 20 21 21 16 50 51 55 56 decadd $⊢ 183 + 31 = 214$
58 48 nn0cni $⊢ 21 ∈ ℂ$
59 58 addid1i $⊢ 21 + 0 = 21$
60 3 2 deccl $⊢ 52 ∈ ℕ 0$
61 eqid $⊢ 104 = 104$
62 60 nn0cni $⊢ 52 ∈ ℂ$
63 eqid $⊢ 52 = 52$
64 2p2e4 $⊢ 2 + 2 = 4$
65 3 2 2 63 64 decaddi $⊢ 52 + 2 = 54$
66 62 43 65 addcomli $⊢ 2 + 52 = 54$
67 2 dec0u $⊢ 10 ⋅ 2 = 20$
68 5p1e6 $⊢ 5 + 1 = 6$
69 67 68 oveq12i $⊢ 10 ⋅ 2 + 5 + 1 = 20 + 6$
70 eqid $⊢ 20 = 20$
71 6cn $⊢ 6 ∈ ℂ$
72 71 addid2i $⊢ 0 + 6 = 6$
73 2 5 25 70 72 decaddi $⊢ 20 + 6 = 26$
74 69 73 eqtri $⊢ 10 ⋅ 2 + 5 + 1 = 26$
75 4t2e8 $⊢ 4 ⋅ 2 = 8$
76 75 oveq1i $⊢ 4 ⋅ 2 + 4 = 8 + 4$
77 8p4e12 $⊢ 8 + 4 = 12$
78 76 77 eqtri $⊢ 4 ⋅ 2 + 4 = 12$
79 12 13 3 13 61 66 2 2 16 74 78 decmac $⊢ 104 ⋅ 2 + 2 + 52 = 262$
80 3 dec0u $⊢ 10 ⋅ 5 = 50$
81 43 addid2i $⊢ 0 + 2 = 2$
82 80 81 oveq12i $⊢ 10 ⋅ 5 + 0 + 2 = 50 + 2$
83 eqid $⊢ 50 = 50$
84 3 5 2 83 81 decaddi $⊢ 50 + 2 = 52$
85 82 84 eqtri $⊢ 10 ⋅ 5 + 0 + 2 = 52$
86 5cn $⊢ 5 ∈ ℂ$
87 4cn $⊢ 4 ∈ ℂ$
88 5t4e20 $⊢ 5 ⋅ 4 = 20$
89 86 87 88 mulcomli $⊢ 4 ⋅ 5 = 20$
90 2 5 31 89 decsuc $⊢ 4 ⋅ 5 + 1 = 21$
91 12 13 5 16 61 28 3 16 2 85 90 decmac $⊢ 104 ⋅ 5 + 1 = 521$
92 2 3 2 16 27 59 14 16 60 79 91 decma2c $⊢ 104 ⋅ 25 + 21 + 0 = 2621$
93 14 nn0cni $⊢ 104 ∈ ℂ$
94 93 mul01i $⊢ 104 ⋅ 0 = 0$
95 94 oveq1i $⊢ 104 ⋅ 0 + 4 = 0 + 4$
96 87 addid2i $⊢ 0 + 4 = 4$
97 13 dec0h $⊢ 4 = 04$
98 95 96 97 3eqtri $⊢ 104 ⋅ 0 + 4 = 04$
99 4 5 48 13 49 57 14 13 5 92 98 decma2c $⊢ 104 ⋅ 250 + 183 + 31 = 26214$
100 eqid $⊢ 10 = 10$
101 3cn $⊢ 3 ∈ ℂ$
102 101 mulid2i $⊢ 1 ⋅ 3 = 3$
103 00id $⊢ 0 + 0 = 0$
104 102 103 oveq12i $⊢ 1 ⋅ 3 + 0 + 0 = 3 + 0$
105 101 addid1i $⊢ 3 + 0 = 3$
106 104 105 eqtri $⊢ 1 ⋅ 3 + 0 + 0 = 3$
107 101 mul02i $⊢ 0 ⋅ 3 = 0$
108 107 oveq1i $⊢ 0 ⋅ 3 + 1 = 0 + 1$
109 108 31 28 3eqtri $⊢ 0 ⋅ 3 + 1 = 01$
110 16 5 5 16 100 28 21 16 5 106 109 decmac $⊢ 10 ⋅ 3 + 1 = 31$
111 4t3e12 $⊢ 4 ⋅ 3 = 12$
112 16 2 2 111 64 decaddi $⊢ 4 ⋅ 3 + 2 = 14$
113 12 13 2 61 21 13 16 110 112 decrmac $⊢ 104 ⋅ 3 + 2 = 314$
114 6 21 22 2 1 46 14 13 47 99 113 decma2c $⊢ 104 ⋅ N + 1832 = 262144$
115 eqid $⊢ 512 = 512$
116 12 2 deccl $⊢ 102 ∈ ℕ 0$
117 eqid $⊢ 51 = 51$
118 eqid $⊢ 102 = 102$
119 86 30 68 addcomli $⊢ 1 + 5 = 6$
120 16 5 3 16 100 117 119 31 decadd $⊢ 10 + 51 = 61$
121 7nn0 $⊢ 7 ∈ ℕ 0$
122 6p1e7 $⊢ 6 + 1 = 7$
123 121 dec0h $⊢ 7 = 07$
124 122 123 eqtri $⊢ 6 + 1 = 07$
125 31 oveq2i $⊢ 5 ⋅ 5 + 0 + 1 = 5 ⋅ 5 + 1$
126 5t5e25 $⊢ 5 ⋅ 5 = 25$
127 2 3 68 126 decsuc $⊢ 5 ⋅ 5 + 1 = 26$
128 125 127 eqtri $⊢ 5 ⋅ 5 + 0 + 1 = 26$
129 86 mulid2i $⊢ 1 ⋅ 5 = 5$
130 129 oveq1i $⊢ 1 ⋅ 5 + 7 = 5 + 7$
131 7cn $⊢ 7 ∈ ℂ$
132 7p5e12 $⊢ 7 + 5 = 12$
133 131 86 132 addcomli $⊢ 5 + 7 = 12$
134 130 133 eqtri $⊢ 1 ⋅ 5 + 7 = 12$
135 3 16 5 121 117 124 3 2 16 128 134 decmac $⊢ 51 ⋅ 5 + 6 + 1 = 262$
136 86 43 35 mulcomli $⊢ 2 ⋅ 5 = 10$
137 16 5 31 136 decsuc $⊢ 2 ⋅ 5 + 1 = 11$
138 17 2 25 16 115 120 3 16 16 135 137 decmac $⊢ 512 ⋅ 5 + 10 + 51 = 2621$
139 17 nn0cni $⊢ 51 ∈ ℂ$
140 139 mulid1i $⊢ 51 ⋅ 1 = 51$
141 43 mulid1i $⊢ 2 ⋅ 1 = 2$
142 141 oveq1i $⊢ 2 ⋅ 1 + 2 = 2 + 2$
143 142 64 eqtri $⊢ 2 ⋅ 1 + 2 = 4$
144 17 2 2 115 16 140 143 decrmanc $⊢ 512 ⋅ 1 + 2 = 514$
145 3 16 12 2 117 118 18 13 17 138 144 decma2c $⊢ 512 ⋅ 51 + 102 = 26214$
146 43 mulid2i $⊢ 1 ⋅ 2 = 2$
147 2 3 16 117 35 146 decmul1 $⊢ 51 ⋅ 2 = 102$
148 2 17 2 115 147 29 decmul1 $⊢ 512 ⋅ 2 = 1024$
149 18 17 2 115 13 116 145 148 decmul2c $⊢ 512 ⋅ 512 = 262144$
150 114 149 eqtr4i $⊢ 104 ⋅ N + 1832 = 512 ⋅ 512$
151 9 10 11 15 18 23 41 45 150 mod2xi $⊢ 2 18 mod N = 1832 mod N$