chtublem - Metamath Proof Explorer

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

Theorem chtublem 22509

Description: Lemma for chtub 22510. (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 10475	. . . . . 6
2		nnmulcl 10341	. . . . . 6 $/\$
3	1, 2	mpan 665	. . . . 5
4	3	nnred 10333	. . . 4
5		peano2rem 9671	. . . 4
6	4, 5	syl 16	. . 3
7		chtcl 22406	. . 3
8	6, 7	syl 16	. 2
9		nnre 10325	. . . 4
10		chtcl 22406	. . . 4
11	9, 10	syl 16	. . 3
12		nnnn0 10582	. . . . . . 7
13		2m1e1 10432	. . . . . . . . . . 11
14	13	oveq2i 6101	. . . . . . . . . 10
15	3	nncnd 10334	. . . . . . . . . . . 12
16		2cn 10388	. . . . . . . . . . . . 13
17		ax-1cn 9336	. . . . . . . . . . . . 13
18		subsub 9635	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1301	. . . . . . . . . . . 12
20	15, 19	syl 16	. . . . . . . . . . 11
21		nncn 10326	. . . . . . . . . . . . . 14
22		subdi 9774	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1300	. . . . . . . . . . . . . 14
24	21, 23	syl 16	. . . . . . . . . . . . 13
25		2t1e2 10466	. . . . . . . . . . . . . 14
26	25	oveq2i 6101	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2489	. . . . . . . . . . . 12
28	27	oveq1d 6105	. . . . . . . . . . 11
29	20, 28	eqtr4d 2476	. . . . . . . . . 10
30	14, 29	syl5eqr 2487	. . . . . . . . 9
31		2nn0 10592	. . . . . . . . . . 11
32		nnm1nn0 10617	. . . . . . . . . . 11
33		nn0mulcl 10612	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 658	. . . . . . . . . 10
35		nn0p1nn 10615	. . . . . . . . . 10
36	34, 35	syl 16	. . . . . . . . 9
37	30, 36	eqeltrd 2515	. . . . . . . 8
38		nnnn0 10582	. . . . . . . 8
39	37, 38	syl 16	. . . . . . 7
40		1re 9381	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10344	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 9950	. . . . . . . . 9
44	21	2timesd 10563	. . . . . . . . 9
45	43, 44	breqtrrd 4315	. . . . . . . 8
46		leaddsub 9811	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1213	. . . . . . . 8
48	45, 47	mpbid 210	. . . . . . 7
49		elfz2nn0 11476	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1167	. . . . . 6
51		bccl2 12095	. . . . . 6
52	50, 51	syl 16	. . . . 5
53	52	nnrpd 11022	. . . 4
54	53	relogcld 22031	. . 3
55	11, 54	readdcld 9409	. 2
56		4re 10394	. . . . . 6
57		4pos 10413	. . . . . 6
58	56, 57	elrpii 10990	. . . . 5
59		relogcl 21986	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10633	. . . 4
62		remulcl 9363	. . . 4 $/\$
63	60, 61, 62	sylancr 658	. . 3
64	11, 63	readdcld 9409	. 2
65		iftrue 3794	. . . . . . . . . . . 12
66	65	adantl 463	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 458	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 462	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 13913	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10622	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 658	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3794	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6105	. . . . . . . . . . . . . . 15
74	73	breq2d 4301	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 222	. . . . . . . . . . . . 13 $/\$
76	75	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 13762	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 721	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 750	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 13763	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 10742	. . . . . . . . . . . . . . . . . . . 20
82		eluz 10870	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 475	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 13584	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12057	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 16	. . . . . . . . . . . . . . . . . 18
91		pcelnn 13932	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 475	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10360	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3796	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6105	. . . . . . . . . . . . . . . 16
98	97	ad2antll 723	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10634	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9566	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12077	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 9735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10634	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9717	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6106	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2473	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6106	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10664	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10350	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 529	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12057	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 16	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12057	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 16	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10365	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 13915	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1213	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10664	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10350	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 529	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 462	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10664	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10350	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 529	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 462	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 13914	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1213	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6106	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2477	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 13800	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1184	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	12, 148	sylan 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 177	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	80	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 456	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 10664	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 13563	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12056	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4301	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 462	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 177	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 13933	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 462	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 13933	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 462	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6108	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9540	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2489	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6106	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 13912	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 475	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10634	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9704	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4315	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 612	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 158	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4309	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 434	. . . . . . . . 9 $/\$
188		1nn0 10591	. . . . . . . . . . . . 13
189		0nn0 10590	. . . . . . . . . . . . 13
190	188, 189	keepel 3854	. . . . . . . . . . . 12
191		nn0addcl 10611	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 658	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10635	. . . . . . . . . 10 $/\$
194		iffalse 3796	. . . . . . . . . . 11
195	194	breq1d 4299	. . . . . . . . . 10
196	193, 195	syl5ibrcom 222	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 158	. . . . . . . 8 $/\$
198		eqid 2441	. . . . . . . . . . . . 13
199	198	prmorcht 22475	. . . . . . . . . . . 12
200	37, 199	syl 16	. . . . . . . . . . 11
201	200	oveq2d 6106	. . . . . . . . . 10
202	201	adantr 462	. . . . . . . . 9 $/\$
203		nncn 10326	. . . . . . . . . . . . . 14
204	203	exp1d 11999	. . . . . . . . . . . . 13
205	204	ifeq1d 3804	. . . . . . . . . . . 12
206	205	mpteq2ia 4371	. . . . . . . . . . 11
207	206	eqcomi 2445	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2797	. . . . . . . . . 10 $/\$
210	37	adantr 462	. . . . . . . . . 10 $/\$
211		eqidd 2442	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 13950	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2473	. . . . . . . 8 $/\$
214		efchtcl 22408	. . . . . . . . . . . . 13
215	9, 214	syl 16	. . . . . . . . . . . 12
216	215	adantr 462	. . . . . . . . . . 11 $/\$
217		nnz 10664	. . . . . . . . . . . 12
218		nnne0 10350	. . . . . . . . . . . 12
219	217, 218	jca 529	. . . . . . . . . . 11 $/\$
220	216, 219	syl 16	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10664	. . . . . . . . . . . 12
222		nnne0 10350	. . . . . . . . . . . 12
223	221, 222	jca 529	. . . . . . . . . . 11 $/\$
224	68, 223	syl 16	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 13914	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1213	. . . . . . . . 9 $/\$
227	198	prmorcht 22475	. . . . . . . . . . . . 13
228	227	oveq2d 6106	. . . . . . . . . . . 12
229	228	adantr 462	. . . . . . . . . . 11 $/\$
230		simpl 454	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 13950	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2473	. . . . . . . . . 10 $/\$
233	232	oveq1d 6105	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2473	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4319	. . . . . . 7 $/\$
236	235	ralrimiva 2797	. . . . . 6
237		efchtcl 22408	. . . . . . . . 9
238	6, 237	syl 16	. . . . . . . 8
239	238	nnzd 10742	. . . . . . 7
240	215, 52	nnmulcld 10365	. . . . . . . 8
241	240	nnzd 10742	. . . . . . 7
242		pc2dvds 13941	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 656	. . . . . 6
244	236, 243	mpbird 232	. . . . 5
245		dvdsle 13574	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 656	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9408	. . . . . 6
249	54	recnd 9408	. . . . . 6
250		efadd 13375	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 656	. . . . 5
252	53	reeflogd 22032	. . . . . 6
253	252	oveq2d 6106	. . . . 5
254	251, 253	eqtrd 2473	. . . 4
255	247, 254	breqtrrd 4315	. . 3
256		efle 13398	. . . 4 $/\$
257	8, 55, 256	syl2anc 656	. . 3
258	255, 257	mpbird 232	. 2
259		fzfid 11791	. . . . . . . . 9
260		elfzelz 11449	. . . . . . . . . . 11
261		bccl 12094	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 474	. . . . . . . . . 10 $/\$
263	262	nn0red 10633	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10635	. . . . . . . . 9 $/\$
265		nn0uz 10891	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2531	. . . . . . . . . . 11
267		fzss1 11493	. . . . . . . . . . 11
268	266, 267	syl 16	. . . . . . . . . 10
269		eluz 10870	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 656	. . . . . . . . . . . 12
271	48, 270	mpbird 232	. . . . . . . . . . 11
272		fzss2 11494	. . . . . . . . . . 11
273	271, 272	syl 16	. . . . . . . . . 10
274	268, 273	sstrd 3363	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13255	. . . . . . . 8
276	32	nn0zd 10741	. . . . . . . . . . . 12
277		bccmpl 12081	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 656	. . . . . . . . . . . . . 14
279	111	oveq2d 6106	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2473	. . . . . . . . . . . . 13
281	52	nncnd 10334	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2516	. . . . . . . . . . . 12
283		oveq2 6098	. . . . . . . . . . . . 13
284	283	fsum1 13214	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 656	. . . . . . . . . . 11
286	285, 280	eqtr4d 2476	. . . . . . . . . 10
287	286	oveq1d 6105	. . . . . . . . 9
288	21, 105	npcand 9719	. . . . . . . . . . 11
289		uzid 10871	. . . . . . . . . . . . 13
290	276, 289	syl 16	. . . . . . . . . . . 12
291		peano2uz 10904	. . . . . . . . . . . 12
292	290, 291	syl 16	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2516	. . . . . . . . . 10
294	274	sselda 3353	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10634	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 467	. . . . . . . . . 10 $/\$
297		oveq2 6098	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13216	. . . . . . . . 9
299	281	2timesd 10563	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2484	. . . . . . . 8
301		binom11 13291	. . . . . . . . 9
302	39, 301	syl 16	. . . . . . . 8
303	275, 300, 302	3brtr4d 4319	. . . . . . 7
304		mulcom 9364	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 658	. . . . . . 7
306	30	oveq2d 6106	. . . . . . . 8
307		expp1 11868	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 658	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12007	. . . . . . . . . 10
312		sq2 11958	. . . . . . . . . . 11
313	312	oveq1i 6100	. . . . . . . . . 10
314	311, 313	syl6eq 2489	. . . . . . . . 9
315	314	oveq1d 6105	. . . . . . . 8
316	306, 308, 315	3eqtrd 2477	. . . . . . 7
317	303, 305, 316	3brtr3d 4318	. . . . . 6
318	52	nnred 10333	. . . . . . 7
319		reexpcl 11878	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 658	. . . . . . 7
321		2re 10387	. . . . . . . . 9
322		2pos 10409	. . . . . . . . 9
323	321, 322	pm3.2i 452	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10177	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1213	. . . . . 6
327	317, 326	mpbird 232	. . . . 5
328	60	recni 9394	. . . . . . . 8
329		mulcom 9364	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 658	. . . . . . 7
331	330	fveq2d 5692	. . . . . 6
332		reexplog 22002	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 658	. . . . . 6
334	331, 333	eqtr4d 2476	. . . . 5
335	327, 252, 334	3brtr4d 4319	. . . 4
336		efle 13398	. . . . 5 $/\$
337	54, 63, 336	syl2anc 656	. . . 4
338	335, 337	mpbird 232	. . 3
339	54, 63, 11, 338	leadd2dd 9950	. 2
340	8, 55, 64, 258, 339	letrd 9524	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1364

wcel 1761

wne 2604

wral 2713

wss 3325

cif 3788 class class class wbr 4289

cmpt 4347

cfv 5415 (class class class)co 6090

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

clt 9414

cle 9415

cmin 9591

cdiv 9989

cn 10318

c2 10367

c4 10369

cn0 10575

cz 10642

cuz 10857

crp 10987

cfz 11433

cseq 11802

cexp 11861

cfa 12047

cbc 12074

csu 13159

ce 13343

cdivides 13531

cprime 13759

cpc 13899

clog 21965

ccht 22387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357 ax-mulf 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-iin 4171 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-om 6476 df-1st 6576 df-2nd 6577 df-supp 6690 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-ixp 7260 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-fsupp 7617 df-fi 7657 df-sup 7687 df-oi 7720 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-4 10378 df-5 10379 df-6 10380 df-7 10381 df-8 10382 df-9 10383 df-10 10384 df-n0 10576 df-z 10643 df-dec 10752 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-ioo 11300 df-ioc 11301 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-mod 11705 df-seq 11803 df-exp 11862 df-fac 12048 df-bc 12075 df-hash 12100 df-shft 12552 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-limsup 12945 df-clim 12962 df-rlim 12963 df-sum 13160 df-ef 13349 df-sin 13351 df-cos 13352 df-pi 13354 df-dvds 13532 df-gcd 13687 df-prm 13760 df-pc 13900 df-struct 14172 df-ndx 14173 df-slot 14174 df-base 14175 df-sets 14176 df-ress 14177 df-plusg 14247 df-mulr 14248 df-starv 14249 df-sca 14250 df-vsca 14251 df-ip 14252 df-tset 14253 df-ple 14254 df-ds 14256 df-unif 14257 df-hom 14258 df-cco 14259 df-rest 14357 df-topn 14358 df-0g 14376 df-gsum 14377 df-topgen 14378 df-pt 14379 df-prds 14382 df-xrs 14436 df-qtop 14441 df-imas 14442 df-xps 14444 df-mre 14520 df-mrc 14521 df-acs 14523 df-mnd 15411 df-submnd 15461 df-mulg 15541 df-cntz 15828 df-cmn 16272 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-fbas 17773 df-fg 17774 df-cnfld 17778 df-top 18462 df-bases 18464 df-topon 18465 df-topsp 18466 df-cld 18582 df-ntr 18583 df-cls 18584 df-nei 18661 df-lp 18699 df-perf 18700 df-cn 18790 df-cnp 18791 df-haus 18878 df-tx 19094 df-hmeo 19287 df-fil 19378 df-fm 19470 df-flim 19471 df-flf 19472 df-xms 19854 df-ms 19855 df-tms 19856 df-cncf 20413 df-limc 21300 df-dv 21301 df-log 21967 df-cht 22393

This theorem is referenced by: chtub 22510

W3C validator