4001lem2 - Metamath Proof Explorer

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

Theorem 4001lem2 14473

Description: Lemma for 4001prm 14476. 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 10805	. . . . . 6
3		0nn0 10801	. . . . . 6
4	2, 3	deccl 10981	. . . . 5 ;
5	4, 3	deccl 10981	. . . 4 ;;
6		1nn 10538	. . . 4
7	5, 6	decnncl 10980	. . 3 ;;;
8	1, 7	eqeltri 2546	. 2
9		2nn 10684	. 2
10		9nn0 10810	. . . . 5
11	2, 10	deccl 10981	. . . 4 ;
12	11, 3	deccl 10981	. . 3 ;;
13	12	nn0zi 10880	. 2 ;;
14		1nn0 10802	. . . . 5
15	14, 2	deccl 10981	. . . 4 ;
16	15, 3	deccl 10981	. . 3 ;;
17	16, 14	deccl 10981	. 2 ;;;
18		2nn0 10803	. . . . 5
19		3nn0 10804	. . . . 5
20	18, 19	deccl 10981	. . . 4 ;
21	20, 14	deccl 10981	. . 3 ;;
22	21, 14	deccl 10981	. 2 ;;;
23	18, 3	deccl 10981	. . . 4 ;
24	23, 3	deccl 10981	. . 3 ;;
25	23, 19	deccl 10981	. . . 4 ;;
26	25	nn0zi 10880	. . 3 ;;
27	10, 3	deccl 10981	. . . 4 ;
28	27, 18	deccl 10981	. . 3 ;;
29	1	4001lem1 14472	. . 3 ;; ;;
30		eqid 2462	. . . 4 ;; ;;
31		eqid 2462	. . . . . . 7 ; ;
32		2t2e4 10676	. . . . . . . . 9
33	32	oveq1i 6287	. . . . . . . 8
34		4cn 10604	. . . . . . . . 9
35	34	addid1i 9757	. . . . . . . 8
36	33, 35	eqtri 2491	. . . . . . 7
37		2cn 10597	. . . . . . . . 9
38	37	mul01i 9760	. . . . . . . 8
39	3	dec0h 10983	. . . . . . . 8 ;
40	38, 39	eqtri 2491	. . . . . . 7 ;
41	18, 18, 3, 31, 3, 3, 36, 40	decmul2c 11015	. . . . . 6 ; ;
42	41	oveq1i 6287	. . . . 5 ; ;
43	4	nn0cni 10798	. . . . . 6 ;
44	43	addid1i 9757	. . . . 5 ; ;
45	42, 44	eqtri 2491	. . . 4 ; ;
46	18, 23, 3, 30, 3, 3, 45, 40	decmul2c 11015	. . 3 ;; ;;
47		eqid 2462	. . . . 5 ;;; ;;;
48		6nn0 10807	. . . . . . 7
49	14, 48	deccl 10981	. . . . . 6 ;
50		eqid 2462	. . . . . 6 ;; ;;
51		eqid 2462	. . . . . . 7 ;; ;;
52		eqid 2462	. . . . . . . 8 ; ;
53		4p2e6 10661	. . . . . . . 8
54	14, 2, 18, 52, 53	decaddi 11011	. . . . . . 7 ; ;
55		00id 9745	. . . . . . 7
56	15, 3, 18, 3, 51, 31, 54, 55	decadd 11008	. . . . . 6 ;; ; ;;
57		eqid 2462	. . . . . . 7 ; ;
58	49	nn0cni 10798	. . . . . . . 8 ;
59	58	addid1i 9757	. . . . . . 7 ; ;
60		eqid 2462	. . . . . . . 8 ;; ;;
61		ax-1cn 9541	. . . . . . . . . 10
62	61	addid1i 9757	. . . . . . . . 9
63	14	dec0h 10983	. . . . . . . . 9 ;
64	62, 63	eqtri 2491	. . . . . . . 8 ;
65	61	addid2i 9758	. . . . . . . . . 10
66	65, 63	eqtri 2491	. . . . . . . . 9 ;
67		4t2e8 10680	. . . . . . . . . . . 12
68	34, 37, 67	mulcomli 9594	. . . . . . . . . . 11
69	68, 55	oveq12i 6289	. . . . . . . . . 10
70		8cn 10612	. . . . . . . . . . 11
71	70	addid1i 9757	. . . . . . . . . 10
72	69, 71	eqtri 2491	. . . . . . . . 9
73	34	mul02i 9759	. . . . . . . . . . 11
74	73	oveq1i 6287	. . . . . . . . . 10
75	74, 65, 63	3eqtri 2495	. . . . . . . . 9 ;
76	18, 3, 3, 14, 31, 66, 2, 14, 3, 72, 75	decmac 11006	. . . . . . . 8 ; ;
77		2p1e3 10650	. . . . . . . . 9
78		3cn 10601	. . . . . . . . . 10
79		4t3e12 11039	. . . . . . . . . 10 ;
80	34, 78, 79	mulcomli 9594	. . . . . . . . 9 ;
81	14, 18, 77, 80	decsuc 10990	. . . . . . . 8 ;
82	23, 19, 3, 14, 60, 64, 2, 19, 14, 76, 81	decmac 11006	. . . . . . 7 ;; ;;
83	25	nn0cni 10798	. . . . . . . . . 10 ;;
84	83	mul01i 9760	. . . . . . . . 9 ;;
85	84	oveq1i 6287	. . . . . . . 8 ;;
86		6cn 10608	. . . . . . . . 9
87	86	addid2i 9758	. . . . . . . 8
88	48	dec0h 10983	. . . . . . . 8 ;
89	85, 87, 88	3eqtri 2495	. . . . . . 7 ;; ;
90	2, 3, 14, 48, 57, 59, 25, 48, 3, 82, 89	decma2c 11007	. . . . . 6 ;; ; ; ;;;
91	84	oveq1i 6287	. . . . . . 7 ;;
92	91, 55, 39	3eqtri 2495	. . . . . 6 ;; ;
93	4, 3, 49, 3, 50, 56, 25, 3, 3, 90, 92	decma2c 11007	. . . . 5 ;; ;; ;; ; ;;;;
94	55, 39	eqtri 2491	. . . . . . 7 ;
95	37	mulid1i 9589	. . . . . . . . 9
96	95, 55	oveq12i 6289	. . . . . . . 8
97	37	addid1i 9757	. . . . . . . 8
98	96, 97	eqtri 2491	. . . . . . 7
99	61	mul02i 9759	. . . . . . . . 9
100	99	oveq1i 6287	. . . . . . . 8
101	100, 55, 39	3eqtri 2495	. . . . . . 7 ;
102	18, 3, 3, 3, 31, 94, 14, 3, 3, 98, 101	decmac 11006	. . . . . 6 ; ;
103	78	mulid1i 9589	. . . . . . . 8
104	103	oveq1i 6287	. . . . . . 7
105		3p1e4 10652	. . . . . . 7
106	2	dec0h 10983	. . . . . . 7 ;
107	104, 105, 106	3eqtri 2495	. . . . . 6 ;
108	23, 19, 3, 14, 60, 63, 14, 2, 3, 102, 107	decmac 11006	. . . . 5 ;; ;;
109	5, 14, 16, 14, 1, 47, 25, 2, 23, 93, 108	decma2c 11007	. . . 4 ;; ;;; ;;;;;
110		eqid 2462	. . . . 5 ;; ;;
111		8nn0 10809	. . . . . . 7
112	14, 111	deccl 10981	. . . . . 6 ;
113	112, 3	deccl 10981	. . . . 5 ;;
114		eqid 2462	. . . . . 6 ; ;
115		eqid 2462	. . . . . 6 ;; ;;
116	112	nn0cni 10798	. . . . . . . 8 ;
117	116	addid1i 9757	. . . . . . 7 ; ;
118		1p2e3 10651	. . . . . . . . 9
119	19	dec0h 10983	. . . . . . . . 9 ;
120	118, 119	eqtri 2491	. . . . . . . 8 ;
121		9t9e81 11069	. . . . . . . . . 10 ;
122	121	oveq1i 6287	. . . . . . . . 9 ;
123	111, 14	deccl 10981	. . . . . . . . . . 11 ;
124	123	nn0cni 10798	. . . . . . . . . 10 ;
125	124	addid1i 9757	. . . . . . . . 9 ; ;
126	122, 125	eqtri 2491	. . . . . . . 8 ;
127		9cn 10614	. . . . . . . . . . 11
128	127	mul02i 9759	. . . . . . . . . 10
129	128	oveq1i 6287	. . . . . . . . 9
130	78	addid2i 9758	. . . . . . . . 9
131	129, 130	eqtri 2491	. . . . . . . 8
132	10, 3, 3, 19, 114, 120, 10, 126, 131	decma 11005	. . . . . . 7 ; ;;
133		9t2e18 11062	. . . . . . . . 9 ;
134	127, 37, 133	mulcomli 9594	. . . . . . . 8 ;
135		1p1e2 10640	. . . . . . . 8
136		8p8e16 11028	. . . . . . . 8 ;
137	14, 111, 111, 134, 135, 48, 136	decaddci 11012	. . . . . . 7 ;
138	27, 18, 14, 111, 110, 117, 10, 48, 18, 132, 137	decmac 11006	. . . . . 6 ;; ; ;;;
139	28	nn0cni 10798	. . . . . . . . 9 ;;
140	139	mul01i 9760	. . . . . . . 8 ;;
141	140	oveq1i 6287	. . . . . . 7 ;;
142	141, 55, 39	3eqtri 2495	. . . . . 6 ;; ;
143	10, 3, 112, 3, 114, 115, 28, 3, 3, 138, 142	decma2c 11007	. . . . 5 ;; ; ;; ;;;;
144	133	oveq1i 6287	. . . . . . . . . 10 ;
145	144, 117	eqtri 2491	. . . . . . . . 9 ;
146	37	mul02i 9759	. . . . . . . . . 10
147	146, 39	eqtri 2491	. . . . . . . . 9 ;
148	18, 10, 3, 114, 3, 3, 145, 147	decmul1c 11014	. . . . . . . 8 ; ;;
149	148	oveq1i 6287	. . . . . . 7 ; ;;
150	113	nn0cni 10798	. . . . . . . 8 ;;
151	150	addid1i 9757	. . . . . . 7 ;; ;;
152	149, 151	eqtri 2491	. . . . . 6 ; ;;
153	32, 106	eqtri 2491	. . . . . 6 ;
154	18, 27, 18, 110, 2, 3, 152, 153	decmul1c 11014	. . . . 5 ;; ;;;
155	28, 27, 18, 110, 2, 113, 143, 154	decmul2c 11015	. . . 4 ;; ;; ;;;;;
156	109, 155	eqtr4i 2494	. . 3 ;; ;;; ;; ;;
157	8, 9, 24, 26, 28, 17, 29, 46, 156	mod2xi 14405	. 2 ;; ;;;
158	68	oveq1i 6287	. . . . . . 7
159	158, 71	eqtri 2491	. . . . . 6
160	18, 2, 3, 57, 3, 3, 159, 40	decmul2c 11015	. . . . 5 ; ;
161	160	oveq1i 6287	. . . 4 ; ;
162	111, 3	deccl 10981	. . . . . 6 ;
163	162	nn0cni 10798	. . . . 5 ;
164	163	addid1i 9757	. . . 4 ; ;
165	161, 164	eqtri 2491	. . 3 ; ;
166	18, 4, 3, 50, 3, 3, 165, 40	decmul2c 11015	. 2 ;; ;;
167		eqid 2462	. . . 4 ;;; ;;;
168	18, 111	deccl 10981	. . . . 5 ;
169		eqid 2462	. . . . . 6 ;; ;;
170		eqid 2462	. . . . . 6 ; ;
171		7nn0 10808	. . . . . . 7
172		7p1e8 10656	. . . . . . 7
173		eqid 2462	. . . . . . . 8 ; ;
174		4p3e7 10662	. . . . . . . . 9
175	34, 78, 174	addcomli 9762	. . . . . . . 8
176	18, 19, 2, 173, 175	decaddi 11011	. . . . . . 7 ; ;
177	18, 171, 172, 176	decsuc 10990	. . . . . 6 ; ;
178		9p1e10 10658	. . . . . . 7
179	127, 61, 178	addcomli 9762	. . . . . 6
180	20, 14, 2, 10, 169, 170, 177, 179	decaddc2 11010	. . . . 5 ;; ; ;;
181	168	nn0cni 10798	. . . . . . 7 ;
182	181	addid1i 9757	. . . . . 6 ; ;
183		eqid 2462	. . . . . . 7 ;; ;;
184	18	dec0h 10983	. . . . . . . 8 ;
185	97, 184	eqtri 2491	. . . . . . 7 ;
186	130	oveq2i 6288	. . . . . . . . 9
187		4t4e16 11040	. . . . . . . . . 10 ;
188		6p3e9 10669	. . . . . . . . . 10
189	14, 48, 19, 187, 188	decaddi 11011	. . . . . . . . 9 ;
190	186, 189	eqtri 2491	. . . . . . . 8 ;
191		9t4e36 11064	. . . . . . . . . 10 ;
192	191	oveq1i 6287	. . . . . . . . 9 ;
193	19, 48	deccl 10981	. . . . . . . . . . 11 ;
194	193	nn0cni 10798	. . . . . . . . . 10 ;
195	194	addid1i 9757	. . . . . . . . 9 ; ;
196	192, 195	eqtri 2491	. . . . . . . 8 ;
197	2, 10, 3, 3, 170, 94, 2, 48, 19, 190, 196	decmac 11006	. . . . . . 7 ; ;;
198	73	oveq1i 6287	. . . . . . . 8
199	37	addid2i 9758	. . . . . . . 8
200	198, 199, 184	3eqtri 2495	. . . . . . 7 ;
201	11, 3, 3, 18, 183, 185, 2, 18, 3, 197, 200	decmac 11006	. . . . . 6 ;; ;;;
202	12	nn0cni 10798	. . . . . . . . 9 ;;
203	202	mul01i 9760	. . . . . . . 8 ;;
204	203	oveq1i 6287	. . . . . . 7 ;;
205	70	addid2i 9758	. . . . . . 7
206	111	dec0h 10983	. . . . . . 7 ;
207	204, 205, 206	3eqtri 2495	. . . . . 6 ;; ;
208	2, 3, 18, 111, 57, 182, 12, 111, 3, 201, 207	decma2c 11007	. . . . 5 ;; ; ; ;;;;
209	203	oveq1i 6287	. . . . . 6 ;;
210	209, 55, 39	3eqtri 2495	. . . . 5 ;; ;
211	4, 3, 168, 3, 50, 180, 12, 3, 3, 208, 210	decma2c 11007	. . . 4 ;; ;; ;; ; ;;;;;
212	34	mulid1i 9589	. . . . . . . 8
213	212, 55	oveq12i 6289	. . . . . . 7
214	213, 35	eqtri 2491	. . . . . 6
215	127	mulid1i 9589	. . . . . . . 8
216	215	oveq1i 6287	. . . . . . 7
217	127	addid1i 9757	. . . . . . 7
218	10	dec0h 10983	. . . . . . 7 ;
219	216, 217, 218	3eqtri 2495	. . . . . 6 ;
220	2, 10, 3, 3, 170, 94, 14, 10, 3, 214, 219	decmac 11006	. . . . 5 ; ;
221	99	oveq1i 6287	. . . . . 6
222	221, 65, 63	3eqtri 2495	. . . . 5 ;
223	11, 3, 3, 14, 183, 63, 14, 14, 3, 220, 222	decmac 11006	. . . 4 ;; ;;
224	5, 14, 21, 14, 1, 167, 12, 14, 11, 211, 223	decma2c 11007	. . 3 ;; ;;; ;;;;;;
225	15	nn0cni 10798	. . . . . . 7 ;
226	225	addid1i 9757	. . . . . 6 ; ;
227		5nn0 10806	. . . . . . . 8
228	227, 48	deccl 10981	. . . . . . 7 ;
229	228, 3	deccl 10981	. . . . . 6 ;;
230		eqid 2462	. . . . . . . 8 ;; ;;
231	228	nn0cni 10798	. . . . . . . . 9 ;
232	231	addid2i 9758	. . . . . . . 8 ; ;
233	3, 14, 228, 3, 63, 230, 232, 62	decadd 11008	. . . . . . 7 ;; ;;
234	231	addid1i 9757	. . . . . . . 8 ; ;
235		5cn 10606	. . . . . . . . . . 11
236	235	addid1i 9757	. . . . . . . . . 10
237	227	dec0h 10983	. . . . . . . . . 10 ;
238	236, 237	eqtri 2491	. . . . . . . . 9 ;
239	61	mulid1i 9589	. . . . . . . . . . 11
240	239, 55	oveq12i 6289	. . . . . . . . . 10
241	240, 62	eqtri 2491	. . . . . . . . 9
242	212	oveq1i 6287	. . . . . . . . . 10
243		5p4e9 10666	. . . . . . . . . . 11
244	235, 34, 243	addcomli 9762	. . . . . . . . . 10
245	242, 244, 218	3eqtri 2495	. . . . . . . . 9 ;
246	14, 2, 3, 227, 52, 238, 14, 10, 3, 241, 245	decmac 11006	. . . . . . . 8 ; ;
247	99	oveq1i 6287	. . . . . . . . 9
248	247, 87, 88	3eqtri 2495	. . . . . . . 8 ;
249	15, 3, 227, 48, 51, 234, 14, 48, 3, 246, 248	decmac 11006	. . . . . . 7 ;; ; ;;
250	239	oveq1i 6287	. . . . . . . 8
251	250, 135, 184	3eqtri 2495	. . . . . . 7 ;
252	16, 14, 228, 14, 47, 233, 14, 18, 3, 249, 251	decmac 11006	. . . . . 6 ;;; ;; ;;;
253	34	mulid2i 9590	. . . . . . . . . . 11
254	253, 65	oveq12i 6289	. . . . . . . . . 10
255		4p1e5 10653	. . . . . . . . . 10
256	254, 255	eqtri 2491	. . . . . . . . 9
257	187	oveq1i 6287	. . . . . . . . . 10 ;
258	257, 59	eqtri 2491	. . . . . . . . 9 ;
259	14, 2, 3, 3, 52, 94, 2, 48, 14, 256, 258	decmac 11006	. . . . . . . 8 ; ;
260	73	oveq1i 6287	. . . . . . . . 9
261	260, 55, 39	3eqtri 2495	. . . . . . . 8 ;
262	15, 3, 3, 3, 51, 94, 2, 3, 3, 259, 261	decmac 11006	. . . . . . 7 ;; ;;
263	253	oveq1i 6287	. . . . . . . 8
264		4p4e8 10663	. . . . . . . 8
265	263, 264, 206	3eqtri 2495	. . . . . . 7 ;
266	16, 14, 3, 2, 47, 106, 2, 111, 3, 262, 265	decmac 11006	. . . . . 6 ;;; ;;;
267	14, 2, 14, 2, 52, 226, 17, 111, 229, 252, 266	decma2c 11007	. . . . 5 ;;; ; ; ;;;;
268	17	nn0cni 10798	. . . . . . . 8 ;;;
269	268	mul01i 9760	. . . . . . 7 ;;;
270	269	oveq1i 6287	. . . . . 6 ;;;
271	270, 55, 39	3eqtri 2495	. . . . 5 ;;; ;
272	15, 3, 15, 3, 51, 51, 17, 3, 3, 267, 271	decma2c 11007	. . . 4 ;;; ;; ;; ;;;;;
273	268	mulid1i 9589	. . . 4 ;;; ;;;
274	17, 16, 14, 47, 14, 16, 272, 273	decmul2c 11015	. . 3 ;;; ;;; ;;;;;;
275	224, 274	eqtr4i 2494	. 2 ;; ;;; ;;; ;;;
276	8, 9, 5, 13, 17, 22, 157, 166, 275	mod2xi 14405	1 ;; ;;;

