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 = ; ; ; 2 5 0 3
Assertion 2503lem1 
|- ( ( 2 ^ ; 1 8 ) mod N ) = ( ; ; ; 1 8 3 2 mod N )

Proof

Step Hyp Ref Expression
1 2503prm.1 
 |-  N = ; ; ; 2 5 0 3
2 2nn0 
 |-  2 e. NN0
3 5nn0 
 |-  5 e. NN0
4 2 3 deccl 
 |-  ; 2 5 e. NN0
5 0nn0 
 |-  0 e. NN0
6 4 5 deccl 
 |-  ; ; 2 5 0 e. NN0
7 3nn 
 |-  3 e. NN
8 6 7 decnncl 
 |-  ; ; ; 2 5 0 3 e. NN
9 1 8 eqeltri 
 |-  N e. NN
10 2nn 
 |-  2 e. NN
11 9nn0 
 |-  9 e. NN0
12 10nn0 
 |-  ; 1 0 e. NN0
13 4nn0 
 |-  4 e. NN0
14 12 13 deccl 
 |-  ; ; 1 0 4 e. NN0
15 14 nn0zi 
 |-  ; ; 1 0 4 e. ZZ
16 1nn0 
 |-  1 e. NN0
17 3 16 deccl 
 |-  ; 5 1 e. NN0
18 17 2 deccl 
 |-  ; ; 5 1 2 e. NN0
19 8nn0 
 |-  8 e. NN0
20 16 19 deccl 
 |-  ; 1 8 e. NN0
21 3nn0 
 |-  3 e. NN0
22 20 21 deccl 
 |-  ; ; 1 8 3 e. NN0
23 22 2 deccl 
 |-  ; ; ; 1 8 3 2 e. NN0
24 8p1e9 
 |-  ( 8 + 1 ) = 9
25 6nn0 
 |-  6 e. NN0
26 2exp8 
 |-  ( 2 ^ 8 ) = ; ; 2 5 6
27 eqid 
 |-  ; 2 5 = ; 2 5
28 16 dec0h 
 |-  1 = ; 0 1
29 2t2e4 
 |-  ( 2 x. 2 ) = 4
30 ax-1cn 
 |-  1 e. CC
31 30 addid2i 
 |-  ( 0 + 1 ) = 1
32 29 31 oveq12i 
 |-  ( ( 2 x. 2 ) + ( 0 + 1 ) ) = ( 4 + 1 )
33 4p1e5 
 |-  ( 4 + 1 ) = 5
34 32 33 eqtri 
 |-  ( ( 2 x. 2 ) + ( 0 + 1 ) ) = 5
35 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
36 16 5 31 35 decsuc 
 |-  ( ( 5 x. 2 ) + 1 ) = ; 1 1
37 2 3 5 16 27 28 2 16 16 34 36 decmac 
 |-  ( ( ; 2 5 x. 2 ) + 1 ) = ; 5 1
38 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
39 2 4 25 26 2 16 37 38 decmul1c 
 |-  ( ( 2 ^ 8 ) x. 2 ) = ; ; 5 1 2
40 2 19 24 39 numexpp1 
 |-  ( 2 ^ 9 ) = ; ; 5 1 2
41 40 oveq1i 
 |-  ( ( 2 ^ 9 ) mod N ) = ( ; ; 5 1 2 mod N )
42 9cn 
 |-  9 e. CC
43 2cn 
 |-  2 e. CC
44 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
45 42 43 44 mulcomli 
 |-  ( 2 x. 9 ) = ; 1 8
46 eqid 
 |-  ; ; ; 1 8 3 2 = ; ; ; 1 8 3 2
47 21 16 deccl 
 |-  ; 3 1 e. NN0
48 2 16 deccl 
 |-  ; 2 1 e. NN0
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 e. CC
59 58 addid1i 
 |-  ( ; 2 1 + 0 ) = ; 2 1
60 3 2 deccl 
 |-  ; 5 2 e. NN0
61 eqid 
 |-  ; ; 1 0 4 = ; ; 1 0 4
62 60 nn0cni 
 |-  ; 5 2 e. CC
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 x. 2 ) = ; 2 0
68 5p1e6 
 |-  ( 5 + 1 ) = 6
