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 12nn0 ⊢ 1 2 ∈ ℕ0
3 5nn0 ⊢ 5 ∈ ℕ0
4 2 3 deccl ⊢ 1 2 5 ∈ ℕ0
5 9nn ⊢ 9 ∈ ℕ
6 4 5 decnncl ⊢ 1 2 5 9 ∈ ℕ
7 1 6 eqeltri ⊢ 𝑁 ∈ ℕ
8 2nn ⊢ 2 ∈ ℕ
9 1nn0 ⊢ 1 ∈ ℕ0
10 7nn0 ⊢ 7 ∈ ℕ0
11 9 10 deccl ⊢ 1 7 ∈ ℕ0
12 4nn0 ⊢ 4 ∈ ℕ0
13 9 12 deccl ⊢ 1 4 ∈ ℕ0
14 13 nn0zi ⊢ 1 4 ∈ ℤ
15 3nn0 ⊢ 3 ∈ ℕ0
16 9 15 deccl ⊢ 1 3 ∈ ℕ0
17 6nn0 ⊢ 6 ∈ ℕ0
18 16 17 deccl ⊢ 1 3 6 ∈ ℕ0
19 8nn0 ⊢ 8 ∈ ℕ0
20 19 10 deccl ⊢ 8 7 ∈ ℕ0
21 0nn0 ⊢ 0 ∈ ℕ0
22 20 21 deccl ⊢ 8 7 0 ∈ ℕ0
23 1 1259lem1 ⊢ ( ( 2 ↑ 1 7 ) mod 𝑁 ) = ( 1 3 6 mod 𝑁 )
24 2nn0 ⊢ 2 ∈ ℕ0
25 eqid ⊢ 1 7 = 1 7
26 2cn ⊢ 2 ∈ ℂ
27 26 mulridi ⊢ ( 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 24 9 10 25 12 9 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 19 10 9 24 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 12 dec0h ⊢ 4 = 0 4
50 48 49 eqtri ⊢ ( 1 + 3 ) = 0 4
51 46 mulridi ⊢ ( 1 · 1 ) = 1
52 00id ⊢ ( 0 + 0 ) = 0
53 51 52 oveq12i ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
54 46 addridi ⊢ ( 1 + 0 ) = 1
55 53 54 eqtri ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = 1
56 4cn ⊢ 4 ∈ ℂ
57 56 mulridi ⊢ ( 4 · 1 ) = 4
58 57 oveq1i ⊢ ( ( 4 · 1 ) + 4 ) = ( 4 + 4 )
59 4p4e8 ⊢ ( 4 + 4 ) = 8
60 19 dec0h ⊢ 8 = 0 8
61 58 59 60 3eqtri ⊢ ( ( 4 · 1 ) + 4 ) = 0 8
62 9 12 21 12 44 50 9 19 21 55 61 decmac ⊢ ( ( 1 4 · 1 ) + ( 1 + 3 ) ) = 1 8
63 17 dec0h ⊢ 6 = 0 6
64 26 mullidi ⊢ ( 1 · 2 ) = 2
65 46 addlidi ⊢ ( 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 9 12 21 17 44 63 24 12 9 67 71 decmac ⊢ ( ( 1 4 · 2 ) + 6 ) = 3 4
73 9 24 9 17 39 43 13 12 15 62 72 decma2c ⊢ ( ( 1 4 · 1 2 ) + ( 9 + 7 ) ) = 1 8 4
74 35 dec0h ⊢ 9 = 0 9
75 5cn ⊢ 5 ∈ ℂ
76 75 mullidi ⊢ ( 1 · 5 ) = 5
77 26 addlidi ⊢ ( 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 addlidi ⊢ ( 0 + 9 ) = 9
85 24 21 35 82 84 decaddi ⊢ ( ( 4 · 5 ) + 9 ) = 2 9
86 9 12 21 35 44 74 3 35 24 80 85 decmac ⊢ ( ( 1 4 · 5 ) + 9 ) = 7 9
87 2 3 35 35 37 42 13 35 10 73 86 decma2c ⊢ ( ( 1 4 · 1 2 5 ) + ( 8 7 + 1 2 ) ) = 1 8 4 9
88 83 mullidi ⊢ ( 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 9 12 44 17 15 91 93 decmul1c ⊢ ( 1 4 · 9 ) = 1 2 6
95 94 oveq1i ⊢ ( ( 1 4 · 9 ) + 0 ) = ( 1 2 6 + 0 )
96 2 17 deccl ⊢ 1 2 6 ∈ ℕ0
97 96 nn0cni ⊢ 1 2 6 ∈ ℂ
98 97 addridi ⊢ ( 1 2 6 + 0 ) = 1 2 6
99 95 98 eqtri ⊢ ( ( 1 4 · 9 ) + 0 ) = 1 2 6
100 4 35 20 21 1 36 13 17 2 87 99 decma2c ⊢ ( ( 1 4 · 𝑁 ) + 8 7 0 ) = 1 8 4 9 6
101 eqid ⊢ 1 3 6 = 1 3 6
102 19 9 deccl ⊢ 8 1 ∈ ℕ0
103 eqid ⊢ 1 3 = 1 3
104 eqid ⊢ 8 1 = 8 1
105 12 21 deccl ⊢ 4 0 ∈ ℕ0
106 eqid ⊢ 4 0 = 4 0
107 56 addlidi ⊢ ( 0 + 4 ) = 4
108 8cn ⊢ 8 ∈ ℂ
109 108 addridi ⊢ ( 8 + 0 ) = 8
110 21 19 12 21 60 106 107 109 decadd ⊢ ( 8 + 4 0 ) = 4 8
111 4p1e5 ⊢ ( 4 + 1 ) = 5
112 3 dec0h ⊢ 5 = 0 5
113 111 112 eqtri ⊢ ( 4 + 1 ) = 0 5
114 45 mulridi ⊢ ( 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 9 15 21 3 103 113 9 19 21 55 118 decmac ⊢ ( ( 1 3 · 1 ) + ( 4 + 1 ) ) = 1 8
120 6cn ⊢ 6 ∈ ℂ
121 120 mulridi ⊢ ( 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 16 17 12 19 101 110 9 12 9 119 124 decmac ⊢ ( ( 1 3 6 · 1 ) + ( 8 + 4 0 ) ) = 1 8 4
126 9 dec0h ⊢ 1 = 0 1
127 65 126 eqtri ⊢ ( 0 + 1 ) = 0 1
128 45 mullidi ⊢ ( 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 9 15 21 9 103 127 15 21 9 130 134 decmac ⊢ ( ( 1 3 · 3 ) + ( 0 + 1 ) ) = 4 0
136 6t3e18 ⊢ ( 6 · 3 ) = 1 8
137 9 19 9 136 40 decaddi ⊢ ( ( 6 · 3 ) + 1 ) = 1 9
138 16 17 21 9 101 126 15 35 9 135 137 decmac ⊢ ( ( 1 3 6 · 3 ) + 1 ) = 4 0 9
139 9 15 19 9 103 104 18 35 105 125 138 decma2c ⊢ ( ( 1 3 6 · 1 3 ) + 8 1 ) = 1 8 4 9
140 15 dec0h ⊢ 3 = 0 3
141 120 mullidi ⊢ ( 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 9 19 15 145 146 9 147 decaddci ⊢ ( ( 3 · 6 ) + 3 ) = 2 1
149 9 15 21 15 103 140 17 9 24 144 148 decmac ⊢ ( ( 1 3 · 6 ) + 3 ) = 8 1
150 6t6e36 ⊢ ( 6 · 6 ) = 3 6
151 17 16 17 101 17 15 149 150 decmul1c ⊢ ( 1 3 6 · 6 ) = 8 1 6
152 18 16 17 101 17 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 7 8 11 14 18 22 23 34 153 mod2xi ⊢ ( ( 2 ↑ 3 4 ) mod 𝑁 ) = ( 8 7 0 mod 𝑁 )