Colors of variables: wff setvar class

Syntax hints:

wceq 1374 (class class class)co 6277

cc0 9483

c1 9484

caddc 9486

cmul 9488

cn 10527

c2 10576

c3 10577

c4 10578

c5 10579

c6 10580

c7 10581

c8 10582

c9 10583

c10 10584 ;cdc 10967

cmo 11954

cexp 12124

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440 ax-sep 4563 ax-nul 4571 ax-pow 4620 ax-pr 4681 ax-un 6569 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-pre-sup 9561

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2274 df-mo 2275 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-ne 2659 df-nel 2660 df-ral 2814 df-rex 2815 df-reu 2816 df-rmo 2817 df-rab 2818 df-v 3110 df-sbc 3327 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3781 df-if 3935 df-pw 4007 df-sn 4023 df-pr 4025 df-tp 4027 df-op 4029 df-uni 4241 df-iun 4322 df-br 4443 df-opab 4501 df-mpt 4502 df-tr 4536 df-eprel 4786 df-id 4790 df-po 4795 df-so 4796 df-fr 4833 df-we 4835 df-ord 4876 df-on 4877 df-lim 4878 df-suc 4879 df-xp 5000 df-rel 5001 df-cnv 5002 df-co 5003 df-dm 5004 df-rn 5005 df-res 5006 df-ima 5007 df-iota 5544 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6674 df-2nd 6777 df-recs 7034 df-rdg 7068 df-er 7303 df-en 7509 df-dom 7510 df-sdom 7511 df-sup 7892 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9798 df-neg 9799 df-div 10198 df-nn 10528 df-2 10585 df-3 10586 df-4 10587 df-5 10588 df-6 10589 df-7 10590 df-8 10591 df-9 10592 df-10 10593 df-n0 10787 df-z 10856 df-dec 10968 df-uz 11074 df-rp 11212 df-fl 11888 df-mod 11955 df-seq 12066 df-exp 12125

This theorem is referenced by: 4001lem3 14474 4001lem4 14475

W3C validator