chtublem - Metamath Proof Explorer

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

Theorem chtublem 22555

Description: Lemma for chtub 22556. (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 10484	. . . . . 6
2		nnmulcl 10350	. . . . . 6 $/\$
3	1, 2	mpan 670	. . . . 5
4	3	nnred 10342	. . . 4
5		peano2rem 9680	. . . 4
6	4, 5	syl 16	. . 3
7		chtcl 22452	. . 3
8	6, 7	syl 16	. 2
9		nnre 10334	. . . 4
10		chtcl 22452	. . . 4
11	9, 10	syl 16	. . 3
12		nnnn0 10591	. . . . . . 7
13		2m1e1 10441	. . . . . . . . . . 11
14	13	oveq2i 6107	. . . . . . . . . 10
15	3	nncnd 10343	. . . . . . . . . . . 12
16		2cn 10397	. . . . . . . . . . . . 13
17		ax-1cn 9345	. . . . . . . . . . . . 13
18		subsub 9644	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1306	. . . . . . . . . . . 12
20	15, 19	syl 16	. . . . . . . . . . 11
21		nncn 10335	. . . . . . . . . . . . . 14
22		subdi 9783	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1305	. . . . . . . . . . . . . 14
24	21, 23	syl 16	. . . . . . . . . . . . 13
25		2t1e2 10475	. . . . . . . . . . . . . 14
26	25	oveq2i 6107	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2491	. . . . . . . . . . . 12
28	27	oveq1d 6111	. . . . . . . . . . 11
29	20, 28	eqtr4d 2478	. . . . . . . . . 10
30	14, 29	syl5eqr 2489	. . . . . . . . 9
31		2nn0 10601	. . . . . . . . . . 11
32		nnm1nn0 10626	. . . . . . . . . . 11
33		nn0mulcl 10621	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 663	. . . . . . . . . 10
35		nn0p1nn 10624	. . . . . . . . . 10
36	34, 35	syl 16	. . . . . . . . 9
37	30, 36	eqeltrd 2517	. . . . . . . 8
38		nnnn0 10591	. . . . . . . 8
39	37, 38	syl 16	. . . . . . 7
40		1re 9390	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10353	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 9959	. . . . . . . . 9
44	21	2timesd 10572	. . . . . . . . 9
45	43, 44	breqtrrd 4323	. . . . . . . 8
46		leaddsub 9820	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1218	. . . . . . . 8
48	45, 47	mpbid 210	. . . . . . 7
49		elfz2nn0 11485	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1172	. . . . . 6
51		bccl2 12104	. . . . . 6
52	50, 51	syl 16	. . . . 5
53	52	nnrpd 11031	. . . 4
54	53	relogcld 22077	. . 3
55	11, 54	readdcld 9418	. 2
56		4re 10403	. . . . . 6
57		4pos 10422	. . . . . 6
58	56, 57	elrpii 10999	. . . . 5
59		relogcl 22032	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10642	. . . 4
62		remulcl 9372	. . . 4 $/\$
63	60, 61, 62	sylancr 663	. . 3
64	11, 63	readdcld 9418	. 2
65		iftrue 3802	. . . . . . . . . . . 12
66	65	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 13922	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10631	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 663	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3802	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6111	. . . . . . . . . . . . . . 15
74	73	breq2d 4309	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 222	. . . . . . . . . . . . 13 $/\$
76	75	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 13771	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 13772	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 10751	. . . . . . . . . . . . . . . . . . . 20
82		eluz 10879	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 478	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 13593	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12066	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 16	. . . . . . . . . . . . . . . . . 18
91		pcelnn 13941	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 478	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10369	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3804	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6111	. . . . . . . . . . . . . . . 16
98	97	ad2antll 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10643	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9575	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12086	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 9744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6111	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10643	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9726	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5700	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6111	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6112	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2475	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10673	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10359	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12066	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 16	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12066	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 16	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10374	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 13924	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1218	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10673	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10359	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10673	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10359	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 13923	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1218	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2479	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 756	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 13809	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1189	. . . . . . . . . . . . . . . . . . . . . . . 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 10673	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 13572	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12065	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4309	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 177	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 13942	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 13942	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6114	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9549	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2491	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6112	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 13921	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 478	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10643	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9713	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2479	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4323	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 615	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 158	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4317	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 434	. . . . . . . . 9 $/\$
188		1nn0 10600	. . . . . . . . . . . . 13
189		0nn0 10599	. . . . . . . . . . . . 13
190	188, 189	keepel 3862	. . . . . . . . . . . 12
191		nn0addcl 10620	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 663	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10644	. . . . . . . . . 10 $/\$
194		iffalse 3804	. . . . . . . . . . 11
195	194	breq1d 4307	. . . . . . . . . 10
196	193, 195	syl5ibrcom 222	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 158	. . . . . . . 8 $/\$
198		eqid 2443	. . . . . . . . . . . . 13
199	198	prmorcht 22521	. . . . . . . . . . . 12
200	37, 199	syl 16	. . . . . . . . . . 11
201	200	oveq2d 6112	. . . . . . . . . 10
202	201	adantr 465	. . . . . . . . 9 $/\$
203		nncn 10335	. . . . . . . . . . . . . 14
204	203	exp1d 12008	. . . . . . . . . . . . 13
205	204	ifeq1d 3812	. . . . . . . . . . . 12
206	205	mpteq2ia 4379	. . . . . . . . . . 11
207	206	eqcomi 2447	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2804	. . . . . . . . . 10 $/\$
210	37	adantr 465	. . . . . . . . . 10 $/\$
211		eqidd 2444	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 13959	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2475	. . . . . . . 8 $/\$
214		efchtcl 22454	. . . . . . . . . . . . 13
215	9, 214	syl 16	. . . . . . . . . . . 12
216	215	adantr 465	. . . . . . . . . . 11 $/\$
217		nnz 10673	. . . . . . . . . . . 12
218		nnne0 10359	. . . . . . . . . . . 12
219	217, 218	jca 532	. . . . . . . . . . 11 $/\$
220	216, 219	syl 16	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10673	. . . . . . . . . . . 12
222		nnne0 10359	. . . . . . . . . . . 12
223	221, 222	jca 532	. . . . . . . . . . 11 $/\$
224	68, 223	syl 16	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 13923	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1218	. . . . . . . . 9 $/\$
227	198	prmorcht 22521	. . . . . . . . . . . . 13
228	227	oveq2d 6112	. . . . . . . . . . . 12
229	228	adantr 465	. . . . . . . . . . 11 $/\$
230		simpl 457	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 13959	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2475	. . . . . . . . . 10 $/\$
233	232	oveq1d 6111	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2475	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4327	. . . . . . 7 $/\$
236	235	ralrimiva 2804	. . . . . 6
237		efchtcl 22454	. . . . . . . . 9
238	6, 237	syl 16	. . . . . . . 8
239	238	nnzd 10751	. . . . . . 7
240	215, 52	nnmulcld 10374	. . . . . . . 8
241	240	nnzd 10751	. . . . . . 7
242		pc2dvds 13950	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 661	. . . . . 6
244	236, 243	mpbird 232	. . . . 5
245		dvdsle 13583	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 661	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9417	. . . . . 6
249	54	recnd 9417	. . . . . 6
250		efadd 13384	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 661	. . . . 5
252	53	reeflogd 22078	. . . . . 6
253	252	oveq2d 6112	. . . . 5
254	251, 253	eqtrd 2475	. . . 4
255	247, 254	breqtrrd 4323	. . 3
256		efle 13407	. . . 4 $/\$
257	8, 55, 256	syl2anc 661	. . 3
258	255, 257	mpbird 232	. 2
259		fzfid 11800	. . . . . . . . 9
260		elfzelz 11458	. . . . . . . . . . 11
261		bccl 12103	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 477	. . . . . . . . . 10 $/\$
263	262	nn0red 10642	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10644	. . . . . . . . 9 $/\$
265		nn0uz 10900	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2533	. . . . . . . . . . 11
267		fzss1 11502	. . . . . . . . . . 11
268	266, 267	syl 16	. . . . . . . . . 10
269		eluz 10879	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 661	. . . . . . . . . . . 12
271	48, 270	mpbird 232	. . . . . . . . . . 11
272		fzss2 11503	. . . . . . . . . . 11
273	271, 272	syl 16	. . . . . . . . . 10
274	268, 273	sstrd 3371	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13264	. . . . . . . 8
276	32	nn0zd 10750	. . . . . . . . . . . 12
277		bccmpl 12090	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 661	. . . . . . . . . . . . . 14
279	111	oveq2d 6112	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2475	. . . . . . . . . . . . 13
281	52	nncnd 10343	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2518	. . . . . . . . . . . 12
283		oveq2 6104	. . . . . . . . . . . . 13
284	283	fsum1 13223	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 661	. . . . . . . . . . 11
286	285, 280	eqtr4d 2478	. . . . . . . . . 10
287	286	oveq1d 6111	. . . . . . . . 9
288	21, 105	npcand 9728	. . . . . . . . . . 11
289		uzid 10880	. . . . . . . . . . . . 13
290	276, 289	syl 16	. . . . . . . . . . . 12
291		peano2uz 10913	. . . . . . . . . . . 12
292	290, 291	syl 16	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2518	. . . . . . . . . 10
294	274	sselda 3361	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10643	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 470	. . . . . . . . . 10 $/\$
297		oveq2 6104	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13225	. . . . . . . . 9
299	281	2timesd 10572	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2486	. . . . . . . 8
301		binom11 13300	. . . . . . . . 9
302	39, 301	syl 16	. . . . . . . 8
303	275, 300, 302	3brtr4d 4327	. . . . . . 7
304		mulcom 9373	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 663	. . . . . . 7
306	30	oveq2d 6112	. . . . . . . 8
307		expp1 11877	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 663	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12016	. . . . . . . . . 10
312		sq2 11967	. . . . . . . . . . 11
313	312	oveq1i 6106	. . . . . . . . . 10
314	311, 313	syl6eq 2491	. . . . . . . . 9
315	314	oveq1d 6111	. . . . . . . 8
316	306, 308, 315	3eqtrd 2479	. . . . . . 7
317	303, 305, 316	3brtr3d 4326	. . . . . 6
318	52	nnred 10342	. . . . . . 7
319		reexpcl 11887	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 663	. . . . . . 7
321		2re 10396	. . . . . . . . 9
322		2pos 10418	. . . . . . . . 9
323	321, 322	pm3.2i 455	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10186	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1218	. . . . . 6
327	317, 326	mpbird 232	. . . . 5
328	60	recni 9403	. . . . . . . 8
329		mulcom 9373	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 663	. . . . . . 7
331	330	fveq2d 5700	. . . . . 6
332		reexplog 22048	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 663	. . . . . 6
334	331, 333	eqtr4d 2478	. . . . 5
335	327, 252, 334	3brtr4d 4327	. . . 4
336		efle 13407	. . . . 5 $/\$
337	54, 63, 336	syl2anc 661	. . . 4
338	335, 337	mpbird 232	. . 3
339	54, 63, 11, 338	leadd2dd 9959	. 2
340	8, 55, 64, 258, 339	letrd 9533	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wne 2611

wral 2720

wss 3333

cif 3796 class class class wbr 4297

cmpt 4355

cfv 5423 (class class class)co 6096

cc 9285

cr 9286

cc0 9287

c1 9288

caddc 9290

cmul 9292

clt 9423

cle 9424

cmin 9600

cdiv 9998

cn 10327

c2 10376

c4 10378

cn0 10584

cz 10651

cuz 10866

crp 10996

cfz 11442

cseq 11811

cexp 11870

cfa 12056

cbc 12083

csu 13168

ce 13352

cdivides 13540

cprime 13768

cpc 13908

clog 22011

ccht 22433

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377 ax-inf2 7852 ax-cnex 9343 ax-resscn 9344 ax-1cn 9345 ax-icn 9346 ax-addcl 9347 ax-addrcl 9348 ax-mulcl 9349 ax-mulrcl 9350 ax-mulcom 9351 ax-addass 9352 ax-mulass 9353 ax-distr 9354 ax-i2m1 9355 ax-1ne0 9356 ax-1rid 9357 ax-rnegex 9358 ax-rrecex 9359 ax-cnre 9360 ax-pre-lttri 9361 ax-pre-lttrn 9362 ax-pre-ltadd 9363 ax-pre-mulgt0 9364 ax-pre-sup 9365 ax-addf 9366 ax-mulf 9367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-nel 2614 df-ral 2725 df-rex 2726 df-reu 2727 df-rmo 2728 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-pss 3349 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-tp 3887 df-op 3889 df-uni 4097 df-int 4134 df-iun 4178 df-iin 4179 df-br 4298 df-opab 4356 df-mpt 4357 df-tr 4391 df-eprel 4637 df-id 4641 df-po 4646 df-so 4647 df-fr 4684 df-se 4685 df-we 4686 df-ord 4727 df-on 4728 df-lim 4729 df-suc 4730 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-isom 5432 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-of 6325 df-om 6482 df-1st 6582 df-2nd 6583 df-supp 6696 df-recs 6837 df-rdg 6871 df-1o 6925 df-2o 6926 df-oadd 6929 df-er 7106 df-map 7221 df-pm 7222 df-ixp 7269 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-fsupp 7626 df-fi 7666 df-sup 7696 df-oi 7729 df-card 8114 df-cda 8342 df-pnf 9425 df-mnf 9426 df-xr 9427 df-ltxr 9428 df-le 9429 df-sub 9602 df-neg 9603 df-div 9999 df-nn 10328 df-2 10385 df-3 10386 df-4 10387 df-5 10388 df-6 10389 df-7 10390 df-8 10391 df-9 10392 df-10 10393 df-n0 10585 df-z 10652 df-dec 10761 df-uz 10867 df-q 10959 df-rp 10997 df-xneg 11094 df-xadd 11095 df-xmul 11096 df-ioo 11309 df-ioc 11310 df-ico 11311 df-icc 11312 df-fz 11443 df-fzo 11554 df-fl 11647 df-mod 11714 df-seq 11812 df-exp 11871 df-fac 12057 df-bc 12084 df-hash 12109 df-shft 12561 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-limsup 12954 df-clim 12971 df-rlim 12972 df-sum 13169 df-ef 13358 df-sin 13360 df-cos 13361 df-pi 13363 df-dvds 13541 df-gcd 13696 df-prm 13769 df-pc 13909 df-struct 14181 df-ndx 14182 df-slot 14183 df-base 14184 df-sets 14185 df-ress 14186 df-plusg 14256 df-mulr 14257 df-starv 14258 df-sca 14259 df-vsca 14260 df-ip 14261 df-tset 14262 df-ple 14263 df-ds 14265 df-unif 14266 df-hom 14267 df-cco 14268 df-rest 14366 df-topn 14367 df-0g 14385 df-gsum 14386 df-topgen 14387 df-pt 14388 df-prds 14391 df-xrs 14445 df-qtop 14450 df-imas 14451 df-xps 14453 df-mre 14529 df-mrc 14530 df-acs 14532 df-mnd 15420 df-submnd 15470 df-mulg 15553 df-cntz 15840 df-cmn 16284 df-psmet 17814 df-xmet 17815 df-met 17816 df-bl 17817 df-mopn 17818 df-fbas 17819 df-fg 17820 df-cnfld 17824 df-top 18508 df-bases 18510 df-topon 18511 df-topsp 18512 df-cld 18628 df-ntr 18629 df-cls 18630 df-nei 18707 df-lp 18745 df-perf 18746 df-cn 18836 df-cnp 18837 df-haus 18924 df-tx 19140 df-hmeo 19333 df-fil 19424 df-fm 19516 df-flim 19517 df-flf 19518 df-xms 19900 df-ms 19901 df-tms 19902 df-cncf 20459 df-limc 21346 df-dv 21347 df-log 22013 df-cht 22439

This theorem is referenced by: chtub 22556

W3C validator