chtublem - Metamath Proof Explorer

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

Theorem chtublem 24137

Description: Lemma for chtub 24138. (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 10774	. . . . . 6
2		nnmulcl 10639	. . . . . 6 $/\$
3	1, 2	mpan 674	. . . . 5
4	3	nnred 10631	. . . 4
5		peano2rem 9948	. . . 4
6	4, 5	syl 17	. . 3
7		chtcl 24034	. . 3
8	6, 7	syl 17	. 2
9		nnre 10623	. . . 4
10		chtcl 24034	. . . 4
11	9, 10	syl 17	. . 3
12		nnnn0 10883	. . . . . . 7
13		2m1e1 10731	. . . . . . . . . . 11
14	13	oveq2i 6316	. . . . . . . . . 10
15	3	nncnd 10632	. . . . . . . . . . . 12
16		2cn 10687	. . . . . . . . . . . . 13
17		ax-1cn 9604	. . . . . . . . . . . . 13
18		subsub 9911	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1352	. . . . . . . . . . . 12
20	15, 19	syl 17	. . . . . . . . . . 11
21		nncn 10624	. . . . . . . . . . . . . 14
22		subdi 10059	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1351	. . . . . . . . . . . . . 14
24	21, 23	syl 17	. . . . . . . . . . . . 13
25		2t1e2 10765	. . . . . . . . . . . . . 14
26	25	oveq2i 6316	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2479	. . . . . . . . . . . 12
28	27	oveq1d 6320	. . . . . . . . . . 11
29	20, 28	eqtr4d 2466	. . . . . . . . . 10
30	14, 29	syl5eqr 2477	. . . . . . . . 9
31		2nn0 10893	. . . . . . . . . . 11
32		nnm1nn0 10918	. . . . . . . . . . 11
33		nn0mulcl 10913	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 667	. . . . . . . . . 10
35		nn0p1nn 10916	. . . . . . . . . 10
36	34, 35	syl 17	. . . . . . . . 9
37	30, 36	eqeltrd 2507	. . . . . . . 8
38		nnnn0 10883	. . . . . . . 8
39	37, 38	syl 17	. . . . . . 7
40		1re 9649	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10642	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 10235	. . . . . . . . 9
44	21	2timesd 10862	. . . . . . . . 9
45	43, 44	breqtrrd 4450	. . . . . . . 8
46		leaddsub 10097	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1264	. . . . . . . 8
48	45, 47	mpbid 213	. . . . . . 7
49		elfz2nn0 11892	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1189	. . . . . 6
51		bccl2 12514	. . . . . 6
52	50, 51	syl 17	. . . . 5
53	52	nnrpd 11346	. . . 4
54	53	relogcld 23570	. . 3
55	11, 54	readdcld 9677	. 2
56		4re 10693	. . . . . 6
57		4pos 10712	. . . . . 6
58	56, 57	elrpii 11312	. . . . 5
59		relogcl 23523	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10933	. . . 4
62		remulcl 9631	. . . 4 $/\$
63	60, 61, 62	sylancr 667	. . 3
64	11, 63	readdcld 9677	. 2
65		iftrue 3917	. . . . . . . . . . . 12
66	65	adantl 467	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 462	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 14799	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10923	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 667	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3917	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6320	. . . . . . . . . . . . . . 15
74	73	breq2d 4435	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 225	. . . . . . . . . . . . 13 $/\$
76	75	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 14624	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 14625	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 11046	. . . . . . . . . . . . . . . . . . . 20
82		eluz 11179	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 480	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 235	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 14359	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12475	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 17	. . . . . . . . . . . . . . . . . 18
91		pcelnn 14818	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 480	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 235	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3920	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6320	. . . . . . . . . . . . . . . 16
98	97	ad2antll 733	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10934	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9841	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12496	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 17	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 10013	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9995	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2463	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6321	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10966	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10649	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 534	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12475	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 17	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12475	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 17	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10664	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 466	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 14801	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10966	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10649	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 534	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10966	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10649	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 534	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 14800	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6321	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2467	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 764	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 14670	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1207	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	12, 148	sylan 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 180	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	80	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 460	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 10966	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 14337	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12474	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4435	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 237	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 180	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 14819	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 235	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 14819	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 235	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6323	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9815	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6321	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 14798	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 480	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10934	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9982	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4450	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 618	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 161	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4444	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 435	. . . . . . . . 9 $/\$
188		1nn0 10892	. . . . . . . . . . . . 13
189		0nn0 10891	. . . . . . . . . . . . 13
190	188, 189	keepel 3978	. . . . . . . . . . . 12
191		nn0addcl 10912	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 667	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10935	. . . . . . . . . 10 $/\$
194		iffalse 3920	. . . . . . . . . . 11
195	194	breq1d 4433	. . . . . . . . . 10
196	193, 195	syl5ibrcom 225	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 161	. . . . . . . 8 $/\$
198		eqid 2422	. . . . . . . . . . . . 13
199	198	prmorcht 24103	. . . . . . . . . . . 12
200	37, 199	syl 17	. . . . . . . . . . 11
201	200	oveq2d 6321	. . . . . . . . . 10
202	201	adantr 466	. . . . . . . . 9 $/\$
203		nncn 10624	. . . . . . . . . . . . . 14
204	203	exp1d 12417	. . . . . . . . . . . . 13
205	204	ifeq1d 3929	. . . . . . . . . . . 12
206	205	mpteq2ia 4506	. . . . . . . . . . 11
207	206	eqcomi 2435	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2836	. . . . . . . . . 10 $/\$
210	37	adantr 466	. . . . . . . . . 10 $/\$
211		eqidd 2423	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 14836	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2463	. . . . . . . 8 $/\$
214		efchtcl 24036	. . . . . . . . . . . . 13
215	9, 214	syl 17	. . . . . . . . . . . 12
216	215	adantr 466	. . . . . . . . . . 11 $/\$
217		nnz 10966	. . . . . . . . . . . 12
218		nnne0 10649	. . . . . . . . . . . 12
219	217, 218	jca 534	. . . . . . . . . . 11 $/\$
220	216, 219	syl 17	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10966	. . . . . . . . . . . 12
222		nnne0 10649	. . . . . . . . . . . 12
223	221, 222	jca 534	. . . . . . . . . . 11 $/\$
224	68, 223	syl 17	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 14800	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1264	. . . . . . . . 9 $/\$
227	198	prmorcht 24103	. . . . . . . . . . . . 13
228	227	oveq2d 6321	. . . . . . . . . . . 12
229	228	adantr 466	. . . . . . . . . . 11 $/\$
230		simpl 458	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 14836	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2463	. . . . . . . . . 10 $/\$
233	232	oveq1d 6320	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2463	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4454	. . . . . . 7 $/\$
236	235	ralrimiva 2836	. . . . . 6
237		efchtcl 24036	. . . . . . . . 9
238	6, 237	syl 17	. . . . . . . 8
239	238	nnzd 11046	. . . . . . 7
240	215, 52	nnmulcld 10664	. . . . . . . 8
241	240	nnzd 11046	. . . . . . 7
242		pc2dvds 14827	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 665	. . . . . 6
244	236, 243	mpbird 235	. . . . 5
245		dvdsle 14349	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 665	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9676	. . . . . 6
249	54	recnd 9676	. . . . . 6
250		efadd 14147	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 665	. . . . 5
252	53	reeflogd 23571	. . . . . 6
253	252	oveq2d 6321	. . . . 5
254	251, 253	eqtrd 2463	. . . 4
255	247, 254	breqtrrd 4450	. . 3
256		efle 14171	. . . 4 $/\$
257	8, 55, 256	syl2anc 665	. . 3
258	255, 257	mpbird 235	. 2
259		fzfid 12192	. . . . . . . . 9
260		elfzelz 11807	. . . . . . . . . . 11
261		bccl 12513	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 479	. . . . . . . . . 10 $/\$
263	262	nn0red 10933	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10935	. . . . . . . . 9 $/\$
265		nn0uz 11200	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2517	. . . . . . . . . . 11
267		fzss1 11844	. . . . . . . . . . 11
268	266, 267	syl 17	. . . . . . . . . 10
269		eluz 11179	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 665	. . . . . . . . . . . 12
271	48, 270	mpbird 235	. . . . . . . . . . 11
272		fzss2 11845	. . . . . . . . . . 11
273	271, 272	syl 17	. . . . . . . . . 10
274	268, 273	sstrd 3474	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13855	. . . . . . . 8
276	32	nn0zd 11045	. . . . . . . . . . . 12
277		bccmpl 12500	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 665	. . . . . . . . . . . . . 14
279	111	oveq2d 6321	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2463	. . . . . . . . . . . . 13
281	52	nncnd 10632	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2508	. . . . . . . . . . . 12
283		oveq2 6313	. . . . . . . . . . . . 13
284	283	fsum1 13807	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 665	. . . . . . . . . . 11
286	285, 280	eqtr4d 2466	. . . . . . . . . 10
287	286	oveq1d 6320	. . . . . . . . 9
288	21, 105	npcand 9997	. . . . . . . . . . 11
289		uzid 11180	. . . . . . . . . . . . 13
290	276, 289	syl 17	. . . . . . . . . . . 12
291		peano2uz 11219	. . . . . . . . . . . 12
292	290, 291	syl 17	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2508	. . . . . . . . . 10
294	274	sselda 3464	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10934	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 472	. . . . . . . . . 10 $/\$
297		oveq2 6313	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13811	. . . . . . . . 9
299	281	2timesd 10862	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2474	. . . . . . . 8
301		binom11 13889	. . . . . . . . 9
302	39, 301	syl 17	. . . . . . . 8
303	275, 300, 302	3brtr4d 4454	. . . . . . 7
304		mulcom 9632	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 667	. . . . . . 7
306	30	oveq2d 6321	. . . . . . . 8
307		expp1 12285	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 667	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12425	. . . . . . . . . 10
312		sq2 12377	. . . . . . . . . . 11
313	312	oveq1i 6315	. . . . . . . . . 10
314	311, 313	syl6eq 2479	. . . . . . . . 9
315	314	oveq1d 6320	. . . . . . . 8
316	306, 308, 315	3eqtrd 2467	. . . . . . 7
317	303, 305, 316	3brtr3d 4453	. . . . . 6
318	52	nnred 10631	. . . . . . 7
319		reexpcl 12295	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 667	. . . . . . 7
321		2re 10686	. . . . . . . . 9
322		2pos 10708	. . . . . . . . 9
323	321, 322	pm3.2i 456	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10464	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1264	. . . . . 6
327	317, 326	mpbird 235	. . . . 5
328	60	recni 9662	. . . . . . . 8
329		mulcom 9632	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 667	. . . . . . 7
331	330	fveq2d 5885	. . . . . 6
332		reexplog 23542	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 667	. . . . . 6
334	331, 333	eqtr4d 2466	. . . . 5
335	327, 252, 334	3brtr4d 4454	. . . 4
336		efle 14171	. . . . 5 $/\$
337	54, 63, 336	syl2anc 665	. . . 4
338	335, 337	mpbird 235	. . 3
339	54, 63, 11, 338	leadd2dd 10235	. 2
340	8, 55, 64, 258, 339	letrd 9799	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370

wceq 1437

wcel 1872

wne 2614

wral 2771

wss 3436

cif 3911 class class class wbr 4423

cmpt 4482

cfv 5601 (class class class)co 6305

cc 9544

cr 9545

cc0 9546

c1 9547

caddc 9549

cmul 9551

clt 9682

cle 9683

cmin 9867

cdiv 10276

cn 10616

c2 10666

c4 10668

cn0 10876

cz 10944

cuz 11166

crp 11309

cfz 11791

cseq 12219

cexp 12278

cfa 12465

cbc 12493

csu 13751

ce 14113

cdvds 14304

cprime 14621

cpc 14785

clog 23502

ccht 24015

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-inf2 8155 ax-cnex 9602 ax-resscn 9603 ax-1cn 9604 ax-icn 9605 ax-addcl 9606 ax-addrcl 9607 ax-mulcl 9608 ax-mulrcl 9609 ax-mulcom 9610 ax-addass 9611 ax-mulass 9612 ax-distr 9613 ax-i2m1 9614 ax-1ne0 9615 ax-1rid 9616 ax-rnegex 9617 ax-rrecex 9618 ax-cnre 9619 ax-pre-lttri 9620 ax-pre-lttrn 9621 ax-pre-ltadd 9622 ax-pre-mulgt0 9623 ax-pre-sup 9624 ax-addf 9625 ax-mulf 9626

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-iin 4302 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-supp 6926 df-wrecs 7039 df-recs 7101 df-rdg 7139 df-1o 7193 df-2o 7194 df-oadd 7197 df-er 7374 df-map 7485 df-pm 7486 df-ixp 7534 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-fsupp 7893 df-fi 7934 df-sup 7965 df-inf 7966 df-oi 8034 df-card 8381 df-cda 8605 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-sub 9869 df-neg 9870 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-5 10678 df-6 10679 df-7 10680 df-8 10681 df-9 10682 df-10 10683 df-n0 10877 df-z 10945 df-dec 11059 df-uz 11167 df-q 11272 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-ioo 11646 df-ioc 11647 df-ico 11648 df-icc 11649 df-fz 11792 df-fzo 11923 df-fl 12034 df-mod 12103 df-seq 12220 df-exp 12279 df-fac 12466 df-bc 12494 df-hash 12522 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13525 df-clim 13551 df-rlim 13552 df-sum 13752 df-ef 14120 df-sin 14122 df-cos 14123 df-pi 14125 df-dvds 14305 df-gcd 14468 df-prm 14622 df-pc 14786 df-struct 15122 df-ndx 15123 df-slot 15124 df-base 15125 df-sets 15126 df-ress 15127 df-plusg 15202 df-mulr 15203 df-starv 15204 df-sca 15205 df-vsca 15206 df-ip 15207 df-tset 15208 df-ple 15209 df-ds 15211 df-unif 15212 df-hom 15213 df-cco 15214 df-rest 15320 df-topn 15321 df-0g 15339 df-gsum 15340 df-topgen 15341 df-pt 15342 df-prds 15345 df-xrs 15399 df-qtop 15405 df-imas 15406 df-xps 15409 df-mre 15491 df-mrc 15492 df-acs 15494 df-mgm 16487 df-sgrp 16526 df-mnd 16536 df-submnd 16582 df-mulg 16675 df-cntz 16970 df-cmn 17431 df-psmet 18961 df-xmet 18962 df-met 18963 df-bl 18964 df-mopn 18965 df-fbas 18966 df-fg 18967 df-cnfld 18970 df-top 19919 df-bases 19920 df-topon 19921 df-topsp 19922 df-cld 20032 df-ntr 20033 df-cls 20034 df-nei 20112 df-lp 20150 df-perf 20151 df-cn 20241 df-cnp 20242 df-haus 20329 df-tx 20575 df-hmeo 20768 df-fil 20859 df-fm 20951 df-flim 20952 df-flf 20953 df-xms 21333 df-ms 21334 df-tms 21335 df-cncf 21908 df-limc 22819 df-dv 22820 df-log 23504 df-cht 24021

This theorem is referenced by: chtub 24138

W3C validator