4001lem2 - Metamath Proof Explorer

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

Theorem 4001lem2 15161

Description: Lemma for 4001prm 15164. 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 10916	. . . . . 6
3		0nn0 10912	. . . . . 6
4	2, 3	deccl 11093	. . . . 5 ;
5	4, 3	deccl 11093	. . . 4 ;;
6		1nn 10647	. . . 4
7	5, 6	decnncl 11092	. . 3 ;;;
8	1, 7	eqeltri 2535	. 2
9		2nn 10795	. 2
10		9nn0 10921	. . . . 5
11	2, 10	deccl 11093	. . . 4 ;
12	11, 3	deccl 11093	. . 3 ;;
13	12	nn0zi 10990	. 2 ;;
14		1nn0 10913	. . . . 5
15	14, 2	deccl 11093	. . . 4 ;
16	15, 3	deccl 11093	. . 3 ;;
17	16, 14	deccl 11093	. 2 ;;;
18		2nn0 10914	. . . . 5
19		3nn0 10915	. . . . 5
20	18, 19	deccl 11093	. . . 4 ;
21	20, 14	deccl 11093	. . 3 ;;
22	21, 14	deccl 11093	. 2 ;;;
23	18, 3	deccl 11093	. . . 4 ;
24	23, 3	deccl 11093	. . 3 ;;
25	23, 19	deccl 11093	. . . 4 ;;
26	25	nn0zi 10990	. . 3 ;;
27	10, 3	deccl 11093	. . . 4 ;
28	27, 18	deccl 11093	. . 3 ;;
29	1	4001lem1 15160	. . 3 ;; ;;
30		eqid 2461	. . . 4 ;; ;;
31		eqid 2461	. . . . . . 7 ; ;
32		2t2e4 10787	. . . . . . . . 9
33	32	oveq1i 6324	. . . . . . . 8
34		4cn 10714	. . . . . . . . 9
35	34	addid1i 9845	. . . . . . . 8
36	33, 35	eqtri 2483	. . . . . . 7
37		2cn 10707	. . . . . . . . 9
38	37	mul01i 9848	. . . . . . . 8
39	3	dec0h 11095	. . . . . . . 8 ;
40	38, 39	eqtri 2483	. . . . . . 7 ;
41	18, 18, 3, 31, 3, 3, 36, 40	decmul2c 11127	. . . . . 6 ; ;
42	41	oveq1i 6324	. . . . 5 ; ;
43	4	nn0cni 10909	. . . . . 6 ;
44	43	addid1i 9845	. . . . 5 ; ;
45	42, 44	eqtri 2483	. . . 4 ; ;
46	18, 23, 3, 30, 3, 3, 45, 40	decmul2c 11127	. . 3 ;; ;;
47		eqid 2461	. . . . 5 ;;; ;;;
48		6nn0 10918	. . . . . . 7
49	14, 48	deccl 11093	. . . . . 6 ;
50		eqid 2461	. . . . . 6 ;; ;;
51		eqid 2461	. . . . . . 7 ;; ;;
52		eqid 2461	. . . . . . . 8 ; ;
53		4p2e6 10772	. . . . . . . 8
54	14, 2, 18, 52, 53	decaddi 11123	. . . . . . 7 ; ;
55		00id 9833	. . . . . . 7
56	15, 3, 18, 3, 51, 31, 54, 55	decadd 11120	. . . . . 6 ;; ; ;;
57		eqid 2461	. . . . . . 7 ; ;
58	49	nn0cni 10909	. . . . . . . 8 ;
59	58	addid1i 9845	. . . . . . 7 ; ;
60		eqid 2461	. . . . . . . 8 ;; ;;
61		ax-1cn 9622	. . . . . . . . . 10
62	61	addid1i 9845	. . . . . . . . 9
63	14	dec0h 11095	. . . . . . . . 9 ;
64	62, 63	eqtri 2483	. . . . . . . 8 ;
65	61	addid2i 9846	. . . . . . . . . 10
66	65, 63	eqtri 2483	. . . . . . . . 9 ;
67		4t2e8 10791	. . . . . . . . . . . 12
68	34, 37, 67	mulcomli 9675	. . . . . . . . . . 11
69	68, 55	oveq12i 6326	. . . . . . . . . 10
70		8cn 10722	. . . . . . . . . . 11
71	70	addid1i 9845	. . . . . . . . . 10
72	69, 71	eqtri 2483	. . . . . . . . 9
73	34	mul02i 9847	. . . . . . . . . . 11
74	73	oveq1i 6324	. . . . . . . . . 10
75	74, 65, 63	3eqtri 2487	. . . . . . . . 9 ;
76	18, 3, 3, 14, 31, 66, 2, 14, 3, 72, 75	decmac 11118	. . . . . . . 8 ; ;
77		2p1e3 10761	. . . . . . . . 9
78		3cn 10711	. . . . . . . . . 10
79		4t3e12 11151	. . . . . . . . . 10 ;
80	34, 78, 79	mulcomli 9675	. . . . . . . . 9 ;
81	14, 18, 77, 80	decsuc 11102	. . . . . . . 8 ;
82	23, 19, 3, 14, 60, 64, 2, 19, 14, 76, 81	decmac 11118	. . . . . . 7 ;; ;;
83	25	nn0cni 10909	. . . . . . . . . 10 ;;
84	83	mul01i 9848	. . . . . . . . 9 ;;
85	84	oveq1i 6324	. . . . . . . 8 ;;
86		6cn 10718	. . . . . . . . 9
87	86	addid2i 9846	. . . . . . . 8
88	48	dec0h 11095	. . . . . . . 8 ;
89	85, 87, 88	3eqtri 2487	. . . . . . 7 ;; ;
90	2, 3, 14, 48, 57, 59, 25, 48, 3, 82, 89	decma2c 11119	. . . . . 6 ;; ; ; ;;;
91	84	oveq1i 6324	. . . . . . 7 ;;
92	91, 55, 39	3eqtri 2487	. . . . . 6 ;; ;
93	4, 3, 49, 3, 50, 56, 25, 3, 3, 90, 92	decma2c 11119	. . . . 5 ;; ;; ;; ; ;;;;
94	55, 39	eqtri 2483	. . . . . . 7 ;
95	37	mulid1i 9670	. . . . . . . . 9
96	95, 55	oveq12i 6326	. . . . . . . 8
97	37	addid1i 9845	. . . . . . . 8
98	96, 97	eqtri 2483	. . . . . . 7
99	61	mul02i 9847	. . . . . . . . 9
100	99	oveq1i 6324	. . . . . . . 8
101	100, 55, 39	3eqtri 2487	. . . . . . 7 ;
102	18, 3, 3, 3, 31, 94, 14, 3, 3, 98, 101	decmac 11118	. . . . . 6 ; ;
103	78	mulid1i 9670	. . . . . . . 8
104	103	oveq1i 6324	. . . . . . 7
105		3p1e4 10763	. . . . . . 7
106	2	dec0h 11095	. . . . . . 7 ;
107	104, 105, 106	3eqtri 2487	. . . . . 6 ;
108	23, 19, 3, 14, 60, 63, 14, 2, 3, 102, 107	decmac 11118	. . . . 5 ;; ;;
109	5, 14, 16, 14, 1, 47, 25, 2, 23, 93, 108	decma2c 11119	. . . 4 ;; ;;; ;;;;;
110		eqid 2461	. . . . 5 ;; ;;
111		8nn0 10920	. . . . . . 7
112	14, 111	deccl 11093	. . . . . 6 ;
113	112, 3	deccl 11093	. . . . 5 ;;
114		eqid 2461	. . . . . 6 ; ;
115		eqid 2461	. . . . . 6 ;; ;;
116	112	nn0cni 10909	. . . . . . . 8 ;
117	116	addid1i 9845	. . . . . . 7 ; ;
118		1p2e3 10762	. . . . . . . . 9
119	19	dec0h 11095	. . . . . . . . 9 ;
120	118, 119	eqtri 2483	. . . . . . . 8 ;
121		9t9e81 11181	. . . . . . . . . 10 ;
122	121	oveq1i 6324	. . . . . . . . 9 ;
123	111, 14	deccl 11093	. . . . . . . . . . 11 ;
124	123	nn0cni 10909	. . . . . . . . . 10 ;
125	124	addid1i 9845	. . . . . . . . 9 ; ;
126	122, 125	eqtri 2483	. . . . . . . 8 ;
127		9cn 10724	. . . . . . . . . . 11
128	127	mul02i 9847	. . . . . . . . . 10
129	128	oveq1i 6324	. . . . . . . . 9
130	78	addid2i 9846	. . . . . . . . 9
131	129, 130	eqtri 2483	. . . . . . . 8
132	10, 3, 3, 19, 114, 120, 10, 126, 131	decma 11117	. . . . . . 7 ; ;;
133		9t2e18 11174	. . . . . . . . 9 ;
134	127, 37, 133	mulcomli 9675	. . . . . . . 8 ;
135		1p1e2 10750	. . . . . . . 8
136		8p8e16 11140	. . . . . . . 8 ;
137	14, 111, 111, 134, 135, 48, 136	decaddci 11124	. . . . . . 7 ;
138	27, 18, 14, 111, 110, 117, 10, 48, 18, 132, 137	decmac 11118	. . . . . 6 ;; ; ;;;
139	28	nn0cni 10909	. . . . . . . . 9 ;;
140	139	mul01i 9848	. . . . . . . 8 ;;
141	140	oveq1i 6324	. . . . . . 7 ;;
142	141, 55, 39	3eqtri 2487	. . . . . 6 ;; ;
143	10, 3, 112, 3, 114, 115, 28, 3, 3, 138, 142	decma2c 11119	. . . . 5 ;; ; ;; ;;;;
144	133	oveq1i 6324	. . . . . . . . . 10 ;
145	144, 117	eqtri 2483	. . . . . . . . 9 ;
146	37	mul02i 9847	. . . . . . . . . 10
147	146, 39	eqtri 2483	. . . . . . . . 9 ;
148	18, 10, 3, 114, 3, 3, 145, 147	decmul1c 11126	. . . . . . . 8 ; ;;
149	148	oveq1i 6324	. . . . . . 7 ; ;;
150	113	nn0cni 10909	. . . . . . . 8 ;;
151	150	addid1i 9845	. . . . . . 7 ;; ;;
152	149, 151	eqtri 2483	. . . . . 6 ; ;;
153	32, 106	eqtri 2483	. . . . . 6 ;
154	18, 27, 18, 110, 2, 3, 152, 153	decmul1c 11126	. . . . 5 ;; ;;;
155	28, 27, 18, 110, 2, 113, 143, 154	decmul2c 11127	. . . 4 ;; ;; ;;;;;
156	109, 155	eqtr4i 2486	. . 3 ;; ;;; ;; ;;
157	8, 9, 24, 26, 28, 17, 29, 46, 156	mod2xi 15089	. 2 ;; ;;;
158	68	oveq1i 6324	. . . . . . 7
159	158, 71	eqtri 2483	. . . . . 6
160	18, 2, 3, 57, 3, 3, 159, 40	decmul2c 11127	. . . . 5 ; ;
161	160	oveq1i 6324	. . . 4 ; ;
162	111, 3	deccl 11093	. . . . . 6 ;
163	162	nn0cni 10909	. . . . 5 ;
164	163	addid1i 9845	. . . 4 ; ;
165	161, 164	eqtri 2483	. . 3 ; ;
166	18, 4, 3, 50, 3, 3, 165, 40	decmul2c 11127	. 2 ;; ;;
167		eqid 2461	. . . 4 ;;; ;;;
168	18, 111	deccl 11093	. . . . 5 ;
169		eqid 2461	. . . . . 6 ;; ;;
170		eqid 2461	. . . . . 6 ; ;
171		7nn0 10919	. . . . . . 7
172		7p1e8 10767	. . . . . . 7
173		eqid 2461	. . . . . . . 8 ; ;
174		4p3e7 10773	. . . . . . . . 9
175	34, 78, 174	addcomli 9850	. . . . . . . 8
176	18, 19, 2, 173, 175	decaddi 11123	. . . . . . 7 ; ;
177	18, 171, 172, 176	decsuc 11102	. . . . . 6 ; ;
178		9p1e10 10769	. . . . . . 7
179	127, 61, 178	addcomli 9850	. . . . . 6
180	20, 14, 2, 10, 169, 170, 177, 179	decaddc2 11122	. . . . 5 ;; ; ;;
181	168	nn0cni 10909	. . . . . . 7 ;
182	181	addid1i 9845	. . . . . 6 ; ;
183		eqid 2461	. . . . . . 7 ;; ;;
184	18	dec0h 11095	. . . . . . . 8 ;
185	97, 184	eqtri 2483	. . . . . . 7 ;
186	130	oveq2i 6325	. . . . . . . . 9
187		4t4e16 11152	. . . . . . . . . 10 ;
188		6p3e9 10780	. . . . . . . . . 10
189	14, 48, 19, 187, 188	decaddi 11123	. . . . . . . . 9 ;
190	186, 189	eqtri 2483	. . . . . . . 8 ;
191		9t4e36 11176	. . . . . . . . . 10 ;
192	191	oveq1i 6324	. . . . . . . . 9 ;
193	19, 48	deccl 11093	. . . . . . . . . . 11 ;
194	193	nn0cni 10909	. . . . . . . . . 10 ;
195	194	addid1i 9845	. . . . . . . . 9 ; ;
196	192, 195	eqtri 2483	. . . . . . . 8 ;
197	2, 10, 3, 3, 170, 94, 2, 48, 19, 190, 196	decmac 11118	. . . . . . 7 ; ;;
198	73	oveq1i 6324	. . . . . . . 8
199	37	addid2i 9846	. . . . . . . 8
200	198, 199, 184	3eqtri 2487	. . . . . . 7 ;
201	11, 3, 3, 18, 183, 185, 2, 18, 3, 197, 200	decmac 11118	. . . . . 6 ;; ;;;
202	12	nn0cni 10909	. . . . . . . . 9 ;;
203	202	mul01i 9848	. . . . . . . 8 ;;
204	203	oveq1i 6324	. . . . . . 7 ;;
205	70	addid2i 9846	. . . . . . 7
206	111	dec0h 11095	. . . . . . 7 ;
207	204, 205, 206	3eqtri 2487	. . . . . 6 ;; ;
208	2, 3, 18, 111, 57, 182, 12, 111, 3, 201, 207	decma2c 11119	. . . . 5 ;; ; ; ;;;;
209	203	oveq1i 6324	. . . . . 6 ;;
210	209, 55, 39	3eqtri 2487	. . . . 5 ;; ;
211	4, 3, 168, 3, 50, 180, 12, 3, 3, 208, 210	decma2c 11119	. . . 4 ;; ;; ;; ; ;;;;;
212	34	mulid1i 9670	. . . . . . . 8
213	212, 55	oveq12i 6326	. . . . . . 7
214	213, 35	eqtri 2483	. . . . . 6
215	127	mulid1i 9670	. . . . . . . 8
216	215	oveq1i 6324	. . . . . . 7
217	127	addid1i 9845	. . . . . . 7
218	10	dec0h 11095	. . . . . . 7 ;
219	216, 217, 218	3eqtri 2487	. . . . . 6 ;
220	2, 10, 3, 3, 170, 94, 14, 10, 3, 214, 219	decmac 11118	. . . . 5 ; ;
221	99	oveq1i 6324	. . . . . 6
222	221, 65, 63	3eqtri 2487	. . . . 5 ;
223	11, 3, 3, 14, 183, 63, 14, 14, 3, 220, 222	decmac 11118	. . . 4 ;; ;;
224	5, 14, 21, 14, 1, 167, 12, 14, 11, 211, 223	decma2c 11119	. . 3 ;; ;;; ;;;;;;
225	15	nn0cni 10909	. . . . . . 7 ;
226	225	addid1i 9845	. . . . . 6 ; ;
227		5nn0 10917	. . . . . . . 8
228	227, 48	deccl 11093	. . . . . . 7 ;
229	228, 3	deccl 11093	. . . . . 6 ;;
230		eqid 2461	. . . . . . . 8 ;; ;;
231	228	nn0cni 10909	. . . . . . . . 9 ;
232	231	addid2i 9846	. . . . . . . 8 ; ;
233	3, 14, 228, 3, 63, 230, 232, 62	decadd 11120	. . . . . . 7 ;; ;;
234	231	addid1i 9845	. . . . . . . 8 ; ;
235		5cn 10716	. . . . . . . . . . 11
236	235	addid1i 9845	. . . . . . . . . 10
237	227	dec0h 11095	. . . . . . . . . 10 ;
238	236, 237	eqtri 2483	. . . . . . . . 9 ;
239	61	mulid1i 9670	. . . . . . . . . . 11
240	239, 55	oveq12i 6326	. . . . . . . . . 10
241	240, 62	eqtri 2483	. . . . . . . . 9
242	212	oveq1i 6324	. . . . . . . . . 10
243		5p4e9 10777	. . . . . . . . . . 11
244	235, 34, 243	addcomli 9850	. . . . . . . . . 10
245	242, 244, 218	3eqtri 2487	. . . . . . . . 9 ;
246	14, 2, 3, 227, 52, 238, 14, 10, 3, 241, 245	decmac 11118	. . . . . . . 8 ; ;
247	99	oveq1i 6324	. . . . . . . . 9
248	247, 87, 88	3eqtri 2487	. . . . . . . 8 ;
249	15, 3, 227, 48, 51, 234, 14, 48, 3, 246, 248	decmac 11118	. . . . . . 7 ;; ; ;;
250	239	oveq1i 6324	. . . . . . . 8
251	250, 135, 184	3eqtri 2487	. . . . . . 7 ;
252	16, 14, 228, 14, 47, 233, 14, 18, 3, 249, 251	decmac 11118	. . . . . 6 ;;; ;; ;;;
253	34	mulid2i 9671	. . . . . . . . . . 11
254	253, 65	oveq12i 6326	. . . . . . . . . 10
255		4p1e5 10764	. . . . . . . . . 10
256	254, 255	eqtri 2483	. . . . . . . . 9
257	187	oveq1i 6324	. . . . . . . . . 10 ;
258	257, 59	eqtri 2483	. . . . . . . . 9 ;
259	14, 2, 3, 3, 52, 94, 2, 48, 14, 256, 258	decmac 11118	. . . . . . . 8 ; ;
260	73	oveq1i 6324	. . . . . . . . 9
261	260, 55, 39	3eqtri 2487	. . . . . . . 8 ;
262	15, 3, 3, 3, 51, 94, 2, 3, 3, 259, 261	decmac 11118	. . . . . . 7 ;; ;;
263	253	oveq1i 6324	. . . . . . . 8
264		4p4e8 10774	. . . . . . . 8
265	263, 264, 206	3eqtri 2487	. . . . . . 7 ;
266	16, 14, 3, 2, 47, 106, 2, 111, 3, 262, 265	decmac 11118	. . . . . 6 ;;; ;;;
267	14, 2, 14, 2, 52, 226, 17, 111, 229, 252, 266	decma2c 11119	. . . . 5 ;;; ; ; ;;;;
268	17	nn0cni 10909	. . . . . . . 8 ;;;
269	268	mul01i 9848	. . . . . . 7 ;;;
270	269	oveq1i 6324	. . . . . 6 ;;;
271	270, 55, 39	3eqtri 2487	. . . . 5 ;;; ;
272	15, 3, 15, 3, 51, 51, 17, 3, 3, 267, 271	decma2c 11119	. . . 4 ;;; ;; ;; ;;;;;
273	268	mulid1i 9670	. . . 4 ;;; ;;;
274	17, 16, 14, 47, 14, 16, 272, 273	decmul2c 11127	. . 3 ;;; ;;; ;;;;;;
275	224, 274	eqtr4i 2486	. 2 ;; ;;; ;;; ;;;
276	8, 9, 5, 13, 17, 22, 157, 166, 275	mod2xi 15089	1 ;; ;;;

