chtublem - Metamath Proof Explorer

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

Theorem chtublem 23611

Description: Lemma for chtub 23612. (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 10714	. . . . . 6
2		nnmulcl 10579	. . . . . 6 $/\$
3	1, 2	mpan 670	. . . . 5
4	3	nnred 10571	. . . 4
5		peano2rem 9905	. . . 4
6	4, 5	syl 16	. . 3
7		chtcl 23508	. . 3
8	6, 7	syl 16	. 2
9		nnre 10563	. . . 4
10		chtcl 23508	. . . 4
11	9, 10	syl 16	. . 3
12		nnnn0 10823	. . . . . . 7
13		2m1e1 10671	. . . . . . . . . . 11
14	13	oveq2i 6307	. . . . . . . . . 10
15	3	nncnd 10572	. . . . . . . . . . . 12
16		2cn 10627	. . . . . . . . . . . . 13
17		ax-1cn 9567	. . . . . . . . . . . . 13
18		subsub 9868	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1316	. . . . . . . . . . . 12
20	15, 19	syl 16	. . . . . . . . . . 11
21		nncn 10564	. . . . . . . . . . . . . 14
22		subdi 10011	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1315	. . . . . . . . . . . . . 14
24	21, 23	syl 16	. . . . . . . . . . . . 13
25		2t1e2 10705	. . . . . . . . . . . . . 14
26	25	oveq2i 6307	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2514	. . . . . . . . . . . 12
28	27	oveq1d 6311	. . . . . . . . . . 11
29	20, 28	eqtr4d 2501	. . . . . . . . . 10
30	14, 29	syl5eqr 2512	. . . . . . . . 9
31		2nn0 10833	. . . . . . . . . . 11
32		nnm1nn0 10858	. . . . . . . . . . 11
33		nn0mulcl 10853	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 663	. . . . . . . . . 10
35		nn0p1nn 10856	. . . . . . . . . 10
36	34, 35	syl 16	. . . . . . . . 9
37	30, 36	eqeltrd 2545	. . . . . . . 8
38		nnnn0 10823	. . . . . . . 8
39	37, 38	syl 16	. . . . . . 7
40		1re 9612	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10582	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 10188	. . . . . . . . 9
44	21	2timesd 10802	. . . . . . . . 9
45	43, 44	breqtrrd 4482	. . . . . . . 8
46		leaddsub 10049	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1228	. . . . . . . 8
48	45, 47	mpbid 210	. . . . . . 7
49		elfz2nn0 11794	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1180	. . . . . 6
51		bccl2 12403	. . . . . 6
52	50, 51	syl 16	. . . . 5
53	52	nnrpd 11280	. . . 4
54	53	relogcld 23133	. . 3
55	11, 54	readdcld 9640	. 2
56		4re 10633	. . . . . 6
57		4pos 10652	. . . . . 6
58	56, 57	elrpii 11248	. . . . 5
59		relogcl 23088	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10874	. . . 4
62		remulcl 9594	. . . 4 $/\$
63	60, 61, 62	sylancr 663	. . 3
64	11, 63	readdcld 9640	. 2
65		iftrue 3950	. . . . . . . . . . . 12
66	65	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 14385	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10863	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 663	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3950	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6311	. . . . . . . . . . . . . . 15
74	73	breq2d 4468	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 222	. . . . . . . . . . . . 13 $/\$
76	75	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 14231	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 14232	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 10989	. . . . . . . . . . . . . . . . . . . 20
82		eluz 11119	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 478	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 14052	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12365	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 16	. . . . . . . . . . . . . . . . . 18
91		pcelnn 14404	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 478	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10599	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3953	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6311	. . . . . . . . . . . . . . . 16
98	97	ad2antll 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10875	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9798	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12385	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 9970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10875	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9952	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2498	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10907	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10589	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12365	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 16	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12365	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 16	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10604	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 14387	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10907	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10589	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10907	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10589	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 14386	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2502	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 757	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 14270	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1198	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	12, 148	sylan 471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 177	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	80	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 10907	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 14030	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12364	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 177	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 14405	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 14405	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6314	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9772	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2514	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6312	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 14384	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 478	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10875	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9939	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2502	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2502	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 615	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 158	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4476	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 434	. . . . . . . . 9 $/\$
188		1nn0 10832	. . . . . . . . . . . . 13
189		0nn0 10831	. . . . . . . . . . . . 13
190	188, 189	keepel 4012	. . . . . . . . . . . 12
191		nn0addcl 10852	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 663	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10876	. . . . . . . . . 10 $/\$
194		iffalse 3953	. . . . . . . . . . 11
195	194	breq1d 4466	. . . . . . . . . 10
196	193, 195	syl5ibrcom 222	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 158	. . . . . . . 8 $/\$
198		eqid 2457	. . . . . . . . . . . . 13
199	198	prmorcht 23577	. . . . . . . . . . . 12
200	37, 199	syl 16	. . . . . . . . . . 11
201	200	oveq2d 6312	. . . . . . . . . 10
202	201	adantr 465	. . . . . . . . 9 $/\$
203		nncn 10564	. . . . . . . . . . . . . 14
204	203	exp1d 12307	. . . . . . . . . . . . 13
205	204	ifeq1d 3962	. . . . . . . . . . . 12
206	205	mpteq2ia 4539	. . . . . . . . . . 11
207	206	eqcomi 2470	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2871	. . . . . . . . . 10 $/\$
210	37	adantr 465	. . . . . . . . . 10 $/\$
211		eqidd 2458	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 14422	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2498	. . . . . . . 8 $/\$
214		efchtcl 23510	. . . . . . . . . . . . 13
215	9, 214	syl 16	. . . . . . . . . . . 12
216	215	adantr 465	. . . . . . . . . . 11 $/\$
217		nnz 10907	. . . . . . . . . . . 12
218		nnne0 10589	. . . . . . . . . . . 12
219	217, 218	jca 532	. . . . . . . . . . 11 $/\$
220	216, 219	syl 16	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10907	. . . . . . . . . . . 12
222		nnne0 10589	. . . . . . . . . . . 12
223	221, 222	jca 532	. . . . . . . . . . 11 $/\$
224	68, 223	syl 16	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 14386	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1228	. . . . . . . . 9 $/\$
227	198	prmorcht 23577	. . . . . . . . . . . . 13
228	227	oveq2d 6312	. . . . . . . . . . . 12
229	228	adantr 465	. . . . . . . . . . 11 $/\$
230		simpl 457	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 14422	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2498	. . . . . . . . . 10 $/\$
233	232	oveq1d 6311	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2498	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4486	. . . . . . 7 $/\$
236	235	ralrimiva 2871	. . . . . 6
237		efchtcl 23510	. . . . . . . . 9
238	6, 237	syl 16	. . . . . . . 8
239	238	nnzd 10989	. . . . . . 7
240	215, 52	nnmulcld 10604	. . . . . . . 8
241	240	nnzd 10989	. . . . . . 7
242		pc2dvds 14413	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 661	. . . . . 6
244	236, 243	mpbird 232	. . . . 5
245		dvdsle 14042	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 661	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9639	. . . . . 6
249	54	recnd 9639	. . . . . 6
250		efadd 13840	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 661	. . . . 5
252	53	reeflogd 23134	. . . . . 6
253	252	oveq2d 6312	. . . . 5
254	251, 253	eqtrd 2498	. . . 4
255	247, 254	breqtrrd 4482	. . 3
256		efle 13864	. . . 4 $/\$
257	8, 55, 256	syl2anc 661	. . 3
258	255, 257	mpbird 232	. 2
259		fzfid 12085	. . . . . . . . 9
260		elfzelz 11713	. . . . . . . . . . 11
261		bccl 12402	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 477	. . . . . . . . . 10 $/\$
263	262	nn0red 10874	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10876	. . . . . . . . 9 $/\$
265		nn0uz 11140	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2555	. . . . . . . . . . 11
267		fzss1 11747	. . . . . . . . . . 11
268	266, 267	syl 16	. . . . . . . . . 10
269		eluz 11119	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 661	. . . . . . . . . . . 12
271	48, 270	mpbird 232	. . . . . . . . . . 11
272		fzss2 11748	. . . . . . . . . . 11
273	271, 272	syl 16	. . . . . . . . . 10
274	268, 273	sstrd 3509	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13621	. . . . . . . 8
276	32	nn0zd 10988	. . . . . . . . . . . 12
277		bccmpl 12389	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 661	. . . . . . . . . . . . . 14
279	111	oveq2d 6312	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2498	. . . . . . . . . . . . 13
281	52	nncnd 10572	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2546	. . . . . . . . . . . 12
283		oveq2 6304	. . . . . . . . . . . . 13
284	283	fsum1 13575	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 661	. . . . . . . . . . 11
286	285, 280	eqtr4d 2501	. . . . . . . . . 10
287	286	oveq1d 6311	. . . . . . . . 9
288	21, 105	npcand 9954	. . . . . . . . . . 11
289		uzid 11120	. . . . . . . . . . . . 13
290	276, 289	syl 16	. . . . . . . . . . . 12
291		peano2uz 11159	. . . . . . . . . . . 12
292	290, 291	syl 16	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2546	. . . . . . . . . 10
294	274	sselda 3499	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10875	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 470	. . . . . . . . . 10 $/\$
297		oveq2 6304	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13577	. . . . . . . . 9
299	281	2timesd 10802	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2509	. . . . . . . 8
301		binom11 13655	. . . . . . . . 9
302	39, 301	syl 16	. . . . . . . 8
303	275, 300, 302	3brtr4d 4486	. . . . . . 7
304		mulcom 9595	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 663	. . . . . . 7
306	30	oveq2d 6312	. . . . . . . 8
307		expp1 12175	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 663	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12315	. . . . . . . . . 10
312		sq2 12266	. . . . . . . . . . 11
313	312	oveq1i 6306	. . . . . . . . . 10
314	311, 313	syl6eq 2514	. . . . . . . . 9
315	314	oveq1d 6311	. . . . . . . 8
316	306, 308, 315	3eqtrd 2502	. . . . . . 7
317	303, 305, 316	3brtr3d 4485	. . . . . 6
318	52	nnred 10571	. . . . . . 7
319		reexpcl 12185	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 663	. . . . . . 7
321		2re 10626	. . . . . . . . 9
322		2pos 10648	. . . . . . . . 9
323	321, 322	pm3.2i 455	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10415	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1228	. . . . . 6
327	317, 326	mpbird 232	. . . . 5
328	60	recni 9625	. . . . . . . 8
329		mulcom 9595	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 663	. . . . . . 7
331	330	fveq2d 5876	. . . . . 6
332		reexplog 23104	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 663	. . . . . 6
334	331, 333	eqtr4d 2501	. . . . 5
335	327, 252, 334	3brtr4d 4486	. . . 4
336		efle 13864	. . . . 5 $/\$
337	54, 63, 336	syl2anc 661	. . . 4
338	335, 337	mpbird 232	. . 3
339	54, 63, 11, 338	leadd2dd 10188	. 2
340	8, 55, 64, 258, 339	letrd 9756	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1395

wcel 1819

wne 2652

wral 2807

wss 3471

cif 3944 class class class wbr 4456

cmpt 4515

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

clt 9645

cle 9646

cmin 9824

cdiv 10227

cn 10556

c2 10606

c4 10608

cn0 10816

cz 10885

cuz 11106

crp 11245

cfz 11697

cseq 12109

cexp 12168

cfa 12355

cbc 12382

csu 13519

ce 13808

cdvds 13997

cprime 14228

cpc 14371

clog 23067

ccht 23489

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588 ax-mulf 9589

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-ixp 7489 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ioc 11559 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11821 df-fl 11931 df-mod 11999 df-seq 12110 df-exp 12169 df-fac 12356 df-bc 12383 df-hash 12408 df-shft 12911 df-cj 12943 df-re 12944 df-im 12945 df-sqrt 13079 df-abs 13080 df-limsup 13305 df-clim 13322 df-rlim 13323 df-sum 13520 df-ef 13814 df-sin 13816 df-cos 13817 df-pi 13819 df-dvds 13998 df-gcd 14156 df-prm 14229 df-pc 14372 df-struct 14645 df-ndx 14646 df-slot 14647 df-base 14648 df-sets 14649 df-ress 14650 df-plusg 14724 df-mulr 14725 df-starv 14726 df-sca 14727 df-vsca 14728 df-ip 14729 df-tset 14730 df-ple 14731 df-ds 14733 df-unif 14734 df-hom 14735 df-cco 14736 df-rest 14839 df-topn 14840 df-0g 14858 df-gsum 14859 df-topgen 14860 df-pt 14861 df-prds 14864 df-xrs 14918 df-qtop 14923 df-imas 14924 df-xps 14926 df-mre 15002 df-mrc 15003 df-acs 15005 df-mgm 15998 df-sgrp 16037 df-mnd 16047 df-submnd 16093 df-mulg 16186 df-cntz 16481 df-cmn 16926 df-psmet 18537 df-xmet 18538 df-met 18539 df-bl 18540 df-mopn 18541 df-fbas 18542 df-fg 18543 df-cnfld 18547 df-top 19525 df-bases 19527 df-topon 19528 df-topsp 19529 df-cld 19646 df-ntr 19647 df-cls 19648 df-nei 19725 df-lp 19763 df-perf 19764 df-cn 19854 df-cnp 19855 df-haus 19942 df-tx 20188 df-hmeo 20381 df-fil 20472 df-fm 20564 df-flim 20565 df-flf 20566 df-xms 20948 df-ms 20949 df-tms 20950 df-cncf 21507 df-limc 22395 df-dv 22396 df-log 23069 df-cht 23495

This theorem is referenced by: chtub 23612

W3C validator