Metamath Proof Explorer

Theorem 1259lem1

Description: Lemma for 1259prm . Calculate a power mod. In decimal, we calculate 2 ^ 1 6 = 5 2 N + 6 8 == 6 8 and 2 ^ 1 7 == 6 8 x. 2 = 1 3 6 in this lemma. (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 1259lem1 ( ( 2 ↑ 1 7 ) mod 𝑁 ) = ( 1 3 6 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 6nn0 ⊢ 6 ∈ ℕ0
12 2 11 deccl ⊢ 1 6 ∈ ℕ0
13 0z ⊢ 0 ∈ ℤ
14 8nn0 ⊢ 8 ∈ ℕ0
15 11 14 deccl ⊢ 6 8 ∈ ℕ0
16 3nn0 ⊢ 3 ∈ ℕ0
17 2 16 deccl ⊢ 1 3 ∈ ℕ0
18 17 11 deccl ⊢ 1 3 6 ∈ ℕ0
19 5 3 deccl ⊢ 5 2 ∈ ℕ0
20 19 nn0zi ⊢ 5 2 ∈ ℤ
21 3 14 nn0expcli ⊢ ( 2 ↑ 8 ) ∈ ℕ0
22 eqid ⊢ ( ( 2 ↑ 8 ) mod 𝑁 ) = ( ( 2 ↑ 8 ) mod 𝑁 )
23 14 nn0cni ⊢ 8 ∈ ℂ
24 2cn ⊢ 2 ∈ ℂ
25 8t2e16 ⊢ ( 8 · 2 ) = 1 6
26 23 24 25 mulcomli ⊢ ( 2 · 8 ) = 1 6
27 9nn0 ⊢ 9 ∈ ℕ0
28 eqid ⊢ 6 8 = 6 8
29 4nn0 ⊢ 4 ∈ ℕ0
30 7nn0 ⊢ 7 ∈ ℕ0
31 29 30 deccl ⊢ 4 7 ∈ ℕ0
32 eqid ⊢ 1 2 5 = 1 2 5
33 0nn0 ⊢ 0 ∈ ℕ0
34 11 dec0h ⊢ 6 = 0 6
35 eqid ⊢ 4 7 = 4 7
36 4cn ⊢ 4 ∈ ℂ
37 36 addid2i ⊢ ( 0 + 4 ) = 4
38 37 oveq1i ⊢ ( ( 0 + 4 ) + 1 ) = ( 4 + 1 )
39 4p1e5 ⊢ ( 4 + 1 ) = 5
40 38 39 eqtri ⊢ ( ( 0 + 4 ) + 1 ) = 5
41 7cn ⊢ 7 ∈ ℂ
42 6cn ⊢ 6 ∈ ℂ
43 7p6e13 ⊢ ( 7 + 6 ) = 1 3
44 41 42 43 addcomli ⊢ ( 6 + 7 ) = 1 3
45 33 11 29 30 34 35 40 16 44 decaddc ⊢ ( 6 + 4 7 ) = 5 3
46 3 11 deccl ⊢ 2 6 ∈ ℕ0
47 eqid ⊢ 1 2 = 1 2
48 5 dec0h ⊢ 5 = 0 5
49 eqid ⊢ 2 6 = 2 6
50 24 addid2i ⊢ ( 0 + 2 ) = 2
51 50 oveq1i ⊢ ( ( 0 + 2 ) + 1 ) = ( 2 + 1 )
52 2p1e3 ⊢ ( 2 + 1 ) = 3
53 51 52 eqtri ⊢ ( ( 0 + 2 ) + 1 ) = 3
54 5cn ⊢ 5 ∈ ℂ
55 6p5e11 ⊢ ( 6 + 5 ) = 1 1
56 42 54 55 addcomli ⊢ ( 5 + 6 ) = 1 1
57 33 5 3 11 48 49 53 2 56 decaddc ⊢ ( 5 + 2 6 ) = 3 1
58 10nn0 ⊢ 1 0 ∈ ℕ0
59 eqid ⊢ 5 2 = 5 2
60 58 nn0cni ⊢ 1 0 ∈ ℂ
61 3cn ⊢ 3 ∈ ℂ
62 dec10p ⊢ ( 1 0 + 3 ) = 1 3
63 60 61 62 addcomli ⊢ ( 3 + 1 0 ) = 1 3
64 54 mulid1i ⊢ ( 5 · 1 ) = 5
65 1p0e1 ⊢ ( 1 + 0 ) = 1
66 64 65 oveq12i ⊢ ( ( 5 · 1 ) + ( 1 + 0 ) ) = ( 5 + 1 )
67 5p1e6 ⊢ ( 5 + 1 ) = 6
68 66 67 eqtri ⊢ ( ( 5 · 1 ) + ( 1 + 0 ) ) = 6
69 24 mulid1i ⊢ ( 2 · 1 ) = 2
70 69 oveq1i ⊢ ( ( 2 · 1 ) + 3 ) = ( 2 + 3 )
71 3p2e5 ⊢ ( 3 + 2 ) = 5
72 61 24 71 addcomli ⊢ ( 2 + 3 ) = 5
73 70 72 48 3eqtri ⊢ ( ( 2 · 1 ) + 3 ) = 0 5
74 5 3 2 16 59 63 2 5 33 68 73 decmac ⊢ ( ( 5 2 · 1 ) + ( 3 + 1 0 ) ) = 6 5
75 2 dec0h ⊢ 1 = 0 1
76 5t2e10 ⊢ ( 5 · 2 ) = 1 0
77 00id ⊢ ( 0 + 0 ) = 0
78 76 77 oveq12i ⊢ ( ( 5 · 2 ) + ( 0 + 0 ) ) = ( 1 0 + 0 )
79 dec10p ⊢ ( 1 0 + 0 ) = 1 0
80 78 79 eqtri ⊢ ( ( 5 · 2 ) + ( 0 + 0 ) ) = 1 0
81 2t2e4 ⊢ ( 2 · 2 ) = 4
82 81 oveq1i ⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 )
83 82 39 48 3eqtri ⊢ ( ( 2 · 2 ) + 1 ) = 0 5
84 5 3 33 2 59 75 3 5 33 80 83 decmac ⊢ ( ( 5 2 · 2 ) + 1 ) = 1 0 5
85 2 3 16 2 47 57 19 5 58 74 84 decma2c ⊢ ( ( 5 2 · 1 2 ) + ( 5 + 2 6 ) ) = 6 5 5
86 5t5e25 ⊢ ( 5 · 5 ) = 2 5
87 3 5 67 86 decsuc ⊢ ( ( 5 · 5 ) + 1 ) = 2 6
88 54 24 76 mulcomli ⊢ ( 2 · 5 ) = 1 0
89 61 addid2i ⊢ ( 0 + 3 ) = 3
90 2 33 16 88 89 decaddi ⊢ ( ( 2 · 5 ) + 3 ) = 1 3
91 5 3 16 59 5 16 2 87 90 decrmac ⊢ ( ( 5 2 · 5 ) + 3 ) = 2 6 3
92 4 5 5 16 32 45 19 16 46 85 91 decma2c ⊢ ( ( 5 2 · 1 2 5 ) + ( 6 + 4 7 ) ) = 6 5 5 3
93 9cn ⊢ 9 ∈ ℂ
94 9t5e45 ⊢ ( 9 · 5 ) = 4 5
95 93 54 94 mulcomli ⊢ ( 5 · 9 ) = 4 5
96 5p2e7 ⊢ ( 5 + 2 ) = 7
97 29 5 3 95 96 decaddi ⊢ ( ( 5 · 9 ) + 2 ) = 4 7
98 9t2e18 ⊢ ( 9 · 2 ) = 1 8
99 93 24 98 mulcomli ⊢ ( 2 · 9 ) = 1 8
100 1p1e2 ⊢ ( 1 + 1 ) = 2
101 8p8e16 ⊢ ( 8 + 8 ) = 1 6
102 2 14 14 99 100 11 101 decaddci ⊢ ( ( 2 · 9 ) + 8 ) = 2 6
103 5 3 14 59 27 11 3 97 102 decrmac ⊢ ( ( 5 2 · 9 ) + 8 ) = 4 7 6
104 6 27 11 14 1 28 19 11 31 92 103 decma2c ⊢ ( ( 5 2 · 𝑁 ) + 6 8 ) = 6 5 5 3 6
105 2exp16 ⊢ ( 2 ↑ 1 6 ) = 6 5 5 3 6
106 eqid ⊢ ( 2 ↑ 8 ) = ( 2 ↑ 8 )
107 eqid ⊢ ( ( 2 ↑ 8 ) · ( 2 ↑ 8 ) ) = ( ( 2 ↑ 8 ) · ( 2 ↑ 8 ) )
108 3 14 26 106 107 numexp2x ⊢ ( 2 ↑ 1 6 ) = ( ( 2 ↑ 8 ) · ( 2 ↑ 8 ) )
109 104 105 108 3eqtr2i ⊢ ( ( 5 2 · 𝑁 ) + 6 8 ) = ( ( 2 ↑ 8 ) · ( 2 ↑ 8 ) )
110 9 10 14 20 21 15 22 26 109 mod2xi ⊢ ( ( 2 ↑ 1 6 ) mod 𝑁 ) = ( 6 8 mod 𝑁 )
111 6p1e7 ⊢ ( 6 + 1 ) = 7
112 eqid ⊢ 1 6 = 1 6
113 2 11 111 112 decsuc ⊢ ( 1 6 + 1 ) = 1 7
114 18 nn0cni ⊢ 1 3 6 ∈ ℂ
115 114 addid2i ⊢ ( 0 + 1 3 6 ) = 1 3 6
116 9 nncni ⊢ 𝑁 ∈ ℂ
117 116 mul02i ⊢ ( 0 · 𝑁 ) = 0
118 117 oveq1i ⊢ ( ( 0 · 𝑁 ) + 1 3 6 ) = ( 0 + 1 3 6 )
119 6t2e12 ⊢ ( 6 · 2 ) = 1 2
120 2 3 52 119 decsuc ⊢ ( ( 6 · 2 ) + 1 ) = 1 3
121 3 11 14 28 11 2 120 25 decmul1c ⊢ ( 6 8 · 2 ) = 1 3 6
122 115 118 121 3eqtr4i ⊢ ( ( 0 · 𝑁 ) + 1 3 6 ) = ( 6 8 · 2 )
123 9 10 12 13 15 18 110 113 122 modxp1i ⊢ ( ( 2 ↑ 1 7 ) mod 𝑁 ) = ( 1 3 6 mod 𝑁 )