Colors of variables: wff setvar class

Syntax hints:

wceq 1454 (class class class)co 6314

cc0 9564

c1 9565

caddc 9567

cmul 9569

cn 10636

c2 10686

c3 10687

c4 10688

c5 10689

c6 10690

c7 10691

c8 10692

c9 10693

c10 10694 ;cdc 11079

cmo 12127

cexp 12303

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609 ax-cnex 9620 ax-resscn 9621 ax-1cn 9622 ax-icn 9623 ax-addcl 9624 ax-addrcl 9625 ax-mulcl 9626 ax-mulrcl 9627 ax-mulcom 9628 ax-addass 9629 ax-mulass 9630 ax-distr 9631 ax-i2m1 9632 ax-1ne0 9633 ax-1rid 9634 ax-rnegex 9635 ax-rrecex 9636 ax-cnre 9637 ax-pre-lttri 9638 ax-pre-lttrn 9639 ax-pre-ltadd 9640 ax-pre-mulgt0 9641 ax-pre-sup 9642

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-nel 2635 df-ral 2753 df-rex 2754 df-reu 2755 df-rmo 2756 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-pss 3431 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-tp 3984 df-op 3986 df-uni 4212 df-iun 4293 df-br 4416 df-opab 4475 df-mpt 4476 df-tr 4511 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-lim 5446 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-riota 6276 df-ov 6317 df-oprab 6318 df-mpt2 6319 df-om 6719 df-2nd 6820 df-wrecs 7053 df-recs 7115 df-rdg 7153 df-er 7388 df-en 7595 df-dom 7596 df-sdom 7597 df-sup 7981 df-inf 7982 df-pnf 9702 df-mnf 9703 df-xr 9704 df-ltxr 9705 df-le 9706 df-sub 9887 df-neg 9888 df-div 10297 df-nn 10637 df-2 10695 df-3 10696 df-4 10697 df-5 10698 df-6 10699 df-7 10700 df-8 10701 df-9 10702 df-10 10703 df-n0 10898 df-z 10966 df-dec 11080 df-uz 11188 df-rp 11331 df-fl 12059 df-mod 12128 df-seq 12245 df-exp 12304

This theorem is referenced by: 4001lem3 15162 4001lem4 15163

W3C validator