chtublem - Metamath Proof Explorer

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

Theorem chtublem 23214

Description: Lemma for chtub 23215. (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 10689	. . . . . 6
2		nnmulcl 10555	. . . . . 6 $/\$
3	1, 2	mpan 670	. . . . 5
4	3	nnred 10547	. . . 4
5		peano2rem 9882	. . . 4
6	4, 5	syl 16	. . 3
7		chtcl 23111	. . 3
8	6, 7	syl 16	. 2
9		nnre 10539	. . . 4
10		chtcl 23111	. . . 4
11	9, 10	syl 16	. . 3
12		nnnn0 10798	. . . . . . 7
13		2m1e1 10646	. . . . . . . . . . 11
14	13	oveq2i 6293	. . . . . . . . . 10
15	3	nncnd 10548	. . . . . . . . . . . 12
16		2cn 10602	. . . . . . . . . . . . 13
17		ax-1cn 9546	. . . . . . . . . . . . 13
18		subsub 9845	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1316	. . . . . . . . . . . 12
20	15, 19	syl 16	. . . . . . . . . . 11
21		nncn 10540	. . . . . . . . . . . . . 14
22		subdi 9986	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1315	. . . . . . . . . . . . . 14
24	21, 23	syl 16	. . . . . . . . . . . . 13
25		2t1e2 10680	. . . . . . . . . . . . . 14
26	25	oveq2i 6293	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2524	. . . . . . . . . . . 12
28	27	oveq1d 6297	. . . . . . . . . . 11
29	20, 28	eqtr4d 2511	. . . . . . . . . 10
30	14, 29	syl5eqr 2522	. . . . . . . . 9
31		2nn0 10808	. . . . . . . . . . 11
32		nnm1nn0 10833	. . . . . . . . . . 11
33		nn0mulcl 10828	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 663	. . . . . . . . . 10
35		nn0p1nn 10831	. . . . . . . . . 10
36	34, 35	syl 16	. . . . . . . . 9
37	30, 36	eqeltrd 2555	. . . . . . . 8
38		nnnn0 10798	. . . . . . . 8
39	37, 38	syl 16	. . . . . . 7
40		1re 9591	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10558	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 10163	. . . . . . . . 9
44	21	2timesd 10777	. . . . . . . . 9
45	43, 44	breqtrrd 4473	. . . . . . . 8
46		leaddsub 10024	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1228	. . . . . . . 8
48	45, 47	mpbid 210	. . . . . . 7
49		elfz2nn0 11764	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1180	. . . . . 6
51		bccl2 12365	. . . . . 6
52	50, 51	syl 16	. . . . 5
53	52	nnrpd 11251	. . . 4
54	53	relogcld 22736	. . 3
55	11, 54	readdcld 9619	. 2
56		4re 10608	. . . . . 6
57		4pos 10627	. . . . . 6
58	56, 57	elrpii 11219	. . . . 5
59		relogcl 22691	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10849	. . . 4
62		remulcl 9573	. . . 4 $/\$
63	60, 61, 62	sylancr 663	. . 3
64	11, 63	readdcld 9619	. 2
65		iftrue 3945	. . . . . . . . . . . 12
66	65	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 14229	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10838	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 663	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3945	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6297	. . . . . . . . . . . . . . 15
74	73	breq2d 4459	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 222	. . . . . . . . . . . . 13 $/\$
76	75	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 14075	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 726	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 14076	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 10961	. . . . . . . . . . . . . . . . . . . 20
82		eluz 11091	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 478	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 13896	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12327	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 16	. . . . . . . . . . . . . . . . . 18
91		pcelnn 14248	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 478	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10574	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3948	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6297	. . . . . . . . . . . . . . . 16
98	97	ad2antll 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10850	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9776	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12347	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 9946	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6297	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10850	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9928	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6297	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6298	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2508	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6298	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10882	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10564	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 532	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12327	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 16	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12327	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 16	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10579	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 14231	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10882	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10564	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10882	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10564	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 14230	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6298	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2512	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 756	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 14114	. . . . . . . . . . . . . . . . . . . . . . . . 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 10882	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 13875	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12326	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4459	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 177	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 14249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 14249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 478	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6300	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9750	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2524	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6298	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 14228	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 478	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10850	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9915	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2512	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2512	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 615	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 158	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4467	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 434	. . . . . . . . 9 $/\$
188		1nn0 10807	. . . . . . . . . . . . 13
189		0nn0 10806	. . . . . . . . . . . . 13
190	188, 189	keepel 4007	. . . . . . . . . . . 12
191		nn0addcl 10827	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 663	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10851	. . . . . . . . . 10 $/\$
194		iffalse 3948	. . . . . . . . . . 11
195	194	breq1d 4457	. . . . . . . . . 10
196	193, 195	syl5ibrcom 222	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 158	. . . . . . . 8 $/\$
198		eqid 2467	. . . . . . . . . . . . 13
199	198	prmorcht 23180	. . . . . . . . . . . 12
200	37, 199	syl 16	. . . . . . . . . . 11
201	200	oveq2d 6298	. . . . . . . . . 10
202	201	adantr 465	. . . . . . . . 9 $/\$
203		nncn 10540	. . . . . . . . . . . . . 14
204	203	exp1d 12269	. . . . . . . . . . . . 13
205	204	ifeq1d 3957	. . . . . . . . . . . 12
206	205	mpteq2ia 4529	. . . . . . . . . . 11
207	206	eqcomi 2480	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2878	. . . . . . . . . 10 $/\$
210	37	adantr 465	. . . . . . . . . 10 $/\$
211		eqidd 2468	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 14266	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2508	. . . . . . . 8 $/\$
214		efchtcl 23113	. . . . . . . . . . . . 13
215	9, 214	syl 16	. . . . . . . . . . . 12
216	215	adantr 465	. . . . . . . . . . 11 $/\$
217		nnz 10882	. . . . . . . . . . . 12
218		nnne0 10564	. . . . . . . . . . . 12
219	217, 218	jca 532	. . . . . . . . . . 11 $/\$
220	216, 219	syl 16	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10882	. . . . . . . . . . . 12
222		nnne0 10564	. . . . . . . . . . . 12
223	221, 222	jca 532	. . . . . . . . . . 11 $/\$
224	68, 223	syl 16	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 14230	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1228	. . . . . . . . 9 $/\$
227	198	prmorcht 23180	. . . . . . . . . . . . 13
228	227	oveq2d 6298	. . . . . . . . . . . 12
229	228	adantr 465	. . . . . . . . . . 11 $/\$
230		simpl 457	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 14266	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2508	. . . . . . . . . 10 $/\$
233	232	oveq1d 6297	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2508	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4477	. . . . . . 7 $/\$
236	235	ralrimiva 2878	. . . . . 6
237		efchtcl 23113	. . . . . . . . 9
238	6, 237	syl 16	. . . . . . . 8
239	238	nnzd 10961	. . . . . . 7
240	215, 52	nnmulcld 10579	. . . . . . . 8
241	240	nnzd 10961	. . . . . . 7
242		pc2dvds 14257	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 661	. . . . . 6
244	236, 243	mpbird 232	. . . . 5
245		dvdsle 13886	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 661	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9618	. . . . . 6
249	54	recnd 9618	. . . . . 6
250		efadd 13687	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 661	. . . . 5
252	53	reeflogd 22737	. . . . . 6
253	252	oveq2d 6298	. . . . 5
254	251, 253	eqtrd 2508	. . . 4
255	247, 254	breqtrrd 4473	. . 3
256		efle 13710	. . . 4 $/\$
257	8, 55, 256	syl2anc 661	. . 3
258	255, 257	mpbird 232	. 2
259		fzfid 12047	. . . . . . . . 9
260		elfzelz 11684	. . . . . . . . . . 11
261		bccl 12364	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 477	. . . . . . . . . 10 $/\$
263	262	nn0red 10849	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10851	. . . . . . . . 9 $/\$
265		nn0uz 11112	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2565	. . . . . . . . . . 11
267		fzss1 11718	. . . . . . . . . . 11
268	266, 267	syl 16	. . . . . . . . . 10
269		eluz 11091	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 661	. . . . . . . . . . . 12
271	48, 270	mpbird 232	. . . . . . . . . . 11
272		fzss2 11719	. . . . . . . . . . 11
273	271, 272	syl 16	. . . . . . . . . 10
274	268, 273	sstrd 3514	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13569	. . . . . . . 8
276	32	nn0zd 10960	. . . . . . . . . . . 12
277		bccmpl 12351	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 661	. . . . . . . . . . . . . 14
279	111	oveq2d 6298	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2508	. . . . . . . . . . . . 13
281	52	nncnd 10548	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2556	. . . . . . . . . . . 12
283		oveq2 6290	. . . . . . . . . . . . 13
284	283	fsum1 13523	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 661	. . . . . . . . . . 11
286	285, 280	eqtr4d 2511	. . . . . . . . . 10
287	286	oveq1d 6297	. . . . . . . . 9
288	21, 105	npcand 9930	. . . . . . . . . . 11
289		uzid 11092	. . . . . . . . . . . . 13
290	276, 289	syl 16	. . . . . . . . . . . 12
291		peano2uz 11130	. . . . . . . . . . . 12
292	290, 291	syl 16	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2556	. . . . . . . . . 10
294	274	sselda 3504	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10850	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 470	. . . . . . . . . 10 $/\$
297		oveq2 6290	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13525	. . . . . . . . 9
299	281	2timesd 10777	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2519	. . . . . . . 8
301		binom11 13603	. . . . . . . . 9
302	39, 301	syl 16	. . . . . . . 8
303	275, 300, 302	3brtr4d 4477	. . . . . . 7
304		mulcom 9574	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 663	. . . . . . 7
306	30	oveq2d 6298	. . . . . . . 8
307		expp1 12137	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 663	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12277	. . . . . . . . . 10
312		sq2 12228	. . . . . . . . . . 11
313	312	oveq1i 6292	. . . . . . . . . 10
314	311, 313	syl6eq 2524	. . . . . . . . 9
315	314	oveq1d 6297	. . . . . . . 8
316	306, 308, 315	3eqtrd 2512	. . . . . . 7
317	303, 305, 316	3brtr3d 4476	. . . . . 6
318	52	nnred 10547	. . . . . . 7
319		reexpcl 12147	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 663	. . . . . . 7
321		2re 10601	. . . . . . . . 9
322		2pos 10623	. . . . . . . . 9
323	321, 322	pm3.2i 455	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10390	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1228	. . . . . 6
327	317, 326	mpbird 232	. . . . 5
328	60	recni 9604	. . . . . . . 8
329		mulcom 9574	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 663	. . . . . . 7
331	330	fveq2d 5868	. . . . . 6
332		reexplog 22707	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 663	. . . . . 6
334	331, 333	eqtr4d 2511	. . . . 5
335	327, 252, 334	3brtr4d 4477	. . . 4
336		efle 13710	. . . . 5 $/\$
337	54, 63, 336	syl2anc 661	. . . 4
338	335, 337	mpbird 232	. . 3
339	54, 63, 11, 338	leadd2dd 10163	. 2
340	8, 55, 64, 258, 339	letrd 9734	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662

wral 2814

wss 3476

cif 3939 class class class wbr 4447

cmpt 4505

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

clt 9624

cle 9625

cmin 9801

cdiv 10202

cn 10532

c2 10581

c4 10583

cn0 10791

cz 10860

cuz 11078

crp 11216

cfz 11668

cseq 12071

cexp 12130

cfa 12317

cbc 12344

csu 13467

ce 13655

cdivides 13843

cprime 14072

cpc 14215

clog 22670

ccht 23092

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-fac 12318 df-bc 12345 df-hash 12370 df-shft 12859 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-limsup 13253 df-clim 13270 df-rlim 13271 df-sum 13468 df-ef 13661 df-sin 13663 df-cos 13664 df-pi 13666 df-dvds 13844 df-gcd 14000 df-prm 14073 df-pc 14216 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-limc 22005 df-dv 22006 df-log 22672 df-cht 23098

This theorem is referenced by: chtub 23215

W3C validator