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 ⊢ 𝑁 = 1 2 5 9
Assertion 1259lem2 ( ( 2 ↑ 3 4 ) mod 𝑁 ) = ( 8 7 0 mod 𝑁 )

Proof

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