4001lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 4001lem1		Structured version Visualization version Unicode version

Theorem 4001lem1 15848

Description: Lemma for 4001prm 15852. Calculate a power mod. In decimal, we calculate

and

. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)

**Hypothesis**
Ref	Expression
4001prm.1	;;;

**Assertion**
Ref	Expression
4001lem1	;; ;;

**Proof of Theorem 4001lem1**
Step	Hyp	Ref	Expression
1		4001prm.1	. . 3 ;;;
2		4nn0 11311	. . . . . 6
3		0nn0 11307	. . . . . 6
4	2, 3	deccl 11512	. . . . 5 ;
5	4, 3	deccl 11512	. . . 4 ;;
6		1nn 11031	. . . 4
7	5, 6	decnncl 11518	. . 3 ;;;
8	1, 7	eqeltri 2697	. 2
9		2nn 11185	. 2
10		10nn0 11516	. . 3 ;
11	10, 3	deccl 11512	. 2 ;;
12		9nn0 11316	. . . 4
13	12, 2	deccl 11512	. . 3 ;
14	13	nn0zi 11402	. 2 ;
15		6nn0 11313	. . . 4
16		1nn0 11308	. . . 4
17	15, 16	deccl 11512	. . 3 ;
18	17, 2	deccl 11512	. 2 ;;
19	12, 3	deccl 11512	. . 3 ;
20		2nn0 11309	. . 3
21	19, 20	deccl 11512	. 2 ;;
22		5nn0 11312	. . . 4
23	22, 3	deccl 11512	. . 3 ;
24		8nn0 11315	. . . . . 6
25	20, 24	deccl 11512	. . . . 5 ;
26	25, 15	deccl 11512	. . . 4 ;;
27	26	nn0zi 11402	. . 3 ;;
28		7nn0 11314	. . . . 5
29	10, 28	deccl 11512	. . . 4 ;;
30	29, 3	deccl 11512	. . 3 ;;;
31	20, 22	deccl 11512	. . . 4 ;
32	10, 2	deccl 11512	. . . . . 6 ;;
33	32, 15	deccl 11512	. . . . 5 ;;;
34	33	nn0zi 11402	. . . 4 ;;;
35	20, 3	deccl 11512	. . . . . 6 ;
36	35, 2	deccl 11512	. . . . 5 ;;
37	36, 15	deccl 11512	. . . 4 ;;;
38	20, 2	deccl 11512	. . . . 5 ;
39		0z 11388	. . . . 5
40	10, 20	deccl 11512	. . . . . 6 ;;
41		3nn0 11310	. . . . . 6
42	40, 41	deccl 11512	. . . . 5 ;;;
43	16, 20	deccl 11512	. . . . . 6 ;
44		2z 11409	. . . . . 6
45	12, 22	deccl 11512	. . . . . 6 ;
46		1z 11407	. . . . . . 7
47	15, 2	deccl 11512	. . . . . . 7 ;
48		2exp6 15795	. . . . . . . 8 ;
49	48	oveq1i 6660	. . . . . . 7 ;
50		6cn 11102	. . . . . . . 8
51		2cn 11091	. . . . . . . 8
52		6t2e12 11641	. . . . . . . 8 ;
53	50, 51, 52	mulcomli 10047	. . . . . . 7 ;
54		eqid 2622	. . . . . . . . 9 ; ;
55		eqid 2622	. . . . . . . . . 10 ;; ;;
56		9cn 11108	. . . . . . . . . . . 12
57	56	addid1i 10223	. . . . . . . . . . 11
58	12	dec0h 11522	. . . . . . . . . . 11 ;
59	57, 58	eqtri 2644	. . . . . . . . . 10 ;
60		eqid 2622	. . . . . . . . . . 11 ; ;
61		00id 10211	. . . . . . . . . . . 12
62	3	dec0h 11522	. . . . . . . . . . . 12 ;
63	61, 62	eqtri 2644	. . . . . . . . . . 11 ;
64		4cn 11098	. . . . . . . . . . . . . 14
65	64	mulid2i 10043	. . . . . . . . . . . . 13
66	65, 61	oveq12i 6662	. . . . . . . . . . . 12
67	64	addid1i 10223	. . . . . . . . . . . 12
68	66, 67	eqtri 2644	. . . . . . . . . . 11
69		ax-1cn 9994	. . . . . . . . . . . . . 14
70	69	mul01i 10226	. . . . . . . . . . . . 13
71	70	oveq1i 6660	. . . . . . . . . . . 12
72	71, 61, 62	3eqtri 2648	. . . . . . . . . . 11 ;
73	2, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72	decma2c 11568	. . . . . . . . . 10 ; ;
74	70	oveq1i 6660	. . . . . . . . . . 11
75	56	addid2i 10224	. . . . . . . . . . 11
76	74, 75, 58	3eqtri 2648	. . . . . . . . . 10 ;
77	4, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76	decma2c 11568	. . . . . . . . 9 ;; ;;
78	69	mulid1i 10042	. . . . . . . . . . 11
79	78	oveq1i 6660	. . . . . . . . . 10
80		5cn 11100	. . . . . . . . . . 11
81		5p1e6 11155	. . . . . . . . . . 11
82	80, 69, 81	addcomli 10228	. . . . . . . . . 10
83	15	dec0h 11522	. . . . . . . . . 10 ;
84	79, 82, 83	3eqtri 2648	. . . . . . . . 9 ;
85	5, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84	decma2c 11568	. . . . . . . 8 ; ;;;
86		eqid 2622	. . . . . . . . 9 ; ;
87		eqid 2622	. . . . . . . . . 10 ; ;
88		2p2e4 11144	. . . . . . . . . . . 12
89	88	oveq2i 6661	. . . . . . . . . . 11
90		6t6e36 11646	. . . . . . . . . . . 12 ;
91		3p1e4 11153	. . . . . . . . . . . 12
92		6p4e10 11598	. . . . . . . . . . . 12 ;
93	41, 15, 2, 90, 91, 92	decaddci2 11581	. . . . . . . . . . 11 ;
94	89, 93	eqtri 2644	. . . . . . . . . 10 ;
95		6t4e24 11643	. . . . . . . . . . . 12 ;
96	50, 64, 95	mulcomli 10047	. . . . . . . . . . 11 ;
97		5p4e9 11167	. . . . . . . . . . . 12
98	80, 64, 97	addcomli 10228	. . . . . . . . . . 11
99	20, 2, 22, 96, 98	decaddi 11579	. . . . . . . . . 10 ;
100	15, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99	decmac 11566	. . . . . . . . 9 ; ; ;;
101		4p1e5 11154	. . . . . . . . . . 11
102	20, 2, 101, 95	decsuc 11535	. . . . . . . . . 10 ;
103		4t4e16 11633	. . . . . . . . . 10 ;
104	2, 15, 2, 86, 15, 16, 102, 103	decmul1c 11587	. . . . . . . . 9 ; ;;
105	47, 15, 2, 86, 15, 31, 100, 104	decmul2c 11589	. . . . . . . 8 ; ; ;;;
106	85, 105	eqtr4i 2647	. . . . . . 7 ; ; ;
107	8, 9, 15, 46, 47, 45, 49, 53, 106	mod2xi 15773	. . . . . 6 ; ;
108		eqid 2622	. . . . . . 7 ; ;
109	51	mulid1i 10042	. . . . . . . . 9
110	109	oveq1i 6660	. . . . . . . 8
111	51	addid1i 10223	. . . . . . . 8
112	110, 111	eqtri 2644	. . . . . . 7
113		2t2e4 11177	. . . . . . . 8
114	2	dec0h 11522	. . . . . . . 8 ;
115	113, 114	eqtri 2644	. . . . . . 7 ;
116	20, 16, 20, 108, 2, 3, 112, 115	decmul2c 11589	. . . . . 6 ; ;
117		eqid 2622	. . . . . . . 8 ;;; ;;;
118	40	nn0cni 11304	. . . . . . . . . 10 ;;
119	118	addid1i 10223	. . . . . . . . 9 ;; ;;
120		dec10p 11553	. . . . . . . . . 10 ; ;
121		4t2e8 11181	. . . . . . . . . . . . 13
122	64, 51, 121	mulcomli 10047	. . . . . . . . . . . 12
123	69	addid1i 10223	. . . . . . . . . . . 12
124	122, 123	oveq12i 6662	. . . . . . . . . . 11
125		8p1e9 11158	. . . . . . . . . . 11
126	124, 125	eqtri 2644	. . . . . . . . . 10
127	51	mul01i 10226	. . . . . . . . . . . 12
128	127	oveq1i 6660	. . . . . . . . . . 11
129	128, 61, 62	3eqtri 2648	. . . . . . . . . 10 ;
130	2, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129	decma2c 11568	. . . . . . . . 9 ; ; ;
131	127	oveq1i 6660	. . . . . . . . . 10
132	51	addid2i 10224	. . . . . . . . . 10
133	20	dec0h 11522	. . . . . . . . . 10 ;
134	131, 132, 133	3eqtri 2648	. . . . . . . . 9 ;
135	4, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134	decma2c 11568	. . . . . . . 8 ;; ;; ;;
136	109	oveq1i 6660	. . . . . . . . 9
137		3cn 11095	. . . . . . . . . 10
138		3p2e5 11160	. . . . . . . . . 10
139	137, 51, 138	addcomli 10228	. . . . . . . . 9
140	22	dec0h 11522	. . . . . . . . 9 ;
141	136, 139, 140	3eqtri 2648	. . . . . . . 8 ;
142	5, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141	decma2c 11568	. . . . . . 7 ;;; ;;;
143	2, 28	deccl 11512	. . . . . . . 8 ;
144		eqid 2622	. . . . . . . . 9 ; ;
145	98	oveq2i 6661	. . . . . . . . . 10
146		9t9e81 11670	. . . . . . . . . . 11 ;
147		9p1e10 11496	. . . . . . . . . . . 12 ;
148	56, 69, 147	addcomli 10228	. . . . . . . . . . 11 ;
149	24, 16, 12, 146, 125, 148	decaddci2 11581	. . . . . . . . . 10 ;
150	145, 149	eqtri 2644	. . . . . . . . 9 ;
151		9t5e45 11666	. . . . . . . . . . 11 ;
152	56, 80, 151	mulcomli 10047	. . . . . . . . . 10 ;
153		7cn 11104	. . . . . . . . . . 11
154		7p5e12 11607	. . . . . . . . . . 11 ;
155	153, 80, 154	addcomli 10228	. . . . . . . . . 10 ;
156	2, 22, 28, 152, 101, 20, 155	decaddci 11580	. . . . . . . . 9 ;
157	12, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156	decmac 11566	. . . . . . . 8 ; ; ;;
158		5p2e7 11165	. . . . . . . . . 10
159	2, 22, 20, 151, 158	decaddi 11579	. . . . . . . . 9 ;
160		5t5e25 11639	. . . . . . . . 9 ;
161	22, 12, 22, 54, 22, 20, 159, 160	decmul1c 11587	. . . . . . . 8 ; ;;
162	45, 12, 22, 54, 22, 143, 157, 161	decmul2c 11589	. . . . . . 7 ; ; ;;;
163	142, 162	eqtr4i 2647	. . . . . 6 ;;; ; ;
164	8, 9, 43, 44, 45, 42, 107, 116, 163	mod2xi 15773	. . . . 5 ; ;;;
165		eqid 2622	. . . . . 6 ; ;
166	20, 2, 101, 165	decsuc 11535	. . . . 5 ; ;
167	37	nn0cni 11304	. . . . . . 7 ;;;
168	167	addid2i 10224	. . . . . 6 ;;; ;;;
169	8	nncni 11030	. . . . . . . 8
170	169	mul02i 10225	. . . . . . 7
171	170	oveq1i 6660	. . . . . 6 ;;; ;;;
172		eqid 2622	. . . . . . . 8 ;; ;;
173	20	dec0u 11520	. . . . . . . 8 ; ;
174	20, 10, 20, 172, 2, 173, 113	decmul1 11585	. . . . . . 7 ;; ;;
175		3t2e6 11179	. . . . . . 7
176	20, 40, 41, 117, 15, 174, 175	decmul1 11585	. . . . . 6 ;;; ;;;
177	168, 171, 176	3eqtr4i 2654	. . . . 5 ;;; ;;;
178	8, 9, 38, 39, 42, 37, 164, 166, 177	modxp1i 15774	. . . 4 ; ;;;
179	113	oveq1i 6660	. . . . . 6
180	179, 101	eqtri 2644	. . . . 5
181		5t2e10 11634	. . . . . 6 ;
182	80, 51, 181	mulcomli 10047	. . . . 5 ;
183	20, 20, 22, 87, 3, 16, 180, 182	decmul2c 11589	. . . 4 ; ;
184		eqid 2622	. . . . . 6 ;;; ;;;
185	20, 16	deccl 11512	. . . . . . 7 ;
186		eqid 2622	. . . . . . . 8 ;; ;;
187		eqid 2622	. . . . . . . 8 ;; ;;
188		0p1e1 11132	. . . . . . . . 9
189		10p10e20 11628	. . . . . . . . 9 ; ; ;
190	20, 3, 188, 189	decsuc 11535	. . . . . . . 8 ; ; ;
191		7p4e11 11605	. . . . . . . 8 ;
192	10, 28, 10, 2, 186, 187, 190, 16, 191	decaddc 11572	. . . . . . 7 ;; ;; ;;
193	185	nn0cni 11304	. . . . . . . . 9 ;
194	193	addid1i 10223	. . . . . . . 8 ; ;
195	111, 20	eqeltri 2697	. . . . . . . . 9
196		eqid 2622	. . . . . . . . 9 ;;; ;;;
197		dfdec10 11497	. . . . . . . . . . 11 ; ;
198	197	eqcomi 2631	. . . . . . . . . 10 ; ;
199		6p2e8 11169	. . . . . . . . . . 11
200	16, 15, 20, 103, 199	decaddi 11579	. . . . . . . . . 10 ;
201	10, 2, 20, 187, 2, 24, 16, 198, 200	decrmac 11577	. . . . . . . . 9 ;; ;;
202	95, 111	oveq12i 6662	. . . . . . . . . 10 ;
203		4p2e6 11162	. . . . . . . . . . 11
204	20, 2, 20, 165, 203	decaddi 11579	. . . . . . . . . 10 ; ;
205	202, 204	eqtri 2644	. . . . . . . . 9 ;
206	32, 15, 195, 196, 2, 15, 20, 201, 205	decrmac 11577	. . . . . . . 8 ;;; ;;;
207	33	nn0cni 11304	. . . . . . . . . . 11 ;;;
208	207	mul01i 10226	. . . . . . . . . 10 ;;;
209	208	oveq1i 6660	. . . . . . . . 9 ;;;
210	16	dec0h 11522	. . . . . . . . 9 ;
211	209, 188, 210	3eqtri 2648	. . . . . . . 8 ;;; ;
212	2, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211	decma2c 11568	. . . . . . 7 ;;; ; ; ;;;;
213	4, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211	decma2c 11568	. . . . . 6 ;;; ;; ;; ;; ;;;;;
214	207	mulid1i 10042	. . . . . . . 8 ;;; ;;;
215	214	oveq1i 6660	. . . . . . 7 ;;; ;;;
216	207	addid1i 10223	. . . . . . 7 ;;; ;;;
217	215, 216	eqtri 2644	. . . . . 6 ;;; ;;;
218	5, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217	decma2c 11568	. . . . 5 ;;; ;;; ;;;;;;
219		eqid 2622	. . . . . 6 ;;; ;;;
220	43, 20	deccl 11512	. . . . . . 7 ;;
221	220, 28	deccl 11512	. . . . . 6 ;;;
222		eqid 2622	. . . . . . 7 ;; ;;
223		eqid 2622	. . . . . . 7 ;;; ;;;
224	24, 16	deccl 11512	. . . . . . . 8 ;
225	224, 12	deccl 11512	. . . . . . 7 ;;
226		eqid 2622	. . . . . . . 8 ; ;
227		eqid 2622	. . . . . . . . 9 ;; ;;
228		eqid 2622	. . . . . . . . 9 ;; ;;
229		eqid 2622	. . . . . . . . . . 11 ; ;
230		8cn 11106	. . . . . . . . . . . 12
231	230, 69, 125	addcomli 10228	. . . . . . . . . . 11
232		2p1e3 11151	. . . . . . . . . . 11
233	16, 20, 24, 16, 108, 229, 231, 232	decadd 11570	. . . . . . . . . 10 ; ; ;
234	12, 41, 91, 233	decsuc 11535	. . . . . . . . 9 ; ; ;
235		9p2e11 11619	. . . . . . . . . 10 ;
236	56, 51, 235	addcomli 10228	. . . . . . . . 9 ;
237	43, 20, 224, 12, 227, 228, 234, 16, 236	decaddc 11572	. . . . . . . 8 ;; ;; ;;
238	13	nn0cni 11304	. . . . . . . . . 10 ;
239	238	addid1i 10223	. . . . . . . . 9 ; ;
240	123, 16	eqeltri 2697	. . . . . . . . . . 11
241	51	mul02i 10225	. . . . . . . . . . . . 13
242	241, 123	oveq12i 6662	. . . . . . . . . . . 12
243	242, 188	eqtri 2644	. . . . . . . . . . 11
244	20, 3, 240, 226, 20, 113, 243	decrmanc 11576	. . . . . . . . . 10 ; ;
245	121	oveq1i 6660	. . . . . . . . . . 11
246	230	addid1i 10223	. . . . . . . . . . 11
247	24	dec0h 11522	. . . . . . . . . . 11 ;
248	245, 246, 247	3eqtri 2648	. . . . . . . . . 10 ;
249	35, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248	decmac 11566	. . . . . . . . 9 ;; ;;
250	64, 51, 203	addcomli 10228	. . . . . . . . . 10
251	16, 20, 2, 52, 250	decaddi 11579	. . . . . . . . 9 ;
252	36, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251	decmac 11566	. . . . . . . 8 ;;; ; ;;;
253	167	mul01i 10226	. . . . . . . . . 10 ;;;
254	253	oveq1i 6660	. . . . . . . . 9 ;;;
255	254, 188, 210	3eqtri 2648	. . . . . . . 8 ;;; ;
256	20, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255	decma2c 11568	. . . . . . 7 ;;; ; ;; ;; ;;;;
257	41	dec0h 11522	. . . . . . . . 9 ;
258	188, 16	eqeltri 2697	. . . . . . . . . 10
259	64	mul02i 10225	. . . . . . . . . . . 12
260	259, 188	oveq12i 6662	. . . . . . . . . . 11
261	260, 188	eqtri 2644	. . . . . . . . . 10
262	20, 3, 258, 226, 2, 122, 261	decrmanc 11576	. . . . . . . . 9 ; ;
263		6p3e9 11170	. . . . . . . . . 10
264	16, 15, 41, 103, 263	decaddi 11579	. . . . . . . . 9 ;
265	35, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264	decmac 11566	. . . . . . . 8 ;; ;;
266	153, 64, 191	addcomli 10228	. . . . . . . . 9 ;
267	20, 2, 28, 95, 232, 16, 266	decaddci 11580	. . . . . . . 8 ;
268	36, 15, 28, 219, 2, 16, 41, 265, 267	decrmac 11577	. . . . . . 7 ;;; ;;;
269	35, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268	decma2c 11568	. . . . . 6 ;;; ;; ;;; ;;;;;
270	50	mul02i 10225	. . . . . . . . . . 11
271	270	oveq1i 6660	. . . . . . . . . 10
272	271, 132	eqtri 2644	. . . . . . . . 9
273	20, 3, 20, 226, 15, 53, 272	decrmanc 11576	. . . . . . . 8 ; ;;
274		4p3e7 11163	. . . . . . . . 9
275	20, 2, 41, 96, 274	decaddi 11579	. . . . . . . 8 ;
276	35, 2, 41, 222, 15, 28, 20, 273, 275	decrmac 11577	. . . . . . 7 ;; ;;;
277	15, 36, 15, 219, 15, 41, 276, 90	decmul1c 11587	. . . . . 6 ;;; ;;;;
278	37, 36, 15, 219, 15, 221, 269, 277	decmul2c 11589	. . . . 5 ;;; ;;; ;;;;;;
279	218, 278	eqtr4i 2647	. . . 4 ;;; ;;; ;;; ;;;
280	8, 9, 31, 34, 37, 30, 178, 183, 279	mod2xi 15773	. . 3 ; ;;;
281	23	nn0cni 11304	. . . 4 ;
282		eqid 2622	. . . . 5 ; ;
283	20, 22, 3, 282, 3, 181, 241	decmul1 11585	. . . 4 ; ;;
284	281, 51, 283	mulcomli 10047	. . 3 ; ;;
285		eqid 2622	. . . . 5 ;; ;;
286	20, 12	deccl 11512	. . . . 5 ;
287		eqid 2622	. . . . . . 7 ; ;
288		eqid 2622	. . . . . . 7 ; ;
289	199	oveq1i 6660	. . . . . . . 8
290	289, 125	eqtri 2644	. . . . . . 7
291	15, 16, 20, 12, 287, 288, 290, 148	decaddc2 11575	. . . . . 6 ; ; ;
292	61, 3	eqeltri 2697	. . . . . . . 8
293		eqid 2622	. . . . . . . 8 ;; ;;
294		eqid 2622	. . . . . . . . 9 ; ;
295	122	oveq1i 6660	. . . . . . . . . 10
296		8p3e11 11612	. . . . . . . . . 10 ;
297	295, 296	eqtri 2644	. . . . . . . . 9 ;
298		8t4e32 11656	. . . . . . . . . 10 ;
299	41, 20, 20, 298, 88	decaddi 11579	. . . . . . . . 9 ;
300	20, 24, 20, 294, 2, 2, 41, 297, 299	decrmac 11577	. . . . . . . 8 ; ;;
301	95, 61	oveq12i 6662	. . . . . . . . 9 ;
302	38	nn0cni 11304	. . . . . . . . . 10 ;
303	302	addid1i 10223	. . . . . . . . 9 ; ;
304	301, 303	eqtri 2644	. . . . . . . 8 ;
305	25, 15, 292, 293, 2, 2, 20, 300, 304	decrmac 11577	. . . . . . 7 ;; ;;;
306	26	nn0cni 11304	. . . . . . . . . 10 ;;
307	306	mul01i 10226	. . . . . . . . 9 ;;
308	307	oveq1i 6660	. . . . . . . 8 ;;
309	308, 75, 58	3eqtri 2648	. . . . . . 7 ;; ;
310	2, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309	decma2c 11568	. . . . . 6 ;; ; ;;;;
311	307	oveq1i 6660	. . . . . . 7 ;;
312	311, 61, 62	3eqtri 2648	. . . . . 6 ;; ;
313	4, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312	decma2c 11568	. . . . 5 ;; ;; ; ; ;;;;;
314	230	mulid1i 10042	. . . . . . . 8
315	16, 20, 24, 294, 24, 109, 314	decmul1 11585	. . . . . . 7 ; ;
316	20, 24, 125, 315	decsuc 11535	. . . . . 6 ; ;
317	50	mulid1i 10042	. . . . . . . 8
318	317	oveq1i 6660	. . . . . . 7
319	318, 92	eqtri 2644	. . . . . 6 ;
320	25, 15, 2, 293, 16, 3, 16, 316, 319	decrmac 11577	. . . . 5 ;; ;;
321	5, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320	decma2c 11568	. . . 4 ;; ;; ;;;;;;
322	16, 16	deccl 11512	. . . . . . . . 9 ;
323	322, 2	deccl 11512	. . . . . . . 8 ;;
324	323, 2	deccl 11512	. . . . . . 7 ;;;
325	324, 12	deccl 11512	. . . . . 6 ;;;;
326	28, 2	deccl 11512	. . . . . . . 8 ;
327	326, 12	deccl 11512	. . . . . . 7 ;;
328		eqid 2622	. . . . . . . 8 ; ;
329		eqid 2622	. . . . . . . 8 ;; ;;
330	326	nn0cni 11304	. . . . . . . . . 10 ;
331	330	addid1i 10223	. . . . . . . . 9 ; ;
332	153	addid1i 10223	. . . . . . . . . . 11
333	332, 28	eqeltri 2697	. . . . . . . . . 10
334	10	nn0cni 11304	. . . . . . . . . . . 12 ;
335	334	mulid1i 10042	. . . . . . . . . . 11 ; ;
336	16, 3, 188, 335	decsuc 11535	. . . . . . . . . 10 ; ;
337	153	mulid1i 10042	. . . . . . . . . . . 12
338	337, 332	oveq12i 6662	. . . . . . . . . . 11
339		7p7e14 11609	. . . . . . . . . . 11 ;
340	338, 339	eqtri 2644	. . . . . . . . . 10 ;
341	10, 28, 333, 186, 16, 2, 16, 336, 340	decrmac 11577	. . . . . . . . 9 ;; ;;
342	69	mul02i 10225	. . . . . . . . . . 11
343	342	oveq1i 6660	. . . . . . . . . 10
344	64	addid2i 10224	. . . . . . . . . 10
345	343, 344, 114	3eqtri 2648	. . . . . . . . 9 ;
346	29, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345	decmac 11566	. . . . . . . 8 ;;; ; ;;;
347	30	nn0cni 11304	. . . . . . . . . . 11 ;;;
348	347	mul01i 10226	. . . . . . . . . 10 ;;;
349	348	oveq1i 6660	. . . . . . . . 9 ;;;
350	349, 75, 58	3eqtri 2648	. . . . . . . 8 ;;; ;
351	16, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350	decma2c 11568	. . . . . . 7 ;;; ; ;; ;;;;
352		dfdec10 11497	. . . . . . . . . 10 ; ;
353	352	eqcomi 2631	. . . . . . . . 9 ; ;
354		7t7e49 11653	. . . . . . . . 9 ;
355	28, 10, 28, 186, 12, 2, 353, 354	decmul1c 11587	. . . . . . . 8 ;; ;;
356	153	mul02i 10225	. . . . . . . 8
357	28, 29, 3, 184, 3, 355, 356	decmul1 11585	. . . . . . 7 ;;; ;;;
358	30, 10, 28, 186, 3, 327, 351, 357	decmul2c 11589	. . . . . 6 ;;; ;; ;;;;;
359	325, 3, 3, 358, 61	decaddi 11579	. . . . 5 ;;; ;; ;;;;;
360	348, 62	eqtri 2644	. . . . 5 ;;; ;
361	30, 29, 3, 184, 3, 3, 359, 360	decmul2c 11589	. . . 4 ;;; ;;; ;;;;;;
362	321, 361	eqtr4i 2647	. . 3 ;; ;; ;;; ;;;
363	8, 9, 23, 27, 30, 18, 280, 284, 362	mod2xi 15773	. 2 ;; ;;
364	11	nn0cni 11304	. . 3 ;;
365		eqid 2622	. . . 4 ;; ;;
366	20, 10, 3, 365, 3, 173, 241	decmul1 11585	. . 3 ;; ;;
367	364, 51, 366	mulcomli 10047	. 2 ;; ;;
368		eqid 2622	. . . 4 ;; ;;
369		eqid 2622	. . . . . 6 ; ;
370	12, 3, 12, 369, 75	decaddi 11579	. . . . 5 ; ;
371		eqid 2622	. . . . . . 7 ; ;
372		6p1e7 11156	. . . . . . . 8
373		9t4e36 11665	. . . . . . . 8 ;
374	41, 15, 372, 373	decsuc 11535	. . . . . . 7 ;
375	103, 61	oveq12i 6662	. . . . . . . 8 ;
376	16, 15	deccl 11512	. . . . . . . . . 10 ;
377	376	nn0cni 11304	. . . . . . . . 9 ;
378	377	addid1i 10223	. . . . . . . 8 ; ;
379	375, 378	eqtri 2644	. . . . . . 7 ;
380	12, 2, 292, 371, 2, 15, 16, 374, 379	decrmac 11577	. . . . . 6 ; ;;
381	238	mul01i 10226	. . . . . . . 8 ;
382	381	oveq1i 6660	. . . . . . 7 ;
383	382, 75, 58	3eqtri 2648	. . . . . 6 ; ;
384	2, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383	decma2c 11568	. . . . 5 ; ; ;;;
385	4, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383	decma2c 11568	. . . 4 ; ;; ; ;;;;
386	56	mulid1i 10042	. . . . 5
387	64	mulid1i 10042	. . . . . . 7
388	387	oveq1i 6660	. . . . . 6
389	388, 203	eqtri 2644	. . . . 5
390	12, 2, 20, 371, 16, 386, 389	decrmanc 11576	. . . 4 ; ;
391	5, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390	decma2c 11568	. . 3 ; ;; ;;;;;
392	38, 22	deccl 11512	. . . 4 ;;
393		eqid 2622	. . . . 5 ;; ;;
394	50, 51, 199	addcomli 10228	. . . . . . 7
395	20, 2, 15, 16, 165, 287, 394, 101	decadd 11570	. . . . . 6 ; ; ;
396		8p2e10 11610	. . . . . . 7 ;
397	41, 15, 372, 90	decsuc 11535	. . . . . . 7 ;
398	50	mulid2i 10043	. . . . . . . . 9
399	398	oveq1i 6660	. . . . . . . 8
400	50	addid1i 10223	. . . . . . . 8
401	399, 400	eqtri 2644	. . . . . . 7
402	15, 16, 16, 3, 287, 396, 15, 397, 401	decma 11564	. . . . . 6 ; ;;
403	17, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99	decmac 11566	. . . . 5 ;; ; ; ;;;
404	16, 15, 16, 287, 16, 317, 78	decmul1 11585	. . . . . 6 ; ;
405	387	oveq1i 6660	. . . . . . 7
406	405, 98	eqtri 2644	. . . . . 6
407	17, 2, 22, 285, 16, 404, 406	decrmanc 11576	. . . . 5 ;; ;;
408	15, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407	decma2c 11568	. . . 4 ;; ; ;; ;;;;
409	65	oveq1i 6660	. . . . . . 7
410	409, 101	eqtri 2644	. . . . . 6
411	15, 16, 16, 287, 2, 95, 410	decrmanc 11576	. . . . 5 ; ;;
412	2, 17, 2, 285, 15, 16, 411, 103	decmul1c 11587	. . . 4 ;; ;;;
413	18, 17, 2, 285, 15, 392, 408, 412	decmul2c 11589	. . 3 ;; ;; ;;;;;
414	391, 413	eqtr4i 2647	. 2 ; ;; ;; ;;
415	8, 9, 11, 14, 18, 21, 363, 367, 414	mod2xi 15773	1 ;; ;;

Colors of variables: wff setvar class

Syntax hints:

wceq 1483 (class class class)co 6650

cc0 9936

c1 9937

caddc 9939

cmul 9941

cn 11020

c2 11070

c3 11071

c4 11072

c5 11073

c6 11074

c7 11075

c8 11076

c9 11077

cn0 11292 ;cdc 11493

cmo 12668

cexp 12860

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861

This theorem is referenced by: 4001lem2 15849 4001lem3 15850

W3C validator