chtublem - Metamath Proof Explorer

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

Theorem chtublem 20948

Description: Lemma for chtub 20949. (Contributed by Mario Carneiro, 13-Mar-2014.)

**Assertion**
Ref	Expression
chtublem

Proof of Theorem chtublem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn 10089	. . . . . 6
2		nnmulcl 9979	. . . . . 6 $/\$
3	1, 2	mpan 652	. . . . 5
4	3	nnred 9971	. . . 4
5		peano2rem 9323	. . . 4
6	4, 5	syl 16	. . 3
7		chtcl 20845	. . 3
8	6, 7	syl 16	. 2
9		nnre 9963	. . . 4
10		chtcl 20845	. . . 4
11	9, 10	syl 16	. . 3
12		nnnn0 10184	. . . . . . 7
13		2m1e1 10051	. . . . . . . . . . 11
14	13	oveq2i 6051	. . . . . . . . . 10
15	3	nncnd 9972	. . . . . . . . . . . 12
16		2cn 10026	. . . . . . . . . . . . 13
17		ax-1cn 9004	. . . . . . . . . . . . 13
18		subsub 9287	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1271	. . . . . . . . . . . 12
20	15, 19	syl 16	. . . . . . . . . . 11
21		nncn 9964	. . . . . . . . . . . . . 14
22		subdi 9423	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1270	. . . . . . . . . . . . . 14
24	21, 23	syl 16	. . . . . . . . . . . . 13
25	16	mulid1i 9048	. . . . . . . . . . . . . 14
26	25	oveq2i 6051	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2452	. . . . . . . . . . . 12
28	27	oveq1d 6055	. . . . . . . . . . 11
29	20, 28	eqtr4d 2439	. . . . . . . . . 10
30	14, 29	syl5eqr 2450	. . . . . . . . 9
31		2nn0 10194	. . . . . . . . . . 11
32		nnm1nn0 10217	. . . . . . . . . . 11
33		nn0mulcl 10212	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 645	. . . . . . . . . 10
35		nn0p1nn 10215	. . . . . . . . . 10
36	34, 35	syl 16	. . . . . . . . 9
37	30, 36	eqeltrd 2478	. . . . . . . 8
38		nnnn0 10184	. . . . . . . 8
39	37, 38	syl 16	. . . . . . 7
40		1re 9046	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 9982	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 9597	. . . . . . . . 9
44	21	2timesd 10166	. . . . . . . . 9
45	43, 44	breqtrrd 4198	. . . . . . . 8
46		leaddsub 9460	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1184	. . . . . . . 8
48	45, 47	mpbid 202	. . . . . . 7
49		elfz2nn0 11038	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1138	. . . . . 6
51		bccl2 11569	. . . . . 6
52	50, 51	syl 16	. . . . 5
53	52	nnrpd 10603	. . . 4
54	53	relogcld 20471	. . 3
55	11, 54	readdcld 9071	. 2
56		4re 10029	. . . . . 6
57		4pos 10042	. . . . . 6
58	56, 57	elrpii 10571	. . . . 5
59		relogcl 20426	. . . . 5
60	58, 59	ax-mp 8	. . . 4
61	32	nn0red 10231	. . . 4
62		remulcl 9031	. . . 4 $/\$
63	60, 61, 62	sylancr 645	. . 3
64	11, 63	readdcld 9071	. 2
65		iftrue 3705	. . . . . . . . . . . 12
66	65	adantl 453	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 448	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 452	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 13179	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10222	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 645	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3705	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6055	. . . . . . . . . . . . . . 15
74	73	breq2d 4184	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 214	. . . . . . . . . . . . 13 $/\$
76	75	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 13037	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 708	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 13038	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 10330	. . . . . . . . . . . . . . . . . . . 20
82		eluz 10455	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 12859	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 20	. . . . . . . . . . . . . . . . . 18
89		faccl 11531	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 16	. . . . . . . . . . . . . . . . . 18
91		pcelnn 13198	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 465	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 224	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 9998	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3706	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6055	. . . . . . . . . . . . . . . 16
98	97	ad2antll 710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10232	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9223	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 11551	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 9387	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10232	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9369	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2436	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10259	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 9988	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 519	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 11531	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 16	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 11531	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 16	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10003	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 13181	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10259	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 9988	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 519	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10259	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 9988	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 519	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 13180	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2440	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 734	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 13073	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1155	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	12, 148	sylan 458	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 170	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	80	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 446	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 10259	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 12839	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 11530	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4184	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 226	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 170	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 13199	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 224	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 13199	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 224	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9197	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6056	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 13178	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10232	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9356	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2440	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2440	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4198	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 599	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 152	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4192	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 424	. . . . . . . . 9 $/\$
188		1nn0 10193	. . . . . . . . . . . . 13
189		0nn0 10192	. . . . . . . . . . . . 13
190	188, 189	keepel 3756	. . . . . . . . . . . 12
191		nn0addcl 10211	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 645	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10233	. . . . . . . . . 10 $/\$
194		iffalse 3706	. . . . . . . . . . 11
195	194	breq1d 4182	. . . . . . . . . 10
196	193, 195	syl5ibrcom 214	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 152	. . . . . . . 8 $/\$
198		eqid 2404	. . . . . . . . . . . . 13
199	198	prmorcht 20914	. . . . . . . . . . . 12
200	37, 199	syl 16	. . . . . . . . . . 11
201	200	oveq2d 6056	. . . . . . . . . 10
202	201	adantr 452	. . . . . . . . 9 $/\$
203		nncn 9964	. . . . . . . . . . . . . 14
204	203	exp1d 11473	. . . . . . . . . . . . 13
205	204	ifeq1d 3713	. . . . . . . . . . . 12
206	205	mpteq2ia 4251	. . . . . . . . . . 11
207	206	eqcomi 2408	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2749	. . . . . . . . . 10 $/\$
210	37	adantr 452	. . . . . . . . . 10 $/\$
211		eqidd 2405	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 13216	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2436	. . . . . . . 8 $/\$
214		efchtcl 20847	. . . . . . . . . . . . 13
215	9, 214	syl 16	. . . . . . . . . . . 12
216	215	adantr 452	. . . . . . . . . . 11 $/\$
217		nnz 10259	. . . . . . . . . . . 12
218		nnne0 9988	. . . . . . . . . . . 12
219	217, 218	jca 519	. . . . . . . . . . 11 $/\$
220	216, 219	syl 16	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10259	. . . . . . . . . . . 12
222		nnne0 9988	. . . . . . . . . . . 12
223	221, 222	jca 519	. . . . . . . . . . 11 $/\$
224	68, 223	syl 16	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 13180	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1184	. . . . . . . . 9 $/\$
227	198	prmorcht 20914	. . . . . . . . . . . . 13
228	227	oveq2d 6056	. . . . . . . . . . . 12
229	228	adantr 452	. . . . . . . . . . 11 $/\$
230		simpl 444	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 13216	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2436	. . . . . . . . . 10 $/\$
233	232	oveq1d 6055	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2436	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4202	. . . . . . 7 $/\$
236	235	ralrimiva 2749	. . . . . 6
237		efchtcl 20847	. . . . . . . . 9
238	6, 237	syl 16	. . . . . . . 8
239	238	nnzd 10330	. . . . . . 7
240	215, 52	nnmulcld 10003	. . . . . . . 8
241	240	nnzd 10330	. . . . . . 7
242		pc2dvds 13207	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 643	. . . . . 6
244	236, 243	mpbird 224	. . . . 5
245		dvdsle 12850	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 643	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9070	. . . . . 6
249	54	recnd 9070	. . . . . 6
250		efadd 12651	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 643	. . . . 5
252	53	reeflogd 20472	. . . . . 6
253	252	oveq2d 6056	. . . . 5
254	251, 253	eqtrd 2436	. . . 4
255	247, 254	breqtrrd 4198	. . 3
256		efle 12674	. . . 4 $/\$
257	8, 55, 256	syl2anc 643	. . 3
258	255, 257	mpbird 224	. 2
259		fzfid 11267	. . . . . . . . 9
260		elfzelz 11015	. . . . . . . . . . 11
261		bccl 11568	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 464	. . . . . . . . . 10 $/\$
263	262	nn0red 10231	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10233	. . . . . . . . 9 $/\$
265		nn0uz 10476	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2494	. . . . . . . . . . 11
267		fzss1 11047	. . . . . . . . . . 11
268	266, 267	syl 16	. . . . . . . . . 10
269		eluz 10455	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 643	. . . . . . . . . . . 12
271	48, 270	mpbird 224	. . . . . . . . . . 11
272		fzss2 11048	. . . . . . . . . . 11
273	271, 272	syl 16	. . . . . . . . . 10
274	268, 273	sstrd 3318	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 12530	. . . . . . . 8
276	32	nn0zd 10329	. . . . . . . . . . . 12
277		bccmpl 11555	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 643	. . . . . . . . . . . . . 14
279	111	oveq2d 6056	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2436	. . . . . . . . . . . . 13
281	52	nncnd 9972	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2479	. . . . . . . . . . . 12
283		oveq2 6048	. . . . . . . . . . . . 13
284	283	fsum1 12490	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 643	. . . . . . . . . . 11
286	285, 280	eqtr4d 2439	. . . . . . . . . 10
287	286	oveq1d 6055	. . . . . . . . 9
288	21, 105	npcand 9371	. . . . . . . . . . 11
289		uzid 10456	. . . . . . . . . . . . 13
290	276, 289	syl 16	. . . . . . . . . . . 12
291		peano2uz 10486	. . . . . . . . . . . 12
292	290, 291	syl 16	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2479	. . . . . . . . . 10
294	274	sselda 3308	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10232	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 457	. . . . . . . . . 10 $/\$
297		oveq2 6048	. . . . . . . . . 10
298	293, 296, 297	fsumm1 12492	. . . . . . . . 9
299	281	2timesd 10166	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2447	. . . . . . . 8
301		binom11 12566	. . . . . . . . 9
302	39, 301	syl 16	. . . . . . . 8
303	275, 300, 302	3brtr4d 4202	. . . . . . 7
304		mulcom 9032	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 645	. . . . . . 7
306	30	oveq2d 6056	. . . . . . . 8
307		expp1 11343	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 645	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 11481	. . . . . . . . . 10
312		sq2 11432	. . . . . . . . . . 11
313	312	oveq1i 6050	. . . . . . . . . 10
314	311, 313	syl6eq 2452	. . . . . . . . 9
315	314	oveq1d 6055	. . . . . . . 8
316	306, 308, 315	3eqtrd 2440	. . . . . . 7
317	303, 305, 316	3brtr3d 4201	. . . . . 6
318	52	nnred 9971	. . . . . . 7
319		reexpcl 11353	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 645	. . . . . . 7
321		2re 10025	. . . . . . . . 9
322		2pos 10038	. . . . . . . . 9
323	321, 322	pm3.2i 442	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 9818	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1184	. . . . . 6
327	317, 326	mpbird 224	. . . . 5
328	60	recni 9058	. . . . . . . 8
329		mulcom 9032	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 645	. . . . . . 7
331	330	fveq2d 5691	. . . . . 6
332		reexplog 20442	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 645	. . . . . 6
334	331, 333	eqtr4d 2439	. . . . 5
335	327, 252, 334	3brtr4d 4202	. . . 4
336		efle 12674	. . . . 5 $/\$
337	54, 63, 336	syl2anc 643	. . . 4
338	335, 337	mpbird 224	. . 3
339	54, 63, 11, 338	leadd2dd 9597	. 2
340	8, 55, 64, 258, 339	letrd 9183	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721

wne 2567

wral 2666

wss 3280

cif 3699 class class class wbr 4172

cmpt 4226

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

clt 9076

cle 9077

cmin 9247

cdiv 9633

cn 9956

c2 10005

c4 10007

cn0 10177

cz 10238

cuz 10444

crp 10568

cfz 10999

cseq 11278

cexp 11337

cfa 11521

cbc 11548

csu 12434

ce 12619

cdivides 12807

cprime 13034

cpc 13165

clog 20405

ccht 20826

This theorem is referenced by: chtub 20949

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-dvds 12808 df-gcd 12962 df-prm 13035 df-pc 13166 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407 df-cht 20832

W3C validator