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 ⊢ 𝑁 = 2 5 0 3
Assertion 2503lem1 ( ( 2 ↑ 1 8 ) mod 𝑁 ) = ( 1 8 3 2 mod 𝑁 )

Proof

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