This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcn2p1

Description: Compute the binomial coefficient " ( N + 1 ) choose 2 " from " N choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018)

Ref Expression
Assertion bcn2p1 
|- ( N e. NN0 -> ( N + ( N _C 2 ) ) = ( ( N + 1 ) _C 2 ) )

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
2 2z 
 |-  2 e. ZZ
3 bccl 
 |-  ( ( N e. NN0 /\ 2 e. ZZ ) -> ( N _C 2 ) e. NN0 )
4 2 3 mpan2 
 |-  ( N e. NN0 -> ( N _C 2 ) e. NN0 )
5 4 nn0cnd 
 |-  ( N e. NN0 -> ( N _C 2 ) e. CC )
6 1 5 addcomd 
 |-  ( N e. NN0 -> ( N + ( N _C 2 ) ) = ( ( N _C 2 ) + N ) )
7 bcn1 
 |-  ( N e. NN0 -> ( N _C 1 ) = N )
8 1e2m1 
 |-  1 = ( 2 - 1 )
9 8 a1i 
 |-  ( N e. NN0 -> 1 = ( 2 - 1 ) )
10 9 oveq2d 
 |-  ( N e. NN0 -> ( N _C 1 ) = ( N _C ( 2 - 1 ) ) )
11 7 10 eqtr3d 
 |-  ( N e. NN0 -> N = ( N _C ( 2 - 1 ) ) )
12 11 oveq2d 
 |-  ( N e. NN0 -> ( ( N _C 2 ) + N ) = ( ( N _C 2 ) + ( N _C ( 2 - 1 ) ) ) )
13 bcpasc 
 |-  ( ( N e. NN0 /\ 2 e. ZZ ) -> ( ( N _C 2 ) + ( N _C ( 2 - 1 ) ) ) = ( ( N + 1 ) _C 2 ) )
14 2 13 mpan2 
 |-  ( N e. NN0 -> ( ( N _C 2 ) + ( N _C ( 2 - 1 ) ) ) = ( ( N + 1 ) _C 2 ) )
15 6 12 14 3eqtrd 
 |-  ( N e. NN0 -> ( N + ( N _C 2 ) ) = ( ( N + 1 ) _C 2 ) )