prmpwdvds - Intuitionistic Logic Explorer

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

Theorem prmpwdvds 12524

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 5929	. . . . . 6
2	1	breq2d 4045	. . . . 5
3		oveq1 5929	. . . . . . 7
4	3	breq2d 4045	. . . . . 6
5	4	notbid 668	. . . . 5
6	2, 5	anbi12d 473	. . . 4 $/\$ $/\$
7	6	imbi1d 231	. . 3 $/\$ $/\$
8		oveq2 5930	. . . . . . . . . . . . 13
9	8	oveq2d 5938	. . . . . . . . . . . 12
10	9	breq2d 4045	. . . . . . . . . . 11
11		oveq1 5929	. . . . . . . . . . . . . . 15
12	11	oveq2d 5938	. . . . . . . . . . . . . 14
13	12	oveq2d 5938	. . . . . . . . . . . . 13
14	13	breq2d 4045	. . . . . . . . . . . 12
15	14	notbid 668	. . . . . . . . . . 11
16	10, 15	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
17	8	breq1d 4043	. . . . . . . . . 10
18	16, 17	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
19	18	ralbidv 2497	. . . . . . . 8 $/\$ $/\$
20	19	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
21		oveq2 5930	. . . . . . . . . . . . 13
22	21	oveq2d 5938	. . . . . . . . . . . 12
23	22	breq2d 4045	. . . . . . . . . . 11
24		oveq1 5929	. . . . . . . . . . . . . . 15
25	24	oveq2d 5938	. . . . . . . . . . . . . 14
26	25	oveq2d 5938	. . . . . . . . . . . . 13
27	26	breq2d 4045	. . . . . . . . . . . 12
28	27	notbid 668	. . . . . . . . . . 11
29	23, 28	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
30	21	breq1d 4043	. . . . . . . . . 10
31	29, 30	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
32	31	ralbidv 2497	. . . . . . . 8 $/\$ $/\$
33	32	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
34		oveq2 5930	. . . . . . . . . . . . 13
35	34	oveq2d 5938	. . . . . . . . . . . 12
36	35	breq2d 4045	. . . . . . . . . . 11
37		oveq1 5929	. . . . . . . . . . . . . . 15
38	37	oveq2d 5938	. . . . . . . . . . . . . 14
39	38	oveq2d 5938	. . . . . . . . . . . . 13
40	39	breq2d 4045	. . . . . . . . . . . 12
41	40	notbid 668	. . . . . . . . . . 11
42	36, 41	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
43	34	breq1d 4043	. . . . . . . . . 10
44	42, 43	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
45	44	ralbidv 2497	. . . . . . . 8 $/\$ $/\$
46	45	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
47		oveq2 5930	. . . . . . . . . . . . 13
48	47	oveq2d 5938	. . . . . . . . . . . 12
49	48	breq2d 4045	. . . . . . . . . . 11
50		oveq1 5929	. . . . . . . . . . . . . . 15
51	50	oveq2d 5938	. . . . . . . . . . . . . 14
52	51	oveq2d 5938	. . . . . . . . . . . . 13
53	52	breq2d 4045	. . . . . . . . . . . 12
54	53	notbid 668	. . . . . . . . . . 11
55	49, 54	anbi12d 473	. . . . . . . . . 10 $/\$ $/\$
56	47	breq1d 4043	. . . . . . . . . 10
57	55, 56	imbi12d 234	. . . . . . . . 9 $/\$ $/\$
58	57	ralbidv 2497	. . . . . . . 8 $/\$ $/\$
59	58	imbi2d 230	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
60		breq1 4036	. . . . . . . . . . . . . 14
61		breq1 4036	. . . . . . . . . . . . . . 15
62	61	notbid 668	. . . . . . . . . . . . . 14
63	60, 62	anbi12d 473	. . . . . . . . . . . . 13 $/\$ $/\$
64		breq2 4037	. . . . . . . . . . . . 13
65	63, 64	imbi12d 234	. . . . . . . . . . . 12 $/\$ $/\$
66	65	imbi2d 230	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
67		simplrl 535	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
68		prmnn 12278	. . . . . . . . . . . . . . . 16
69	67, 68	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
70		simpll 527	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71		dvdsdc 11963	. . . . . . . . . . . . . . 15 $/\$ DECID
72	69, 70, 71	syl2anc 411	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ DECID
73		coprm 12312	. . . . . . . . . . . . . . . 16 $/\$
74	67, 70, 73	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		zcn 9331	. . . . . . . . . . . . . . . . . . . . 21
76	75	ad2antll 491	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
77		prmz 12279	. . . . . . . . . . . . . . . . . . . . . 22
78	77	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
79	78	zcnd 9449	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
80	76, 79	mulcomd 8048	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
81	80	breq2d 4045	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
82		simpl 109	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
83	78, 82	gcdcomd 12141	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	83	eqeq1d 2205	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
85	81, 84	anbi12d 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
86		simprr 531	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
87		coprmdvds 12260	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
88	82, 78, 86, 87	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
89	85, 88	sylbid 150	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
90	89	expdimp 259	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
91	74, 90	sylbid 150	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92		con1dc 857	. . . . . . . . . . . . . 14 DECID
93	72, 91, 92	sylc 62	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
94	93	expimpd 363	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
95	94	ex 115	. . . . . . . . . . 11 $/\$ $/\$
96	66, 95	vtoclga 2830	. . . . . . . . . 10 $/\$ $/\$
97	96	impl 380	. . . . . . . . 9 $/\$ $/\$ $/\$
98	77	zcnd 9449	. . . . . . . . . . . . . 14
99	98	exp1d 10760	. . . . . . . . . . . . 13
100	99	ad2antlr 489	. . . . . . . . . . . 12 $/\$ $/\$
101	100	oveq2d 5938	. . . . . . . . . . 11 $/\$ $/\$
102	101	breq2d 4045	. . . . . . . . . 10 $/\$ $/\$
103		1m1e0 9059	. . . . . . . . . . . . . . . 16
104	103	oveq2i 5933	. . . . . . . . . . . . . . 15
105	77	ad2antlr 489	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
106	105	zcnd 9449	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	106	exp0d 10759	. . . . . . . . . . . . . . 15 $/\$ $/\$
108	104, 107	eqtrid 2241	. . . . . . . . . . . . . 14 $/\$ $/\$
109	108	oveq2d 5938	. . . . . . . . . . . . 13 $/\$ $/\$
110	75	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
111	110	mulridd 8043	. . . . . . . . . . . . 13 $/\$ $/\$
112	109, 111	eqtrd 2229	. . . . . . . . . . . 12 $/\$ $/\$
113	112	breq2d 4045	. . . . . . . . . . 11 $/\$ $/\$
114	113	notbid 668	. . . . . . . . . 10 $/\$ $/\$
115	102, 114	anbi12d 473	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116	106	exp1d 10760	. . . . . . . . . 10 $/\$ $/\$
117	116	breq1d 4043	. . . . . . . . 9 $/\$ $/\$
118	97, 115, 117	3imtr4d 203	. . . . . . . 8 $/\$ $/\$ $/\$
119	118	ralrimiva 2570	. . . . . . 7 $/\$ $/\$
120		oveq1 5929	. . . . . . . . . . . . . 14
121	120	breq2d 4045	. . . . . . . . . . . . 13
122		oveq1 5929	. . . . . . . . . . . . . . 15
123	122	breq2d 4045	. . . . . . . . . . . . . 14
124	123	notbid 668	. . . . . . . . . . . . 13
125	121, 124	anbi12d 473	. . . . . . . . . . . 12 $/\$ $/\$
126	125	imbi1d 231	. . . . . . . . . . 11 $/\$ $/\$
127	126	cbvralvw 2733	. . . . . . . . . 10 $/\$ $/\$
128		simprr 531	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129	77	ad2antrl 490	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	128, 129	zmulcld 9454	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131		oveq1 5929	. . . . . . . . . . . . . . . . . 18
132	131	breq2d 4045	. . . . . . . . . . . . . . . . 17
133		oveq1 5929	. . . . . . . . . . . . . . . . . . 19
134	133	breq2d 4045	. . . . . . . . . . . . . . . . . 18
135	134	notbid 668	. . . . . . . . . . . . . . . . 17
136	132, 135	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$
137	136	imbi1d 231	. . . . . . . . . . . . . . 15 $/\$ $/\$
138	137	rspcv 2864	. . . . . . . . . . . . . 14 $/\$ $/\$
139	130, 138	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
140		nnnn0 9256	. . . . . . . . . . . . . . . . . . . 20
141	140	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
142		zexpcl 10646	. . . . . . . . . . . . . . . . . . 19 $/\$
143	129, 141, 142	syl2anc 411	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
144		simplr 528	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
145		divides 11954	. . . . . . . . . . . . . . . . . 18 $/\$
146	143, 144, 145	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
147	94	adantll 476	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
148	68	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
149	148	nncnd 9004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
150	140	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
151	149, 150	expp1d 10766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
152	148, 150	nnexpcld 10787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
153	152	nncnd 9004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
154	153, 149	mulcomd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
155	151, 154	eqtrd 2229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
156	155	oveq2d 5938	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
157	75	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
158	157, 149, 153	mulassd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
159	156, 158	eqtr4d 2232	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
160	159	breq2d 4045	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		simplr 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
162		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
163	148	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
164	162, 163	zmulcld 9454	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
165	152	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
166	152	nnne0d 9035	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
167		dvdsmulcr 11986	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
168	161, 164, 165, 166, 167	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	160, 168	bitrd 188	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170		dvdsmulcr 11986	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	161, 162, 165, 166, 170	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
172	171	notbid 668	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
173	169, 172	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	155	breq1d 4043	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
175		dvdsmulcr 11986	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
176	163, 161, 165, 166, 175	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
177	174, 176	bitrd 188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
178	147, 173, 177	3imtr4d 203	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
179	178	an32s 568	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
180		breq1 4036	. . . . . . . . . . . . . . . . . . . . . 22
181		breq1 4036	. . . . . . . . . . . . . . . . . . . . . . 23
182	181	notbid 668	. . . . . . . . . . . . . . . . . . . . . 22
183	180, 182	anbi12d 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
184		breq2 4037	. . . . . . . . . . . . . . . . . . . . 21
185	183, 184	imbi12d 234	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
186	179, 185	syl5ibcom 155	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
187	186	rexlimdva 2614	. . . . . . . . . . . . . . . . . 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 9449	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
194	143	zcnd 9449	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	192, 193, 194	mulassd 8050	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
196	193, 194	mulcomd 8048	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
197	193, 141	expp1d 10766	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
198	196, 197	eqtr4d 2232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
199	198	oveq2d 5938	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
200	195, 199	eqtrd 2229	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
201	200	breq2d 4045	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
202		nnm1nn0 9290	. . . . . . . . . . . . . . . . . . . . . . 23
203	202	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
204		zexpcl 10646	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
205	129, 203, 204	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	205	zcnd 9449	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	192, 193, 206	mulassd 8050	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
208	193, 206	mulcomd 8048	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
209		simpll 527	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
210		expm1t 10659	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
211	193, 209, 210	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
212	208, 211	eqtr4d 2232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
213	212	oveq2d 5938	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
214	207, 213	eqtrd 2229	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
215	214	breq2d 4045	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
216	215	notbid 668	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
217	201, 216	anbi12d 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
218	217	imbi1d 231	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
219		nncn 8998	. . . . . . . . . . . . . . . . . . . . . 22
220	219	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
221		ax-1cn 7972	. . . . . . . . . . . . . . . . . . . . 21
222		pncan 8232	. . . . . . . . . . . . . . . . . . . . 21 $/\$
223	220, 221, 222	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
224	223	oveq2d 5938	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
225	224	oveq2d 5938	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
226	225	breq2d 4045	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
227	226	notbid 668	. . . . . . . . . . . . . . . 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 2577	. . . . . . . . . 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 9006	. . . . . 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 2873	. 2 $/\$ $/\$ $/\$ $/\$
243	242	3impia 1202	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 DECID wdc 835 $/\$ w3a 980

wceq 1364

wcel 2167

wne 2367

wral 2475

wrex 2476 class class class wbr 4033 (class class class)co 5922

cc 7877

cc0 7879

c1 7880

caddc 7882

cmul 7884

cmin 8197

cn 8990

cn0 9249

cz 9326

cexp 10630

cdvds 11952

cgcd 12120

cprime 12275

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-1o 6474 df-2o 6475 df-er 6592 df-en 6800 df-sup 7050 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-dvds 11953 df-gcd 12121 df-prm 12276

This theorem is referenced by: pockthlem 12525

W3C validator