69 67 68 oveq12i 
 |-  ( ( ; 1 0 x. 2 ) + ( 5 + 1 ) ) = ( ; 2 0 + 6 )
70 eqid 
 |-  ; 2 0 = ; 2 0
71 6cn 
 |-  6 e. CC
72 71 addid2i 
 |-  ( 0 + 6 ) = 6
73 2 5 25 70 72 decaddi 
 |-  ( ; 2 0 + 6 ) = ; 2 6
74 69 73 eqtri 
 |-  ( ( ; 1 0 x. 2 ) + ( 5 + 1 ) ) = ; 2 6
75 4t2e8 
 |-  ( 4 x. 2 ) = 8
76 75 oveq1i 
 |-  ( ( 4 x. 2 ) + 4 ) = ( 8 + 4 )
77 8p4e12 
 |-  ( 8 + 4 ) = ; 1 2
78 76 77 eqtri 
 |-  ( ( 4 x. 2 ) + 4 ) = ; 1 2
79 12 13 3 13 61 66 2 2 16 74 78 decmac 
 |-  ( ( ; ; 1 0 4 x. 2 ) + ( 2 + ; 5 2 ) ) = ; ; 2 6 2
80 3 dec0u 
 |-  ( ; 1 0 x. 5 ) = ; 5 0
81 43 addid2i 
 |-  ( 0 + 2 ) = 2
82 80 81 oveq12i 
 |-  ( ( ; 1 0 x. 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 x. 5 ) + ( 0 + 2 ) ) = ; 5 2
86 5cn 
 |-  5 e. CC
87 4cn 
 |-  4 e. CC
88 5t4e20 
 |-  ( 5 x. 4 ) = ; 2 0
89 86 87 88 mulcomli 
 |-  ( 4 x. 5 ) = ; 2 0
90 2 5 31 89 decsuc 
 |-  ( ( 4 x. 5 ) + 1 ) = ; 2 1
91 12 13 5 16 61 28 3 16 2 85 90 decmac 
 |-  ( ( ; ; 1 0 4 x. 5 ) + 1 ) = ; ; 5 2 1
92 2 3 2 16 27 59 14 16 60 79 91 decma2c 
 |-  ( ( ; ; 1 0 4 x. ; 2 5 ) + ( ; 2 1 + 0 ) ) = ; ; ; 2 6 2 1
93 14 nn0cni 
 |-  ; ; 1 0 4 e. CC
94 93 mul01i 
 |-  ( ; ; 1 0 4 x. 0 ) = 0
95 94 oveq1i 
 |-  ( ( ; ; 1 0 4 x. 0 ) + 4 ) = ( 0 + 4 )
96 87 addid2i 
 |-  ( 0 + 4 ) = 4
97 13 dec0h 
 |-  4 = ; 0 4
98 95 96 97 3eqtri 
 |-  ( ( ; ; 1 0 4 x. 0 ) + 4 ) = ; 0 4
99 4 5 48 13 49 57 14 13 5 92 98 decma2c 
 |-  ( ( ; ; 1 0 4 x. ; ; 2 5 0 ) + ( ; ; 1 8 3 + ; 3 1 ) ) = ; ; ; ; 2 6 2 1 4
100 eqid 
 |-  ; 1 0 = ; 1 0
101 3cn 
 |-  3 e. CC
102 101 mulid2i 
 |-  ( 1 x. 3 ) = 3
103 00id 
 |-  ( 0 + 0 ) = 0
104 102 103 oveq12i 
 |-  ( ( 1 x. 3 ) + ( 0 + 0 ) ) = ( 3 + 0 )
105 101 addid1i 
 |-  ( 3 + 0 ) = 3
106 104 105 eqtri 
 |-  ( ( 1 x. 3 ) + ( 0 + 0 ) ) = 3
107 101 mul02i 
 |-  ( 0 x. 3 ) = 0
108 107 oveq1i 
 |-  ( ( 0 x. 3 ) + 1 ) = ( 0 + 1 )
109 108 31 28 3eqtri 
 |-  ( ( 0 x. 3 ) + 1 ) = ; 0 1
