![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > bcval5 | Unicode version |
Description: Write out the top and
bottom parts of the binomial coefficient
( N ) = ( N ( N 1 ) ( ( N ) 1 ) )
explicitly. In this form, it is valid even for , although it
is no longer valid for nonpositive . (Contributed by Mario
Carneiro, 22-May-2014.) |
Ref | Expression |
---|---|
bcval5 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bcval2 12383 | . . . 4 | |
2 | 1 | adantl 466 | . . 3 |
3 | mulcl 9597 | . . . . . . . . 9 | |
4 | 3 | adantl 466 | . . . . . . . 8 |
5 | mulass 9601 | . . . . . . . . 9 | |
6 | 5 | adantl 466 | . . . . . . . 8 |
7 | simplr 755 | . . . . . . . . . . . . 13 | |
8 | elfzuz3 11714 | . . . . . . . . . . . . . 14 | |
9 | 8 | adantl 466 | . . . . . . . . . . . . 13 |
10 | eluznn 11181 | . . . . . . . . . . . . 13 | |
11 | 7, 9, 10 | syl2anc 661 | . . . . . . . . . . . 12 |
12 | 11 | adantrr 716 | . . . . . . . . . . 11 |
13 | simplr 755 | . . . . . . . . . . 11 | |
14 | nnre 10568 | . . . . . . . . . . . 12 | |
15 | nnrp 11258 | . . . . . . . . . . . 12 | |
16 | ltsubrp 11280 | . . . . . . . . . . . 12 | |
17 | 14, 15, 16 | syl2an 477 | . . . . . . . . . . 11 |
18 | 12, 13, 17 | syl2anc 661 | . . . . . . . . . 10 |
19 | 12 | nnzd 10993 | . . . . . . . . . . . 12 |
20 | nnz 10911 | . . . . . . . . . . . . 13 | |
21 | 20 | ad2antlr 726 | . . . . . . . . . . . 12 |
22 | 19, 21 | zsubcld 10999 | . . . . . . . . . . 11 |
23 | zltp1le 10938 | . . . . . . . . . . 11 | |
24 | 22, 19, 23 | syl2anc 661 | . . . . . . . . . 10 |
25 | 18, 24 | mpbid 210 | . . . . . . . . 9 |
26 | 22 | peano2zd 10997 | . . . . . . . . . 10 |
27 | eluz 11123 | . . . . . . . . . 10 | |
28 | 26, 19, 27 | syl2anc 661 | . . . . . . . . 9 |
29 | 25, 28 | mpbird 232 | . . . . . . . 8 |
30 | simprr 757 | . . . . . . . . 9 | |
31 | nnuz 11145 | . . . . . . . . 9 | |
32 | 30, 31 | syl6eleq 2555 | . . . . . . . 8 |
33 | fvi 5930 | . . . . . . . . . 10 | |
34 | elfzelz 11717 | . . . . . . . . . . 11 | |
35 | 34 | zcnd 10995 | . . . . . . . . . 10 |
36 | 33, 35 | eqeltrd 2545 | . . . . . . . . 9 |
37 | 36 | adantl 466 | . . . . . . . 8 |
38 | 4, 6, 29, 32, 37 | seqsplit 12140 | . . . . . . 7 |
39 | facnn 12355 | . . . . . . . 8 | |
40 | 12, 39 | syl 16 | . . . . . . 7 |
41 | facnn 12355 | . . . . . . . . 9 | |
42 | 30, 41 | syl 16 | . . . . . . . 8 |
43 | 42 | oveq1d 6311 | . . . . . . 7 |
44 | 38, 40, 43 | 3eqtr4d 2508 | . . . . . 6 |
45 | 44 | expr 615 | . . . . 5 |
46 | simpll 753 | . . . . . . . . 9 | |
47 | faccl 12363 | . . . . . . . . 9 | |
48 | nncn 10569 | . . . . . . . . 9 | |
49 | 46, 47, 48 | 3syl 20 | . . . . . . . 8 |
50 | 49 | mulid2d 9635 | . . . . . . 7 |
51 | 11, 39 | syl 16 | . . . . . . . 8 |
52 | 51 | oveq2d 6312 | . . . . . . 7 |
53 | 50, 52 | eqtr3d 2500 | . . . . . 6 |
54 | fveq2 5871 | . . . . . . . . 9 | |
55 | fac0 12356 | . . . . . . . . 9 | |
56 | 54, 55 | syl6eq 2514 | . . . . . . . 8 |
57 | oveq1 6303 | . . . . . . . . . . 11 | |
58 | 0p1e1 10672 | . . . . . . . . . . 11 | |
59 | 57, 58 | syl6eq 2514 | . . . . . . . . . 10 |
60 | 59 | seqeq1d 12113 | . . . . . . . . 9 |
61 | 60 | fveq1d 5873 | . . . . . . . 8 |
62 | 56, 61 | oveq12d 6314 | . . . . . . 7 |
63 | 62 | eqeq2d 2471 | . . . . . 6 |
64 | 53, 63 | syl5ibrcom 222 | . . . . 5 |
65 | fznn0sub 11745 | . . . . . . 7 | |
66 | 65 | adantl 466 | . . . . . 6 |
67 | elnn0 10822 | . . . . . 6 | |
68 | 66, 67 | sylib 196 | . . . . 5 |
69 | 45, 64, 68 | mpjaod 381 | . . . 4 |
70 | 69 | oveq1d 6311 | . . 3 |
71 | eqid 2457 | . . . . . 6 | |
72 | nn0z 10912 | . . . . . . . . 9 | |
73 | zsubcl 10931 | . . . . . . . . 9 | |
74 | 72, 20, 73 | syl2an 477 | . . . . . . . 8 |
75 | 74 | peano2zd 10997 | . . . . . . 7 |
76 | 75 | adantr 465 | . . . . . 6 |
77 | fvi 5930 | . . . . . . . 8 | |
78 | eluzelcn 11121 | . . . . . . . 8 | |
79 | 77, 78 | eqeltrd 2545 | . . . . . . 7 |
80 | 79 | adantl 466 | . . . . . 6 |
81 | 3 | adantl 466 | . . . . . 6 |
82 | 71, 76, 80, 81 | seqf 12128 | . . . . 5 |
83 | 11, 7, 17 | syl2anc 661 | . . . . . . 7 |
84 | 74 | adantr 465 | . . . . . . . 8 |
85 | 11 | nnzd 10993 | . . . . . . . 8 |
86 | 84, 85, 23 | syl2anc 661 | . . . . . . 7 |
87 | 83, 86 | mpbid 210 | . . . . . 6 |
88 | 76, 85, 27 | syl2anc 661 | . . . . . 6 |
89 | 87, 88 | mpbird 232 | . . . . 5 |
90 | 82, 89 | ffvelrnd 6032 | . . . 4 |
91 | elfznn0 11800 | . . . . . . 7 | |
92 | 91 | adantl 466 | . . . . . 6 |
93 | faccl 12363 | . . . . . 6 | |
94 | 92, 93 | syl 16 | . . . . 5 |
95 | 94 | nncnd 10577 | . . . 4 |
96 | faccl 12363 | . . . . . 6 | |
97 | 66, 96 | syl 16 | . . . . 5 |
98 | 97 | nncnd 10577 | . . . 4 |
99 | 94 | nnne0d 10605 | . . . 4 |
100 | 97 | nnne0d 10605 | . . . 4 |
101 | 90, 95, 98, 99, 100 | divcan5d 10371 | . . 3 |
102 | 2, 70, 101 | 3eqtrd 2502 | . 2 |
103 | nnnn0 10827 | . . . . 5 | |
104 | 103 | ad2antlr 726 | . . . 4 |
105 | nncn 10569 | . . . . 5 | |
106 | nnne0 10593 | . . . . 5 | |
107 | 105, 106 | div0d 10344 | . . . 4 |
108 | 104, 93, 107 | 3syl 20 | . . 3 |
109 | 3 | adantl 466 | . . . . 5 |
110 | fvi 5930 | . . . . . . 7 | |
111 | elfzelz 11717 | . . . . . . . 8 | |
112 | 111 | zcnd 10995 | . . . . . . 7 |
113 | 110, 112 | eqeltrd 2545 | . . . . . 6 |
114 | 113 | adantl 466 | . . . . 5 |
115 | mul02 9779 | . . . . . 6 | |
116 | 115 | adantl 466 | . . . . 5 |
117 | mul01 9780 | . . . . . 6 | |
118 | 117 | adantl 466 | . . . . 5 |
119 | simpr 461 | . . . . . . . . 9 | |
120 | nn0uz 11144 | . . . . . . . . . . . 12 | |
121 | 104, 120 | syl6eleq 2555 | . . . . . . . . . . 11 |
122 | 72 | ad2antrr 725 | . . . . . . . . . . 11 |
123 | elfz5 11709 | . . . . . . . . . . 11 | |
124 | 121, 122, 123 | syl2anc 661 | . . . . . . . . . 10 |
125 | nn0re 10829 | . . . . . . . . . . . 12 | |
126 | 125 | ad2antrr 725 | . . . . . . . . . . 11 |
127 | nnre 10568 | . . . . . . . . . . . 12 | |
128 | 127 | ad2antlr 726 | . . . . . . . . . . 11 |
129 | 126, 128 | subge0d 10167 | . . . . . . . . . 10 |
130 | 124, 129 | bitr4d 256 | . . . . . . . . 9 |
131 | 119, 130 | mtbid 300 | . . . . . . . 8 |
132 | 74 | adantr 465 | . . . . . . . . . 10 |
133 | 132 | zred 10994 | . . . . . . . . 9 |
134 | 0re 9617 | . . . . . . . . 9 | |
135 | ltnle 9685 | . . . . . . . . 9 | |
136 | 133, 134, 135 | sylancl 662 | . . . . . . . 8 |
137 | 131, 136 | mpbird 232 | . . . . . . 7 |
138 | 0z 10900 | . . . . . . . 8 | |
139 | zltp1le 10938 | . . . . . . . 8 | |
140 | 132, 138, 139 | sylancl 662 | . . . . . . 7 |
141 | 137, 140 | mpbid 210 | . . . . . 6 |
142 | nn0ge0 10846 | . . . . . . 7 | |
143 | 142 | ad2antrr 725 | . . . . . 6 |
144 | 0zd 10901 | . . . . . . 7 | |
145 | 75 | adantr 465 | . . . . . . 7 |
146 | elfz 11707 | . . . . . . 7 | |
147 | 144, 145, 122, 146 | syl3anc 1228 | . . . . . 6 |
148 | 141, 143, 147 | mpbir2and 922 | . . . . 5 |
149 | simpll 753 | . . . . 5 | |
150 | 0cn 9609 | . . . . . 6 | |
151 | fvi 5930 | . . . . . 6 | |
152 | 150, 151 | mp1i 12 | . . . . 5 |
153 | 109, 114, 116, 118, 148, 149, 152 | seqz 12155 | . . . 4 |
154 | 153 | oveq1d 6311 | . . 3 |
155 | bcval3 12384 | . . . . 5 | |
156 | 20, 155 | syl3an2 1262 | . . . 4 |
157 | 156 | 3expa 1196 | . . 3 |
158 | 108, 154, 157 | 3eqtr4rd 2509 | . 2 |
159 | 102, 158 | pm2.61dan 791 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4
<-> wb 184 \/ wo 368 /\ wa 369
/\ w3a 973 = wceq 1395 e. wcel 1818
class class class wbr 4452 cid 4795
` cfv 5593 (class class class)co 6296
cc 9511 cr 9512 0 cc0 9513 1 c1 9514
caddc 9516 cmul 9518 clt 9649 cle 9650 cmin 9828 cdiv 10231 cn 10561 cn0 10820
cz 10889 cuz 11110
crp 11249
cfz 11701 seq cseq 12107 cfa 12353 cbc 12380 |
This theorem is referenced by: bcn2 12397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-8 1820 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-sep 4573 ax-nul 4581 ax-pow 4630 ax-pr 4691 ax-un 6592 ax-cnex 9569 ax-resscn 9570 ax-1cn 9571 ax-icn 9572 ax-addcl 9573 ax-addrcl 9574 ax-mulcl 9575 ax-mulrcl 9576 ax-mulcom 9577 ax-addass 9578 ax-mulass 9579 ax-distr 9580 ax-i2m1 9581 ax-1ne0 9582 ax-1rid 9583 ax-rnegex 9584 ax-rrecex 9585 ax-cnre 9586 ax-pre-lttri 9587 ax-pre-lttrn 9588 ax-pre-ltadd 9589 ax-pre-mulgt0 9590 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 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 3435 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-pss 3491 df-nul 3785 df-if 3942 df-pw 4014 df-sn 4030 df-pr 4032 df-tp 4034 df-op 4036 df-uni 4250 df-iun 4332 df-br 4453 df-opab 4511 df-mpt 4512 df-tr 4546 df-eprel 4796 df-id 4800 df-po 4805 df-so 4806 df-fr 4843 df-we 4845 df-ord 4886 df-on 4887 df-lim 4888 df-suc 4889 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-riota 6257 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6701 df-1st 6800 df-2nd 6801 df-recs 7061 df-rdg 7095 df-er 7330 df-en 7537 df-dom 7538 df-sdom 7539 df-pnf 9651 df-mnf 9652 df-xr 9653 df-ltxr 9654 df-le 9655 df-sub 9830 df-neg 9831 df-div 10232 df-nn 10562 df-n0 10821 df-z 10890 df-uz 11111 df-rp 11250 df-fz 11702 df-seq 12108 df-fac 12354 df-bc 12381 |
Copyright terms: Public domain | W3C validator |