Metamath Proof Explorer

Theorem 1259lem2

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

Ref Expression
Hypothesis 1259prm.1 
|- N = ; ; ; 1 2 5 9
Assertion 1259lem2 
|- ( ( 2 ^ ; 3 4 ) mod N ) = ( ; ; 8 7 0 mod N )

Proof

Step Hyp Ref Expression
1 1259prm.1 
 |-  N = ; ; ; 1 2 5 9
2 1nn0 
 |-  1 e. NN0
3 2nn0 
 |-  2 e. NN0
4 2 3 deccl 
 |-  ; 1 2 e. NN0
5 5nn0 
 |-  5 e. NN0
6 4 5 deccl 
 |-  ; ; 1 2 5 e. NN0
7 9nn 
 |-  9 e. NN
8 6 7 decnncl 
 |-  ; ; ; 1 2 5 9 e. NN
9 1 8 eqeltri 
 |-  N e. NN
10 2nn 
 |-  2 e. NN
11 7nn0 
 |-  7 e. NN0
12 2 11 deccl 
 |-  ; 1 7 e. NN0
13 4nn0 
 |-  4 e. NN0
14 2 13 deccl 
 |-  ; 1 4 e. NN0
15 14 nn0zi 
 |-  ; 1 4 e. ZZ
16 3nn0 
 |-  3 e. NN0
17 2 16 deccl 
 |-  ; 1 3 e. NN0
18 6nn0 
 |-  6 e. NN0
19 17 18 deccl 
 |-  ; ; 1 3 6 e. NN0
20 8nn0 
 |-  8 e. NN0
21 20 11 deccl 
 |-  ; 8 7 e. NN0
22 0nn0 
 |-  0 e. NN0
23 21 22 deccl 
 |-  ; ; 8 7 0 e. NN0
24 1 1259lem1 
 |-  ( ( 2 ^ ; 1 7 ) mod N ) = ( ; ; 1 3 6 mod N )
25 eqid 
 |-  ; 1 7 = ; 1 7
26 2cn 
 |-  2 e. CC
27 26 mulridi 
 |-  ( 2 x. 1 ) = 2
28 27 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
29 2p1e3 
 |-  ( 2 + 1 ) = 3
30 28 29 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
31 7cn 
 |-  7 e. CC
32 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
33 31 26 32 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
34 3 2 11 25 13 2 30 33 decmul2c 
 |-  ( 2 x. ; 1 7 ) = ; 3 4
35 9nn0 
 |-  9 e. NN0
36 eqid 
 |-  ; ; 8 7 0 = ; ; 8 7 0
37 eqid 
 |-  ; ; 1 2 5 = ; ; 1 2 5
38 eqid 
 |-  ; 8 7 = ; 8 7
39 eqid 
 |-  ; 1 2 = ; 1 2
40 8p1e9 
 |-  ( 8 + 1 ) = 9
41 7p2e9 
 |-  ( 7 + 2 ) = 9
42 20 11 2 3 38 39 40 41 decadd 
 |-  ( ; 8 7 + ; 1 2 ) = ; 9 9
43 9p7e16 
 |-  ( 9 + 7 ) = ; 1 6
44 eqid 
 |-  ; 1 4 = ; 1 4
45 3cn 
 |-  3 e. CC
46 ax-1cn 
 |-  1 e. CC
47 3p1e4 
 |-  ( 3 + 1 ) = 4
48 45 46 47 addcomli 
 |-  ( 1 + 3 ) = 4
49 13 dec0h 
 |-  4 = ; 0 4
50 48 49 eqtri 
 |-  ( 1 + 3 ) = ; 0 4
51 46 mulridi 
 |-  ( 1 x. 1 ) = 1
52 00id 
 |-  ( 0 + 0 ) = 0
53 51 52 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
54 46 addridi 
 |-  ( 1 + 0 ) = 1
55 53 54 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
56 4cn 
 |-  4 e. CC
57 56 mulridi 
 |-  ( 4 x. 1 ) = 4
58 57 oveq1i 
 |-  ( ( 4 x. 1 ) + 4 ) = ( 4 + 4 )
59 4p4e8 
 |-  ( 4 + 4 ) = 8
60 20 dec0h 
 |-  8 = ; 0 8
61 58 59 60 3eqtri 
 |-  ( ( 4 x. 1 ) + 4 ) = ; 0 8
62 2 13 22 13 44 50 2 20 22 55 61 decmac 
 |-  ( ( ; 1 4 x. 1 ) + ( 1 + 3 ) ) = ; 1 8
63 18 dec0h 
 |-  6 = ; 0 6
64 26 mullidi 
 |-  ( 1 x. 2 ) = 2
