Metamath Proof Explorer

Theorem 4001lem3

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

Ref Expression
Hypothesis 4001prm.1 ⊢ 𝑁 = 4 0 0 1
Assertion 4001lem3 ( ( 2 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 )

Proof

Step Hyp Ref Expression
1 4001prm.1 ⊢ 𝑁 = 4 0 0 1
2 4nn0 ⊢ 4 ∈ ℕ0
3 0nn0 ⊢ 0 ∈ ℕ0
4 2 3 deccl ⊢ 4 0 ∈ ℕ0
5 4 3 deccl ⊢ 4 0 0 ∈ ℕ0
6 1nn ⊢ 1 ∈ ℕ
7 5 6 decnncl ⊢ 4 0 0 1 ∈ ℕ
8 1 7 eqeltri ⊢ 𝑁 ∈ ℕ
9 2nn ⊢ 2 ∈ ℕ
10 2nn0 ⊢ 2 ∈ ℕ0
11 10 3 deccl ⊢ 2 0 ∈ ℕ0
12 11 3 deccl ⊢ 2 0 0 ∈ ℕ0
13 12 3 deccl ⊢ 2 0 0 0 ∈ ℕ0
14 0z ⊢ 0 ∈ ℤ
15 1nn0 ⊢ 1 ∈ ℕ0
16 10nn0 ⊢ 1 0 ∈ ℕ0
17 16 3 deccl ⊢ 1 0 0 ∈ ℕ0
18 17 3 deccl ⊢ 1 0 0 0 ∈ ℕ0
19 8nn0 ⊢ 8 ∈ ℕ0
20 19 3 deccl ⊢ 8 0 ∈ ℕ0
21 20 3 deccl ⊢ 8 0 0 ∈ ℕ0
22 5nn0 ⊢ 5 ∈ ℕ0
23 22 10 deccl ⊢ 5 2 ∈ ℕ0
24 23 15 deccl ⊢ 5 2 1 ∈ ℕ0
25 24 nn0zi ⊢ 5 2 1 ∈ ℤ
26 3nn0 ⊢ 3 ∈ ℕ0
27 10 26 deccl ⊢ 2 3 ∈ ℕ0
28 27 15 deccl ⊢ 2 3 1 ∈ ℕ0
29 28 15 deccl ⊢ 2 3 1 1 ∈ ℕ0
30 9nn0 ⊢ 9 ∈ ℕ0
31 30 3 deccl ⊢ 9 0 ∈ ℕ0
32 31 10 deccl ⊢ 9 0 2 ∈ ℕ0
33 1 4001lem2 ⊢ ( ( 2 ↑ 8 0 0 ) mod 𝑁 ) = ( 2 3 1 1 mod 𝑁 )
34 1 4001lem1 ⊢ ( ( 2 ↑ 2 0 0 ) mod 𝑁 ) = ( 9 0 2 mod 𝑁 )
35 eqid ⊢ 8 0 0 = 8 0 0
36 eqid ⊢ 2 0 0 = 2 0 0
37 eqid ⊢ 8 0 = 8 0
38 eqid ⊢ 2 0 = 2 0
39 8p2e10 ⊢ ( 8 + 2 ) = 1 0
40 00id ⊢ ( 0 + 0 ) = 0
41 19 3 10 3 37 38 39 40 decadd ⊢ ( 8 0 + 2 0 ) = 1 0 0
42 20 3 11 3 35 36 41 40 decadd ⊢ ( 8 0 0 + 2 0 0 ) = 1 0 0 0
43 15 dec0h ⊢ 1 = 0 1
44 eqid ⊢ 4 0 0 = 4 0 0
45 23 nn0cni ⊢ 5 2 ∈ ℂ
46 45 addid2i ⊢ ( 0 + 5 2 ) = 5 2
47 eqid ⊢ 4 0 = 4 0
48 5cn ⊢ 5 ∈ ℂ
49 48 addid1i ⊢ ( 5 + 0 ) = 5
50 22 dec0h ⊢ 5 = 0 5
51 49 50 eqtri ⊢ ( 5 + 0 ) = 0 5
52 40 3 eqeltri ⊢ ( 0 + 0 ) ∈ ℕ0
53 eqid ⊢ 5 2 1 = 5 2 1
54 eqid ⊢ 5 2 = 5 2
55 5t4e20 ⊢ ( 5 · 4 ) = 2 0
56 4cn ⊢ 4 ∈ ℂ
57 2cn ⊢ 2 ∈ ℂ
58 4t2e8 ⊢ ( 4 · 2 ) = 8
59 56 57 58 mulcomli ⊢ ( 2 · 4 ) = 8
60 2 22 10 54 55 59 decmul1 ⊢ ( 5 2 · 4 ) = 2 0 8
61 56 mulid2i ⊢ ( 1 · 4 ) = 4
62 61 40 oveq12i ⊢ ( ( 1 · 4 ) + ( 0 + 0 ) ) = ( 4 + 0 )
63 56 addid1i ⊢ ( 4 + 0 ) = 4
64 62 63 eqtri ⊢ ( ( 1 · 4 ) + ( 0 + 0 ) ) = 4
65 23 15 52 53 2 60 64 decrmanc ⊢ ( ( 5 2 1 · 4 ) + ( 0 + 0 ) ) = 2 0 8 4
66 24 nn0cni ⊢ 5 2 1 ∈ ℂ
67 66 mul01i ⊢ ( 5 2 1 · 0 ) = 0
68 67 oveq1i ⊢ ( ( 5 2 1 · 0 ) + 5 ) = ( 0 + 5 )
69 48 addid2i ⊢ ( 0 + 5 ) = 5
70 68 69 50 3eqtri ⊢ ( ( 5 2 1 · 0 ) + 5 ) = 0 5
71 2 3 3 22 47 51 24 22 3 65 70 decma2c ⊢ ( ( 5 2 1 · 4 0 ) + ( 5 + 0 ) ) = 2 0 8 4 5
72 67 oveq1i ⊢ ( ( 5 2 1 · 0 ) + 2 ) = ( 0 + 2 )
73 57 addid2i ⊢ ( 0 + 2 ) = 2
74 10 dec0h ⊢ 2 = 0 2
75 72 73 74 3eqtri ⊢ ( ( 5 2 1 · 0 ) + 2 ) = 0 2
76 4 3 22 10 44 46 24 10 3 71 75 decma2c ⊢ ( ( 5 2 1 · 4 0 0 ) + ( 0 + 5 2 ) ) = 2 0 8 4 5 2
77 45 mulid1i ⊢ ( 5 2 · 1 ) = 5 2
78 ax-1cn ⊢ 1 ∈ ℂ
79 78 mulid2i ⊢ ( 1 · 1 ) = 1
80 79 oveq1i ⊢ ( ( 1 · 1 ) + 1 ) = ( 1 + 1 )
81 1p1e2 ⊢ ( 1 + 1 ) = 2
82 80 81 eqtri ⊢ ( ( 1 · 1 ) + 1 ) = 2
83 23 15 15 53 15 77 82 decrmanc ⊢ ( ( 5 2 1 · 1 ) + 1 ) = 5 2 2
84 5 15 3 15 1 43 24 10 23 76 83 decma2c ⊢ ( ( 5 2 1 · 𝑁 ) + 1 ) = 2 0 8 4 5 2 2
85 eqid ⊢ 9 0 2 = 9 0 2
86 6nn0 ⊢ 6 ∈ ℕ0
87 2 86 deccl ⊢ 4 6 ∈ ℕ0
88 87 10 deccl ⊢ 4 6 2 ∈ ℕ0
89 eqid ⊢ 9 0 = 9 0
90 eqid ⊢ 4 6 2 = 4 6 2
91 eqid ⊢ 2 3 1 1 = 2 3 1 1
92 87 nn0cni ⊢ 4 6 ∈ ℂ
93 92 addid1i ⊢ ( 4 6 + 0 ) = 4 6
94 4p1e5 ⊢ ( 4 + 1 ) = 5
95 94 22 eqeltri ⊢ ( 4 + 1 ) ∈ ℕ0
96 eqid ⊢ 2 3 1 = 2 3 1
97 eqid ⊢ 2 3 = 2 3
98 9cn ⊢ 9 ∈ ℂ
99 9t2e18 ⊢ ( 9 · 2 ) = 1 8
100 98 57 99 mulcomli ⊢ ( 2 · 9 ) = 1 8
101 15 19 10 100 81 39 decaddci2 ⊢ ( ( 2 · 9 ) + 2 ) = 2 0
102 7nn0 ⊢ 7 ∈ ℕ0
103 7p1e8 ⊢ ( 7 + 1 ) = 8
104 3cn ⊢ 3 ∈ ℂ
105 9t3e27 ⊢ ( 9 · 3 ) = 2 7
106 98 104 105 mulcomli ⊢ ( 3 · 9 ) = 2 7
107 10 102 103 106 decsuc ⊢ ( ( 3 · 9 ) + 1 ) = 2 8
108 10 26 15 97 30 19 10 101 107 decrmac ⊢ ( ( 2 3 · 9 ) + 1 ) = 2 0 8
109 98 mulid2i ⊢ ( 1 · 9 ) = 9
110 109 94 oveq12i ⊢ ( ( 1 · 9 ) + ( 4 + 1 ) ) = ( 9 + 5 )
111 9p5e14 ⊢ ( 9 + 5 ) = 1 4
112 110 111 eqtri ⊢ ( ( 1 · 9 ) + ( 4 + 1 ) ) = 1 4
113 27 15 95 96 30 2 15 108 112 decrmac ⊢ ( ( 2 3 1 · 9 ) + ( 4 + 1 ) ) = 2 0 8 4
114 109 oveq1i ⊢ ( ( 1 · 9 ) + 6 ) = ( 9 + 6 )
115 9p6e15 ⊢ ( 9 + 6 ) = 1 5
116 114 115 eqtri ⊢ ( ( 1 · 9 ) + 6 ) = 1 5
117 28 15 2 86 91 93 30 22 15 113 116 decmac ⊢ ( ( 2 3 1 1 · 9 ) + ( 4 6 + 0 ) ) = 2 0 8 4 5
118 29 nn0cni ⊢ 2 3 1 1 ∈ ℂ
119 118 mul01i ⊢ ( 2 3 1 1 · 0 ) = 0
120 119 oveq1i ⊢ ( ( 2 3 1 1 · 0 ) + 2 ) = ( 0 + 2 )
121 120 73 74 3eqtri ⊢ ( ( 2 3 1 1 · 0 ) + 2 ) = 0 2
122 30 3 87 10 89 90 29 10 3 117 121 decma2c ⊢ ( ( 2 3 1 1 · 9 0 ) + 4 6 2 ) = 2 0 8 4 5 2
123 2t2e4 ⊢ ( 2 · 2 ) = 4
124 3t2e6 ⊢ ( 3 · 2 ) = 6
125 10 10 26 97 123 124 decmul1 ⊢ ( 2 3 · 2 ) = 4 6
126 57 mulid2i ⊢ ( 1 · 2 ) = 2
127 10 27 15 96 125 126 decmul1 ⊢ ( 2 3 1 · 2 ) = 4 6 2
128 10 28 15 91 127 126 decmul1 ⊢ ( 2 3 1 1 · 2 ) = 4 6 2 2
129 29 31 10 85 10 88 122 128 decmul2c ⊢ ( 2 3 1 1 · 9 0 2 ) = 2 0 8 4 5 2 2
130 84 129 eqtr4i ⊢ ( ( 5 2 1 · 𝑁 ) + 1 ) = ( 2 3 1 1 · 9 0 2 )
131 8 9 21 25 29 15 12 32 33 34 42 130 modxai ⊢ ( ( 2 ↑ 1 0 0 0 ) mod 𝑁 ) = ( 1 mod 𝑁 )
132 18 nn0cni ⊢ 1 0 0 0 ∈ ℂ
133 eqid ⊢ 1 0 0 0 = 1 0 0 0
134 eqid ⊢ 1 0 0 = 1 0 0
135 10 dec0u ⊢ ( 1 0 · 2 ) = 2 0
136 57 mul02i ⊢ ( 0 · 2 ) = 0
137 10 16 3 134 135 136 decmul1 ⊢ ( 1 0 0 · 2 ) = 2 0 0
138 10 17 3 133 137 136 decmul1 ⊢ ( 1 0 0 0 · 2 ) = 2 0 0 0
139 132 57 138 mulcomli ⊢ ( 2 · 1 0 0 0 ) = 2 0 0 0
140 8 nncni ⊢ 𝑁 ∈ ℂ
141 140 mul02i ⊢ ( 0 · 𝑁 ) = 0
142 141 oveq1i ⊢ ( ( 0 · 𝑁 ) + 1 ) = ( 0 + 1 )
143 78 addid2i ⊢ ( 0 + 1 ) = 1
144 79 143 eqtr4i ⊢ ( 1 · 1 ) = ( 0 + 1 )
145 142 144 eqtr4i ⊢ ( ( 0 · 𝑁 ) + 1 ) = ( 1 · 1 )
146 8 9 18 14 15 15 131 139 145 mod2xi ⊢ ( ( 2 ↑ 2 0 0 0 ) mod 𝑁 ) = ( 1 mod 𝑁 )
147 13 nn0cni ⊢ 2 0 0 0 ∈ ℂ
148 eqid ⊢ 2 0 0 0 = 2 0 0 0
149 10 10 3 38 123 136 decmul1 ⊢ ( 2 0 · 2 ) = 4 0
150 10 11 3 36 149 136 decmul1 ⊢ ( 2 0 0 · 2 ) = 4 0 0
151 10 12 3 148 150 136 decmul1 ⊢ ( 2 0 0 0 · 2 ) = 4 0 0 0
152 147 57 151 mulcomli ⊢ ( 2 · 2 0 0 0 ) = 4 0 0 0
153 5 3 deccl ⊢ 4 0 0 0 ∈ ℕ0
154 153 nn0cni ⊢ 4 0 0 0 ∈ ℂ
155 eqid ⊢ 4 0 0 0 = 4 0 0 0
156 5 3 143 155 decsuc ⊢ ( 4 0 0 0 + 1 ) = 4 0 0 1
157 1 156 eqtr4i ⊢ 𝑁 = ( 4 0 0 0 + 1 )
158 154 78 157 mvrraddi ⊢ ( 𝑁 − 1 ) = 4 0 0 0
159 152 158 eqtr4i ⊢ ( 2 · 2 0 0 0 ) = ( 𝑁 − 1 )
160 8 9 13 14 15 15 146 159 145 mod2xi ⊢ ( ( 2 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 )