110 16 5 5 16 100 28 21 16 5 106 109 decmac 
 |-  ( ( ; 1 0 x. 3 ) + 1 ) = ; 3 1
111 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
112 16 2 2 111 64 decaddi 
 |-  ( ( 4 x. 3 ) + 2 ) = ; 1 4
113 12 13 2 61 21 13 16 110 112 decrmac 
 |-  ( ( ; ; 1 0 4 x. 3 ) + 2 ) = ; ; 3 1 4
114 6 21 22 2 1 46 14 13 47 99 113 decma2c 
 |-  ( ( ; ; 1 0 4 x. N ) + ; ; ; 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 e. NN0
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 e. NN0
122 6p1e7 
 |-  ( 6 + 1 ) = 7
123 121 dec0h 
 |-  7 = ; 0 7
124 122 123 eqtri 
 |-  ( 6 + 1 ) = ; 0 7
125 31 oveq2i 
 |-  ( ( 5 x. 5 ) + ( 0 + 1 ) ) = ( ( 5 x. 5 ) + 1 )
126 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
127 2 3 68 126 decsuc 
 |-  ( ( 5 x. 5 ) + 1 ) = ; 2 6
128 125 127 eqtri 
 |-  ( ( 5 x. 5 ) + ( 0 + 1 ) ) = ; 2 6
129 86 mulid2i 
 |-  ( 1 x. 5 ) = 5
130 129 oveq1i 
 |-  ( ( 1 x. 5 ) + 7 ) = ( 5 + 7 )
131 7cn 
 |-  7 e. CC
132 7p5e12 
 |-  ( 7 + 5 ) = ; 1 2
133 131 86 132 addcomli 
 |-  ( 5 + 7 ) = ; 1 2
134 130 133 eqtri 
 |-  ( ( 1 x. 5 ) + 7 ) = ; 1 2
135 3 16 5 121 117 124 3 2 16 128 134 decmac 
 |-  ( ( ; 5 1 x. 5 ) + ( 6 + 1 ) ) = ; ; 2 6 2
136 86 43 35 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
137 16 5 31 136 decsuc 
 |-  ( ( 2 x. 5 ) + 1 ) = ; 1 1
138 17 2 25 16 115 120 3 16 16 135 137 decmac 
 |-  ( ( ; ; 5 1 2 x. 5 ) + ( ; 1 0 + ; 5 1 ) ) = ; ; ; 2 6 2 1
139 17 nn0cni 
 |-  ; 5 1 e. CC
140 139 mulid1i 
 |-  ( ; 5 1 x. 1 ) = ; 5 1
141 43 mulid1i 
 |-  ( 2 x. 1 ) = 2
142 141 oveq1i 
 |-  ( ( 2 x. 1 ) + 2 ) = ( 2 + 2 )
143 142 64 eqtri 
 |-  ( ( 2 x. 1 ) + 2 ) = 4
144 17 2 2 115 16 140 143 decrmanc 
 |-  ( ( ; ; 5 1 2 x. 1 ) + 2 ) = ; ; 5 1 4
145 3 16 12 2 117 118 18 13 17 138 144 decma2c 
 |-  ( ( ; ; 5 1 2 x. ; 5 1 ) + ; ; 1 0 2 ) = ; ; ; ; 2 6 2 1 4
146 43 mulid2i 
 |-  ( 1 x. 2 ) = 2
147 2 3 16 117 35 146 decmul1 
 |-  ( ; 5 1 x. 2 ) = ; ; 1 0 2
148 2 17 2 115 147 29 decmul1 
 |-  ( ; ; 5 1 2 x. 2 ) = ; ; ; 1 0 2 4
149 18 17 2 115 13 116 145 148 decmul2c 
 |-  ( ; ; 5 1 2 x. ; ; 5 1 2 ) = ; ; ; ; ; 2 6 2 1 4 4
150 114 149 eqtr4i 
 |-  ( ( ; ; 1 0 4 x. N ) + ; ; ; 1 8 3 2 ) = ( ; ; 5 1 2 x. ; ; 5 1 2 )
151 9 10 11 15 18 23 41 45 150 mod2xi 
 |-  ( ( 2 ^ ; 1 8 ) mod N ) = ( ; ; ; 1 8 3 2 mod N )