prmpwdvds - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > prmpwdvds		Unicode version

Theorem prmpwdvds 12285

Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)

**Assertion**
Ref	Expression
prmpwdvds	$/\$ $/\$ $/\$ $/\$ $/\$

Proof of Theorem prmpwdvds Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 5849	. . . . . 6
2	1	breq2d 3994	. . . . 5
3		oveq1 5849	. . . . . . 7
4	3	breq2d 3994	. . . . . 6
5	4	notbid 657	. . . . 5
6	2, 5	anbi12d 465	. . . 4 $/\$ $/\$
7	6	imbi1d 230	. . 3 $/\$ $/\$
8		oveq2 5850	. . . . . . . . . . . . 13
9	8	oveq2d 5858	. . . . . . . . . . . 12
10	9	breq2d 3994	. . . . . . . . . . 11
11		oveq1 5849	. . . . . . . . . . . . . . 15
12	11	oveq2d 5858	. . . . . . . . . . . . . 14
13	12	oveq2d 5858	. . . . . . . . . . . . 13
14	13	breq2d 3994	. . . . . . . . . . . 12
15	14	notbid 657	. . . . . . . . . . 11
16	10, 15	anbi12d 465	. . . . . . . . . 10 $/\$ $/\$
17	8	breq1d 3992	. . . . . . . . . 10
18	16, 17	imbi12d 233	. . . . . . . . 9 $/\$ $/\$
19	18	ralbidv 2466	. . . . . . . 8 $/\$ $/\$
20	19	imbi2d 229	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
21		oveq2 5850	. . . . . . . . . . . . 13
22	21	oveq2d 5858	. . . . . . . . . . . 12
23	22	breq2d 3994	. . . . . . . . . . 11
24		oveq1 5849	. . . . . . . . . . . . . . 15
25	24	oveq2d 5858	. . . . . . . . . . . . . 14
26	25	oveq2d 5858	. . . . . . . . . . . . 13
27	26	breq2d 3994	. . . . . . . . . . . 12
28	27	notbid 657	. . . . . . . . . . 11
29	23, 28	anbi12d 465	. . . . . . . . . 10 $/\$ $/\$
30	21	breq1d 3992	. . . . . . . . . 10
31	29, 30	imbi12d 233	. . . . . . . . 9 $/\$ $/\$
32	31	ralbidv 2466	. . . . . . . 8 $/\$ $/\$
33	32	imbi2d 229	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
34		oveq2 5850	. . . . . . . . . . . . 13
35	34	oveq2d 5858	. . . . . . . . . . . 12
36	35	breq2d 3994	. . . . . . . . . . 11
37		oveq1 5849	. . . . . . . . . . . . . . 15
38	37	oveq2d 5858	. . . . . . . . . . . . . 14
39	38	oveq2d 5858	. . . . . . . . . . . . 13
40	39	breq2d 3994	. . . . . . . . . . . 12
41	40	notbid 657	. . . . . . . . . . 11
42	36, 41	anbi12d 465	. . . . . . . . . 10 $/\$ $/\$
43	34	breq1d 3992	. . . . . . . . . 10
44	42, 43	imbi12d 233	. . . . . . . . 9 $/\$ $/\$
45	44	ralbidv 2466	. . . . . . . 8 $/\$ $/\$
46	45	imbi2d 229	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		oveq2 5850	. . . . . . . . . . . . 13
48	47	oveq2d 5858	. . . . . . . . . . . 12
49	48	breq2d 3994	. . . . . . . . . . 11
50		oveq1 5849	. . . . . . . . . . . . . . 15
51	50	oveq2d 5858	. . . . . . . . . . . . . 14
52	51	oveq2d 5858	. . . . . . . . . . . . 13
53	52	breq2d 3994	. . . . . . . . . . . 12
54	53	notbid 657	. . . . . . . . . . 11
55	49, 54	anbi12d 465	. . . . . . . . . 10 $/\$ $/\$
56	47	breq1d 3992	. . . . . . . . . 10
57	55, 56	imbi12d 233	. . . . . . . . 9 $/\$ $/\$
58	57	ralbidv 2466	. . . . . . . 8 $/\$ $/\$
59	58	imbi2d 229	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
60		breq1 3985	. . . . . . . . . . . . . 14
61		breq1 3985	. . . . . . . . . . . . . . 15
62	61	notbid 657	. . . . . . . . . . . . . 14
63	60, 62	anbi12d 465	. . . . . . . . . . . . 13 $/\$ $/\$
64		breq2 3986	. . . . . . . . . . . . 13
65	63, 64	imbi12d 233	. . . . . . . . . . . 12 $/\$ $/\$
66	65	imbi2d 229	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67		simplrl 525	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
68		prmnn 12042	. . . . . . . . . . . . . . . 16
69	67, 68	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
70		simpll 519	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71		dvdsdc 11738	. . . . . . . . . . . . . . 15 $/\$ DECID
72	69, 70, 71	syl2anc 409	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ DECID
73		coprm 12076	. . . . . . . . . . . . . . . 16 $/\$
74	67, 70, 73	syl2anc 409	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		zcn 9196	. . . . . . . . . . . . . . . . . . . . 21
76	75	ad2antll 483	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
77		prmz 12043	. . . . . . . . . . . . . . . . . . . . . 22
78	77	ad2antrl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
79	78	zcnd 9314	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
80	76, 79	mulcomd 7920	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
81	80	breq2d 3994	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
82		simpl 108	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
83	78, 82	gcdcomd 11907	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	83	eqeq1d 2174	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
85	81, 84	anbi12d 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
86		simprr 522	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87		coprmdvds 12024	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
88	82, 78, 86, 87	syl3anc 1228	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
89	85, 88	sylbid 149	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	89	expdimp 257	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
91	74, 90	sylbid 149	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92		con1dc 846	. . . . . . . . . . . . . 14 DECID
93	72, 91, 92	sylc 62	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
94	93	expimpd 361	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
95	94	ex 114	. . . . . . . . . . 11 $/\$ $/\$
96	66, 95	vtoclga 2792	. . . . . . . . . 10 $/\$ $/\$
97	96	impl 378	. . . . . . . . 9 $/\$ $/\$ $/\$
98	77	zcnd 9314	. . . . . . . . . . . . . 14
99	98	exp1d 10583	. . . . . . . . . . . . 13
100	99	ad2antlr 481	. . . . . . . . . . . 12 $/\$ $/\$
101	100	oveq2d 5858	. . . . . . . . . . 11 $/\$ $/\$
102	101	breq2d 3994	. . . . . . . . . 10 $/\$ $/\$
103		1m1e0 8926	. . . . . . . . . . . . . . . 16
104	103	oveq2i 5853	. . . . . . . . . . . . . . 15
105	77	ad2antlr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
106	105	zcnd 9314	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	106	exp0d 10582	. . . . . . . . . . . . . . 15 $/\$ $/\$
108	104, 107	syl5eq 2211	. . . . . . . . . . . . . 14 $/\$ $/\$
109	108	oveq2d 5858	. . . . . . . . . . . . 13 $/\$ $/\$
110	75	adantl 275	. . . . . . . . . . . . . 14 $/\$ $/\$
111	110	mulid1d 7916	. . . . . . . . . . . . 13 $/\$ $/\$
112	109, 111	eqtrd 2198	. . . . . . . . . . . 12 $/\$ $/\$
113	112	breq2d 3994	. . . . . . . . . . 11 $/\$ $/\$
114	113	notbid 657	. . . . . . . . . 10 $/\$ $/\$
115	102, 114	anbi12d 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116	106	exp1d 10583	. . . . . . . . . 10 $/\$ $/\$
117	116	breq1d 3992	. . . . . . . . 9 $/\$ $/\$
118	97, 115, 117	3imtr4d 202	. . . . . . . 8 $/\$ $/\$ $/\$
119	118	ralrimiva 2539	. . . . . . 7 $/\$ $/\$
120		oveq1 5849	. . . . . . . . . . . . . 14
121	120	breq2d 3994	. . . . . . . . . . . . 13
122		oveq1 5849	. . . . . . . . . . . . . . 15
123	122	breq2d 3994	. . . . . . . . . . . . . 14
124	123	notbid 657	. . . . . . . . . . . . 13
125	121, 124	anbi12d 465	. . . . . . . . . . . 12 $/\$ $/\$
126	125	imbi1d 230	. . . . . . . . . . 11 $/\$ $/\$
127	126	cbvralvw 2696	. . . . . . . . . 10 $/\$ $/\$
128		simprr 522	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129	77	ad2antrl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	128, 129	zmulcld 9319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131		oveq1 5849	. . . . . . . . . . . . . . . . . 18
132	131	breq2d 3994	. . . . . . . . . . . . . . . . 17
133		oveq1 5849	. . . . . . . . . . . . . . . . . . 19
134	133	breq2d 3994	. . . . . . . . . . . . . . . . . 18
135	134	notbid 657	. . . . . . . . . . . . . . . . 17
136	132, 135	anbi12d 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$
137	136	imbi1d 230	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	137	rspcv 2826	. . . . . . . . . . . . . 14 $/\$ $/\$
139	130, 138	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
140		nnnn0 9121	. . . . . . . . . . . . . . . . . . . 20
141	140	ad2antrr 480	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
142		zexpcl 10470	. . . . . . . . . . . . . . . . . . 19 $/\$
143	129, 141, 142	syl2anc 409	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
144		simplr 520	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
145		divides 11729	. . . . . . . . . . . . . . . . . 18 $/\$
146	143, 144, 145	syl2anc 409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	94	adantll 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
148	68	ad2antrl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
149	148	nncnd 8871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
150	140	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
151	149, 150	expp1d 10589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
152	148, 150	nnexpcld 10610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
153	152	nncnd 8871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
154	153, 149	mulcomd 7920	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
155	151, 154	eqtrd 2198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
156	155	oveq2d 5858	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
157	75	ad2antll 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
158	157, 149, 153	mulassd 7922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
159	156, 158	eqtr4d 2201	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
160	159	breq2d 3994	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		simplr 520	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
162		simprr 522	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
163	148	nnzd 9312	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
164	162, 163	zmulcld 9319	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
165	152	nnzd 9312	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
166	152	nnne0d 8902	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
167		dvdsmulcr 11761	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
168	161, 164, 165, 166, 167	syl112anc 1232	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	160, 168	bitrd 187	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170		dvdsmulcr 11761	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	161, 162, 165, 166, 170	syl112anc 1232	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
172	171	notbid 657	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
173	169, 172	anbi12d 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	155	breq1d 3992	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
175		dvdsmulcr 11761	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
176	163, 161, 165, 166, 175	syl112anc 1232	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
177	174, 176	bitrd 187	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
178	147, 173, 177	3imtr4d 202	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
179	178	an32s 558	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
180		breq1 3985	. . . . . . . . . . . . . . . . . . . . . 22
181		breq1 3985	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	notbid 657	. . . . . . . . . . . . . . . . . . . . . 22
183	180, 182	anbi12d 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
184		breq2 3986	. . . . . . . . . . . . . . . . . . . . 21
185	183, 184	imbi12d 233	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
186	179, 185	syl5ibcom 154	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
187	186	rexlimdva 2583	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
188	187	adantlr 469	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
189	146, 188	sylbid 149	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
190	189	com23 78	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
191	190	a2d 26	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
192	75	ad2antll 483	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
193	129	zcnd 9314	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
194	143	zcnd 9314	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	192, 193, 194	mulassd 7922	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
196	193, 194	mulcomd 7920	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
197	193, 141	expp1d 10589	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	196, 197	eqtr4d 2201	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
199	198	oveq2d 5858	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
200	195, 199	eqtrd 2198	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
201	200	breq2d 3994	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
202		nnm1nn0 9155	. . . . . . . . . . . . . . . . . . . . . . 23
203	202	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
204		zexpcl 10470	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
205	129, 203, 204	syl2anc 409	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	205	zcnd 9314	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	192, 193, 206	mulassd 7922	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
208	193, 206	mulcomd 7920	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
209		simpll 519	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
210		expm1t 10483	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
211	193, 209, 210	syl2anc 409	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
212	208, 211	eqtr4d 2201	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
213	212	oveq2d 5858	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
214	207, 213	eqtrd 2198	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
215	214	breq2d 3994	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
216	215	notbid 657	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
217	201, 216	anbi12d 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
218	217	imbi1d 230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
219		nncn 8865	. . . . . . . . . . . . . . . . . . . . . 22
220	219	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
221		ax-1cn 7846	. . . . . . . . . . . . . . . . . . . . 21
222		pncan 8104	. . . . . . . . . . . . . . . . . . . . 21 $/\$
223	220, 221, 222	sylancl 410	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
224	223	oveq2d 5858	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
225	224	oveq2d 5858	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
226	225	breq2d 3994	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
227	226	notbid 657	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
228	227	anbi2d 460	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	imbi1d 230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
230	191, 218, 229	3imtr4d 202	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
231	139, 230	syld 45	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
232	231	anassrs 398	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
233	232	ralrimdva 2546	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
234	127, 233	syl5bi 151	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
235	234	expl 376	. . . . . . . 8 $/\$ $/\$ $/\$
236	235	a2d 26	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
237	20, 33, 46, 59, 119, 236	nnind 8873	. . . . . 6 $/\$ $/\$
238	237	com12 30	. . . . 5 $/\$ $/\$
239	238	impr 377	. . . 4 $/\$ $/\$ $/\$
240	239	adantll 468	. . 3 $/\$ $/\$ $/\$ $/\$
241		simpll 519	. . 3 $/\$ $/\$ $/\$
242	7, 240, 241	rspcdva 2835	. 2 $/\$ $/\$ $/\$ $/\$
243	242	3impia 1190	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 DECID wdc 824 $/\$ w3a 968

wceq 1343

wcel 2136

wne 2336

wral 2444

wrex 2445 class class class wbr 3982 (class class class)co 5842

cc 7751

cc0 7753

c1 7754

caddc 7756

cmul 7758

cmin 8069

cn 8857

cn0 9114

cz 9191

cexp 10454

cdvds 11727

cgcd 11875

cprime 12039

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873

This theorem depends on definitions: df-bi 116 df-stab 821 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-frec 6359 df-1o 6384 df-2o 6385 df-er 6501 df-en 6707 df-sup 6949 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-fz 9945 df-fzo 10078 df-fl 10205 df-mod 10258 df-seqfrec 10381 df-exp 10455 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941 df-dvds 11728 df-gcd 11876 df-prm 12040

This theorem is referenced by: pockthlem 12286

W3C validator