binomlem - Metamath Proof Explorer

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

Theorem binomlem 13964

Description: Lemma for binom 13965 (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 473	. . . . 5 $/\$
3	2	oveq1d 6323	. . . 4 $/\$
4		fzfid 12224	. . . . . . 7
5		binomlem.1	. . . . . . 7
6		fzelp1 11874	. . . . . . . . 9
7		binomlem.3	. . . . . . . . . . 11
8		elfzelz 11826	. . . . . . . . . . 11
9		bccl 12545	. . . . . . . . . . 11 $/\$
10	7, 8, 9	syl2an 485	. . . . . . . . . 10 $/\$
11	10	nn0cnd 10951	. . . . . . . . 9 $/\$
12	6, 11	sylan2 482	. . . . . . . 8 $/\$
13		fznn0sub 11857	. . . . . . . . . 10
14		expcl 12328	. . . . . . . . . 10 $/\$
15	5, 13, 14	syl2an 485	. . . . . . . . 9 $/\$
16		binomlem.2	. . . . . . . . . . 11
17		elfznn0 11913	. . . . . . . . . . 11
18		expcl 12328	. . . . . . . . . . 11 $/\$
19	16, 17, 18	syl2an 485	. . . . . . . . . 10 $/\$
20	6, 19	sylan2 482	. . . . . . . . 9 $/\$
21	15, 20	mulcld 9681	. . . . . . . 8 $/\$
22	12, 21	mulcld 9681	. . . . . . 7 $/\$
23	4, 5, 22	fsummulc1 13923	. . . . . 6
24	5	adantr 472	. . . . . . . . 9 $/\$
25	12, 21, 24	mulassd 9684	. . . . . . . 8 $/\$
26	7	nn0cnd 10951	. . . . . . . . . . . . . . 15
27	26	adantr 472	. . . . . . . . . . . . . 14 $/\$
28		1cnd 9677	. . . . . . . . . . . . . 14 $/\$
29		elfzelz 11826	. . . . . . . . . . . . . . . 16
30	29	adantl 473	. . . . . . . . . . . . . . 15 $/\$
31	30	zcnd 11064	. . . . . . . . . . . . . 14 $/\$
32	27, 28, 31	addsubd 10026	. . . . . . . . . . . . 13 $/\$
33	32	oveq2d 6324	. . . . . . . . . . . 12 $/\$
34		expp1 12317	. . . . . . . . . . . . 13 $/\$
35	5, 13, 34	syl2an 485	. . . . . . . . . . . 12 $/\$
36	33, 35	eqtrd 2505	. . . . . . . . . . 11 $/\$
37	36	oveq1d 6323	. . . . . . . . . 10 $/\$
38	15, 24, 20	mul32d 9861	. . . . . . . . . 10 $/\$
39	37, 38	eqtrd 2505	. . . . . . . . 9 $/\$
40	39	oveq2d 6324	. . . . . . . 8 $/\$
41	25, 40	eqtr4d 2508	. . . . . . 7 $/\$
42	41	sumeq2dv 13846	. . . . . 6
43		fzssp1 11867	. . . . . . . 8
44	43	a1i 11	. . . . . . 7
45		fznn0sub 11857	. . . . . . . . . . 11
46		expcl 12328	. . . . . . . . . . 11 $/\$
47	5, 45, 46	syl2an 485	. . . . . . . . . 10 $/\$
48	47, 19	mulcld 9681	. . . . . . . . 9 $/\$
49	11, 48	mulcld 9681	. . . . . . . 8 $/\$
50	6, 49	sylan2 482	. . . . . . 7 $/\$
51	7	adantr 472	. . . . . . . . . 10 $/\$ $\$
52		eldifi 3544	. . . . . . . . . . . 12 $\$
53	52, 8	syl 17	. . . . . . . . . . 11 $\$
54	53	adantl 473	. . . . . . . . . 10 $/\$ $\$
55		eldifn 3545	. . . . . . . . . . 11 $\$
56	55	adantl 473	. . . . . . . . . 10 $/\$ $\$
57		bcval3 12529	. . . . . . . . . 10 $/\$ $/\$
58	51, 54, 56, 57	syl3anc 1292	. . . . . . . . 9 $/\$ $\$
59	58	oveq1d 6323	. . . . . . . 8 $/\$ $\$
60	48	mul02d 9849	. . . . . . . . 9 $/\$
61	52, 60	sylan2 482	. . . . . . . 8 $/\$ $\$
62	59, 61	eqtrd 2505	. . . . . . 7 $/\$ $\$
63		fzssuz 11865	. . . . . . . 8
64	63	a1i 11	. . . . . . 7
65	44, 50, 62, 64	sumss 13867	. . . . . 6
66	23, 42, 65	3eqtrd 2509	. . . . 5
67	66	adantr 472	. . . 4 $/\$
68	3, 67	eqtrd 2505	. . 3 $/\$
69	1	oveq1d 6323	. . . 4
70	4, 16, 22	fsummulc1 13923	. . . . 5
71		1zzd 10992	. . . . . . . 8
72		0z 10972	. . . . . . . . 9
73	72	a1i 11	. . . . . . . 8
74	7	nn0zd 11061	. . . . . . . 8
75	16	adantr 472	. . . . . . . . 9 $/\$
76	22, 75	mulcld 9681	. . . . . . . 8 $/\$
77		oveq2 6316	. . . . . . . . . 10
78		oveq2 6316	. . . . . . . . . . . 12
79	78	oveq2d 6324	. . . . . . . . . . 11
80		oveq2 6316	. . . . . . . . . . 11
81	79, 80	oveq12d 6326	. . . . . . . . . 10
82	77, 81	oveq12d 6326	. . . . . . . . 9
83	82	oveq1d 6323	. . . . . . . 8
84	71, 73, 74, 76, 83	fsumshft 13918	. . . . . . 7
85		oveq1 6315	. . . . . . . . . . 11
86	85	oveq2d 6324	. . . . . . . . . 10
87	85	oveq2d 6324	. . . . . . . . . . . 12
88	87	oveq2d 6324	. . . . . . . . . . 11
89	85	oveq2d 6324	. . . . . . . . . . 11
90	88, 89	oveq12d 6326	. . . . . . . . . 10
91	86, 90	oveq12d 6326	. . . . . . . . 9
92	91	oveq1d 6323	. . . . . . . 8
93	92	cbvsumv 13839	. . . . . . 7
94	84, 93	syl6eq 2521	. . . . . 6
95	26	adantr 472	. . . . . . . . . . . . 13 $/\$
96		elfzelz 11826	. . . . . . . . . . . . . . 15
97	96	adantl 473	. . . . . . . . . . . . . 14 $/\$
98	97	zcnd 11064	. . . . . . . . . . . . 13 $/\$
99		1cnd 9677	. . . . . . . . . . . . 13 $/\$
100	95, 98, 99	subsub3d 10035	. . . . . . . . . . . 12 $/\$
101	100	oveq2d 6324	. . . . . . . . . . 11 $/\$
102	101	oveq1d 6323	. . . . . . . . . 10 $/\$
103	102	oveq2d 6324	. . . . . . . . 9 $/\$
104	103	oveq1d 6323	. . . . . . . 8 $/\$
105		fzp1ss 11873	. . . . . . . . . . . 12
106	72, 105	ax-mp 5	. . . . . . . . . . 11
107	106	sseli 3414	. . . . . . . . . 10
108	7	adantr 472	. . . . . . . . . . . 12 $/\$
109	8	adantl 473	. . . . . . . . . . . . 13 $/\$
110		peano2zm 11004	. . . . . . . . . . . . 13
111	109, 110	syl 17	. . . . . . . . . . . 12 $/\$
112		bccl 12545	. . . . . . . . . . . 12 $/\$
113	108, 111, 112	syl2anc 673	. . . . . . . . . . 11 $/\$
114	113	nn0cnd 10951	. . . . . . . . . 10 $/\$
115	107, 114	sylan2 482	. . . . . . . . 9 $/\$
116	107, 47	sylan2 482	. . . . . . . . . 10 $/\$
117	16	adantr 472	. . . . . . . . . . 11 $/\$
118		elfznn 11854	. . . . . . . . . . . . . 14
119		0p1e1 10743	. . . . . . . . . . . . . . 15
120	119	oveq1i 6318	. . . . . . . . . . . . . 14
121	118, 120	eleq2s 2567	. . . . . . . . . . . . 13
122	121	adantl 473	. . . . . . . . . . . 12 $/\$
123		nnm1nn0 10935	. . . . . . . . . . . 12
124	122, 123	syl 17	. . . . . . . . . . 11 $/\$
125	117, 124	expcld 12454	. . . . . . . . . 10 $/\$
126	116, 125	mulcld 9681	. . . . . . . . 9 $/\$
127	115, 126, 117	mulassd 9684	. . . . . . . 8 $/\$
128	116, 125, 117	mulassd 9684	. . . . . . . . . 10 $/\$
129		expm1t 12338	. . . . . . . . . . . 12 $/\$
130	16, 121, 129	syl2an 485	. . . . . . . . . . 11 $/\$
131	130	oveq2d 6324	. . . . . . . . . 10 $/\$
132	128, 131	eqtr4d 2508	. . . . . . . . 9 $/\$
133	132	oveq2d 6324	. . . . . . . 8 $/\$
134	104, 127, 133	3eqtrd 2509	. . . . . . 7 $/\$
135	134	sumeq2dv 13846	. . . . . 6
136	106	a1i 11	. . . . . . 7
137	114, 48	mulcld 9681	. . . . . . . 8 $/\$
138	107, 137	sylan2 482	. . . . . . 7 $/\$
139	7	adantr 472	. . . . . . . . . 10 $/\$ $\$
140		eldifi 3544	. . . . . . . . . . . . 13 $\$
141	140	adantl 473	. . . . . . . . . . . 12 $/\$ $\$
142	141, 8	syl 17	. . . . . . . . . . 11 $/\$ $\$
143	142, 110	syl 17	. . . . . . . . . 10 $/\$ $\$
144		eldifn 3545	. . . . . . . . . . . 12 $\$
145	144	adantl 473	. . . . . . . . . . 11 $/\$ $\$
146	72	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
147	139	nn0zd 11061	. . . . . . . . . . . . 13 $/\$ $\$
148		1zzd 10992	. . . . . . . . . . . . 13 $/\$ $\$
149		fzaddel 11859	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	146, 147, 143, 148, 149	syl22anc 1293	. . . . . . . . . . . 12 $/\$ $\$
151	142	zcnd 11064	. . . . . . . . . . . . . 14 $/\$ $\$
152		ax-1cn 9615	. . . . . . . . . . . . . 14
153		npcan 9904	. . . . . . . . . . . . . 14 $/\$
154	151, 152, 153	sylancl 675	. . . . . . . . . . . . 13 $/\$ $\$
155	154	eleq1d 2533	. . . . . . . . . . . 12 $/\$ $\$
156	150, 155	bitrd 261	. . . . . . . . . . 11 $/\$ $\$
157	145, 156	mtbird 308	. . . . . . . . . 10 $/\$ $\$
158		bcval3 12529	. . . . . . . . . 10 $/\$ $/\$
159	139, 143, 157, 158	syl3anc 1292	. . . . . . . . 9 $/\$ $\$
160	159	oveq1d 6323	. . . . . . . 8 $/\$ $\$
161	140, 60	sylan2 482	. . . . . . . 8 $/\$ $\$
162	160, 161	eqtrd 2505	. . . . . . 7 $/\$ $\$
163	136, 138, 162, 64	sumss 13867	. . . . . 6
164	94, 135, 163	3eqtrd 2509	. . . . 5
165	70, 164	eqtrd 2505	. . . 4
166	69, 165	sylan9eqr 2527	. . 3 $/\$
167	68, 166	oveq12d 6326	. 2 $/\$
168	5, 16	addcld 9680	. . . . 5
169	168, 7	expp1d 12455	. . . 4
170	168, 7	expcld 12454	. . . . 5
171	170, 5, 16	adddid 9685	. . . 4
172	169, 171	eqtrd 2505	. . 3
173	172	adantr 472	. 2 $/\$
174		bcpasc 12544	. . . . . . . 8 $/\$
175	7, 8, 174	syl2an 485	. . . . . . 7 $/\$
176	175	oveq1d 6323	. . . . . 6 $/\$
177	11, 114, 48	adddird 9686	. . . . . 6 $/\$
178	176, 177	eqtr3d 2507	. . . . 5 $/\$
179	178	sumeq2dv 13846	. . . 4
180		fzfid 12224	. . . . 5
181	180, 49, 137	fsumadd 13882	. . . 4
182	179, 181	eqtrd 2505	. . 3
183	182	adantr 472	. 2 $/\$
184	167, 173, 183	3eqtr4d 2515	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376

wceq 1452

wcel 1904 $\$ cdif 3387

wss 3390

cfv 5589 (class class class)co 6308

cc 9555

cc0 9557

c1 9558

caddc 9560

cmul 9562

cmin 9880

cn 10631

cn0 10893

cz 10961

cuz 11182

cfz 11810

cexp 12310

cbc 12525

csu 13829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-oi 8043 df-card 8391 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-fz 11811 df-fzo 11943 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-sum 13830

This theorem is referenced by: binom 13965

W3C validator