# Metamath Proof Explorer

## Theorem 1259lem3

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

Ref Expression
Hypothesis 1259prm.1 $⊢ N = 1259$
Assertion 1259lem3 $⊢ 2 76 mod N = 5 mod N$

### Proof

Step Hyp Ref Expression
1 1259prm.1 $⊢ N = 1259$
2 1nn0 $⊢ 1 ∈ ℕ 0$
3 2nn0 $⊢ 2 ∈ ℕ 0$
4 2 3 deccl $⊢ 12 ∈ ℕ 0$
5 5nn0 $⊢ 5 ∈ ℕ 0$
6 4 5 deccl $⊢ 125 ∈ ℕ 0$
7 9nn $⊢ 9 ∈ ℕ$
8 6 7 decnncl $⊢ 1259 ∈ ℕ$
9 1 8 eqeltri $⊢ N ∈ ℕ$
10 2nn $⊢ 2 ∈ ℕ$
11 3nn0 $⊢ 3 ∈ ℕ 0$
12 8nn0 $⊢ 8 ∈ ℕ 0$
13 11 12 deccl $⊢ 38 ∈ ℕ 0$
14 4z $⊢ 4 ∈ ℤ$
15 7nn0 $⊢ 7 ∈ ℕ 0$
16 15 2 deccl $⊢ 71 ∈ ℕ 0$
17 4nn0 $⊢ 4 ∈ ℕ 0$
18 11 17 deccl $⊢ 34 ∈ ℕ 0$
19 2 2 deccl $⊢ 11 ∈ ℕ 0$
20 19 nn0zi $⊢ 11 ∈ ℤ$
21 12 15 deccl $⊢ 87 ∈ ℕ 0$
22 0nn0 $⊢ 0 ∈ ℕ 0$
23 21 22 deccl $⊢ 870 ∈ ℕ 0$
24 6nn0 $⊢ 6 ∈ ℕ 0$
25 2 24 deccl $⊢ 16 ∈ ℕ 0$
26 1 1259lem2 $⊢ 2 34 mod N = 870 mod N$
27 2exp4 $⊢ 2 4 = 16$
28 27 oveq1i $⊢ 2 4 mod N = 16 mod N$
29 eqid $⊢ 34 = 34$
30 4p4e8 $⊢ 4 + 4 = 8$
31 11 17 17 29 30 decaddi $⊢ 34 + 4 = 38$
32 9nn0 $⊢ 9 ∈ ℕ 0$
33 eqid $⊢ 71 = 71$
34 10nn0 $⊢ 10 ∈ ℕ 0$
35 eqid $⊢ 11 = 11$
36 34 nn0cni $⊢ 10 ∈ ℂ$
37 7cn $⊢ 7 ∈ ℂ$
38 dec10p $⊢ 10 + 7 = 17$
39 36 37 38 addcomli $⊢ 7 + 10 = 17$
40 2 11 deccl $⊢ 13 ∈ ℕ 0$
41 6 nn0cni $⊢ 125 ∈ ℂ$
42 41 mulid2i $⊢ 1 ⋅ 125 = 125$
43 2 dec0h $⊢ 1 = 01$
44 eqid $⊢ 13 = 13$
45 0p1e1 $⊢ 0 + 1 = 1$
46 3cn $⊢ 3 ∈ ℂ$
47 ax-1cn $⊢ 1 ∈ ℂ$
48 3p1e4 $⊢ 3 + 1 = 4$
49 46 47 48 addcomli $⊢ 1 + 3 = 4$
50 22 2 2 11 43 44 45 49 decadd $⊢ 1 + 13 = 14$
51 2p1e3 $⊢ 2 + 1 = 3$
52 eqid $⊢ 12 = 12$
53 2 3 51 52 decsuc $⊢ 12 + 1 = 13$
54 5p4e9 $⊢ 5 + 4 = 9$
55 4 5 2 17 42 50 53 54 decadd $⊢ 1 ⋅ 125 + 1 + 13 = 139$
56 5cn $⊢ 5 ∈ ℂ$
57 7p5e12 $⊢ 7 + 5 = 12$
58 37 56 57 addcomli $⊢ 5 + 7 = 12$
59 4 5 15 42 53 3 58 decaddci $⊢ 1 ⋅ 125 + 7 = 132$
60 2 2 2 15 35 39 6 3 40 55 59 decmac $⊢ 11 ⋅ 125 + 7 + 10 = 1392$
61 9p1e10 $⊢ 9 + 1 = 10$
62 9cn $⊢ 9 ∈ ℂ$
63 19 nn0cni $⊢ 11 ∈ ℂ$
64 9t11e99 $⊢ 9 ⋅ 11 = 99$
65 62 63 64 mulcomli $⊢ 11 ⋅ 9 = 99$
66 32 61 65 decsucc $⊢ 11 ⋅ 9 + 1 = 100$
67 6 32 15 2 1 33 19 22 34 60 66 decma2c $⊢ 11 ⋅ N + 71 = 13920$
68 eqid $⊢ 16 = 16$
69 5 3 deccl $⊢ 52 ∈ ℕ 0$
70 69 3 deccl $⊢ 522 ∈ ℕ 0$
71 eqid $⊢ 870 = 870$
72 eqid $⊢ 522 = 522$
73 eqid $⊢ 87 = 87$
74 69 nn0cni $⊢ 52 ∈ ℂ$
75 74 addid1i $⊢ 52 + 0 = 52$
76 8cn $⊢ 8 ∈ ℂ$
77 76 mulid1i $⊢ 8 ⋅ 1 = 8$
78 56 addid1i $⊢ 5 + 0 = 5$
79 77 78 oveq12i $⊢ 8 ⋅ 1 + 5 + 0 = 8 + 5$
80 8p5e13 $⊢ 8 + 5 = 13$
81 79 80 eqtri $⊢ 8 ⋅ 1 + 5 + 0 = 13$
82 37 mulid1i $⊢ 7 ⋅ 1 = 7$
83 82 oveq1i $⊢ 7 ⋅ 1 + 2 = 7 + 2$
84 7p2e9 $⊢ 7 + 2 = 9$
85 32 dec0h $⊢ 9 = 09$
86 83 84 85 3eqtri $⊢ 7 ⋅ 1 + 2 = 09$
87 12 15 5 3 73 75 2 32 22 81 86 decmac $⊢ 87 ⋅ 1 + 52 + 0 = 139$
88 47 mul02i $⊢ 0 ⋅ 1 = 0$
89 88 oveq1i $⊢ 0 ⋅ 1 + 2 = 0 + 2$
90 2cn $⊢ 2 ∈ ℂ$
91 90 addid2i $⊢ 0 + 2 = 2$
92 3 dec0h $⊢ 2 = 02$
93 89 91 92 3eqtri $⊢ 0 ⋅ 1 + 2 = 02$
94 21 22 69 3 71 72 2 3 22 87 93 decmac $⊢ 870 ⋅ 1 + 522 = 1392$
95 8t6e48 $⊢ 8 ⋅ 6 = 48$
96 4p1e5 $⊢ 4 + 1 = 5$
97 8p4e12 $⊢ 8 + 4 = 12$
98 17 12 17 95 96 3 97 decaddci $⊢ 8 ⋅ 6 + 4 = 52$
99 7t6e42 $⊢ 7 ⋅ 6 = 42$
100 24 12 15 73 3 17 98 99 decmul1c $⊢ 87 ⋅ 6 = 522$
101 6cn $⊢ 6 ∈ ℂ$
102 101 mul02i $⊢ 0 ⋅ 6 = 0$
103 24 21 22 71 100 102 decmul1 $⊢ 870 ⋅ 6 = 5220$
104 23 2 24 68 22 70 94 103 decmul2c $⊢ 870 ⋅ 16 = 13920$
105 67 104 eqtr4i $⊢ 11 ⋅ N + 71 = 870 ⋅ 16$
106 9 10 18 20 23 16 17 25 26 28 31 105 modxai $⊢ 2 38 mod N = 71 mod N$
107 eqid $⊢ 38 = 38$
108 3t2e6 $⊢ 3 ⋅ 2 = 6$
109 46 90 108 mulcomli $⊢ 2 ⋅ 3 = 6$
110 109 oveq1i $⊢ 2 ⋅ 3 + 1 = 6 + 1$
111 6p1e7 $⊢ 6 + 1 = 7$
112 110 111 eqtri $⊢ 2 ⋅ 3 + 1 = 7$
113 8t2e16 $⊢ 8 ⋅ 2 = 16$
114 76 90 113 mulcomli $⊢ 2 ⋅ 8 = 16$
115 3 11 12 107 24 2 112 114 decmul2c $⊢ 2 ⋅ 38 = 76$
116 5 dec0h $⊢ 5 = 05$
117 eqid $⊢ 125 = 125$
118 4cn $⊢ 4 ∈ ℂ$
119 118 addid2i $⊢ 0 + 4 = 4$
120 17 dec0h $⊢ 4 = 04$
121 119 120 eqtri $⊢ 0 + 4 = 04$
122 91 92 eqtri $⊢ 0 + 2 = 02$
123 118 mulid1i $⊢ 4 ⋅ 1 = 4$
124 123 45 oveq12i $⊢ 4 ⋅ 1 + 0 + 1 = 4 + 1$
125 124 96 eqtri $⊢ 4 ⋅ 1 + 0 + 1 = 5$
126 4t2e8 $⊢ 4 ⋅ 2 = 8$
127 126 oveq1i $⊢ 4 ⋅ 2 + 2 = 8 + 2$
128 8p2e10 $⊢ 8 + 2 = 10$
129 127 128 eqtri $⊢ 4 ⋅ 2 + 2 = 10$
130 2 3 22 3 52 122 17 22 2 125 129 decma2c $⊢ 4 ⋅ 12 + 0 + 2 = 50$
131 5t4e20 $⊢ 5 ⋅ 4 = 20$
132 56 118 131 mulcomli $⊢ 4 ⋅ 5 = 20$
133 3 22 17 132 119 decaddi $⊢ 4 ⋅ 5 + 4 = 24$
134 4 5 22 17 117 121 17 17 3 130 133 decma2c $⊢ 4 ⋅ 125 + 0 + 4 = 504$
135 9t4e36 $⊢ 9 ⋅ 4 = 36$
136 62 118 135 mulcomli $⊢ 4 ⋅ 9 = 36$
137 6p5e11 $⊢ 6 + 5 = 11$
138 11 24 5 136 48 2 137 decaddci $⊢ 4 ⋅ 9 + 5 = 41$
139 6 32 22 5 1 116 17 2 17 134 138 decma2c $⊢ 4 ⋅ N + 5 = 5041$
140 7t7e49 $⊢ 7 ⋅ 7 = 49$
141 17 96 140 decsucc $⊢ 7 ⋅ 7 + 1 = 50$
142 37 mulid2i $⊢ 1 ⋅ 7 = 7$
143 142 oveq1i $⊢ 1 ⋅ 7 + 7 = 7 + 7$
144 7p7e14 $⊢ 7 + 7 = 14$
145 143 144 eqtri $⊢ 1 ⋅ 7 + 7 = 14$
146 15 2 15 33 15 17 2 141 145 decrmac $⊢ 71 ⋅ 7 + 7 = 504$
147 16 nn0cni $⊢ 71 ∈ ℂ$
148 147 mulid1i $⊢ 71 ⋅ 1 = 71$
149 16 15 2 33 2 15 146 148 decmul2c $⊢ 71 ⋅ 71 = 5041$
150 139 149 eqtr4i $⊢ 4 ⋅ N + 5 = 71 ⋅ 71$
151 9 10 13 14 16 5 106 115 150 mod2xi $⊢ 2 76 mod N = 5 mod N$