65 46 addlidi 
 |-  ( 0 + 1 ) = 1
66 64 65 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
67 66 29 eqtri 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = 3
68 4t2e8 
 |-  ( 4 x. 2 ) = 8
69 68 oveq1i 
 |-  ( ( 4 x. 2 ) + 6 ) = ( 8 + 6 )
70 8p6e14 
 |-  ( 8 + 6 ) = ; 1 4
71 69 70 eqtri 
 |-  ( ( 4 x. 2 ) + 6 ) = ; 1 4
72 2 13 22 18 44 63 3 13 2 67 71 decmac 
 |-  ( ( ; 1 4 x. 2 ) + 6 ) = ; 3 4
73 2 3 2 18 39 43 14 13 16 62 72 decma2c 
 |-  ( ( ; 1 4 x. ; 1 2 ) + ( 9 + 7 ) ) = ; ; 1 8 4
74 35 dec0h 
 |-  9 = ; 0 9
75 5cn 
 |-  5 e. CC
76 75 mullidi 
 |-  ( 1 x. 5 ) = 5
77 26 addlidi 
 |-  ( 0 + 2 ) = 2
78 76 77 oveq12i 
 |-  ( ( 1 x. 5 ) + ( 0 + 2 ) ) = ( 5 + 2 )
79 5p2e7 
 |-  ( 5 + 2 ) = 7
80 78 79 eqtri 
 |-  ( ( 1 x. 5 ) + ( 0 + 2 ) ) = 7
81 5t4e20 
 |-  ( 5 x. 4 ) = ; 2 0
82 75 56 81 mulcomli 
 |-  ( 4 x. 5 ) = ; 2 0
83 9cn 
 |-  9 e. CC
84 83 addlidi 
 |-  ( 0 + 9 ) = 9
85 3 22 35 82 84 decaddi 
 |-  ( ( 4 x. 5 ) + 9 ) = ; 2 9
86 2 13 22 35 44 74 5 35 3 80 85 decmac 
 |-  ( ( ; 1 4 x. 5 ) + 9 ) = ; 7 9
87 4 5 35 35 37 42 14 35 11 73 86 decma2c 
 |-  ( ( ; 1 4 x. ; ; 1 2 5 ) + ( ; 8 7 + ; 1 2 ) ) = ; ; ; 1 8 4 9
88 83 mullidi 
 |-  ( 1 x. 9 ) = 9
89 88 oveq1i 
 |-  ( ( 1 x. 9 ) + 3 ) = ( 9 + 3 )
90 9p3e12 
 |-  ( 9 + 3 ) = ; 1 2
91 89 90 eqtri 
 |-  ( ( 1 x. 9 ) + 3 ) = ; 1 2
92 9t4e36 
 |-  ( 9 x. 4 ) = ; 3 6
93 83 56 92 mulcomli 
 |-  ( 4 x. 9 ) = ; 3 6
94 35 2 13 44 18 16 91 93 decmul1c 
 |-  ( ; 1 4 x. 9 ) = ; ; 1 2 6
95 94 oveq1i 
 |-  ( ( ; 1 4 x. 9 ) + 0 ) = ( ; ; 1 2 6 + 0 )
96 4 18 deccl 
 |-  ; ; 1 2 6 e. NN0
97 96 nn0cni 
 |-  ; ; 1 2 6 e. CC
98 97 addridi 
 |-  ( ; ; 1 2 6 + 0 ) = ; ; 1 2 6
99 95 98 eqtri 
 |-  ( ( ; 1 4 x. 9 ) + 0 ) = ; ; 1 2 6
100 6 35 21 22 1 36 14 18 4 87 99 decma2c 
 |-  ( ( ; 1 4 x. N ) + ; ; 8 7 0 ) = ; ; ; ; 1 8 4 9 6
101 eqid 
 |-  ; ; 1 3 6 = ; ; 1 3 6
102 20 2 deccl 
 |-  ; 8 1 e. NN0
103 eqid 
 |-  ; 1 3 = ; 1 3
104 eqid 
 |-  ; 8 1 = ; 8 1
105 13 22 deccl 
 |-  ; 4 0 e. NN0
106 eqid 
 |-  ; 4 0 = ; 4 0
107 56 addlidi 
 |-  ( 0 + 4 ) = 4
108 8cn 
 |-  8 e. CC
109 108 addridi 
 |-  ( 8 + 0 ) = 8
110 22 20 13 22 60 106 107 109 decadd 
 |-  ( 8 + ; 4 0 ) = ; 4 8
111 4p1e5 
 |-  ( 4 + 1 ) = 5
112 5 dec0h 
 |-  5 = ; 0 5
113 111 112 eqtri 
 |-  ( 4 + 1 ) = ; 0 5
