chtublem - Metamath Proof Explorer

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

Theorem chtublem 23759

Description: Lemma for chtub 23760. (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 10654	. . . . . 6
2		nnmulcl 10519	. . . . . 6 $/\$
3	1, 2	mpan 668	. . . . 5
4	3	nnred 10511	. . . 4
5		peano2rem 9842	. . . 4
6	4, 5	syl 17	. . 3
7		chtcl 23656	. . 3
8	6, 7	syl 17	. 2
9		nnre 10503	. . . 4
10		chtcl 23656	. . . 4
11	9, 10	syl 17	. . 3
12		nnnn0 10763	. . . . . . 7
13		2m1e1 10611	. . . . . . . . . . 11
14	13	oveq2i 6245	. . . . . . . . . 10
15	3	nncnd 10512	. . . . . . . . . . . 12
16		2cn 10567	. . . . . . . . . . . . 13
17		ax-1cn 9500	. . . . . . . . . . . . 13
18		subsub 9805	. . . . . . . . . . . . 13 $/\$ $/\$
19	16, 17, 18	mp3an23 1318	. . . . . . . . . . . 12
20	15, 19	syl 17	. . . . . . . . . . 11
21		nncn 10504	. . . . . . . . . . . . . 14
22		subdi 9951	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	16, 17, 22	mp3an13 1317	. . . . . . . . . . . . . 14
24	21, 23	syl 17	. . . . . . . . . . . . 13
25		2t1e2 10645	. . . . . . . . . . . . . 14
26	25	oveq2i 6245	. . . . . . . . . . . . 13
27	24, 26	syl6eq 2459	. . . . . . . . . . . 12
28	27	oveq1d 6249	. . . . . . . . . . 11
29	20, 28	eqtr4d 2446	. . . . . . . . . 10
30	14, 29	syl5eqr 2457	. . . . . . . . 9
31		2nn0 10773	. . . . . . . . . . 11
32		nnm1nn0 10798	. . . . . . . . . . 11
33		nn0mulcl 10793	. . . . . . . . . . 11 $/\$
34	31, 32, 33	sylancr 661	. . . . . . . . . 10
35		nn0p1nn 10796	. . . . . . . . . 10
36	34, 35	syl 17	. . . . . . . . 9
37	30, 36	eqeltrd 2490	. . . . . . . 8
38		nnnn0 10763	. . . . . . . 8
39	37, 38	syl 17	. . . . . . 7
40		1re 9545	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42		nnge1 10522	. . . . . . . . . 10
43	41, 9, 9, 42	leadd2dd 10127	. . . . . . . . 9
44	21	2timesd 10742	. . . . . . . . 9
45	43, 44	breqtrrd 4420	. . . . . . . 8
46		leaddsub 9989	. . . . . . . . 9 $/\$ $/\$
47	9, 41, 4, 46	syl3anc 1230	. . . . . . . 8
48	45, 47	mpbid 210	. . . . . . 7
49		elfz2nn0 11741	. . . . . . 7 $/\$ $/\$
50	12, 39, 48, 49	syl3anbrc 1181	. . . . . 6
51		bccl2 12355	. . . . . 6
52	50, 51	syl 17	. . . . 5
53	52	nnrpd 11220	. . . 4
54	53	relogcld 23194	. . 3
55	11, 54	readdcld 9573	. 2
56		4re 10573	. . . . . 6
57		4pos 10592	. . . . . 6
58	56, 57	elrpii 11186	. . . . 5
59		relogcl 23147	. . . . 5
60	58, 59	ax-mp 5	. . . 4
61	32	nn0red 10814	. . . 4
62		remulcl 9527	. . . 4 $/\$
63	60, 61, 62	sylancr 661	. . 3
64	11, 63	readdcld 9573	. 2
65		iftrue 3890	. . . . . . . . . . . 12
66	65	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
67		simpr 459	. . . . . . . . . . . . . . . 16 $/\$
68	52	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
69	67, 68	pccld 14475	. . . . . . . . . . . . . . 15 $/\$
70		nn0addge1 10803	. . . . . . . . . . . . . . 15 $/\$
71	40, 69, 70	sylancr 661	. . . . . . . . . . . . . 14 $/\$
72		iftrue 3890	. . . . . . . . . . . . . . . 16
73	72	oveq1d 6249	. . . . . . . . . . . . . . 15
74	73	breq2d 4406	. . . . . . . . . . . . . 14
75	71, 74	syl5ibrcom 222	. . . . . . . . . . . . 13 $/\$
76	75	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$
77		prmnn 14321	. . . . . . . . . . . . . . . . . 18
78	77	ad2antlr 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
79		simprl 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
80		prmz 14322	. . . . . . . . . . . . . . . . . . . 20
81	37	nnzd 10927	. . . . . . . . . . . . . . . . . . . 20
82		eluz 11058	. . . . . . . . . . . . . . . . . . . 20 $/\$
83	80, 81, 82	syl2anr 476	. . . . . . . . . . . . . . . . . . 19 $/\$
84	83	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	79, 84	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		dvdsfac 14142	. . . . . . . . . . . . . . . . 17 $/\$
87	78, 85, 86	syl2anc 659	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
88		id 22	. . . . . . . . . . . . . . . . . 18
89		faccl 12317	. . . . . . . . . . . . . . . . . . 19
90	39, 89	syl 17	. . . . . . . . . . . . . . . . . 18
91		pcelnn 14494	. . . . . . . . . . . . . . . . . 18 $/\$
92	88, 90, 91	syl2anr 476	. . . . . . . . . . . . . . . . 17 $/\$
93	92	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	87, 93	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95	94	nnge1d 10539	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
96		iffalse 3893	. . . . . . . . . . . . . . . . 17
97	96	oveq1d 6249	. . . . . . . . . . . . . . . 16
98	97	ad2antll 727	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
99	69	nn0cnd 10815	. . . . . . . . . . . . . . . . 17 $/\$
100	99	addid2d 9735	. . . . . . . . . . . . . . . 16 $/\$
101	100	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
102		bcval2 12337	. . . . . . . . . . . . . . . . . . . . . 22
103	50, 102	syl 17	. . . . . . . . . . . . . . . . . . . . 21
104	44	oveq1d 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	21, 21, 105	addsubassd 9907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	104, 106	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108	107	oveq1d 6249	. . . . . . . . . . . . . . . . . . . . . . . . 25
109	32	nn0cnd 10815	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	21, 109	pncan2d 9889	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	108, 110	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	fveq2d 5809	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	oveq1d 6249	. . . . . . . . . . . . . . . . . . . . . 22
114	113	oveq2d 6250	. . . . . . . . . . . . . . . . . . . . 21
115	103, 114	eqtrd 2443	. . . . . . . . . . . . . . . . . . . 20
116	115	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
117	116	oveq2d 6250	. . . . . . . . . . . . . . . . . 18 $/\$
118		nnz 10847	. . . . . . . . . . . . . . . . . . . . . 22
119		nnne0 10529	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	jca 530	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	90, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
122	121	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
123		faccl 12317	. . . . . . . . . . . . . . . . . . . . . 22
124	32, 123	syl 17	. . . . . . . . . . . . . . . . . . . . 21
125		faccl 12317	. . . . . . . . . . . . . . . . . . . . . 22
126	12, 125	syl 17	. . . . . . . . . . . . . . . . . . . . 21
127	124, 126	nnmulcld 10544	. . . . . . . . . . . . . . . . . . . 20
128	127	adantr 463	. . . . . . . . . . . . . . . . . . 19 $/\$
129		pcdiv 14477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
130	67, 122, 128, 129	syl3anc 1230	. . . . . . . . . . . . . . . . . 18 $/\$
131		nnz 10847	. . . . . . . . . . . . . . . . . . . . . . 23
132		nnne0 10529	. . . . . . . . . . . . . . . . . . . . . . 23
133	131, 132	jca 530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	124, 133	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		nnz 10847	. . . . . . . . . . . . . . . . . . . . . . 23
137		nnne0 10529	. . . . . . . . . . . . . . . . . . . . . . 23
138	136, 137	jca 530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
139	126, 138	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	139	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
141		pcmul 14476	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
142	67, 135, 140, 141	syl3anc 1230	. . . . . . . . . . . . . . . . . . 19 $/\$
143	142	oveq2d 6250	. . . . . . . . . . . . . . . . . 18 $/\$
144	117, 130, 143	3eqtrd 2447	. . . . . . . . . . . . . . . . 17 $/\$
145	144	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
146		simprr 758	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
147		prmfac1 14360	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
148	147	3expia 1199	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
149	12, 148	sylan 469	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	mtod 177	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
152	80	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
153	135	simpld 457	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
154		nnz 10847	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
156		dvdsmultr1 14120	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	152, 153, 155, 156	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158		facnn2 12316	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	158	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
160	159	breq2d 4406	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	157, 160	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	161	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
163	151, 162	mtod 177	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
164		pceq0 14495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	88, 124, 164	syl2anr 476	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	165	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
167	163, 166	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
168		pceq0 14495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	88, 126, 168	syl2anr 476	. . . . . . . . . . . . . . . . . . . . 21 $/\$
170	169	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
171	151, 170	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
172	167, 171	oveq12d 6252	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
173		00id 9709	. . . . . . . . . . . . . . . . . 18
174	172, 173	syl6eq 2459	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
175	174	oveq2d 6250	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		pccl 14474	. . . . . . . . . . . . . . . . . . . 20 $/\$
177	88, 90, 176	syl2anr 476	. . . . . . . . . . . . . . . . . . 19 $/\$
178	177	nn0cnd 10815	. . . . . . . . . . . . . . . . . 18 $/\$
179	178	subid1d 9876	. . . . . . . . . . . . . . . . 17 $/\$
180	179	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
181	145, 175, 180	3eqtrd 2447	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	98, 101, 181	3eqtrd 2447	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183	95, 182	breqtrrd 4420	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
184	183	expr 613	. . . . . . . . . . . 12 $/\$ $/\$
185	76, 184	pm2.61d 158	. . . . . . . . . . 11 $/\$ $/\$
186	66, 185	eqbrtrd 4414	. . . . . . . . . 10 $/\$ $/\$
187	186	ex 432	. . . . . . . . 9 $/\$
188		1nn0 10772	. . . . . . . . . . . . 13
189		0nn0 10771	. . . . . . . . . . . . 13
190	188, 189	keepel 3951	. . . . . . . . . . . 12
191		nn0addcl 10792	. . . . . . . . . . . 12 $/\$
192	190, 69, 191	sylancr 661	. . . . . . . . . . 11 $/\$
193	192	nn0ge0d 10816	. . . . . . . . . 10 $/\$
194		iffalse 3893	. . . . . . . . . . 11
195	194	breq1d 4404	. . . . . . . . . 10
196	193, 195	syl5ibrcom 222	. . . . . . . . 9 $/\$
197	187, 196	pm2.61d 158	. . . . . . . 8 $/\$
198		eqid 2402	. . . . . . . . . . . . 13
199	198	prmorcht 23725	. . . . . . . . . . . 12
200	37, 199	syl 17	. . . . . . . . . . 11
201	200	oveq2d 6250	. . . . . . . . . 10
202	201	adantr 463	. . . . . . . . 9 $/\$
203		nncn 10504	. . . . . . . . . . . . . 14
204	203	exp1d 12259	. . . . . . . . . . . . 13
205	204	ifeq1d 3902	. . . . . . . . . . . 12
206	205	mpteq2ia 4476	. . . . . . . . . . 11
207	206	eqcomi 2415	. . . . . . . . . 10
208	188	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
209	208	ralrimiva 2817	. . . . . . . . . 10 $/\$
210	37	adantr 463	. . . . . . . . . 10 $/\$
211		eqidd 2403	. . . . . . . . . 10
212	207, 209, 210, 67, 211	pcmpt 14512	. . . . . . . . 9 $/\$
213	202, 212	eqtrd 2443	. . . . . . . 8 $/\$
214		efchtcl 23658	. . . . . . . . . . . . 13
215	9, 214	syl 17	. . . . . . . . . . . 12
216	215	adantr 463	. . . . . . . . . . 11 $/\$
217		nnz 10847	. . . . . . . . . . . 12
218		nnne0 10529	. . . . . . . . . . . 12
219	217, 218	jca 530	. . . . . . . . . . 11 $/\$
220	216, 219	syl 17	. . . . . . . . . 10 $/\$ $/\$
221		nnz 10847	. . . . . . . . . . . 12
222		nnne0 10529	. . . . . . . . . . . 12
223	221, 222	jca 530	. . . . . . . . . . 11 $/\$
224	68, 223	syl 17	. . . . . . . . . 10 $/\$ $/\$
225		pcmul 14476	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
226	67, 220, 224, 225	syl3anc 1230	. . . . . . . . 9 $/\$
227	198	prmorcht 23725	. . . . . . . . . . . . 13
228	227	oveq2d 6250	. . . . . . . . . . . 12
229	228	adantr 463	. . . . . . . . . . 11 $/\$
230		simpl 455	. . . . . . . . . . . 12 $/\$
231	207, 209, 230, 67, 211	pcmpt 14512	. . . . . . . . . . 11 $/\$
232	229, 231	eqtrd 2443	. . . . . . . . . 10 $/\$
233	232	oveq1d 6249	. . . . . . . . 9 $/\$
234	226, 233	eqtrd 2443	. . . . . . . 8 $/\$
235	197, 213, 234	3brtr4d 4424	. . . . . . 7 $/\$
236	235	ralrimiva 2817	. . . . . 6
237		efchtcl 23658	. . . . . . . . 9
238	6, 237	syl 17	. . . . . . . 8
239	238	nnzd 10927	. . . . . . 7
240	215, 52	nnmulcld 10544	. . . . . . . 8
241	240	nnzd 10927	. . . . . . 7
242		pc2dvds 14503	. . . . . . 7 $/\$
243	239, 241, 242	syl2anc 659	. . . . . 6
244	236, 243	mpbird 232	. . . . 5
245		dvdsle 14132	. . . . . 6 $/\$
246	239, 240, 245	syl2anc 659	. . . . 5
247	244, 246	mpd 15	. . . 4
248	11	recnd 9572	. . . . . 6
249	54	recnd 9572	. . . . . 6
250		efadd 13930	. . . . . 6 $/\$
251	248, 249, 250	syl2anc 659	. . . . 5
252	53	reeflogd 23195	. . . . . 6
253	252	oveq2d 6250	. . . . 5
254	251, 253	eqtrd 2443	. . . 4
255	247, 254	breqtrrd 4420	. . 3
256		efle 13954	. . . 4 $/\$
257	8, 55, 256	syl2anc 659	. . 3
258	255, 257	mpbird 232	. 2
259		fzfid 12037	. . . . . . . . 9
260		elfzelz 11659	. . . . . . . . . . 11
261		bccl 12354	. . . . . . . . . . 11 $/\$
262	39, 260, 261	syl2an 475	. . . . . . . . . 10 $/\$
263	262	nn0red 10814	. . . . . . . . 9 $/\$
264	262	nn0ge0d 10816	. . . . . . . . 9 $/\$
265		nn0uz 11079	. . . . . . . . . . . 12
266	32, 265	syl6eleq 2500	. . . . . . . . . . 11
267		fzss1 11694	. . . . . . . . . . 11
268	266, 267	syl 17	. . . . . . . . . 10
269		eluz 11058	. . . . . . . . . . . . 13 $/\$
270	154, 81, 269	syl2anc 659	. . . . . . . . . . . 12
271	48, 270	mpbird 232	. . . . . . . . . . 11
272		fzss2 11695	. . . . . . . . . . 11
273	271, 272	syl 17	. . . . . . . . . 10
274	268, 273	sstrd 3451	. . . . . . . . 9
275	259, 263, 264, 274	fsumless 13668	. . . . . . . 8
276	32	nn0zd 10926	. . . . . . . . . . . 12
277		bccmpl 12341	. . . . . . . . . . . . . . 15 $/\$
278	39, 154, 277	syl2anc 659	. . . . . . . . . . . . . 14
279	111	oveq2d 6250	. . . . . . . . . . . . . 14
280	278, 279	eqtrd 2443	. . . . . . . . . . . . 13
281	52	nncnd 10512	. . . . . . . . . . . . 13
282	280, 281	eqeltrrd 2491	. . . . . . . . . . . 12
283		oveq2 6242	. . . . . . . . . . . . 13
284	283	fsum1 13620	. . . . . . . . . . . 12 $/\$
285	276, 282, 284	syl2anc 659	. . . . . . . . . . 11
286	285, 280	eqtr4d 2446	. . . . . . . . . 10
287	286	oveq1d 6249	. . . . . . . . 9
288	21, 105	npcand 9891	. . . . . . . . . . 11
289		uzid 11059	. . . . . . . . . . . . 13
290	276, 289	syl 17	. . . . . . . . . . . 12
291		peano2uz 11098	. . . . . . . . . . . 12
292	290, 291	syl 17	. . . . . . . . . . 11
293	288, 292	eqeltrrd 2491	. . . . . . . . . 10
294	274	sselda 3441	. . . . . . . . . . 11 $/\$
295	262	nn0cnd 10815	. . . . . . . . . . 11 $/\$
296	294, 295	syldan 468	. . . . . . . . . 10 $/\$
297		oveq2 6242	. . . . . . . . . 10
298	293, 296, 297	fsumm1 13624	. . . . . . . . 9
299	281	2timesd 10742	. . . . . . . . 9
300	287, 298, 299	3eqtr4rd 2454	. . . . . . . 8
301		binom11 13702	. . . . . . . . 9
302	39, 301	syl 17	. . . . . . . 8
303	275, 300, 302	3brtr4d 4424	. . . . . . 7
304		mulcom 9528	. . . . . . . 8 $/\$
305	16, 281, 304	sylancr 661	. . . . . . 7
306	30	oveq2d 6250	. . . . . . . 8
307		expp1 12127	. . . . . . . . 9 $/\$
308	16, 34, 307	sylancr 661	. . . . . . . 8
309	16	a1i 11	. . . . . . . . . . 11
310	31	a1i 11	. . . . . . . . . . 11
311	309, 32, 310	expmuld 12267	. . . . . . . . . 10
312		sq2 12219	. . . . . . . . . . 11
313	312	oveq1i 6244	. . . . . . . . . 10
314	311, 313	syl6eq 2459	. . . . . . . . 9
315	314	oveq1d 6249	. . . . . . . 8
316	306, 308, 315	3eqtrd 2447	. . . . . . 7
317	303, 305, 316	3brtr3d 4423	. . . . . 6
318	52	nnred 10511	. . . . . . 7
319		reexpcl 12137	. . . . . . . 8 $/\$
320	56, 32, 319	sylancr 661	. . . . . . 7
321		2re 10566	. . . . . . . . 9
322		2pos 10588	. . . . . . . . 9
323	321, 322	pm3.2i 453	. . . . . . . 8 $/\$
324	323	a1i 11	. . . . . . 7 $/\$
325		lemul1 10355	. . . . . . 7 $/\$ $/\$ $/\$
326	318, 320, 324, 325	syl3anc 1230	. . . . . 6
327	317, 326	mpbird 232	. . . . 5
328	60	recni 9558	. . . . . . . 8
329		mulcom 9528	. . . . . . . 8 $/\$
330	328, 109, 329	sylancr 661	. . . . . . 7
331	330	fveq2d 5809	. . . . . 6
332		reexplog 23166	. . . . . . 7 $/\$
333	58, 276, 332	sylancr 661	. . . . . 6
334	331, 333	eqtr4d 2446	. . . . 5
335	327, 252, 334	3brtr4d 4424	. . . 4
336		efle 13954	. . . . 5 $/\$
337	54, 63, 336	syl2anc 659	. . . 4
338	335, 337	mpbird 232	. . 3
339	54, 63, 11, 338	leadd2dd 10127	. 2
340	8, 55, 64, 258, 339	letrd 9693	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wceq 1405

wcel 1842

wne 2598

wral 2753

wss 3413

cif 3884 class class class wbr 4394

cmpt 4452

cfv 5525 (class class class)co 6234

cc 9440

cr 9441

cc0 9442

c1 9443

caddc 9445

cmul 9447

clt 9578

cle 9579

cmin 9761

cdiv 10167

cn 10496

c2 10546

c4 10548

cn0 10756

cz 10825

cuz 11045

crp 11183

cfz 11643

cseq 12061

cexp 12120

cfa 12307

cbc 12334

csu 13564

ce 13898

cdvds 14087

cprime 14318

cpc 14461

clog 23126

ccht 23637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6530 ax-inf2 8011 ax-cnex 9498 ax-resscn 9499 ax-1cn 9500 ax-icn 9501 ax-addcl 9502 ax-addrcl 9503 ax-mulcl 9504 ax-mulrcl 9505 ax-mulcom 9506 ax-addass 9507 ax-mulass 9508 ax-distr 9509 ax-i2m1 9510 ax-1ne0 9511 ax-1rid 9512 ax-rnegex 9513 ax-rrecex 9514 ax-cnre 9515 ax-pre-lttri 9516 ax-pre-lttrn 9517 ax-pre-ltadd 9518 ax-pre-mulgt0 9519 ax-pre-sup 9520 ax-addf 9521 ax-mulf 9522

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-iin 4273 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-se 4782 df-we 4783 df-ord 4824 df-on 4825 df-lim 4826 df-suc 4827 df-xp 4948 df-rel 4949 df-cnv 4950 df-co 4951 df-dm 4952 df-rn 4953 df-res 4954 df-ima 4955 df-iota 5489 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6196 df-ov 6237 df-oprab 6238 df-mpt2 6239 df-of 6477 df-om 6639 df-1st 6738 df-2nd 6739 df-supp 6857 df-recs 6999 df-rdg 7033 df-1o 7087 df-2o 7088 df-oadd 7091 df-er 7268 df-map 7379 df-pm 7380 df-ixp 7428 df-en 7475 df-dom 7476 df-sdom 7477 df-fin 7478 df-fsupp 7784 df-fi 7825 df-sup 7855 df-oi 7889 df-card 8272 df-cda 8500 df-pnf 9580 df-mnf 9581 df-xr 9582 df-ltxr 9583 df-le 9584 df-sub 9763 df-neg 9764 df-div 10168 df-nn 10497 df-2 10555 df-3 10556 df-4 10557 df-5 10558 df-6 10559 df-7 10560 df-8 10561 df-9 10562 df-10 10563 df-n0 10757 df-z 10826 df-dec 10940 df-uz 11046 df-q 11146 df-rp 11184 df-xneg 11289 df-xadd 11290 df-xmul 11291 df-ioo 11504 df-ioc 11505 df-ico 11506 df-icc 11507 df-fz 11644 df-fzo 11768 df-fl 11879 df-mod 11948 df-seq 12062 df-exp 12121 df-fac 12308 df-bc 12335 df-hash 12360 df-shft 12956 df-cj 12988 df-re 12989 df-im 12990 df-sqrt 13124 df-abs 13125 df-limsup 13350 df-clim 13367 df-rlim 13368 df-sum 13565 df-ef 13904 df-sin 13906 df-cos 13907 df-pi 13909 df-dvds 14088 df-gcd 14246 df-prm 14319 df-pc 14462 df-struct 14735 df-ndx 14736 df-slot 14737 df-base 14738 df-sets 14739 df-ress 14740 df-plusg 14814 df-mulr 14815 df-starv 14816 df-sca 14817 df-vsca 14818 df-ip 14819 df-tset 14820 df-ple 14821 df-ds 14823 df-unif 14824 df-hom 14825 df-cco 14826 df-rest 14929 df-topn 14930 df-0g 14948 df-gsum 14949 df-topgen 14950 df-pt 14951 df-prds 14954 df-xrs 15008 df-qtop 15013 df-imas 15014 df-xps 15016 df-mre 15092 df-mrc 15093 df-acs 15095 df-mgm 16088 df-sgrp 16127 df-mnd 16137 df-submnd 16183 df-mulg 16276 df-cntz 16571 df-cmn 17016 df-psmet 18623 df-xmet 18624 df-met 18625 df-bl 18626 df-mopn 18627 df-fbas 18628 df-fg 18629 df-cnfld 18633 df-top 19583 df-bases 19585 df-topon 19586 df-topsp 19587 df-cld 19704 df-ntr 19705 df-cls 19706 df-nei 19784 df-lp 19822 df-perf 19823 df-cn 19913 df-cnp 19914 df-haus 20001 df-tx 20247 df-hmeo 20440 df-fil 20531 df-fm 20623 df-flim 20624 df-flf 20625 df-xms 21007 df-ms 21008 df-tms 21009 df-cncf 21566 df-limc 22454 df-dv 22455 df-log 23128 df-cht 23643

This theorem is referenced by: chtub 23760

W3C validator