4001lem2 - Metamath Proof Explorer

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

Theorem 4001lem2 14711

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

and

. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)

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

**Assertion**
Ref	Expression
4001lem2	;; ;;;

**Proof of Theorem 4001lem2**
Step	Hyp	Ref	Expression
1		4001prm.1	. . 3 ;;;
2		4nn0 10810	. . . . . 6
3		0nn0 10806	. . . . . 6
4	2, 3	deccl 10990	. . . . 5 ;
5	4, 3	deccl 10990	. . . 4 ;;
6		1nn 10542	. . . 4
7	5, 6	decnncl 10989	. . 3 ;;;
8	1, 7	eqeltri 2538	. 2
9		2nn 10689	. 2
10		9nn0 10815	. . . . 5
11	2, 10	deccl 10990	. . . 4 ;
12	11, 3	deccl 10990	. . 3 ;;
13	12	nn0zi 10885	. 2 ;;
14		1nn0 10807	. . . . 5
15	14, 2	deccl 10990	. . . 4 ;
16	15, 3	deccl 10990	. . 3 ;;
17	16, 14	deccl 10990	. 2 ;;;
18		2nn0 10808	. . . . 5
19		3nn0 10809	. . . . 5
20	18, 19	deccl 10990	. . . 4 ;
21	20, 14	deccl 10990	. . 3 ;;
22	21, 14	deccl 10990	. 2 ;;;
23	18, 3	deccl 10990	. . . 4 ;
24	23, 3	deccl 10990	. . 3 ;;
25	23, 19	deccl 10990	. . . 4 ;;
26	25	nn0zi 10885	. . 3 ;;
27	10, 3	deccl 10990	. . . 4 ;
28	27, 18	deccl 10990	. . 3 ;;
29	1	4001lem1 14710	. . 3 ;; ;;
30		eqid 2454	. . . 4 ;; ;;
31		eqid 2454	. . . . . . 7 ; ;
32		2t2e4 10681	. . . . . . . . 9
33	32	oveq1i 6280	. . . . . . . 8
34		4cn 10609	. . . . . . . . 9
35	34	addid1i 9756	. . . . . . . 8
36	33, 35	eqtri 2483	. . . . . . 7
37		2cn 10602	. . . . . . . . 9
38	37	mul01i 9759	. . . . . . . 8
39	3	dec0h 10992	. . . . . . . 8 ;
40	38, 39	eqtri 2483	. . . . . . 7 ;
41	18, 18, 3, 31, 3, 3, 36, 40	decmul2c 11024	. . . . . 6 ; ;
42	41	oveq1i 6280	. . . . 5 ; ;
43	4	nn0cni 10803	. . . . . 6 ;
44	43	addid1i 9756	. . . . 5 ; ;
45	42, 44	eqtri 2483	. . . 4 ; ;
46	18, 23, 3, 30, 3, 3, 45, 40	decmul2c 11024	. . 3 ;; ;;
47		eqid 2454	. . . . 5 ;;; ;;;
48		6nn0 10812	. . . . . . 7
49	14, 48	deccl 10990	. . . . . 6 ;
50		eqid 2454	. . . . . 6 ;; ;;
51		eqid 2454	. . . . . . 7 ;; ;;
52		eqid 2454	. . . . . . . 8 ; ;
53		4p2e6 10666	. . . . . . . 8
54	14, 2, 18, 52, 53	decaddi 11020	. . . . . . 7 ; ;
55		00id 9744	. . . . . . 7
56	15, 3, 18, 3, 51, 31, 54, 55	decadd 11017	. . . . . 6 ;; ; ;;
57		eqid 2454	. . . . . . 7 ; ;
58	49	nn0cni 10803	. . . . . . . 8 ;
59	58	addid1i 9756	. . . . . . 7 ; ;
60		eqid 2454	. . . . . . . 8 ;; ;;
61		ax-1cn 9539	. . . . . . . . . 10
62	61	addid1i 9756	. . . . . . . . 9
63	14	dec0h 10992	. . . . . . . . 9 ;
64	62, 63	eqtri 2483	. . . . . . . 8 ;
65	61	addid2i 9757	. . . . . . . . . 10
66	65, 63	eqtri 2483	. . . . . . . . 9 ;
67		4t2e8 10685	. . . . . . . . . . . 12
68	34, 37, 67	mulcomli 9592	. . . . . . . . . . 11
69	68, 55	oveq12i 6282	. . . . . . . . . 10
70		8cn 10617	. . . . . . . . . . 11
71	70	addid1i 9756	. . . . . . . . . 10
72	69, 71	eqtri 2483	. . . . . . . . 9
73	34	mul02i 9758	. . . . . . . . . . 11
74	73	oveq1i 6280	. . . . . . . . . 10
75	74, 65, 63	3eqtri 2487	. . . . . . . . 9 ;
76	18, 3, 3, 14, 31, 66, 2, 14, 3, 72, 75	decmac 11015	. . . . . . . 8 ; ;
77		2p1e3 10655	. . . . . . . . 9
78		3cn 10606	. . . . . . . . . 10
79		4t3e12 11048	. . . . . . . . . 10 ;
80	34, 78, 79	mulcomli 9592	. . . . . . . . 9 ;
81	14, 18, 77, 80	decsuc 10999	. . . . . . . 8 ;
82	23, 19, 3, 14, 60, 64, 2, 19, 14, 76, 81	decmac 11015	. . . . . . 7 ;; ;;
83	25	nn0cni 10803	. . . . . . . . . 10 ;;
84	83	mul01i 9759	. . . . . . . . 9 ;;
85	84	oveq1i 6280	. . . . . . . 8 ;;
86		6cn 10613	. . . . . . . . 9
87	86	addid2i 9757	. . . . . . . 8
88	48	dec0h 10992	. . . . . . . 8 ;
89	85, 87, 88	3eqtri 2487	. . . . . . 7 ;; ;
90	2, 3, 14, 48, 57, 59, 25, 48, 3, 82, 89	decma2c 11016	. . . . . 6 ;; ; ; ;;;
91	84	oveq1i 6280	. . . . . . 7 ;;
92	91, 55, 39	3eqtri 2487	. . . . . 6 ;; ;
93	4, 3, 49, 3, 50, 56, 25, 3, 3, 90, 92	decma2c 11016	. . . . 5 ;; ;; ;; ; ;;;;
94	55, 39	eqtri 2483	. . . . . . 7 ;
95	37	mulid1i 9587	. . . . . . . . 9
96	95, 55	oveq12i 6282	. . . . . . . 8
97	37	addid1i 9756	. . . . . . . 8
98	96, 97	eqtri 2483	. . . . . . 7
99	61	mul02i 9758	. . . . . . . . 9
100	99	oveq1i 6280	. . . . . . . 8
101	100, 55, 39	3eqtri 2487	. . . . . . 7 ;
102	18, 3, 3, 3, 31, 94, 14, 3, 3, 98, 101	decmac 11015	. . . . . 6 ; ;
103	78	mulid1i 9587	. . . . . . . 8
104	103	oveq1i 6280	. . . . . . 7
105		3p1e4 10657	. . . . . . 7
106	2	dec0h 10992	. . . . . . 7 ;
107	104, 105, 106	3eqtri 2487	. . . . . 6 ;
108	23, 19, 3, 14, 60, 63, 14, 2, 3, 102, 107	decmac 11015	. . . . 5 ;; ;;
109	5, 14, 16, 14, 1, 47, 25, 2, 23, 93, 108	decma2c 11016	. . . 4 ;; ;;; ;;;;;
110		eqid 2454	. . . . 5 ;; ;;
111		8nn0 10814	. . . . . . 7
112	14, 111	deccl 10990	. . . . . 6 ;
113	112, 3	deccl 10990	. . . . 5 ;;
114		eqid 2454	. . . . . 6 ; ;
115		eqid 2454	. . . . . 6 ;; ;;
116	112	nn0cni 10803	. . . . . . . 8 ;
117	116	addid1i 9756	. . . . . . 7 ; ;
118		1p2e3 10656	. . . . . . . . 9
119	19	dec0h 10992	. . . . . . . . 9 ;
120	118, 119	eqtri 2483	. . . . . . . 8 ;
121		9t9e81 11078	. . . . . . . . . 10 ;
122	121	oveq1i 6280	. . . . . . . . 9 ;
123	111, 14	deccl 10990	. . . . . . . . . . 11 ;
124	123	nn0cni 10803	. . . . . . . . . 10 ;
125	124	addid1i 9756	. . . . . . . . 9 ; ;
126	122, 125	eqtri 2483	. . . . . . . 8 ;
127		9cn 10619	. . . . . . . . . . 11
128	127	mul02i 9758	. . . . . . . . . 10
129	128	oveq1i 6280	. . . . . . . . 9
130	78	addid2i 9757	. . . . . . . . 9
131	129, 130	eqtri 2483	. . . . . . . 8
132	10, 3, 3, 19, 114, 120, 10, 126, 131	decma 11014	. . . . . . 7 ; ;;
133		9t2e18 11071	. . . . . . . . 9 ;
134	127, 37, 133	mulcomli 9592	. . . . . . . 8 ;
135		1p1e2 10645	. . . . . . . 8
136		8p8e16 11037	. . . . . . . 8 ;
137	14, 111, 111, 134, 135, 48, 136	decaddci 11021	. . . . . . 7 ;
138	27, 18, 14, 111, 110, 117, 10, 48, 18, 132, 137	decmac 11015	. . . . . 6 ;; ; ;;;
139	28	nn0cni 10803	. . . . . . . . 9 ;;
140	139	mul01i 9759	. . . . . . . 8 ;;
141	140	oveq1i 6280	. . . . . . 7 ;;
142	141, 55, 39	3eqtri 2487	. . . . . 6 ;; ;
143	10, 3, 112, 3, 114, 115, 28, 3, 3, 138, 142	decma2c 11016	. . . . 5 ;; ; ;; ;;;;
144	133	oveq1i 6280	. . . . . . . . . 10 ;
145	144, 117	eqtri 2483	. . . . . . . . 9 ;
146	37	mul02i 9758	. . . . . . . . . 10
147	146, 39	eqtri 2483	. . . . . . . . 9 ;
148	18, 10, 3, 114, 3, 3, 145, 147	decmul1c 11023	. . . . . . . 8 ; ;;
149	148	oveq1i 6280	. . . . . . 7 ; ;;
150	113	nn0cni 10803	. . . . . . . 8 ;;
151	150	addid1i 9756	. . . . . . 7 ;; ;;
152	149, 151	eqtri 2483	. . . . . 6 ; ;;
153	32, 106	eqtri 2483	. . . . . 6 ;
154	18, 27, 18, 110, 2, 3, 152, 153	decmul1c 11023	. . . . 5 ;; ;;;
155	28, 27, 18, 110, 2, 113, 143, 154	decmul2c 11024	. . . 4 ;; ;; ;;;;;
156	109, 155	eqtr4i 2486	. . 3 ;; ;;; ;; ;;
157	8, 9, 24, 26, 28, 17, 29, 46, 156	mod2xi 14642	. 2 ;; ;;;
158	68	oveq1i 6280	. . . . . . 7
159	158, 71	eqtri 2483	. . . . . 6
160	18, 2, 3, 57, 3, 3, 159, 40	decmul2c 11024	. . . . 5 ; ;
161	160	oveq1i 6280	. . . 4 ; ;
162	111, 3	deccl 10990	. . . . . 6 ;
163	162	nn0cni 10803	. . . . 5 ;
164	163	addid1i 9756	. . . 4 ; ;
165	161, 164	eqtri 2483	. . 3 ; ;
166	18, 4, 3, 50, 3, 3, 165, 40	decmul2c 11024	. 2 ;; ;;
167		eqid 2454	. . . 4 ;;; ;;;
168	18, 111	deccl 10990	. . . . 5 ;
169		eqid 2454	. . . . . 6 ;; ;;
170		eqid 2454	. . . . . 6 ; ;
171		7nn0 10813	. . . . . . 7
172		7p1e8 10661	. . . . . . 7
173		eqid 2454	. . . . . . . 8 ; ;
174		4p3e7 10667	. . . . . . . . 9
175	34, 78, 174	addcomli 9761	. . . . . . . 8
176	18, 19, 2, 173, 175	decaddi 11020	. . . . . . 7 ; ;
177	18, 171, 172, 176	decsuc 10999	. . . . . 6 ; ;
178		9p1e10 10663	. . . . . . 7
179	127, 61, 178	addcomli 9761	. . . . . 6
180	20, 14, 2, 10, 169, 170, 177, 179	decaddc2 11019	. . . . 5 ;; ; ;;
181	168	nn0cni 10803	. . . . . . 7 ;
182	181	addid1i 9756	. . . . . 6 ; ;
183		eqid 2454	. . . . . . 7 ;; ;;
184	18	dec0h 10992	. . . . . . . 8 ;
185	97, 184	eqtri 2483	. . . . . . 7 ;
186	130	oveq2i 6281	. . . . . . . . 9
187		4t4e16 11049	. . . . . . . . . 10 ;
188		6p3e9 10674	. . . . . . . . . 10
189	14, 48, 19, 187, 188	decaddi 11020	. . . . . . . . 9 ;
190	186, 189	eqtri 2483	. . . . . . . 8 ;
191		9t4e36 11073	. . . . . . . . . 10 ;
192	191	oveq1i 6280	. . . . . . . . 9 ;
193	19, 48	deccl 10990	. . . . . . . . . . 11 ;
194	193	nn0cni 10803	. . . . . . . . . 10 ;
195	194	addid1i 9756	. . . . . . . . 9 ; ;
196	192, 195	eqtri 2483	. . . . . . . 8 ;
197	2, 10, 3, 3, 170, 94, 2, 48, 19, 190, 196	decmac 11015	. . . . . . 7 ; ;;
198	73	oveq1i 6280	. . . . . . . 8
199	37	addid2i 9757	. . . . . . . 8
200	198, 199, 184	3eqtri 2487	. . . . . . 7 ;
201	11, 3, 3, 18, 183, 185, 2, 18, 3, 197, 200	decmac 11015	. . . . . 6 ;; ;;;
202	12	nn0cni 10803	. . . . . . . . 9 ;;
203	202	mul01i 9759	. . . . . . . 8 ;;
204	203	oveq1i 6280	. . . . . . 7 ;;
205	70	addid2i 9757	. . . . . . 7
206	111	dec0h 10992	. . . . . . 7 ;
207	204, 205, 206	3eqtri 2487	. . . . . 6 ;; ;
208	2, 3, 18, 111, 57, 182, 12, 111, 3, 201, 207	decma2c 11016	. . . . 5 ;; ; ; ;;;;
209	203	oveq1i 6280	. . . . . 6 ;;
210	209, 55, 39	3eqtri 2487	. . . . 5 ;; ;
211	4, 3, 168, 3, 50, 180, 12, 3, 3, 208, 210	decma2c 11016	. . . 4 ;; ;; ;; ; ;;;;;
212	34	mulid1i 9587	. . . . . . . 8
213	212, 55	oveq12i 6282	. . . . . . 7
214	213, 35	eqtri 2483	. . . . . 6
215	127	mulid1i 9587	. . . . . . . 8
216	215	oveq1i 6280	. . . . . . 7
217	127	addid1i 9756	. . . . . . 7
218	10	dec0h 10992	. . . . . . 7 ;
219	216, 217, 218	3eqtri 2487	. . . . . 6 ;
220	2, 10, 3, 3, 170, 94, 14, 10, 3, 214, 219	decmac 11015	. . . . 5 ; ;
221	99	oveq1i 6280	. . . . . 6
222	221, 65, 63	3eqtri 2487	. . . . 5 ;
223	11, 3, 3, 14, 183, 63, 14, 14, 3, 220, 222	decmac 11015	. . . 4 ;; ;;
224	5, 14, 21, 14, 1, 167, 12, 14, 11, 211, 223	decma2c 11016	. . 3 ;; ;;; ;;;;;;
225	15	nn0cni 10803	. . . . . . 7 ;
226	225	addid1i 9756	. . . . . 6 ; ;
227		5nn0 10811	. . . . . . . 8
228	227, 48	deccl 10990	. . . . . . 7 ;
229	228, 3	deccl 10990	. . . . . 6 ;;
230		eqid 2454	. . . . . . . 8 ;; ;;
231	228	nn0cni 10803	. . . . . . . . 9 ;
232	231	addid2i 9757	. . . . . . . 8 ; ;
233	3, 14, 228, 3, 63, 230, 232, 62	decadd 11017	. . . . . . 7 ;; ;;
234	231	addid1i 9756	. . . . . . . 8 ; ;
235		5cn 10611	. . . . . . . . . . 11
236	235	addid1i 9756	. . . . . . . . . 10
237	227	dec0h 10992	. . . . . . . . . 10 ;
238	236, 237	eqtri 2483	. . . . . . . . 9 ;
239	61	mulid1i 9587	. . . . . . . . . . 11
240	239, 55	oveq12i 6282	. . . . . . . . . 10
241	240, 62	eqtri 2483	. . . . . . . . 9
242	212	oveq1i 6280	. . . . . . . . . 10
243		5p4e9 10671	. . . . . . . . . . 11
244	235, 34, 243	addcomli 9761	. . . . . . . . . 10
245	242, 244, 218	3eqtri 2487	. . . . . . . . 9 ;
246	14, 2, 3, 227, 52, 238, 14, 10, 3, 241, 245	decmac 11015	. . . . . . . 8 ; ;
247	99	oveq1i 6280	. . . . . . . . 9
248	247, 87, 88	3eqtri 2487	. . . . . . . 8 ;
249	15, 3, 227, 48, 51, 234, 14, 48, 3, 246, 248	decmac 11015	. . . . . . 7 ;; ; ;;
250	239	oveq1i 6280	. . . . . . . 8
251	250, 135, 184	3eqtri 2487	. . . . . . 7 ;
252	16, 14, 228, 14, 47, 233, 14, 18, 3, 249, 251	decmac 11015	. . . . . 6 ;;; ;; ;;;
253	34	mulid2i 9588	. . . . . . . . . . 11
254	253, 65	oveq12i 6282	. . . . . . . . . 10
255		4p1e5 10658	. . . . . . . . . 10
256	254, 255	eqtri 2483	. . . . . . . . 9
257	187	oveq1i 6280	. . . . . . . . . 10 ;
258	257, 59	eqtri 2483	. . . . . . . . 9 ;
259	14, 2, 3, 3, 52, 94, 2, 48, 14, 256, 258	decmac 11015	. . . . . . . 8 ; ;
260	73	oveq1i 6280	. . . . . . . . 9
261	260, 55, 39	3eqtri 2487	. . . . . . . 8 ;
262	15, 3, 3, 3, 51, 94, 2, 3, 3, 259, 261	decmac 11015	. . . . . . 7 ;; ;;
263	253	oveq1i 6280	. . . . . . . 8
264		4p4e8 10668	. . . . . . . 8
265	263, 264, 206	3eqtri 2487	. . . . . . 7 ;
266	16, 14, 3, 2, 47, 106, 2, 111, 3, 262, 265	decmac 11015	. . . . . 6 ;;; ;;;
267	14, 2, 14, 2, 52, 226, 17, 111, 229, 252, 266	decma2c 11016	. . . . 5 ;;; ; ; ;;;;
268	17	nn0cni 10803	. . . . . . . 8 ;;;
269	268	mul01i 9759	. . . . . . 7 ;;;
270	269	oveq1i 6280	. . . . . 6 ;;;
271	270, 55, 39	3eqtri 2487	. . . . 5 ;;; ;
272	15, 3, 15, 3, 51, 51, 17, 3, 3, 267, 271	decma2c 11016	. . . 4 ;;; ;; ;; ;;;;;
273	268	mulid1i 9587	. . . 4 ;;; ;;;
274	17, 16, 14, 47, 14, 16, 272, 273	decmul2c 11024	. . 3 ;;; ;;; ;;;;;;
275	224, 274	eqtr4i 2486	. 2 ;; ;;; ;;; ;;;
276	8, 9, 5, 13, 17, 22, 157, 166, 275	mod2xi 14642	1 ;; ;;;

Colors of variables: wff setvar class

Syntax hints:

wceq 1398 (class class class)co 6270

cc0 9481

c1 9482

caddc 9484

cmul 9486

cn 10531

c2 10581

c3 10582

c4 10583

c5 10584

c6 10585

c7 10586

c8 10587

c9 10588

c10 10589 ;cdc 10976

cmo 11978

cexp 12151

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-2nd 6774 df-recs 7034 df-rdg 7068 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-sup 7893 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-nn 10532 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10977 df-uz 11083 df-rp 11222 df-fl 11910 df-mod 11979 df-seq 12093 df-exp 12152

This theorem is referenced by: 4001lem3 14712 4001lem4 14713

W3C validator