binomlem - Metamath Proof Explorer

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

Theorem binomlem 13653

Description: Lemma for binom 13654 (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 466	. . . . 5 $/\$
3	2	oveq1d 6311	. . . 4 $/\$
4		fzfid 12086	. . . . . . 7
5		binomlem.1	. . . . . . 7
6		fzelp1 11758	. . . . . . . . 9
7		binomlem.3	. . . . . . . . . . 11
8		elfzelz 11713	. . . . . . . . . . 11
9		bccl 12403	. . . . . . . . . . 11 $/\$
10	7, 8, 9	syl2an 477	. . . . . . . . . 10 $/\$
11	10	nn0cnd 10875	. . . . . . . . 9 $/\$
12	6, 11	sylan2 474	. . . . . . . 8 $/\$
13		fznn0sub 11742	. . . . . . . . . 10
14		expcl 12187	. . . . . . . . . 10 $/\$
15	5, 13, 14	syl2an 477	. . . . . . . . 9 $/\$
16		binomlem.2	. . . . . . . . . . 11
17		elfznn0 11797	. . . . . . . . . . 11
18		expcl 12187	. . . . . . . . . . 11 $/\$
19	16, 17, 18	syl2an 477	. . . . . . . . . 10 $/\$
20	6, 19	sylan2 474	. . . . . . . . 9 $/\$
21	15, 20	mulcld 9633	. . . . . . . 8 $/\$
22	12, 21	mulcld 9633	. . . . . . 7 $/\$
23	4, 5, 22	fsummulc1 13612	. . . . . 6
24	5	adantr 465	. . . . . . . . 9 $/\$
25	12, 21, 24	mulassd 9636	. . . . . . . 8 $/\$
26	7	nn0cnd 10875	. . . . . . . . . . . . . . 15
27	26	adantr 465	. . . . . . . . . . . . . 14 $/\$
28		1cnd 9629	. . . . . . . . . . . . . 14 $/\$
29		elfzelz 11713	. . . . . . . . . . . . . . . 16
30	29	adantl 466	. . . . . . . . . . . . . . 15 $/\$
31	30	zcnd 10991	. . . . . . . . . . . . . 14 $/\$
32	27, 28, 31	addsubd 9971	. . . . . . . . . . . . 13 $/\$
33	32	oveq2d 6312	. . . . . . . . . . . 12 $/\$
34		expp1 12176	. . . . . . . . . . . . 13 $/\$
35	5, 13, 34	syl2an 477	. . . . . . . . . . . 12 $/\$
36	33, 35	eqtrd 2498	. . . . . . . . . . 11 $/\$
37	36	oveq1d 6311	. . . . . . . . . 10 $/\$
38	15, 24, 20	mul32d 9807	. . . . . . . . . 10 $/\$
39	37, 38	eqtrd 2498	. . . . . . . . 9 $/\$
40	39	oveq2d 6312	. . . . . . . 8 $/\$
41	25, 40	eqtr4d 2501	. . . . . . 7 $/\$
42	41	sumeq2dv 13537	. . . . . 6
43		fzssp1 11752	. . . . . . . 8
44	43	a1i 11	. . . . . . 7
45		fznn0sub 11742	. . . . . . . . . . 11
46		expcl 12187	. . . . . . . . . . 11 $/\$
47	5, 45, 46	syl2an 477	. . . . . . . . . 10 $/\$
48	47, 19	mulcld 9633	. . . . . . . . 9 $/\$
49	11, 48	mulcld 9633	. . . . . . . 8 $/\$
50	6, 49	sylan2 474	. . . . . . 7 $/\$
51	7	adantr 465	. . . . . . . . . 10 $/\$ $\$
52		eldifi 3622	. . . . . . . . . . . 12 $\$
53	52, 8	syl 16	. . . . . . . . . . 11 $\$
54	53	adantl 466	. . . . . . . . . 10 $/\$ $\$
55		eldifn 3623	. . . . . . . . . . 11 $\$
56	55	adantl 466	. . . . . . . . . 10 $/\$ $\$
57		bcval3 12387	. . . . . . . . . 10 $/\$ $/\$
58	51, 54, 56, 57	syl3anc 1228	. . . . . . . . 9 $/\$ $\$
59	58	oveq1d 6311	. . . . . . . 8 $/\$ $\$
60	48	mul02d 9795	. . . . . . . . 9 $/\$
61	52, 60	sylan2 474	. . . . . . . 8 $/\$ $\$
62	59, 61	eqtrd 2498	. . . . . . 7 $/\$ $\$
63		fzssuz 11750	. . . . . . . 8
64	63	a1i 11	. . . . . . 7
65	44, 50, 62, 64	sumss 13558	. . . . . 6
66	23, 42, 65	3eqtrd 2502	. . . . 5
67	66	adantr 465	. . . 4 $/\$
68	3, 67	eqtrd 2498	. . 3 $/\$
69	1	oveq1d 6311	. . . 4
70	4, 16, 22	fsummulc1 13612	. . . . 5
71		1zzd 10916	. . . . . . . 8
72		0z 10896	. . . . . . . . 9
73	72	a1i 11	. . . . . . . 8
74	7	nn0zd 10988	. . . . . . . 8
75	16	adantr 465	. . . . . . . . 9 $/\$
76	22, 75	mulcld 9633	. . . . . . . 8 $/\$
77		oveq2 6304	. . . . . . . . . 10
78		oveq2 6304	. . . . . . . . . . . 12
79	78	oveq2d 6312	. . . . . . . . . . 11
80		oveq2 6304	. . . . . . . . . . 11
81	79, 80	oveq12d 6314	. . . . . . . . . 10
82	77, 81	oveq12d 6314	. . . . . . . . 9
83	82	oveq1d 6311	. . . . . . . 8
84	71, 73, 74, 76, 83	fsumshft 13607	. . . . . . 7
85		oveq1 6303	. . . . . . . . . . 11
86	85	oveq2d 6312	. . . . . . . . . 10
87	85	oveq2d 6312	. . . . . . . . . . . 12
88	87	oveq2d 6312	. . . . . . . . . . 11
89	85	oveq2d 6312	. . . . . . . . . . 11
90	88, 89	oveq12d 6314	. . . . . . . . . 10
91	86, 90	oveq12d 6314	. . . . . . . . 9
92	91	oveq1d 6311	. . . . . . . 8
93	92	cbvsumv 13530	. . . . . . 7
94	84, 93	syl6eq 2514	. . . . . 6
95	26	adantr 465	. . . . . . . . . . . . 13 $/\$
96		elfzelz 11713	. . . . . . . . . . . . . . 15
97	96	adantl 466	. . . . . . . . . . . . . 14 $/\$
98	97	zcnd 10991	. . . . . . . . . . . . 13 $/\$
99		1cnd 9629	. . . . . . . . . . . . 13 $/\$
100	95, 98, 99	subsub3d 9980	. . . . . . . . . . . 12 $/\$
101	100	oveq2d 6312	. . . . . . . . . . 11 $/\$
102	101	oveq1d 6311	. . . . . . . . . 10 $/\$
103	102	oveq2d 6312	. . . . . . . . 9 $/\$
104	103	oveq1d 6311	. . . . . . . 8 $/\$
105		fzp1ss 11757	. . . . . . . . . . . 12
106	72, 105	ax-mp 5	. . . . . . . . . . 11
107	106	sseli 3495	. . . . . . . . . 10
108	7	adantr 465	. . . . . . . . . . . 12 $/\$
109	8	adantl 466	. . . . . . . . . . . . 13 $/\$
110		peano2zm 10928	. . . . . . . . . . . . 13
111	109, 110	syl 16	. . . . . . . . . . . 12 $/\$
112		bccl 12403	. . . . . . . . . . . 12 $/\$
113	108, 111, 112	syl2anc 661	. . . . . . . . . . 11 $/\$
114	113	nn0cnd 10875	. . . . . . . . . 10 $/\$
115	107, 114	sylan2 474	. . . . . . . . 9 $/\$
116	107, 47	sylan2 474	. . . . . . . . . 10 $/\$
117	16	adantr 465	. . . . . . . . . . 11 $/\$
118		elfznn 11739	. . . . . . . . . . . . . 14
119		0p1e1 10668	. . . . . . . . . . . . . . 15
120	119	oveq1i 6306	. . . . . . . . . . . . . 14
121	118, 120	eleq2s 2565	. . . . . . . . . . . . 13
122	121	adantl 466	. . . . . . . . . . . 12 $/\$
123		nnm1nn0 10858	. . . . . . . . . . . 12
124	122, 123	syl 16	. . . . . . . . . . 11 $/\$
125	117, 124	expcld 12313	. . . . . . . . . 10 $/\$
126	116, 125	mulcld 9633	. . . . . . . . 9 $/\$
127	115, 126, 117	mulassd 9636	. . . . . . . 8 $/\$
128	116, 125, 117	mulassd 9636	. . . . . . . . . 10 $/\$
129		expm1t 12197	. . . . . . . . . . . 12 $/\$
130	16, 121, 129	syl2an 477	. . . . . . . . . . 11 $/\$
131	130	oveq2d 6312	. . . . . . . . . 10 $/\$
132	128, 131	eqtr4d 2501	. . . . . . . . 9 $/\$
133	132	oveq2d 6312	. . . . . . . 8 $/\$
134	104, 127, 133	3eqtrd 2502	. . . . . . 7 $/\$
135	134	sumeq2dv 13537	. . . . . 6
136	106	a1i 11	. . . . . . 7
137	114, 48	mulcld 9633	. . . . . . . 8 $/\$
138	107, 137	sylan2 474	. . . . . . 7 $/\$
139	7	adantr 465	. . . . . . . . . 10 $/\$ $\$
140		eldifi 3622	. . . . . . . . . . . . 13 $\$
141	140	adantl 466	. . . . . . . . . . . 12 $/\$ $\$
142	141, 8	syl 16	. . . . . . . . . . 11 $/\$ $\$
143	142, 110	syl 16	. . . . . . . . . 10 $/\$ $\$
144		eldifn 3623	. . . . . . . . . . . 12 $\$
145	144	adantl 466	. . . . . . . . . . 11 $/\$ $\$
146	72	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
147	139	nn0zd 10988	. . . . . . . . . . . . 13 $/\$ $\$
148		1zzd 10916	. . . . . . . . . . . . 13 $/\$ $\$
149		fzaddel 11744	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	146, 147, 143, 148, 149	syl22anc 1229	. . . . . . . . . . . 12 $/\$ $\$
151	142	zcnd 10991	. . . . . . . . . . . . . 14 $/\$ $\$
152		ax-1cn 9567	. . . . . . . . . . . . . 14
153		npcan 9848	. . . . . . . . . . . . . 14 $/\$
154	151, 152, 153	sylancl 662	. . . . . . . . . . . . 13 $/\$ $\$
155	154	eleq1d 2526	. . . . . . . . . . . 12 $/\$ $\$
156	150, 155	bitrd 253	. . . . . . . . . . 11 $/\$ $\$
157	145, 156	mtbird 301	. . . . . . . . . 10 $/\$ $\$
158		bcval3 12387	. . . . . . . . . 10 $/\$ $/\$
159	139, 143, 157, 158	syl3anc 1228	. . . . . . . . 9 $/\$ $\$
160	159	oveq1d 6311	. . . . . . . 8 $/\$ $\$
161	140, 60	sylan2 474	. . . . . . . 8 $/\$ $\$
162	160, 161	eqtrd 2498	. . . . . . 7 $/\$ $\$
163	136, 138, 162, 64	sumss 13558	. . . . . 6
164	94, 135, 163	3eqtrd 2502	. . . . 5
165	70, 164	eqtrd 2498	. . . 4
166	69, 165	sylan9eqr 2520	. . 3 $/\$
167	68, 166	oveq12d 6314	. 2 $/\$
168	5, 16	addcld 9632	. . . . 5
169	168, 7	expp1d 12314	. . . 4
170	168, 7	expcld 12313	. . . . 5
171	170, 5, 16	adddid 9637	. . . 4
172	169, 171	eqtrd 2498	. . 3
173	172	adantr 465	. 2 $/\$
174		bcpasc 12402	. . . . . . . 8 $/\$
175	7, 8, 174	syl2an 477	. . . . . . 7 $/\$
176	175	oveq1d 6311	. . . . . 6 $/\$
177	11, 114, 48	adddird 9638	. . . . . 6 $/\$
178	176, 177	eqtr3d 2500	. . . . 5 $/\$
179	178	sumeq2dv 13537	. . . 4
180		fzfid 12086	. . . . 5
181	180, 49, 137	fsumadd 13573	. . . 4
182	179, 181	eqtrd 2498	. . 3
183	182	adantr 465	. 2 $/\$
184	167, 173, 183	3eqtr4d 2508	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1395

wcel 1819 $\$ cdif 3468

wss 3471

cfv 5594 (class class class)co 6296

cc 9507

cc0 9509

c1 9510

caddc 9512

cmul 9514

cmin 9824

cn 10556

cn0 10816

cz 10885

cuz 11106

cfz 11697

cexp 12169

cbc 12383

csu 13520

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11822 df-seq 12111 df-exp 12170 df-fac 12357 df-bc 12384 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-sum 13521

This theorem is referenced by: binom 13654

W3C validator