prmpwdvds - Intuitionistic Logic Explorer

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

Theorem prmpwdvds 13078

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 6065	. . . . . 6
2	1	breq2d 4126	. . . . 5
3		oveq1 6065	. . . . . . 7
4	3	breq2d 4126	. . . . . 6
5	4	notbid 673	. . . . 5
6	2, 5	anbi12d 473	. . . 4 $/\$ $/\$
7	6	imbi1d 231	. . 3 $/\$ $/\$
8		oveq2 6066	. . . . . . . . . . . . 13
9	8	oveq2d 6074	. . . . . . . . . . . 12
10	9	breq2d 4126	. . . . . . . . . . 11
11		oveq1 6065	. . . . . . . . . . . . . . 15
12	11	oveq2d 6074	. . . . . . . . . . . . . 14
13	12	oveq2d 6074	. . . . . . . . . . . . 13
14	13	breq2d 4126	. . . . . . . . . . . 12
15	14	notbid 673	. . . . . . . . . . 11
16	10, 15	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
17	8	breq1d 4124	. . . . . . . . . 10
18	16, 17	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
19	18	ralbidv 2544	. . . . . . . 8 $/\$ $/\$
20	19	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
21		oveq2 6066	. . . . . . . . . . . . 13
22	21	oveq2d 6074	. . . . . . . . . . . 12
23	22	breq2d 4126	. . . . . . . . . . 11
24		oveq1 6065	. . . . . . . . . . . . . . 15
25	24	oveq2d 6074	. . . . . . . . . . . . . 14
26	25	oveq2d 6074	. . . . . . . . . . . . 13
27	26	breq2d 4126	. . . . . . . . . . . 12
28	27	notbid 673	. . . . . . . . . . 11
29	23, 28	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
30	21	breq1d 4124	. . . . . . . . . 10
31	29, 30	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
32	31	ralbidv 2544	. . . . . . . 8 $/\$ $/\$
33	32	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
34		oveq2 6066	. . . . . . . . . . . . 13
35	34	oveq2d 6074	. . . . . . . . . . . 12
36	35	breq2d 4126	. . . . . . . . . . 11
37		oveq1 6065	. . . . . . . . . . . . . . 15
38	37	oveq2d 6074	. . . . . . . . . . . . . 14
39	38	oveq2d 6074	. . . . . . . . . . . . 13
40	39	breq2d 4126	. . . . . . . . . . . 12
41	40	notbid 673	. . . . . . . . . . 11
42	36, 41	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
43	34	breq1d 4124	. . . . . . . . . 10
44	42, 43	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
45	44	ralbidv 2544	. . . . . . . 8 $/\$ $/\$
46	45	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		oveq2 6066	. . . . . . . . . . . . 13
48	47	oveq2d 6074	. . . . . . . . . . . 12
49	48	breq2d 4126	. . . . . . . . . . 11
50		oveq1 6065	. . . . . . . . . . . . . . 15
51	50	oveq2d 6074	. . . . . . . . . . . . . 14
52	51	oveq2d 6074	. . . . . . . . . . . . 13
53	52	breq2d 4126	. . . . . . . . . . . 12
54	53	notbid 673	. . . . . . . . . . 11
55	49, 54	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
56	47	breq1d 4124	. . . . . . . . . 10
57	55, 56	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
58	57	ralbidv 2544	. . . . . . . 8 $/\$ $/\$
59	58	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
60		breq1 4117	. . . . . . . . . . . . . 14
61		breq1 4117	. . . . . . . . . . . . . . 15
62	61	notbid 673	. . . . . . . . . . . . . 14
63	60, 62	anbi12d 473	. . . . . . . . . . . . 13 $/\$ $/\$
64		breq2 4118	. . . . . . . . . . . . 13
65	63, 64	imbi12d 234	. . . . . . . . . . . 12 $/\$ $/\$
66	65	imbi2d 230	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67		simplrl 537	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
68		prmnn 12832	. . . . . . . . . . . . . . . 16
69	67, 68	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
70		simpll 527	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71		dvdsdc 12509	. . . . . . . . . . . . . . 15 $/\$ DECID
72	69, 70, 71	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ DECID
73		coprm 12866	. . . . . . . . . . . . . . . 16 $/\$
74	67, 70, 73	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		zcn 9599	. . . . . . . . . . . . . . . . . . . . 21
76	75	ad2antll 491	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
77		prmz 12833	. . . . . . . . . . . . . . . . . . . . . 22
78	77	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
79	78	zcnd 9719	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
80	76, 79	mulcomd 8311	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
81	80	breq2d 4126	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
82		simpl 109	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
83	78, 82	gcdcomd 12695	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	83	eqeq1d 2243	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
85	81, 84	anbi12d 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
86		simprr 533	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87		coprmdvds 12814	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
88	82, 78, 86, 87	syl3anc 1274	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
89	85, 88	sylbid 150	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	89	expdimp 259	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
91	74, 90	sylbid 150	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92		con1dc 864	. . . . . . . . . . . . . 14 DECID
93	72, 91, 92	sylc 62	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
94	93	expimpd 363	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
95	94	ex 115	. . . . . . . . . . 11 $/\$ $/\$
96	66, 95	vtoclga 2883	. . . . . . . . . 10 $/\$ $/\$
97	96	impl 380	. . . . . . . . 9 $/\$ $/\$ $/\$
98	77	zcnd 9719	. . . . . . . . . . . . . 14
99	98	exp1d 11055	. . . . . . . . . . . . 13
100	99	ad2antlr 489	. . . . . . . . . . . 12 $/\$ $/\$
101	100	oveq2d 6074	. . . . . . . . . . 11 $/\$ $/\$
102	101	breq2d 4126	. . . . . . . . . 10 $/\$ $/\$
103		1m1e0 9323	. . . . . . . . . . . . . . . 16
104	103	oveq2i 6069	. . . . . . . . . . . . . . 15
105	77	ad2antlr 489	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
106	105	zcnd 9719	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	106	exp0d 11054	. . . . . . . . . . . . . . 15 $/\$ $/\$
108	104, 107	eqtrid 2279	. . . . . . . . . . . . . 14 $/\$ $/\$
109	108	oveq2d 6074	. . . . . . . . . . . . 13 $/\$ $/\$
110	75	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
111	110	mulridd 8307	. . . . . . . . . . . . 13 $/\$ $/\$
112	109, 111	eqtrd 2267	. . . . . . . . . . . 12 $/\$ $/\$
113	112	breq2d 4126	. . . . . . . . . . 11 $/\$ $/\$
114	113	notbid 673	. . . . . . . . . 10 $/\$ $/\$
115	102, 114	anbi12d 473	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116	106	exp1d 11055	. . . . . . . . . 10 $/\$ $/\$
117	116	breq1d 4124	. . . . . . . . 9 $/\$ $/\$
118	97, 115, 117	3imtr4d 203	. . . . . . . 8 $/\$ $/\$ $/\$
119	118	ralrimiva 2617	. . . . . . 7 $/\$ $/\$
120		oveq1 6065	. . . . . . . . . . . . . 14
121	120	breq2d 4126	. . . . . . . . . . . . 13
122		oveq1 6065	. . . . . . . . . . . . . . 15
123	122	breq2d 4126	. . . . . . . . . . . . . 14
124	123	notbid 673	. . . . . . . . . . . . 13
125	121, 124	anbi12d 473	. . . . . . . . . . . 12 $/\$ $/\$
126	125	imbi1d 231	. . . . . . . . . . 11 $/\$ $/\$
127	126	cbvralvw 2784	. . . . . . . . . 10 $/\$ $/\$
128		simprr 533	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129	77	ad2antrl 490	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	128, 129	zmulcld 9724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131		oveq1 6065	. . . . . . . . . . . . . . . . . 18
132	131	breq2d 4126	. . . . . . . . . . . . . . . . 17
133		oveq1 6065	. . . . . . . . . . . . . . . . . . 19
134	133	breq2d 4126	. . . . . . . . . . . . . . . . . 18
135	134	notbid 673	. . . . . . . . . . . . . . . . 17
136	132, 135	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$
137	136	imbi1d 231	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	137	rspcv 2919	. . . . . . . . . . . . . 14 $/\$ $/\$
139	130, 138	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
140		nnnn0 9520	. . . . . . . . . . . . . . . . . . . 20
141	140	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
142		zexpcl 10940	. . . . . . . . . . . . . . . . . . 19 $/\$
143	129, 141, 142	syl2anc 411	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
144		simplr 529	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
145		divides 12500	. . . . . . . . . . . . . . . . . 18 $/\$
146	143, 144, 145	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	94	adantll 476	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
148	68	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
149	148	nncnd 9268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
150	140	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
151	149, 150	expp1d 11061	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
152	148, 150	nnexpcld 11082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
153	152	nncnd 9268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
154	153, 149	mulcomd 8311	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
155	151, 154	eqtrd 2267	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
156	155	oveq2d 6074	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
157	75	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
158	157, 149, 153	mulassd 8313	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
159	156, 158	eqtr4d 2270	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
160	159	breq2d 4126	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		simplr 529	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
162		simprr 533	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
163	148	nnzd 9717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
164	162, 163	zmulcld 9724	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
165	152	nnzd 9717	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
166	152	nnne0d 9299	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
167		dvdsmulcr 12532	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
168	161, 164, 165, 166, 167	syl112anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	160, 168	bitrd 188	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170		dvdsmulcr 12532	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	161, 162, 165, 166, 170	syl112anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
172	171	notbid 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
173	169, 172	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	155	breq1d 4124	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
175		dvdsmulcr 12532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
176	163, 161, 165, 166, 175	syl112anc 1278	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
177	174, 176	bitrd 188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
178	147, 173, 177	3imtr4d 203	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
179	178	an32s 570	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
180		breq1 4117	. . . . . . . . . . . . . . . . . . . . . 22
181		breq1 4117	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	notbid 673	. . . . . . . . . . . . . . . . . . . . . 22
183	180, 182	anbi12d 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
184		breq2 4118	. . . . . . . . . . . . . . . . . . . . 21
185	183, 184	imbi12d 234	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
186	179, 185	syl5ibcom 155	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
187	186	rexlimdva 2662	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
188	187	adantlr 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
189	146, 188	sylbid 150	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
190	189	com23 78	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
191	190	a2d 26	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
192	75	ad2antll 491	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
193	129	zcnd 9719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
194	143	zcnd 9719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	192, 193, 194	mulassd 8313	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
196	193, 194	mulcomd 8311	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
197	193, 141	expp1d 11061	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	196, 197	eqtr4d 2270	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
199	198	oveq2d 6074	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
200	195, 199	eqtrd 2267	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
201	200	breq2d 4126	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
202		nnm1nn0 9554	. . . . . . . . . . . . . . . . . . . . . . 23
203	202	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
204		zexpcl 10940	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
205	129, 203, 204	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	205	zcnd 9719	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	192, 193, 206	mulassd 8313	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
208	193, 206	mulcomd 8311	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
209		simpll 527	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
210		expm1t 10953	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
211	193, 209, 210	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
212	208, 211	eqtr4d 2270	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
213	212	oveq2d 6074	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
214	207, 213	eqtrd 2267	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
215	214	breq2d 4126	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
216	215	notbid 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
217	201, 216	anbi12d 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
218	217	imbi1d 231	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
219		nncn 9262	. . . . . . . . . . . . . . . . . . . . . 22
220	219	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
221		ax-1cn 8236	. . . . . . . . . . . . . . . . . . . . 21
222		pncan 8495	. . . . . . . . . . . . . . . . . . . . 21 $/\$
223	220, 221, 222	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
224	223	oveq2d 6074	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
225	224	oveq2d 6074	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
226	225	breq2d 4126	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
227	226	notbid 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
228	227	anbi2d 464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	imbi1d 231	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
230	191, 218, 229	3imtr4d 203	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
231	139, 230	syld 45	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
232	231	anassrs 400	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
233	232	ralrimdva 2624	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
234	127, 233	biimtrid 152	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
235	234	expl 378	. . . . . . . 8 $/\$ $/\$ $/\$
236	235	a2d 26	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
237	20, 33, 46, 59, 119, 236	nnind 9270	. . . . . 6 $/\$ $/\$
238	237	com12 30	. . . . 5 $/\$ $/\$
239	238	impr 379	. . . 4 $/\$ $/\$ $/\$
240	239	adantll 476	. . 3 $/\$ $/\$ $/\$ $/\$
241		simpll 527	. . 3 $/\$ $/\$ $/\$
242	7, 240, 241	rspcdva 2928	. 2 $/\$ $/\$ $/\$ $/\$
243	242	3impia 1227	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 DECID wdc 842 $/\$ w3a 1005

wceq 1398

wcel 2205

wne 2414

wral 2522

wrex 2523 class class class wbr 4114 (class class class)co 6058

cc 8141

cc0 8143

c1 8144

caddc 8146

cmul 8148

cmin 8460

cn 9254

cn0 9513

cz 9594

cexp 10924

cdvds 12498

cgcd 12674

cprime 12829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261 ax-arch 8262 ax-caucvg 8263

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-frec 6635 df-1o 6660 df-2o 6661 df-er 6780 df-en 6989 df-sup 7288 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-reap 8866 df-ap 8873 df-div 8964 df-inn 9255 df-2 9313 df-3 9314 df-4 9315 df-n0 9514 df-z 9595 df-uz 9872 df-q 9970 df-rp 10005 df-fz 10362 df-fzo 10499 df-fl 10654 df-mod 10709 df-seqfrec 10834 df-exp 10925 df-cj 11552 df-re 11553 df-im 11554 df-rsqrt 11708 df-abs 11709 df-dvds 12499 df-gcd 12675 df-prm 12830

This theorem is referenced by: pockthlem 13079

W3C validator