Step |
Hyp |
Ref |
Expression |
1 |
|
nncn |
|- ( A e. NN -> A e. CC ) |
2 |
|
nncn |
|- ( B e. NN -> B e. CC ) |
3 |
|
ax-1cn |
|- 1 e. CC |
4 |
|
addsub |
|- ( ( A e. CC /\ B e. CC /\ 1 e. CC ) -> ( ( A + B ) - 1 ) = ( ( A - 1 ) + B ) ) |
5 |
3 4
|
mp3an3 |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - 1 ) = ( ( A - 1 ) + B ) ) |
6 |
1 2 5
|
syl2an |
|- ( ( A e. NN /\ B e. NN ) -> ( ( A + B ) - 1 ) = ( ( A - 1 ) + B ) ) |
7 |
|
nnm1nn0 |
|- ( A e. NN -> ( A - 1 ) e. NN0 ) |
8 |
|
nn0nnaddcl |
|- ( ( ( A - 1 ) e. NN0 /\ B e. NN ) -> ( ( A - 1 ) + B ) e. NN ) |
9 |
7 8
|
sylan |
|- ( ( A e. NN /\ B e. NN ) -> ( ( A - 1 ) + B ) e. NN ) |
10 |
6 9
|
eqeltrd |
|- ( ( A e. NN /\ B e. NN ) -> ( ( A + B ) - 1 ) e. NN ) |