binomlem - Metamath Proof Explorer

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

Theorem binomlem 12563

Description: Lemma for binom 12564 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)

**Hypotheses**
Ref	Expression
binomlem.1
binomlem.2
binomlem.3
binomlem.4

**Assertion**
Ref	Expression
binomlem	$/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem binomlem Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		binomlem.4	. . . . . 6
2	1	adantl 453	. . . . 5 $/\$
3	2	oveq1d 6055	. . . 4 $/\$
4		fzfid 11267	. . . . . . 7
5		binomlem.1	. . . . . . 7
6		fzelp1 11055	. . . . . . . . 9
7		binomlem.3	. . . . . . . . . . 11
8		elfzelz 11015	. . . . . . . . . . 11
9		bccl 11568	. . . . . . . . . . 11 $/\$
10	7, 8, 9	syl2an 464	. . . . . . . . . 10 $/\$
11	10	nn0cnd 10232	. . . . . . . . 9 $/\$
12	6, 11	sylan2 461	. . . . . . . 8 $/\$
13		fznn0sub 11041	. . . . . . . . . 10
14		expcl 11354	. . . . . . . . . 10 $/\$
15	5, 13, 14	syl2an 464	. . . . . . . . 9 $/\$
16		binomlem.2	. . . . . . . . . . 11
17		elfznn0 11039	. . . . . . . . . . 11
18		expcl 11354	. . . . . . . . . . 11 $/\$
19	16, 17, 18	syl2an 464	. . . . . . . . . 10 $/\$
20	6, 19	sylan2 461	. . . . . . . . 9 $/\$
21	15, 20	mulcld 9064	. . . . . . . 8 $/\$
22	12, 21	mulcld 9064	. . . . . . 7 $/\$
23	4, 5, 22	fsummulc1 12523	. . . . . 6
24	5	adantr 452	. . . . . . . . 9 $/\$
25	12, 21, 24	mulassd 9067	. . . . . . . 8 $/\$
26	7	nn0cnd 10232	. . . . . . . . . . . . . . 15
27	26	adantr 452	. . . . . . . . . . . . . 14 $/\$
28		ax-1cn 9004	. . . . . . . . . . . . . . 15
29	28	a1i 11	. . . . . . . . . . . . . 14 $/\$
30		elfzelz 11015	. . . . . . . . . . . . . . . 16
31	30	adantl 453	. . . . . . . . . . . . . . 15 $/\$
32	31	zcnd 10332	. . . . . . . . . . . . . 14 $/\$
33	27, 29, 32	addsubd 9388	. . . . . . . . . . . . 13 $/\$
34	33	oveq2d 6056	. . . . . . . . . . . 12 $/\$
35		expp1 11343	. . . . . . . . . . . . 13 $/\$
36	5, 13, 35	syl2an 464	. . . . . . . . . . . 12 $/\$
37	34, 36	eqtrd 2436	. . . . . . . . . . 11 $/\$
38	37	oveq1d 6055	. . . . . . . . . 10 $/\$
39	15, 24, 20	mul32d 9232	. . . . . . . . . 10 $/\$
40	38, 39	eqtrd 2436	. . . . . . . . 9 $/\$
41	40	oveq2d 6056	. . . . . . . 8 $/\$
42	25, 41	eqtr4d 2439	. . . . . . 7 $/\$
43	42	sumeq2dv 12452	. . . . . 6
44		fzssp1 11051	. . . . . . . 8
45	44	a1i 11	. . . . . . 7
46		fznn0sub 11041	. . . . . . . . . . 11
47		expcl 11354	. . . . . . . . . . 11 $/\$
48	5, 46, 47	syl2an 464	. . . . . . . . . 10 $/\$
49	48, 19	mulcld 9064	. . . . . . . . 9 $/\$
50	11, 49	mulcld 9064	. . . . . . . 8 $/\$
51	6, 50	sylan2 461	. . . . . . 7 $/\$
52	7	adantr 452	. . . . . . . . . 10 $/\$ $\$
53		eldifi 3429	. . . . . . . . . . . 12 $\$
54	53, 8	syl 16	. . . . . . . . . . 11 $\$
55	54	adantl 453	. . . . . . . . . 10 $/\$ $\$
56		eldifn 3430	. . . . . . . . . . 11 $\$
57	56	adantl 453	. . . . . . . . . 10 $/\$ $\$
58		bcval3 11552	. . . . . . . . . 10 $/\$ $/\$
59	52, 55, 57, 58	syl3anc 1184	. . . . . . . . 9 $/\$ $\$
60	59	oveq1d 6055	. . . . . . . 8 $/\$ $\$
61	49	mul02d 9220	. . . . . . . . 9 $/\$
62	53, 61	sylan2 461	. . . . . . . 8 $/\$ $\$
63	60, 62	eqtrd 2436	. . . . . . 7 $/\$ $\$
64		fzssuz 11049	. . . . . . . 8
65	64	a1i 11	. . . . . . 7
66	45, 51, 63, 65	sumss 12473	. . . . . 6
67	23, 43, 66	3eqtrd 2440	. . . . 5
68	67	adantr 452	. . . 4 $/\$
69	3, 68	eqtrd 2436	. . 3 $/\$
70	1	oveq1d 6055	. . . 4
71	4, 16, 22	fsummulc1 12523	. . . . 5
72		1z 10267	. . . . . . . . 9
73	72	a1i 11	. . . . . . . 8
74		0z 10249	. . . . . . . . 9
75	74	a1i 11	. . . . . . . 8
76	7	nn0zd 10329	. . . . . . . 8
77	16	adantr 452	. . . . . . . . 9 $/\$
78	22, 77	mulcld 9064	. . . . . . . 8 $/\$
79		oveq2 6048	. . . . . . . . . 10
80		oveq2 6048	. . . . . . . . . . . 12
81	80	oveq2d 6056	. . . . . . . . . . 11
82		oveq2 6048	. . . . . . . . . . 11
83	81, 82	oveq12d 6058	. . . . . . . . . 10
84	79, 83	oveq12d 6058	. . . . . . . . 9
85	84	oveq1d 6055	. . . . . . . 8
86	73, 75, 76, 78, 85	fsumshft 12518	. . . . . . 7
87		oveq1 6047	. . . . . . . . . . 11
88	87	oveq2d 6056	. . . . . . . . . 10
89	87	oveq2d 6056	. . . . . . . . . . . 12
90	89	oveq2d 6056	. . . . . . . . . . 11
91	87	oveq2d 6056	. . . . . . . . . . 11
92	90, 91	oveq12d 6058	. . . . . . . . . 10
93	88, 92	oveq12d 6058	. . . . . . . . 9
94	93	oveq1d 6055	. . . . . . . 8
95	94	cbvsumv 12445	. . . . . . 7
96	86, 95	syl6eq 2452	. . . . . 6
97	26	adantr 452	. . . . . . . . . . . . 13 $/\$
98		elfzelz 11015	. . . . . . . . . . . . . . 15
99	98	adantl 453	. . . . . . . . . . . . . 14 $/\$
100	99	zcnd 10332	. . . . . . . . . . . . 13 $/\$
101	28	a1i 11	. . . . . . . . . . . . 13 $/\$
102	97, 100, 101	subsub3d 9397	. . . . . . . . . . . 12 $/\$
103	102	oveq2d 6056	. . . . . . . . . . 11 $/\$
104	103	oveq1d 6055	. . . . . . . . . 10 $/\$
105	104	oveq2d 6056	. . . . . . . . 9 $/\$
106	105	oveq1d 6055	. . . . . . . 8 $/\$
107		fzp1ss 11054	. . . . . . . . . . . 12
108	74, 107	ax-mp 8	. . . . . . . . . . 11
109	108	sseli 3304	. . . . . . . . . 10
110	7	adantr 452	. . . . . . . . . . . 12 $/\$
111	8	adantl 453	. . . . . . . . . . . . 13 $/\$
112		peano2zm 10276	. . . . . . . . . . . . 13
113	111, 112	syl 16	. . . . . . . . . . . 12 $/\$
114		bccl 11568	. . . . . . . . . . . 12 $/\$
115	110, 113, 114	syl2anc 643	. . . . . . . . . . 11 $/\$
116	115	nn0cnd 10232	. . . . . . . . . 10 $/\$
117	109, 116	sylan2 461	. . . . . . . . 9 $/\$
118	109, 48	sylan2 461	. . . . . . . . . 10 $/\$
119	16	adantr 452	. . . . . . . . . . 11 $/\$
120		elfznn 11036	. . . . . . . . . . . . . 14
121		0p1e1 10049	. . . . . . . . . . . . . . 15
122	121	oveq1i 6050	. . . . . . . . . . . . . 14
123	120, 122	eleq2s 2496	. . . . . . . . . . . . 13
124	123	adantl 453	. . . . . . . . . . . 12 $/\$
125		nnm1nn0 10217	. . . . . . . . . . . 12
126	124, 125	syl 16	. . . . . . . . . . 11 $/\$
127	119, 126	expcld 11478	. . . . . . . . . 10 $/\$
128	118, 127	mulcld 9064	. . . . . . . . 9 $/\$
129	117, 128, 119	mulassd 9067	. . . . . . . 8 $/\$
130	118, 127, 119	mulassd 9067	. . . . . . . . . 10 $/\$
131		expm1t 11363	. . . . . . . . . . . 12 $/\$
132	16, 123, 131	syl2an 464	. . . . . . . . . . 11 $/\$
133	132	oveq2d 6056	. . . . . . . . . 10 $/\$
134	130, 133	eqtr4d 2439	. . . . . . . . 9 $/\$
135	134	oveq2d 6056	. . . . . . . 8 $/\$
136	106, 129, 135	3eqtrd 2440	. . . . . . 7 $/\$
137	136	sumeq2dv 12452	. . . . . 6
138	108	a1i 11	. . . . . . 7
139	116, 49	mulcld 9064	. . . . . . . 8 $/\$
140	109, 139	sylan2 461	. . . . . . 7 $/\$
141	7	adantr 452	. . . . . . . . . 10 $/\$ $\$
142		eldifi 3429	. . . . . . . . . . . . 13 $\$
143	142	adantl 453	. . . . . . . . . . . 12 $/\$ $\$
144	143, 8	syl 16	. . . . . . . . . . 11 $/\$ $\$
145	144, 112	syl 16	. . . . . . . . . 10 $/\$ $\$
146		eldifn 3430	. . . . . . . . . . . 12 $\$
147	146	adantl 453	. . . . . . . . . . 11 $/\$ $\$
148	74	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
149	141	nn0zd 10329	. . . . . . . . . . . . 13 $/\$ $\$
150	72	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
151		fzaddel 11043	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
152	148, 149, 145, 150, 151	syl22anc 1185	. . . . . . . . . . . 12 $/\$ $\$
153	144	zcnd 10332	. . . . . . . . . . . . . 14 $/\$ $\$
154		npcan 9270	. . . . . . . . . . . . . 14 $/\$
155	153, 28, 154	sylancl 644	. . . . . . . . . . . . 13 $/\$ $\$
156	155	eleq1d 2470	. . . . . . . . . . . 12 $/\$ $\$
157	152, 156	bitrd 245	. . . . . . . . . . 11 $/\$ $\$
158	147, 157	mtbird 293	. . . . . . . . . 10 $/\$ $\$
159		bcval3 11552	. . . . . . . . . 10 $/\$ $/\$
160	141, 145, 158, 159	syl3anc 1184	. . . . . . . . 9 $/\$ $\$
161	160	oveq1d 6055	. . . . . . . 8 $/\$ $\$
162	142, 61	sylan2 461	. . . . . . . 8 $/\$ $\$
163	161, 162	eqtrd 2436	. . . . . . 7 $/\$ $\$
164	138, 140, 163, 65	sumss 12473	. . . . . 6
165	96, 137, 164	3eqtrd 2440	. . . . 5
166	71, 165	eqtrd 2436	. . . 4
167	70, 166	sylan9eqr 2458	. . 3 $/\$
168	69, 167	oveq12d 6058	. 2 $/\$
169	5, 16	addcld 9063	. . . . 5
170	169, 7	expp1d 11479	. . . 4
171	169, 7	expcld 11478	. . . . 5
172	171, 5, 16	adddid 9068	. . . 4
173	170, 172	eqtrd 2436	. . 3
174	173	adantr 452	. 2 $/\$
175		bcpasc 11567	. . . . . . . 8 $/\$
176	7, 8, 175	syl2an 464	. . . . . . 7 $/\$
177	176	oveq1d 6055	. . . . . 6 $/\$
178	11, 116, 49	adddird 9069	. . . . . 6 $/\$
179	177, 178	eqtr3d 2438	. . . . 5 $/\$
180	179	sumeq2dv 12452	. . . 4
181		fzfid 11267	. . . . 5
182	181, 50, 139	fsumadd 12487	. . . 4
183	180, 182	eqtrd 2436	. . 3
184	183	adantr 452	. 2 $/\$
185	168, 174, 184	3eqtr4d 2446	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721 $\$ cdif 3277

wss 3280

cfv 5413 (class class class)co 6040

cc 8944

cc0 8946

c1 8947

caddc 8949

cmul 8951

cmin 9247

cn 9956

cn0 10177

cz 10238

cuz 10444

cfz 10999

cexp 11337

cbc 11548

csu 12434

This theorem is referenced by: binom 12564

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435

W3C validator