Theorem 4001lem2

Description: Lemma for 4001prm . Calculate a power mod. In decimal, we calculate 2 ^ 4 0 0 = ( 2 ^ 2 0 0 ) ^ 2 == 9 0 2 ^ 2 = 2 0 3 N + 1 4 0 1 and 2 ^ 8 0 0 = ( 2 ^ 4 0 0 ) ^ 2 == 1 4 0 1 ^ 2 = 4 9 0 N + 2 3 1 1 == 2 3 1 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	$$⊢N=4001$$
Assertion	4001lem2	$$⊢2^{800}\mathrm{mod}N=2311\mathrm{mod}N$$

Proof

Step	Hyp	Ref	Expression
1		4001prm.1	$$⊢N=4001$$
2		4nn0	$$⊢4\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢40\in {\mathbb{N}}_0$$
5	4 3	deccl	$$⊢400\in {\mathbb{N}}_0$$
6		1nn	$$⊢1\in \mathbb{N}$$
7	5 6	decnncl	$$⊢4001\in \mathbb{N}$$
8	1 7	eqeltri	$$⊢N\in \mathbb{N}$$
9		2nn	$$⊢2\in \mathbb{N}$$
10		9nn0	$$⊢9\in {\mathbb{N}}_0$$
11	2 10	deccl	$$⊢49\in {\mathbb{N}}_0$$
12	11 3	deccl	$$⊢490\in {\mathbb{N}}_0$$
13	12	nn0zi	$$⊢490\in \mathbb{Z}$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	14 2	deccl	$$⊢14\in {\mathbb{N}}_0$$
16	15 3	deccl	$$⊢140\in {\mathbb{N}}_0$$
17	16 14	deccl	$$⊢1401\in {\mathbb{N}}_0$$
18		2nn0	$$⊢2\in {\mathbb{N}}_0$$
19		3nn0	$$⊢3\in {\mathbb{N}}_0$$
20	18 19	deccl	$$⊢23\in {\mathbb{N}}_0$$
21	20 14	deccl	$$⊢231\in {\mathbb{N}}_0$$
22	21 14	deccl	$$⊢2311\in {\mathbb{N}}_0$$
23	18 3	deccl	$$⊢20\in {\mathbb{N}}_0$$
24	23 3	deccl	$$⊢200\in {\mathbb{N}}_0$$
25	23 19	deccl	$$⊢203\in {\mathbb{N}}_0$$
26	25	nn0zi	$$⊢203\in \mathbb{Z}$$
27	10 3	deccl	$$⊢90\in {\mathbb{N}}_0$$
28	27 18	deccl	$$⊢902\in {\mathbb{N}}_0$$
29	1	4001lem1	$$⊢2^{200}\mathrm{mod}N=902\mathrm{mod}N$$
30	24	nn0cni	$$⊢200\in ℂ$$
31		2cn	$$⊢2\in ℂ$$
32		eqid	$$⊢200=200$$
33		eqid	$$⊢20=20$$
34		2t2e4	$$⊢2\cdot 2=4$$
35	31	mul02i	$$⊢0\cdot 2=0$$
36	18 18 3 33 34 35	decmul1	$$⊢20\cdot 2=40$$
37	18 23 3 32 36 35	decmul1	$$⊢200\cdot 2=400$$
38	30 31 37	mulcomli	$$⊢2\cdot 200=400$$
39		eqid	$$⊢1401=1401$$
40		6nn0	$$⊢6\in {\mathbb{N}}_0$$
41	14 40	deccl	$$⊢16\in {\mathbb{N}}_0$$
42		eqid	$$⊢400=400$$
43		eqid	$$⊢140=140$$
44		eqid	$$⊢14=14$$
45		4p2e6	$$⊢4+2=6$$
46	14 2 18 44 45	decaddi	$$⊢14+2=16$$
47		00id	$$⊢0+0=0$$
48	15 3 18 3 43 33 46 47	decadd	$$⊢140+20=160$$
49		eqid	$$⊢40=40$$
50	41	nn0cni	$$⊢16\in ℂ$$
51	50	addridi	$$⊢16+0=16$$
52		eqid	$$⊢203=203$$
53		ax-1cn	$$⊢1\in ℂ$$
54	53	addridi	$$⊢1+0=1$$
55	14	dec0h	$$⊢1=01$$
56	54 55	eqtri	$$⊢1+0=01$$
57	53	addlidi	$$⊢0+1=1$$
58	57 14	eqeltri	$$⊢0+1\in {\mathbb{N}}_0$$
59		4cn	$$⊢4\in ℂ$$
60		4t2e8	$$⊢4\cdot 2=8$$
61	59 31 60	mulcomli	$$⊢2\cdot 4=8$$
62	59	mul02i	$$⊢0\cdot 4=0$$
63	62 57	oveq12i	$$⊢0\cdot 4+0+1=0+1$$
64	63 57	eqtri	$$⊢0\cdot 4+0+1=1$$
65	18 3 58 33 2 61 64	decrmanc	$$⊢20\cdot 4+0+1=81$$
66		2p1e3	$$⊢2+1=3$$
67		3cn	$$⊢3\in ℂ$$
68		4t3e12	$$⊢4\cdot 3=12$$
69	59 67 68	mulcomli	$$⊢3\cdot 4=12$$
70	14 18 66 69	decsuc	$$⊢3\cdot 4+1=13$$
71	23 19 3 14 52 56 2 19 14 65 70	decmac	$$⊢203\cdot 4+1+0=813$$
72	25	nn0cni	$$⊢203\in ℂ$$
73	72	mul01i	$$⊢203\cdot 0=0$$
74	73	oveq1i	$$⊢203\cdot 0+6=0+6$$
75		6cn	$$⊢6\in ℂ$$
76	75	addlidi	$$⊢0+6=6$$
77	40	dec0h	$$⊢6=06$$
78	74 76 77	3eqtri	$$⊢203\cdot 0+6=06$$
79	2 3 14 40 49 51 25 40 3 71 78	decma2c	$$⊢203\cdot 40+16+0=8136$$
80	73	oveq1i	$$⊢203\cdot 0+0=0+0$$
81	3	dec0h	$$⊢0=00$$
82	80 47 81	3eqtri	$$⊢203\cdot 0+0=00$$
83	4 3 41 3 42 48 25 3 3 79 82	decma2c	$$⊢203\cdot 400+140+20=81360$$
84	31	mulridi	$$⊢2\cdot 1=2$$
85	53	mul02i	$$⊢0\cdot 1=0$$
86	14 18 3 33 84 85	decmul1	$$⊢20\cdot 1=20$$
87	67	mulridi	$$⊢3\cdot 1=3$$
88	87	oveq1i	$$⊢3\cdot 1+1=3+1$$
89		3p1e4	$$⊢3+1=4$$
90	88 89	eqtri	$$⊢3\cdot 1+1=4$$
91	23 19 14 52 14 86 90	decrmanc	$$⊢203\cdot 1+1=204$$
92	5 14 16 14 1 39 25 2 23 83 91	decma2c	$$⊢203\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1401=813604$$
93		eqid	$$⊢902=902$$
94		8nn0	$$⊢8\in {\mathbb{N}}_0$$
95	14 94	deccl	$$⊢18\in {\mathbb{N}}_0$$
96	95 3	deccl	$$⊢180\in {\mathbb{N}}_0$$
97		eqid	$$⊢90=90$$
98		eqid	$$⊢180=180$$
99	95	nn0cni	$$⊢18\in ℂ$$
100	99	addridi	$$⊢18+0=18$$
101		1p2e3	$$⊢1+2=3$$
102	101 19	eqeltri	$$⊢1+2\in {\mathbb{N}}_0$$
103		9t9e81	$$⊢9\cdot 9=81$$
104		9cn	$$⊢9\in ℂ$$
105	104	mul02i	$$⊢0\cdot 9=0$$
106	105 101	oveq12i	$$⊢0\cdot 9+1+2=0+3$$
107	67	addlidi	$$⊢0+3=3$$
108	106 107	eqtri	$$⊢0\cdot 9+1+2=3$$
109	10 3 102 97 10 103 108	decrmanc	$$⊢90\cdot 9+1+2=813$$
110		9t2e18	$$⊢9\cdot 2=18$$
111	104 31 110	mulcomli	$$⊢2\cdot 9=18$$
112		1p1e2	$$⊢1+1=2$$
113		8p8e16	$$⊢8+8=16$$
114	14 94 94 111 112 40 113	decaddci	$$⊢2\cdot 9+8=26$$
115	27 18 14 94 93 100 10 40 18 109 114	decmac	$$⊢902\cdot 9+18+0=8136$$
116	28	nn0cni	$$⊢902\in ℂ$$
117	116	mul01i	$$⊢902\cdot 0=0$$
118	117	oveq1i	$$⊢902\cdot 0+0=0+0$$
119	118 47 81	3eqtri	$$⊢902\cdot 0+0=00$$
120	10 3 95 3 97 98 28 3 3 115 119	decma2c	$$⊢902\cdot 90+180=81360$$
121	18 10 3 97 110 35	decmul1	$$⊢90\cdot 2=180$$
122	18 27 18 93 121 34	decmul1	$$⊢902\cdot 2=1804$$
123	28 27 18 93 2 96 120 122	decmul2c	$$⊢902\cdot 902=813604$$
124	92 123	eqtr4i	$$⊢203\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1401=902\cdot 902$$
125	8 9 24 26 28 17 29 38 124	mod2xi	$$⊢2^{400}\mathrm{mod}N=1401\mathrm{mod}N$$
126	5	nn0cni	$$⊢400\in ℂ$$
127	18 2 3 49 60 35	decmul1	$$⊢40\cdot 2=80$$
128	18 4 3 42 127 35	decmul1	$$⊢400\cdot 2=800$$
129	126 31 128	mulcomli	$$⊢2\cdot 400=800$$
130		eqid	$$⊢2311=2311$$
131	18 94	deccl	$$⊢28\in {\mathbb{N}}_0$$
132		eqid	$$⊢231=231$$
133		eqid	$$⊢49=49$$
134		7nn0	$$⊢7\in {\mathbb{N}}_0$$
135		7p1e8	$$⊢7+1=8$$
136		eqid	$$⊢23=23$$
137		4p3e7	$$⊢4+3=7$$
138	59 67 137	addcomli	$$⊢3+4=7$$
139	18 19 2 136 138	decaddi	$$⊢23+4=27$$
140	18 134 135 139	decsuc	$$⊢23+4+1=28$$
141		9p1e10	$$⊢9+1=10$$
142	104 53 141	addcomli	$$⊢1+9=10$$
143	20 14 2 10 132 133 140 142	decaddc2	$$⊢231+49=280$$
144	131	nn0cni	$$⊢28\in ℂ$$
145	144	addridi	$$⊢28+0=28$$
146	31	addridi	$$⊢2+0=2$$
147	146 18	eqeltri	$$⊢2+0\in {\mathbb{N}}_0$$
148		eqid	$$⊢490=490$$
149		4t4e16	$$⊢4\cdot 4=16$$
150		6p3e9	$$⊢6+3=9$$
151	14 40 19 149 150	decaddi	$$⊢4\cdot 4+3=19$$
152		9t4e36	$$⊢9\cdot 4=36$$
153	2 2 10 133 40 19 151 152	decmul1c	$$⊢49\cdot 4=196$$
154	62 146	oveq12i	$$⊢0\cdot 4+2+0=0+2$$
155	31	addlidi	$$⊢0+2=2$$
156	154 155	eqtri	$$⊢0\cdot 4+2+0=2$$
157	11 3 147 148 2 153 156	decrmanc	$$⊢490\cdot 4+2+0=1962$$
158	12	nn0cni	$$⊢490\in ℂ$$
159	158	mul01i	$$⊢490\cdot 0=0$$
160	159	oveq1i	$$⊢490\cdot 0+8=0+8$$
161		8cn	$$⊢8\in ℂ$$
162	161	addlidi	$$⊢0+8=8$$
163	94	dec0h	$$⊢8=08$$
164	160 162 163	3eqtri	$$⊢490\cdot 0+8=08$$
165	2 3 18 94 49 145 12 94 3 157 164	decma2c	$$⊢490\cdot 40+28+0=19628$$
166	159	oveq1i	$$⊢490\cdot 0+0=0+0$$
167	166 47 81	3eqtri	$$⊢490\cdot 0+0=00$$
168	4 3 131 3 42 143 12 3 3 165 167	decma2c	$$⊢490\cdot 400+231+49=196280$$
169	59	mulridi	$$⊢4\cdot 1=4$$
170	104	mulridi	$$⊢9\cdot 1=9$$
171	14 2 10 133 169 170	decmul1	$$⊢49\cdot 1=49$$
172	85	oveq1i	$$⊢0\cdot 1+1=0+1$$
173	172 57	eqtri	$$⊢0\cdot 1+1=1$$
174	11 3 14 148 14 171 173	decrmanc	$$⊢490\cdot 1+1=491$$
175	5 14 21 14 1 130 12 14 11 168 174	decma2c	$$⊢490\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2311=1962801$$
176	15	nn0cni	$$⊢14\in ℂ$$
177	176	addridi	$$⊢14+0=14$$
178		5nn0	$$⊢5\in {\mathbb{N}}_0$$
179	178 40	deccl	$$⊢56\in {\mathbb{N}}_0$$
180	179 3	deccl	$$⊢560\in {\mathbb{N}}_0$$
181		eqid	$$⊢560=560$$
182	179	nn0cni	$$⊢56\in ℂ$$
183	182	addlidi	$$⊢0+56=56$$
184	3 14 179 3 55 181 183 54	decadd	$$⊢1+560=561$$
185	182	addridi	$$⊢56+0=56$$
186		5cn	$$⊢5\in ℂ$$
187	186	addridi	$$⊢5+0=5$$
188	187 178	eqeltri	$$⊢5+0\in {\mathbb{N}}_0$$
189	53	mulridi	$$⊢1\cdot 1=1$$
190	169 187	oveq12i	$$⊢4\cdot 1+5+0=4+5$$
191		5p4e9	$$⊢5+4=9$$
192	186 59 191	addcomli	$$⊢4+5=9$$
193	190 192	eqtri	$$⊢4\cdot 1+5+0=9$$
194	14 2 188 44 14 189 193	decrmanc	$$⊢14\cdot 1+5+0=19$$
195	85	oveq1i	$$⊢0\cdot 1+6=0+6$$
196	195 76 77	3eqtri	$$⊢0\cdot 1+6=06$$
197	15 3 178 40 43 185 14 40 3 194 196	decmac	$$⊢140\cdot 1+56+0=196$$
198	189	oveq1i	$$⊢1\cdot 1+1=1+1$$
199	18	dec0h	$$⊢2=02$$
200	198 112 199	3eqtri	$$⊢1\cdot 1+1=02$$
201	16 14 179 14 39 184 14 18 3 197 200	decmac	$$⊢1401\cdot 1+1+560=1962$$
202	59	mullidi	$$⊢1\cdot 4=4$$
203	202	oveq1i	$$⊢1\cdot 4+1=4+1$$
204		4p1e5	$$⊢4+1=5$$
205	203 204	eqtri	$$⊢1\cdot 4+1=5$$
206	2 14 2 44 40 14 205 149	decmul1c	$$⊢14\cdot 4=56$$
207	75	addridi	$$⊢6+0=6$$
208	178 40 3 206 207	decaddi	$$⊢14\cdot 4+0=56$$
209		0cn	$$⊢0\in ℂ$$
210	59	mul01i	$$⊢4\cdot 0=0$$
211	210 81	eqtri	$$⊢4\cdot 0=00$$
212	59 209 211	mulcomli	$$⊢0\cdot 4=00$$
213	2 15 3 43 3 3 208 212	decmul1c	$$⊢140\cdot 4=560$$
214	202	oveq1i	$$⊢1\cdot 4+4=4+4$$
215		4p4e8	$$⊢4+4=8$$
216	214 215	eqtri	$$⊢1\cdot 4+4=8$$
217	16 14 2 39 2 213 216	decrmanc	$$⊢1401\cdot 4+4=5608$$
218	14 2 14 2 44 177 17 94 180 201 217	decma2c	$$⊢1401\cdot 14+14+0=19628$$
219	17	nn0cni	$$⊢1401\in ℂ$$
220	219	mul01i	$$⊢1401\cdot 0=0$$
221	220	oveq1i	$$⊢1401\cdot 0+0=0+0$$
222	221 47 81	3eqtri	$$⊢1401\cdot 0+0=00$$
223	15 3 15 3 43 43 17 3 3 218 222	decma2c	$$⊢1401\cdot 140+140=196280$$
224	219	mulridi	$$⊢1401\cdot 1=1401$$
225	17 16 14 39 14 16 223 224	decmul2c	$$⊢1401\cdot 1401=1962801$$
226	175 225	eqtr4i	$$⊢490\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2311=1401\cdot 1401$$
227	8 9 5 13 17 22 125 129 226	mod2xi	$$⊢2^{800}\mathrm{mod}N=2311\mathrm{mod}N$$