Description: Special case of binom2 where B = 1 . (Contributed by Scott Fenton, 11-May-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | binom21 | |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1cn | |
|
| 2 | binom2 | |
|
| 3 | 1 2 | mpan2 | |
| 4 | mulrid | |
|
| 5 | 4 | oveq2d | |
| 6 | 5 | oveq2d | |
| 7 | sq1 | |
|
| 8 | 7 | a1i | |
| 9 | 6 8 | oveq12d | |
| 10 | 3 9 | eqtrd | |