chtublem - Metamath Proof Explorer

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

Theorem chtublem 24218

Description: Lemma for chtub 24219. (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 10790	. . . . . 6
2		nnmulcl 10654	. . . . . 6 $/\$
3	1, 2	mpan 684	. . . . 5
4	3	nnred 10646	. . . 4
5		peano2rem 9961	. . . 4
6	4, 5	syl 17	. . 3
7		chtcl 24115	. . 3
8	6, 7	syl 17	. 2
9		nnre 10638	. . . 4
10		chtcl 24115	. . . 4
11	9, 10	syl 17	. . 3
12		nnnn0 10900	. . . . . . 7
13		2m1e1 10746	. . . . . . . . . . 11
14	13	oveq2i 6319	. . . . . . . . . 10
15	3	nncnd 10647	. . . . . . . . . . . 12
16		2cn 10702	. . . . . . . . . . . . 13
17		ax-1cn 9615	. . . . . . . . . . . . 13
18		subsub 9924	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1382	. . . . . . . . . . . 12
20	15, 19	syl 17	. . . . . . . . . . 11
21		nncn 10639	. . . . . . . . . . . . . 14
22		subdi 10073	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1381	. . . . . . . . . . . . . 14
24	21, 23	syl 17	. . . . . . . . . . . . 13
25		2t1e2 10781	. . . . . . . . . . . . . 14
26	25	oveq2i 6319	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2521	. . . . . . . . . . . 12
28	27	oveq1d 6323	. . . . . . . . . . 11
29	20, 28	eqtr4d 2508	. . . . . . . . . 10
30	14, 29	syl5eqr 2519	. . . . . . . . 9
31		2nn0 10910	. . . . . . . . . . 11
32		nnm1nn0 10935	. . . . . . . . . . 11
33		nn0mulcl 10930	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 676	. . . . . . . . . 10
35		nn0p1nn 10933	. . . . . . . . . 10
36	34, 35	syl 17	. . . . . . . . 9
37	30, 36	eqeltrd 2549	. . . . . . . 8
38		nnnn0 10900	. . . . . . . 8
39	37, 38	syl 17	. . . . . . 7
40		1re 9660	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10657	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 10249	. . . . . . . . 9
44	21	2timesd 10878	. . . . . . . . 9
45	43, 44	breqtrrd 4422	. . . . . . . 8
46		leaddsub 10111	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1292	. . . . . . . 8
48	45, 47	mpbid 215	. . . . . . 7
49		elfz2nn0 11911	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1214	. . . . . 6
51		bccl2 12546	. . . . . 6
52	50, 51	syl 17	. . . . 5
53	52	nnrpd 11362	. . . 4
54	53	relogcld 23651	. . 3
55	11, 54	readdcld 9688	. 2
56		4re 10708	. . . . . 6
57		4pos 10727	. . . . . 6
58	56, 57	elrpii 11328	. . . . 5
59		relogcl 23604	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10950	. . . 4
62		remulcl 9642	. . . 4 $/\$
63	60, 61, 62	sylancr 676	. . 3
64	11, 63	readdcld 9688	. 2
65		iftrue 3878	. . . . . . . . . . . 12
66	65	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 468	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 14879	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10940	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 676	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3878	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6323	. . . . . . . . . . . . . . 15
74	73	breq2d 4407	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 230	. . . . . . . . . . . . 13 $/\$
76	75	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 14704	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 741	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 14705	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 11062	. . . . . . . . . . . . . . . . . . . 20
82		eluz 11196	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 486	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 240	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 14438	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12507	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 17	. . . . . . . . . . . . . . . . . 18
91		pcelnn 14898	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 486	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 240	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3881	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6323	. . . . . . . . . . . . . . . 16
98	97	ad2antll 743	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10951	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9852	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12528	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 17	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 10025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 10007	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2505	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10983	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10664	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 541	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12507	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 17	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12507	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 17	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10679	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 14881	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1292	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10983	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10664	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10983	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10664	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 14880	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1292	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2509	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 774	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 14750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1233	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	12, 148	sylan 479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 182	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	80	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 10983	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 14415	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12506	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 242	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 182	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 14899	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 486	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 240	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 14899	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 486	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 240	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6326	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9826	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2521	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 14878	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 486	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10951	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9994	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2509	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2509	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4422	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 626	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 163	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4416	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 441	. . . . . . . . 9 $/\$
188		1nn0 10909	. . . . . . . . . . . . 13
189		0nn0 10908	. . . . . . . . . . . . 13
190	188, 189	keepel 3939	. . . . . . . . . . . 12
191		nn0addcl 10929	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 676	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10952	. . . . . . . . . 10 $/\$
194		iffalse 3881	. . . . . . . . . . 11
195	194	breq1d 4405	. . . . . . . . . 10
196	193, 195	syl5ibrcom 230	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 163	. . . . . . . 8 $/\$
198		eqid 2471	. . . . . . . . . . . . 13
199	198	prmorcht 24184	. . . . . . . . . . . 12
200	37, 199	syl 17	. . . . . . . . . . 11
201	200	oveq2d 6324	. . . . . . . . . 10
202	201	adantr 472	. . . . . . . . 9 $/\$
203		nncn 10639	. . . . . . . . . . . . . 14
204	203	exp1d 12449	. . . . . . . . . . . . 13
205	204	ifeq1d 3890	. . . . . . . . . . . 12
206	205	mpteq2ia 4478	. . . . . . . . . . 11
207	206	eqcomi 2480	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2809	. . . . . . . . . 10 $/\$
210	37	adantr 472	. . . . . . . . . 10 $/\$
211		eqidd 2472	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 14916	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2505	. . . . . . . 8 $/\$
214		efchtcl 24117	. . . . . . . . . . . . 13
215	9, 214	syl 17	. . . . . . . . . . . 12
216	215	adantr 472	. . . . . . . . . . 11 $/\$
217		nnz 10983	. . . . . . . . . . . 12
218		nnne0 10664	. . . . . . . . . . . 12
219	217, 218	jca 541	. . . . . . . . . . 11 $/\$
220	216, 219	syl 17	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10983	. . . . . . . . . . . 12
222		nnne0 10664	. . . . . . . . . . . 12
223	221, 222	jca 541	. . . . . . . . . . 11 $/\$
224	68, 223	syl 17	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 14880	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1292	. . . . . . . . 9 $/\$
227	198	prmorcht 24184	. . . . . . . . . . . . 13
228	227	oveq2d 6324	. . . . . . . . . . . 12
229	228	adantr 472	. . . . . . . . . . 11 $/\$
230		simpl 464	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 14916	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2505	. . . . . . . . . 10 $/\$
233	232	oveq1d 6323	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2505	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4426	. . . . . . 7 $/\$
236	235	ralrimiva 2809	. . . . . 6
237		efchtcl 24117	. . . . . . . . 9
238	6, 237	syl 17	. . . . . . . 8
239	238	nnzd 11062	. . . . . . 7
240	215, 52	nnmulcld 10679	. . . . . . . 8
241	240	nnzd 11062	. . . . . . 7
242		pc2dvds 14907	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 673	. . . . . 6
244	236, 243	mpbird 240	. . . . 5
245		dvdsle 14427	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 673	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9687	. . . . . 6
249	54	recnd 9687	. . . . . 6
250		efadd 14225	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 673	. . . . 5
252	53	reeflogd 23652	. . . . . 6
253	252	oveq2d 6324	. . . . 5
254	251, 253	eqtrd 2505	. . . 4
255	247, 254	breqtrrd 4422	. . 3
256		efle 14249	. . . 4 $/\$
257	8, 55, 256	syl2anc 673	. . 3
258	255, 257	mpbird 240	. 2
259		fzfid 12224	. . . . . . . . 9
260		elfzelz 11826	. . . . . . . . . . 11
261		bccl 12545	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 485	. . . . . . . . . 10 $/\$
263	262	nn0red 10950	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10952	. . . . . . . . 9 $/\$
265		nn0uz 11217	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2559	. . . . . . . . . . 11
267		fzss1 11863	. . . . . . . . . . 11
268	266, 267	syl 17	. . . . . . . . . 10
269		eluz 11196	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 673	. . . . . . . . . . . 12
271	48, 270	mpbird 240	. . . . . . . . . . 11
272		fzss2 11864	. . . . . . . . . . 11
273	271, 272	syl 17	. . . . . . . . . 10
274	268, 273	sstrd 3428	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13933	. . . . . . . 8
276	32	nn0zd 11061	. . . . . . . . . . . 12
277		bccmpl 12532	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 673	. . . . . . . . . . . . . 14
279	111	oveq2d 6324	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2505	. . . . . . . . . . . . 13
281	52	nncnd 10647	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2550	. . . . . . . . . . . 12
283		oveq2 6316	. . . . . . . . . . . . 13
284	283	fsum1 13885	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 673	. . . . . . . . . . 11
286	285, 280	eqtr4d 2508	. . . . . . . . . 10
287	286	oveq1d 6323	. . . . . . . . 9
288	21, 105	npcand 10009	. . . . . . . . . . 11
289		uzid 11197	. . . . . . . . . . . . 13
290	276, 289	syl 17	. . . . . . . . . . . 12
291		peano2uz 11235	. . . . . . . . . . . 12
292	290, 291	syl 17	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2550	. . . . . . . . . 10
294	274	sselda 3418	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10951	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 478	. . . . . . . . . 10 $/\$
297		oveq2 6316	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13889	. . . . . . . . 9
299	281	2timesd 10878	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2516	. . . . . . . 8
301		binom11 13967	. . . . . . . . 9
302	39, 301	syl 17	. . . . . . . 8
303	275, 300, 302	3brtr4d 4426	. . . . . . 7
304		mulcom 9643	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 676	. . . . . . 7
306	30	oveq2d 6324	. . . . . . . 8
307		expp1 12317	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 676	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12457	. . . . . . . . . 10
312		sq2 12409	. . . . . . . . . . 11
313	312	oveq1i 6318	. . . . . . . . . 10
314	311, 313	syl6eq 2521	. . . . . . . . 9
315	314	oveq1d 6323	. . . . . . . 8
316	306, 308, 315	3eqtrd 2509	. . . . . . 7
317	303, 305, 316	3brtr3d 4425	. . . . . 6
318	52	nnred 10646	. . . . . . 7
319		reexpcl 12327	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 676	. . . . . . 7
321		2re 10701	. . . . . . . . 9
322		2pos 10723	. . . . . . . . 9
323	321, 322	pm3.2i 462	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10479	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1292	. . . . . 6
327	317, 326	mpbird 240	. . . . 5
328	60	recni 9673	. . . . . . . 8
329		mulcom 9643	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 676	. . . . . . 7
331	330	fveq2d 5883	. . . . . 6
332		reexplog 23623	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 676	. . . . . 6
334	331, 333	eqtr4d 2508	. . . . 5
335	327, 252, 334	3brtr4d 4426	. . . 4
336		efle 14249	. . . . 5 $/\$
337	54, 63, 336	syl2anc 673	. . . 4
338	335, 337	mpbird 240	. . 3
339	54, 63, 11, 338	leadd2dd 10249	. 2
340	8, 55, 64, 258, 339	letrd 9809	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904

wne 2641

wral 2756

wss 3390

cif 3872 class class class wbr 4395

cmpt 4454

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

c2 10681

c4 10683

cn0 10893

cz 10961

cuz 11182

crp 11325

cfz 11810

cseq 12251

cexp 12310

cfa 12497

cbc 12525

csu 13829

ce 14191

cdvds 14382

cprime 14701

cpc 14865

clog 23583

ccht 24096

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cht 24102

This theorem is referenced by: chtub 24219

W3C validator