binomlem - Metamath Proof Explorer

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

Theorem binomlem 13275

Description: Lemma for binom 13276 (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 463	. . . . 5 $/\$
3	2	oveq1d 6095	. . . 4 $/\$
4		fzfid 11779	. . . . . . 7
5		binomlem.1	. . . . . . 7
6		fzelp1 11492	. . . . . . . . 9
7		binomlem.3	. . . . . . . . . . 11
8		elfzelz 11440	. . . . . . . . . . 11
9		bccl 12082	. . . . . . . . . . 11 $/\$
10	7, 8, 9	syl2an 474	. . . . . . . . . 10 $/\$
11	10	nn0cnd 10626	. . . . . . . . 9 $/\$
12	6, 11	sylan2 471	. . . . . . . 8 $/\$
13		fznn0sub 11474	. . . . . . . . . 10
14		expcl 11867	. . . . . . . . . 10 $/\$
15	5, 13, 14	syl2an 474	. . . . . . . . 9 $/\$
16		binomlem.2	. . . . . . . . . . 11
17		elfznn0 11468	. . . . . . . . . . 11
18		expcl 11867	. . . . . . . . . . 11 $/\$
19	16, 17, 18	syl2an 474	. . . . . . . . . 10 $/\$
20	6, 19	sylan2 471	. . . . . . . . 9 $/\$
21	15, 20	mulcld 9394	. . . . . . . 8 $/\$
22	12, 21	mulcld 9394	. . . . . . 7 $/\$
23	4, 5, 22	fsummulc1 13235	. . . . . 6
24	5	adantr 462	. . . . . . . . 9 $/\$
25	12, 21, 24	mulassd 9397	. . . . . . . 8 $/\$
26	7	nn0cnd 10626	. . . . . . . . . . . . . . 15
27	26	adantr 462	. . . . . . . . . . . . . 14 $/\$
28		1cnd 9390	. . . . . . . . . . . . . 14 $/\$
29		elfzelz 11440	. . . . . . . . . . . . . . . 16
30	29	adantl 463	. . . . . . . . . . . . . . 15 $/\$
31	30	zcnd 10736	. . . . . . . . . . . . . 14 $/\$
32	27, 28, 31	addsubd 9728	. . . . . . . . . . . . 13 $/\$
33	32	oveq2d 6096	. . . . . . . . . . . 12 $/\$
34		expp1 11856	. . . . . . . . . . . . 13 $/\$
35	5, 13, 34	syl2an 474	. . . . . . . . . . . 12 $/\$
36	33, 35	eqtrd 2465	. . . . . . . . . . 11 $/\$
37	36	oveq1d 6095	. . . . . . . . . 10 $/\$
38	15, 24, 20	mul32d 9567	. . . . . . . . . 10 $/\$
39	37, 38	eqtrd 2465	. . . . . . . . 9 $/\$
40	39	oveq2d 6096	. . . . . . . 8 $/\$
41	25, 40	eqtr4d 2468	. . . . . . 7 $/\$
42	41	sumeq2dv 13164	. . . . . 6
43		fzssp1 11488	. . . . . . . 8
44	43	a1i 11	. . . . . . 7
45		fznn0sub 11474	. . . . . . . . . . 11
46		expcl 11867	. . . . . . . . . . 11 $/\$
47	5, 45, 46	syl2an 474	. . . . . . . . . 10 $/\$
48	47, 19	mulcld 9394	. . . . . . . . 9 $/\$
49	11, 48	mulcld 9394	. . . . . . . 8 $/\$
50	6, 49	sylan2 471	. . . . . . 7 $/\$
51	7	adantr 462	. . . . . . . . . 10 $/\$ $\$
52		eldifi 3466	. . . . . . . . . . . 12 $\$
53	52, 8	syl 16	. . . . . . . . . . 11 $\$
54	53	adantl 463	. . . . . . . . . 10 $/\$ $\$
55		eldifn 3467	. . . . . . . . . . 11 $\$
56	55	adantl 463	. . . . . . . . . 10 $/\$ $\$
57		bcval3 12066	. . . . . . . . . 10 $/\$ $/\$
58	51, 54, 56, 57	syl3anc 1211	. . . . . . . . 9 $/\$ $\$
59	58	oveq1d 6095	. . . . . . . 8 $/\$ $\$
60	48	mul02d 9555	. . . . . . . . 9 $/\$
61	52, 60	sylan2 471	. . . . . . . 8 $/\$ $\$
62	59, 61	eqtrd 2465	. . . . . . 7 $/\$ $\$
63		fzssuz 11486	. . . . . . . 8
64	63	a1i 11	. . . . . . 7
65	44, 50, 62, 64	sumss 13185	. . . . . 6
66	23, 42, 65	3eqtrd 2469	. . . . 5
67	66	adantr 462	. . . 4 $/\$
68	3, 67	eqtrd 2465	. . 3 $/\$
69	1	oveq1d 6095	. . . 4
70	4, 16, 22	fsummulc1 13235	. . . . 5
71		1zzd 10665	. . . . . . . 8
72		0z 10645	. . . . . . . . 9
73	72	a1i 11	. . . . . . . 8
74	7	nn0zd 10733	. . . . . . . 8
75	16	adantr 462	. . . . . . . . 9 $/\$
76	22, 75	mulcld 9394	. . . . . . . 8 $/\$
77		oveq2 6088	. . . . . . . . . 10
78		oveq2 6088	. . . . . . . . . . . 12
79	78	oveq2d 6096	. . . . . . . . . . 11
80		oveq2 6088	. . . . . . . . . . 11
81	79, 80	oveq12d 6098	. . . . . . . . . 10
82	77, 81	oveq12d 6098	. . . . . . . . 9
83	82	oveq1d 6095	. . . . . . . 8
84	71, 73, 74, 76, 83	fsumshft 13230	. . . . . . 7
85		oveq1 6087	. . . . . . . . . . 11
86	85	oveq2d 6096	. . . . . . . . . 10
87	85	oveq2d 6096	. . . . . . . . . . . 12
88	87	oveq2d 6096	. . . . . . . . . . 11
89	85	oveq2d 6096	. . . . . . . . . . 11
90	88, 89	oveq12d 6098	. . . . . . . . . 10
91	86, 90	oveq12d 6098	. . . . . . . . 9
92	91	oveq1d 6095	. . . . . . . 8
93	92	cbvsumv 13157	. . . . . . 7
94	84, 93	syl6eq 2481	. . . . . 6
95	26	adantr 462	. . . . . . . . . . . . 13 $/\$
96		elfzelz 11440	. . . . . . . . . . . . . . 15
97	96	adantl 463	. . . . . . . . . . . . . 14 $/\$
98	97	zcnd 10736	. . . . . . . . . . . . 13 $/\$
99		1cnd 9390	. . . . . . . . . . . . 13 $/\$
100	95, 98, 99	subsub3d 9737	. . . . . . . . . . . 12 $/\$
101	100	oveq2d 6096	. . . . . . . . . . 11 $/\$
102	101	oveq1d 6095	. . . . . . . . . 10 $/\$
103	102	oveq2d 6096	. . . . . . . . 9 $/\$
104	103	oveq1d 6095	. . . . . . . 8 $/\$
105		fzp1ss 11491	. . . . . . . . . . . 12
106	72, 105	ax-mp 5	. . . . . . . . . . 11
107	106	sseli 3340	. . . . . . . . . 10
108	7	adantr 462	. . . . . . . . . . . 12 $/\$
109	8	adantl 463	. . . . . . . . . . . . 13 $/\$
110		peano2zm 10676	. . . . . . . . . . . . 13
111	109, 110	syl 16	. . . . . . . . . . . 12 $/\$
112		bccl 12082	. . . . . . . . . . . 12 $/\$
113	108, 111, 112	syl2anc 654	. . . . . . . . . . 11 $/\$
114	113	nn0cnd 10626	. . . . . . . . . 10 $/\$
115	107, 114	sylan2 471	. . . . . . . . 9 $/\$
116	107, 47	sylan2 471	. . . . . . . . . 10 $/\$
117	16	adantr 462	. . . . . . . . . . 11 $/\$
118		elfznn 11465	. . . . . . . . . . . . . 14
119		0p1e1 10421	. . . . . . . . . . . . . . 15
120	119	oveq1i 6090	. . . . . . . . . . . . . 14
121	118, 120	eleq2s 2525	. . . . . . . . . . . . 13
122	121	adantl 463	. . . . . . . . . . . 12 $/\$
123		nnm1nn0 10609	. . . . . . . . . . . 12
124	122, 123	syl 16	. . . . . . . . . . 11 $/\$
125	117, 124	expcld 11992	. . . . . . . . . 10 $/\$
126	116, 125	mulcld 9394	. . . . . . . . 9 $/\$
127	115, 126, 117	mulassd 9397	. . . . . . . 8 $/\$
128	116, 125, 117	mulassd 9397	. . . . . . . . . 10 $/\$
129		expm1t 11876	. . . . . . . . . . . 12 $/\$
130	16, 121, 129	syl2an 474	. . . . . . . . . . 11 $/\$
131	130	oveq2d 6096	. . . . . . . . . 10 $/\$
132	128, 131	eqtr4d 2468	. . . . . . . . 9 $/\$
133	132	oveq2d 6096	. . . . . . . 8 $/\$
134	104, 127, 133	3eqtrd 2469	. . . . . . 7 $/\$
135	134	sumeq2dv 13164	. . . . . 6
136	106	a1i 11	. . . . . . 7
137	114, 48	mulcld 9394	. . . . . . . 8 $/\$
138	107, 137	sylan2 471	. . . . . . 7 $/\$
139	7	adantr 462	. . . . . . . . . 10 $/\$ $\$
140		eldifi 3466	. . . . . . . . . . . . 13 $\$
141	140	adantl 463	. . . . . . . . . . . 12 $/\$ $\$
142	141, 8	syl 16	. . . . . . . . . . 11 $/\$ $\$
143	142, 110	syl 16	. . . . . . . . . 10 $/\$ $\$
144		eldifn 3467	. . . . . . . . . . . 12 $\$
145	144	adantl 463	. . . . . . . . . . 11 $/\$ $\$
146	72	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
147	139	nn0zd 10733	. . . . . . . . . . . . 13 $/\$ $\$
148		1zzd 10665	. . . . . . . . . . . . 13 $/\$ $\$
149		fzaddel 11480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	146, 147, 143, 148, 149	syl22anc 1212	. . . . . . . . . . . 12 $/\$ $\$
151	142	zcnd 10736	. . . . . . . . . . . . . 14 $/\$ $\$
152		ax-1cn 9328	. . . . . . . . . . . . . 14
153		npcan 9607	. . . . . . . . . . . . . 14 $/\$
154	151, 152, 153	sylancl 655	. . . . . . . . . . . . 13 $/\$ $\$
155	154	eleq1d 2499	. . . . . . . . . . . 12 $/\$ $\$
156	150, 155	bitrd 253	. . . . . . . . . . 11 $/\$ $\$
157	145, 156	mtbird 301	. . . . . . . . . 10 $/\$ $\$
158		bcval3 12066	. . . . . . . . . 10 $/\$ $/\$
159	139, 143, 157, 158	syl3anc 1211	. . . . . . . . 9 $/\$ $\$
160	159	oveq1d 6095	. . . . . . . 8 $/\$ $\$
161	140, 60	sylan2 471	. . . . . . . 8 $/\$ $\$
162	160, 161	eqtrd 2465	. . . . . . 7 $/\$ $\$
163	136, 138, 162, 64	sumss 13185	. . . . . 6
164	94, 135, 163	3eqtrd 2469	. . . . 5
165	70, 164	eqtrd 2465	. . . 4
166	69, 165	sylan9eqr 2487	. . 3 $/\$
167	68, 166	oveq12d 6098	. 2 $/\$
168	5, 16	addcld 9393	. . . . 5
169	168, 7	expp1d 11993	. . . 4
170	168, 7	expcld 11992	. . . . 5
171	170, 5, 16	adddid 9398	. . . 4
172	169, 171	eqtrd 2465	. . 3
173	172	adantr 462	. 2 $/\$
174		bcpasc 12081	. . . . . . . 8 $/\$
175	7, 8, 174	syl2an 474	. . . . . . 7 $/\$
176	175	oveq1d 6095	. . . . . 6 $/\$
177	11, 114, 48	adddird 9399	. . . . . 6 $/\$
178	176, 177	eqtr3d 2467	. . . . 5 $/\$
179	178	sumeq2dv 13164	. . . 4
180		fzfid 11779	. . . . 5
181	180, 49, 137	fsumadd 13199	. . . 4
182	179, 181	eqtrd 2465	. . 3
183	182	adantr 462	. 2 $/\$
184	167, 173, 183	3eqtr4d 2475	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1362

wcel 1755 $\$ cdif 3313

wss 3316

cfv 5406 (class class class)co 6080

cc 9268

cc0 9270

c1 9271

caddc 9273

cmul 9275

cmin 9583

cn 10310

cn0 10567

cz 10634

cuz 10849

cfz 11424

cexp 11849

cbc 12062

csu 13147

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-oadd 6912 df-er 7089 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-sup 7679 df-oi 7712 df-card 8097 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-n0 10568 df-z 10635 df-uz 10850 df-rp 10980 df-fz 11425 df-fzo 11533 df-seq 11791 df-exp 11850 df-fac 12036 df-bc 12063 df-hash 12088 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-clim 12950 df-sum 13148

This theorem is referenced by: binom 13276

W3C validator