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 ⊢ 𝑁 = 1 2 5 9
Assertion 1259lem3 ( ( 2 ↑ 7 6 ) mod 𝑁 ) = ( 5 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 3nn0 ⊢ 3 ∈ ℕ0
12 8nn0 ⊢ 8 ∈ ℕ0
13 11 12 deccl ⊢ 3 8 ∈ ℕ0
14 4z ⊢ 4 ∈ ℤ
15 7nn0 ⊢ 7 ∈ ℕ0
16 15 2 deccl ⊢ 7 1 ∈ ℕ0
17 4nn0 ⊢ 4 ∈ ℕ0
18 11 17 deccl ⊢ 3 4 ∈ ℕ0
19 2 2 deccl ⊢ 1 1 ∈ ℕ0
20 19 nn0zi ⊢ 1 1 ∈ ℤ
21 12 15 deccl ⊢ 8 7 ∈ ℕ0
22 0nn0 ⊢ 0 ∈ ℕ0
23 21 22 deccl ⊢ 8 7 0 ∈ ℕ0
24 6nn0 ⊢ 6 ∈ ℕ0
25 2 24 deccl ⊢ 1 6 ∈ ℕ0
26 1 1259lem2 ⊢ ( ( 2 ↑ 3 4 ) mod 𝑁 ) = ( 8 7 0 mod 𝑁 )
27 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
28 27 oveq1i ⊢ ( ( 2 ↑ 4 ) mod 𝑁 ) = ( 1 6 mod 𝑁 )
29 eqid ⊢ 3 4 = 3 4
30 4p4e8 ⊢ ( 4 + 4 ) = 8
31 11 17 17 29 30 decaddi ⊢ ( 3 4 + 4 ) = 3 8
32 9nn0 ⊢ 9 ∈ ℕ0
33 eqid ⊢ 7 1 = 7 1
34 10nn0 ⊢ 1 0 ∈ ℕ0
35 eqid ⊢ 1 1 = 1 1
36 34 nn0cni ⊢ 1 0 ∈ ℂ
37 7cn ⊢ 7 ∈ ℂ
38 dec10p ⊢ ( 1 0 + 7 ) = 1 7
39 36 37 38 addcomli ⊢ ( 7 + 1 0 ) = 1 7
40 2 11 deccl ⊢ 1 3 ∈ ℕ0
41 6 nn0cni ⊢ 1 2 5 ∈ ℂ
42 41 mullidi ⊢ ( 1 · 1 2 5 ) = 1 2 5
43 2 dec0h ⊢ 1 = 0 1
44 eqid ⊢ 1 3 = 1 3
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 + 1 3 ) = 1 4
51 2p1e3 ⊢ ( 2 + 1 ) = 3
52 eqid ⊢ 1 2 = 1 2
53 2 3 51 52 decsuc ⊢ ( 1 2 + 1 ) = 1 3
54 5p4e9 ⊢ ( 5 + 4 ) = 9
55 4 5 2 17 42 50 53 54 decadd ⊢ ( ( 1 · 1 2 5 ) + ( 1 + 1 3 ) ) = 1 3 9
56 5cn ⊢ 5 ∈ ℂ
57 7p5e12 ⊢ ( 7 + 5 ) = 1 2
58 37 56 57 addcomli ⊢ ( 5 + 7 ) = 1 2
59 4 5 15 42 53 3 58 decaddci ⊢ ( ( 1 · 1 2 5 ) + 7 ) = 1 3 2
60 2 2 2 15 35 39 6 3 40 55 59 decmac ⊢ ( ( 1 1 · 1 2 5 ) + ( 7 + 1 0 ) ) = 1 3 9 2
61 9p1e10 ⊢ ( 9 + 1 ) = 1 0
62 9cn ⊢ 9 ∈ ℂ
63 19 nn0cni ⊢ 1 1 ∈ ℂ
64 9t11e99 ⊢ ( 9 · 1 1 ) = 9 9
65 62 63 64 mulcomli ⊢ ( 1 1 · 9 ) = 9 9
66 32 61 65 decsucc ⊢ ( ( 1 1 · 9 ) + 1 ) = 1 0 0
67 6 32 15 2 1 33 19 22 34 60 66 decma2c ⊢ ( ( 1 1 · 𝑁 ) + 7 1 ) = 1 3 9 2 0
68 eqid ⊢ 1 6 = 1 6
69 5 3 deccl ⊢ 5 2 ∈ ℕ0
70 69 3 deccl ⊢ 5 2 2 ∈ ℕ0
71 eqid ⊢ 8 7 0 = 8 7 0
72 eqid ⊢ 5 2 2 = 5 2 2
73 eqid ⊢ 8 7 = 8 7
74 69 nn0cni ⊢ 5 2 ∈ ℂ
75 74 addridi ⊢ ( 5 2 + 0 ) = 5 2
76 8cn ⊢ 8 ∈ ℂ
77 76 mulridi ⊢ ( 8 · 1 ) = 8
78 56 addridi ⊢ ( 5 + 0 ) = 5
79 77 78 oveq12i ⊢ ( ( 8 · 1 ) + ( 5 + 0 ) ) = ( 8 + 5 )
80 8p5e13 ⊢ ( 8 + 5 ) = 1 3
81 79 80 eqtri ⊢ ( ( 8 · 1 ) + ( 5 + 0 ) ) = 1 3
82 37 mulridi ⊢ ( 7 · 1 ) = 7
83 82 oveq1i ⊢ ( ( 7 · 1 ) + 2 ) = ( 7 + 2 )
84 7p2e9 ⊢ ( 7 + 2 ) = 9
85 32 dec0h ⊢ 9 = 0 9
86 83 84 85 3eqtri ⊢ ( ( 7 · 1 ) + 2 ) = 0 9
87 12 15 5 3 73 75 2 32 22 81 86 decmac ⊢ ( ( 8 7 · 1 ) + ( 5 2 + 0 ) ) = 1 3 9
88 47 mul02i ⊢ ( 0 · 1 ) = 0
89 88 oveq1i ⊢ ( ( 0 · 1 ) + 2 ) = ( 0 + 2 )
90 2cn ⊢ 2 ∈ ℂ
91 90 addlidi ⊢ ( 0 + 2 ) = 2
92 3 dec0h ⊢ 2 = 0 2
93 89 91 92 3eqtri ⊢ ( ( 0 · 1 ) + 2 ) = 0 2
94 21 22 69 3 71 72 2 3 22 87 93 decmac ⊢ ( ( 8 7 0 · 1 ) + 5 2 2 ) = 1 3 9 2
95 8t6e48 ⊢ ( 8 · 6 ) = 4 8
96 4p1e5 ⊢ ( 4 + 1 ) = 5
97 8p4e12 ⊢ ( 8 + 4 ) = 1 2
98 17 12 17 95 96 3 97 decaddci ⊢ ( ( 8 · 6 ) + 4 ) = 5 2
99 7t6e42 ⊢ ( 7 · 6 ) = 4 2
100 24 12 15 73 3 17 98 99 decmul1c ⊢ ( 8 7 · 6 ) = 5 2 2
101 6cn ⊢ 6 ∈ ℂ
102 101 mul02i ⊢ ( 0 · 6 ) = 0
103 24 21 22 71 100 102 decmul1 ⊢ ( 8 7 0 · 6 ) = 5 2 2 0
104 23 2 24 68 22 70 94 103 decmul2c ⊢ ( 8 7 0 · 1 6 ) = 1 3 9 2 0
105 67 104 eqtr4i ⊢ ( ( 1 1 · 𝑁 ) + 7 1 ) = ( 8 7 0 · 1 6 )
106 9 10 18 20 23 16 17 25 26 28 31 105 modxai ⊢ ( ( 2 ↑ 3 8 ) mod 𝑁 ) = ( 7 1 mod 𝑁 )
107 eqid ⊢ 3 8 = 3 8
108 2t3e6 ⊢ ( 2 · 3 ) = 6
109 108 oveq1i ⊢ ( ( 2 · 3 ) + 1 ) = ( 6 + 1 )
110 6p1e7 ⊢ ( 6 + 1 ) = 7
111 109 110 eqtri ⊢ ( ( 2 · 3 ) + 1 ) = 7
112 8t2e16 ⊢ ( 8 · 2 ) = 1 6
113 76 90 112 mulcomli ⊢ ( 2 · 8 ) = 1 6
114 3 11 12 107 24 2 111 113 decmul2c ⊢ ( 2 · 3 8 ) = 7 6
115 5 dec0h ⊢ 5 = 0 5
116 eqid ⊢ 1 2 5 = 1 2 5
117 4cn ⊢ 4 ∈ ℂ
118 117 addlidi ⊢ ( 0 + 4 ) = 4
119 17 dec0h ⊢ 4 = 0 4
120 118 119 eqtri ⊢ ( 0 + 4 ) = 0 4
121 91 92 eqtri ⊢ ( 0 + 2 ) = 0 2
122 117 mulridi ⊢ ( 4 · 1 ) = 4
123 122 45 oveq12i ⊢ ( ( 4 · 1 ) + ( 0 + 1 ) ) = ( 4 + 1 )
124 123 96 eqtri ⊢ ( ( 4 · 1 ) + ( 0 + 1 ) ) = 5
125 4t2e8 ⊢ ( 4 · 2 ) = 8
126 125 oveq1i ⊢ ( ( 4 · 2 ) + 2 ) = ( 8 + 2 )
127 8p2e10 ⊢ ( 8 + 2 ) = 1 0
128 126 127 eqtri ⊢ ( ( 4 · 2 ) + 2 ) = 1 0
129 2 3 22 3 52 121 17 22 2 124 128 decma2c ⊢ ( ( 4 · 1 2 ) + ( 0 + 2 ) ) = 5 0
130 5t4e20 ⊢ ( 5 · 4 ) = 2 0
131 56 117 130 mulcomli ⊢ ( 4 · 5 ) = 2 0
132 3 22 17 131 118 decaddi ⊢ ( ( 4 · 5 ) + 4 ) = 2 4
133 4 5 22 17 116 120 17 17 3 129 132 decma2c ⊢ ( ( 4 · 1 2 5 ) + ( 0 + 4 ) ) = 5 0 4
134 9t4e36 ⊢ ( 9 · 4 ) = 3 6
135 62 117 134 mulcomli ⊢ ( 4 · 9 ) = 3 6
136 6p5e11 ⊢ ( 6 + 5 ) = 1 1
137 11 24 5 135 48 2 136 decaddci ⊢ ( ( 4 · 9 ) + 5 ) = 4 1
138 6 32 22 5 1 115 17 2 17 133 137 decma2c ⊢ ( ( 4 · 𝑁 ) + 5 ) = 5 0 4 1
139 7t7e49 ⊢ ( 7 · 7 ) = 4 9
140 17 96 139 decsucc ⊢ ( ( 7 · 7 ) + 1 ) = 5 0
141 37 mullidi ⊢ ( 1 · 7 ) = 7
142 141 oveq1i ⊢ ( ( 1 · 7 ) + 7 ) = ( 7 + 7 )
143 7p7e14 ⊢ ( 7 + 7 ) = 1 4
144 142 143 eqtri ⊢ ( ( 1 · 7 ) + 7 ) = 1 4
145 15 2 15 33 15 17 2 140 144 decrmac ⊢ ( ( 7 1 · 7 ) + 7 ) = 5 0 4
146 16 nn0cni ⊢ 7 1 ∈ ℂ
147 146 mulridi ⊢ ( 7 1 · 1 ) = 7 1
148 16 15 2 33 2 15 145 147 decmul2c ⊢ ( 7 1 · 7 1 ) = 5 0 4 1
149 138 148 eqtr4i ⊢ ( ( 4 · 𝑁 ) + 5 ) = ( 7 1 · 7 1 )
150 9 10 13 14 16 5 106 114 149 mod2xi ⊢ ( ( 2 ↑ 7 6 ) mod 𝑁 ) = ( 5 mod 𝑁 )