binomlem - Metamath Proof Explorer

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

Theorem binomlem 13880

Description: Lemma for binom 13881 (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 468	. . . . 5 $/\$
3	2	oveq1d 6318	. . . 4 $/\$
4		fzfid 12187	. . . . . . 7
5		binomlem.1	. . . . . . 7
6		fzelp1 11850	. . . . . . . . 9
7		binomlem.3	. . . . . . . . . . 11
8		elfzelz 11802	. . . . . . . . . . 11
9		bccl 12508	. . . . . . . . . . 11 $/\$
10	7, 8, 9	syl2an 480	. . . . . . . . . 10 $/\$
11	10	nn0cnd 10929	. . . . . . . . 9 $/\$
12	6, 11	sylan2 477	. . . . . . . 8 $/\$
13		fznn0sub 11833	. . . . . . . . . 10
14		expcl 12291	. . . . . . . . . 10 $/\$
15	5, 13, 14	syl2an 480	. . . . . . . . 9 $/\$
16		binomlem.2	. . . . . . . . . . 11
17		elfznn0 11889	. . . . . . . . . . 11
18		expcl 12291	. . . . . . . . . . 11 $/\$
19	16, 17, 18	syl2an 480	. . . . . . . . . 10 $/\$
20	6, 19	sylan2 477	. . . . . . . . 9 $/\$
21	15, 20	mulcld 9665	. . . . . . . 8 $/\$
22	12, 21	mulcld 9665	. . . . . . 7 $/\$
23	4, 5, 22	fsummulc1 13839	. . . . . 6
24	5	adantr 467	. . . . . . . . 9 $/\$
25	12, 21, 24	mulassd 9668	. . . . . . . 8 $/\$
26	7	nn0cnd 10929	. . . . . . . . . . . . . . 15
27	26	adantr 467	. . . . . . . . . . . . . 14 $/\$
28		1cnd 9661	. . . . . . . . . . . . . 14 $/\$
29		elfzelz 11802	. . . . . . . . . . . . . . . 16
30	29	adantl 468	. . . . . . . . . . . . . . 15 $/\$
31	30	zcnd 11043	. . . . . . . . . . . . . 14 $/\$
32	27, 28, 31	addsubd 10009	. . . . . . . . . . . . 13 $/\$
33	32	oveq2d 6319	. . . . . . . . . . . 12 $/\$
34		expp1 12280	. . . . . . . . . . . . 13 $/\$
35	5, 13, 34	syl2an 480	. . . . . . . . . . . 12 $/\$
36	33, 35	eqtrd 2464	. . . . . . . . . . 11 $/\$
37	36	oveq1d 6318	. . . . . . . . . 10 $/\$
38	15, 24, 20	mul32d 9845	. . . . . . . . . 10 $/\$
39	37, 38	eqtrd 2464	. . . . . . . . 9 $/\$
40	39	oveq2d 6319	. . . . . . . 8 $/\$
41	25, 40	eqtr4d 2467	. . . . . . 7 $/\$
42	41	sumeq2dv 13762	. . . . . 6
43		fzssp1 11843	. . . . . . . 8
44	43	a1i 11	. . . . . . 7
45		fznn0sub 11833	. . . . . . . . . . 11
46		expcl 12291	. . . . . . . . . . 11 $/\$
47	5, 45, 46	syl2an 480	. . . . . . . . . 10 $/\$
48	47, 19	mulcld 9665	. . . . . . . . 9 $/\$
49	11, 48	mulcld 9665	. . . . . . . 8 $/\$
50	6, 49	sylan2 477	. . . . . . 7 $/\$
51	7	adantr 467	. . . . . . . . . 10 $/\$ $\$
52		eldifi 3588	. . . . . . . . . . . 12 $\$
53	52, 8	syl 17	. . . . . . . . . . 11 $\$
54	53	adantl 468	. . . . . . . . . 10 $/\$ $\$
55		eldifn 3589	. . . . . . . . . . 11 $\$
56	55	adantl 468	. . . . . . . . . 10 $/\$ $\$
57		bcval3 12492	. . . . . . . . . 10 $/\$ $/\$
58	51, 54, 56, 57	syl3anc 1265	. . . . . . . . 9 $/\$ $\$
59	58	oveq1d 6318	. . . . . . . 8 $/\$ $\$
60	48	mul02d 9833	. . . . . . . . 9 $/\$
61	52, 60	sylan2 477	. . . . . . . 8 $/\$ $\$
62	59, 61	eqtrd 2464	. . . . . . 7 $/\$ $\$
63		fzssuz 11841	. . . . . . . 8
64	63	a1i 11	. . . . . . 7
65	44, 50, 62, 64	sumss 13783	. . . . . 6
66	23, 42, 65	3eqtrd 2468	. . . . 5
67	66	adantr 467	. . . 4 $/\$
68	3, 67	eqtrd 2464	. . 3 $/\$
69	1	oveq1d 6318	. . . 4
70	4, 16, 22	fsummulc1 13839	. . . . 5
71		1zzd 10970	. . . . . . . 8
72		0z 10950	. . . . . . . . 9
73	72	a1i 11	. . . . . . . 8
74	7	nn0zd 11040	. . . . . . . 8
75	16	adantr 467	. . . . . . . . 9 $/\$
76	22, 75	mulcld 9665	. . . . . . . 8 $/\$
77		oveq2 6311	. . . . . . . . . 10
78		oveq2 6311	. . . . . . . . . . . 12
79	78	oveq2d 6319	. . . . . . . . . . 11
80		oveq2 6311	. . . . . . . . . . 11
81	79, 80	oveq12d 6321	. . . . . . . . . 10
82	77, 81	oveq12d 6321	. . . . . . . . 9
83	82	oveq1d 6318	. . . . . . . 8
84	71, 73, 74, 76, 83	fsumshft 13834	. . . . . . 7
85		oveq1 6310	. . . . . . . . . . 11
86	85	oveq2d 6319	. . . . . . . . . 10
87	85	oveq2d 6319	. . . . . . . . . . . 12
88	87	oveq2d 6319	. . . . . . . . . . 11
89	85	oveq2d 6319	. . . . . . . . . . 11
90	88, 89	oveq12d 6321	. . . . . . . . . 10
91	86, 90	oveq12d 6321	. . . . . . . . 9
92	91	oveq1d 6318	. . . . . . . 8
93	92	cbvsumv 13755	. . . . . . 7
94	84, 93	syl6eq 2480	. . . . . 6
95	26	adantr 467	. . . . . . . . . . . . 13 $/\$
96		elfzelz 11802	. . . . . . . . . . . . . . 15
97	96	adantl 468	. . . . . . . . . . . . . 14 $/\$
98	97	zcnd 11043	. . . . . . . . . . . . 13 $/\$
99		1cnd 9661	. . . . . . . . . . . . 13 $/\$
100	95, 98, 99	subsub3d 10018	. . . . . . . . . . . 12 $/\$
101	100	oveq2d 6319	. . . . . . . . . . 11 $/\$
102	101	oveq1d 6318	. . . . . . . . . 10 $/\$
103	102	oveq2d 6319	. . . . . . . . 9 $/\$
104	103	oveq1d 6318	. . . . . . . 8 $/\$
105		fzp1ss 11849	. . . . . . . . . . . 12
106	72, 105	ax-mp 5	. . . . . . . . . . 11
107	106	sseli 3461	. . . . . . . . . 10
108	7	adantr 467	. . . . . . . . . . . 12 $/\$
109	8	adantl 468	. . . . . . . . . . . . 13 $/\$
110		peano2zm 10982	. . . . . . . . . . . . 13
111	109, 110	syl 17	. . . . . . . . . . . 12 $/\$
112		bccl 12508	. . . . . . . . . . . 12 $/\$
113	108, 111, 112	syl2anc 666	. . . . . . . . . . 11 $/\$
114	113	nn0cnd 10929	. . . . . . . . . 10 $/\$
115	107, 114	sylan2 477	. . . . . . . . 9 $/\$
116	107, 47	sylan2 477	. . . . . . . . . 10 $/\$
117	16	adantr 467	. . . . . . . . . . 11 $/\$
118		elfznn 11830	. . . . . . . . . . . . . 14
119		0p1e1 10723	. . . . . . . . . . . . . . 15
120	119	oveq1i 6313	. . . . . . . . . . . . . 14
121	118, 120	eleq2s 2531	. . . . . . . . . . . . 13
122	121	adantl 468	. . . . . . . . . . . 12 $/\$
123		nnm1nn0 10913	. . . . . . . . . . . 12
124	122, 123	syl 17	. . . . . . . . . . 11 $/\$
125	117, 124	expcld 12417	. . . . . . . . . 10 $/\$
126	116, 125	mulcld 9665	. . . . . . . . 9 $/\$
127	115, 126, 117	mulassd 9668	. . . . . . . 8 $/\$
128	116, 125, 117	mulassd 9668	. . . . . . . . . 10 $/\$
129		expm1t 12301	. . . . . . . . . . . 12 $/\$
130	16, 121, 129	syl2an 480	. . . . . . . . . . 11 $/\$
131	130	oveq2d 6319	. . . . . . . . . 10 $/\$
132	128, 131	eqtr4d 2467	. . . . . . . . 9 $/\$
133	132	oveq2d 6319	. . . . . . . 8 $/\$
134	104, 127, 133	3eqtrd 2468	. . . . . . 7 $/\$
135	134	sumeq2dv 13762	. . . . . 6
136	106	a1i 11	. . . . . . 7
137	114, 48	mulcld 9665	. . . . . . . 8 $/\$
138	107, 137	sylan2 477	. . . . . . 7 $/\$
139	7	adantr 467	. . . . . . . . . 10 $/\$ $\$
140		eldifi 3588	. . . . . . . . . . . . 13 $\$
141	140	adantl 468	. . . . . . . . . . . 12 $/\$ $\$
142	141, 8	syl 17	. . . . . . . . . . 11 $/\$ $\$
143	142, 110	syl 17	. . . . . . . . . 10 $/\$ $\$
144		eldifn 3589	. . . . . . . . . . . 12 $\$
145	144	adantl 468	. . . . . . . . . . 11 $/\$ $\$
146	72	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
147	139	nn0zd 11040	. . . . . . . . . . . . 13 $/\$ $\$
148		1zzd 10970	. . . . . . . . . . . . 13 $/\$ $\$
149		fzaddel 11835	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	146, 147, 143, 148, 149	syl22anc 1266	. . . . . . . . . . . 12 $/\$ $\$
151	142	zcnd 11043	. . . . . . . . . . . . . 14 $/\$ $\$
152		ax-1cn 9599	. . . . . . . . . . . . . 14
153		npcan 9886	. . . . . . . . . . . . . 14 $/\$
154	151, 152, 153	sylancl 667	. . . . . . . . . . . . 13 $/\$ $\$
155	154	eleq1d 2492	. . . . . . . . . . . 12 $/\$ $\$
156	150, 155	bitrd 257	. . . . . . . . . . 11 $/\$ $\$
157	145, 156	mtbird 303	. . . . . . . . . 10 $/\$ $\$
158		bcval3 12492	. . . . . . . . . 10 $/\$ $/\$
159	139, 143, 157, 158	syl3anc 1265	. . . . . . . . 9 $/\$ $\$
160	159	oveq1d 6318	. . . . . . . 8 $/\$ $\$
161	140, 60	sylan2 477	. . . . . . . 8 $/\$ $\$
162	160, 161	eqtrd 2464	. . . . . . 7 $/\$ $\$
163	136, 138, 162, 64	sumss 13783	. . . . . 6
164	94, 135, 163	3eqtrd 2468	. . . . 5
165	70, 164	eqtrd 2464	. . . 4
166	69, 165	sylan9eqr 2486	. . 3 $/\$
167	68, 166	oveq12d 6321	. 2 $/\$
168	5, 16	addcld 9664	. . . . 5
169	168, 7	expp1d 12418	. . . 4
170	168, 7	expcld 12417	. . . . 5
171	170, 5, 16	adddid 9669	. . . 4
172	169, 171	eqtrd 2464	. . 3
173	172	adantr 467	. 2 $/\$
174		bcpasc 12507	. . . . . . . 8 $/\$
175	7, 8, 174	syl2an 480	. . . . . . 7 $/\$
176	175	oveq1d 6318	. . . . . 6 $/\$
177	11, 114, 48	adddird 9670	. . . . . 6 $/\$
178	176, 177	eqtr3d 2466	. . . . 5 $/\$
179	178	sumeq2dv 13762	. . . 4
180		fzfid 12187	. . . . 5
181	180, 49, 137	fsumadd 13798	. . . 4
182	179, 181	eqtrd 2464	. . 3
183	182	adantr 467	. 2 $/\$
184	167, 173, 183	3eqtr4d 2474	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1438

wcel 1869 $\$ cdif 3434

wss 3437

cfv 5599 (class class class)co 6303

cc 9539

cc0 9541

c1 9542

caddc 9544

cmul 9546

cmin 9862

cn 10611

cn0 10871

cz 10939

cuz 11161

cfz 11786

cexp 12273

cbc 12488

csu 13745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-fal 1444 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-oadd 7192 df-er 7369 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-sup 7960 df-oi 8029 df-card 8376 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-n0 10872 df-z 10940 df-uz 11162 df-rp 11305 df-fz 11787 df-fzo 11918 df-seq 12215 df-exp 12274 df-fac 12461 df-bc 12489 df-hash 12517 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-clim 13545 df-sum 13746

This theorem is referenced by: binom 13881

W3C validator