114 45 mulridi 
 |-  ( 3 x. 1 ) = 3
115 114 oveq1i 
 |-  ( ( 3 x. 1 ) + 5 ) = ( 3 + 5 )
116 5p3e8 
 |-  ( 5 + 3 ) = 8
117 75 45 116 addcomli 
 |-  ( 3 + 5 ) = 8
118 115 117 60 3eqtri 
 |-  ( ( 3 x. 1 ) + 5 ) = ; 0 8
119 2 16 22 5 103 113 2 20 22 55 118 decmac 
 |-  ( ( ; 1 3 x. 1 ) + ( 4 + 1 ) ) = ; 1 8
120 6cn 
 |-  6 e. CC
121 120 mulridi 
 |-  ( 6 x. 1 ) = 6
122 121 oveq1i 
 |-  ( ( 6 x. 1 ) + 8 ) = ( 6 + 8 )
123 108 120 70 addcomli 
 |-  ( 6 + 8 ) = ; 1 4
124 122 123 eqtri 
 |-  ( ( 6 x. 1 ) + 8 ) = ; 1 4
125 17 18 13 20 101 110 2 13 2 119 124 decmac 
 |-  ( ( ; ; 1 3 6 x. 1 ) + ( 8 + ; 4 0 ) ) = ; ; 1 8 4
126 2 dec0h 
 |-  1 = ; 0 1
127 65 126 eqtri 
 |-  ( 0 + 1 ) = ; 0 1
128 45 mullidi 
 |-  ( 1 x. 3 ) = 3
129 128 65 oveq12i 
 |-  ( ( 1 x. 3 ) + ( 0 + 1 ) ) = ( 3 + 1 )
130 129 47 eqtri 
 |-  ( ( 1 x. 3 ) + ( 0 + 1 ) ) = 4
131 3t3e9 
 |-  ( 3 x. 3 ) = 9
132 131 oveq1i 
 |-  ( ( 3 x. 3 ) + 1 ) = ( 9 + 1 )
133 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
134 132 133 eqtri 
 |-  ( ( 3 x. 3 ) + 1 ) = ; 1 0
135 2 16 22 2 103 127 16 22 2 130 134 decmac 
 |-  ( ( ; 1 3 x. 3 ) + ( 0 + 1 ) ) = ; 4 0
136 6t3e18 
 |-  ( 6 x. 3 ) = ; 1 8
137 2 20 2 136 40 decaddi 
 |-  ( ( 6 x. 3 ) + 1 ) = ; 1 9
138 17 18 22 2 101 126 16 35 2 135 137 decmac 
 |-  ( ( ; ; 1 3 6 x. 3 ) + 1 ) = ; ; 4 0 9
139 2 16 20 2 103 104 19 35 105 125 138 decma2c 
 |-  ( ( ; ; 1 3 6 x. ; 1 3 ) + ; 8 1 ) = ; ; ; 1 8 4 9
140 16 dec0h 
 |-  3 = ; 0 3
141 120 mullidi 
 |-  ( 1 x. 6 ) = 6
142 141 77 oveq12i 
 |-  ( ( 1 x. 6 ) + ( 0 + 2 ) ) = ( 6 + 2 )
143 6p2e8 
 |-  ( 6 + 2 ) = 8
144 142 143 eqtri 
 |-  ( ( 1 x. 6 ) + ( 0 + 2 ) ) = 8
145 120 45 136 mulcomli 
 |-  ( 3 x. 6 ) = ; 1 8
146 1p1e2 
 |-  ( 1 + 1 ) = 2
147 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
148 2 20 16 145 146 2 147 decaddci 
 |-  ( ( 3 x. 6 ) + 3 ) = ; 2 1
149 2 16 22 16 103 140 18 2 3 144 148 decmac 
 |-  ( ( ; 1 3 x. 6 ) + 3 ) = ; 8 1
150 6t6e36 
 |-  ( 6 x. 6 ) = ; 3 6
151 18 17 18 101 18 16 149 150 decmul1c 
 |-  ( ; ; 1 3 6 x. 6 ) = ; ; 8 1 6
152 19 17 18 101 18 102 139 151 decmul2c 
 |-  ( ; ; 1 3 6 x. ; ; 1 3 6 ) = ; ; ; ; 1 8 4 9 6
153 100 152 eqtr4i 
 |-  ( ( ; 1 4 x. N ) + ; ; 8 7 0 ) = ( ; ; 1 3 6 x. ; ; 1 3 6 )
154 9 10 12 15 19 23 24 34 153 mod2xi 
 |-  ( ( 2 ^ ; 3 4 ) mod N ) = ( ; ; 8 7 0 mod N )