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