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 ) ) |