Step |
Hyp |
Ref |
Expression |
1 |
|
elnn0 |
|- ( B e. NN0 <-> ( B e. NN \/ B = 0 ) ) |
2 |
|
elnn0 |
|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) ) |
3 |
|
nnaddcom |
|- ( ( A e. NN /\ B e. NN ) -> ( A + B ) = ( B + A ) ) |
4 |
|
nnre |
|- ( B e. NN -> B e. RR ) |
5 |
|
readdlid |
|- ( B e. RR -> ( 0 + B ) = B ) |
6 |
|
readdrid |
|- ( B e. RR -> ( B + 0 ) = B ) |
7 |
5 6
|
eqtr4d |
|- ( B e. RR -> ( 0 + B ) = ( B + 0 ) ) |
8 |
4 7
|
syl |
|- ( B e. NN -> ( 0 + B ) = ( B + 0 ) ) |
9 |
|
oveq1 |
|- ( A = 0 -> ( A + B ) = ( 0 + B ) ) |
10 |
|
oveq2 |
|- ( A = 0 -> ( B + A ) = ( B + 0 ) ) |
11 |
9 10
|
eqeq12d |
|- ( A = 0 -> ( ( A + B ) = ( B + A ) <-> ( 0 + B ) = ( B + 0 ) ) ) |
12 |
8 11
|
syl5ibrcom |
|- ( B e. NN -> ( A = 0 -> ( A + B ) = ( B + A ) ) ) |
13 |
12
|
impcom |
|- ( ( A = 0 /\ B e. NN ) -> ( A + B ) = ( B + A ) ) |
14 |
3 13
|
jaoian |
|- ( ( ( A e. NN \/ A = 0 ) /\ B e. NN ) -> ( A + B ) = ( B + A ) ) |
15 |
2 14
|
sylanb |
|- ( ( A e. NN0 /\ B e. NN ) -> ( A + B ) = ( B + A ) ) |
16 |
|
nn0re |
|- ( A e. NN0 -> A e. RR ) |
17 |
|
readdrid |
|- ( A e. RR -> ( A + 0 ) = A ) |
18 |
|
readdlid |
|- ( A e. RR -> ( 0 + A ) = A ) |
19 |
17 18
|
eqtr4d |
|- ( A e. RR -> ( A + 0 ) = ( 0 + A ) ) |
20 |
16 19
|
syl |
|- ( A e. NN0 -> ( A + 0 ) = ( 0 + A ) ) |
21 |
|
oveq2 |
|- ( B = 0 -> ( A + B ) = ( A + 0 ) ) |
22 |
|
oveq1 |
|- ( B = 0 -> ( B + A ) = ( 0 + A ) ) |
23 |
21 22
|
eqeq12d |
|- ( B = 0 -> ( ( A + B ) = ( B + A ) <-> ( A + 0 ) = ( 0 + A ) ) ) |
24 |
20 23
|
syl5ibrcom |
|- ( A e. NN0 -> ( B = 0 -> ( A + B ) = ( B + A ) ) ) |
25 |
24
|
imp |
|- ( ( A e. NN0 /\ B = 0 ) -> ( A + B ) = ( B + A ) ) |
26 |
15 25
|
jaodan |
|- ( ( A e. NN0 /\ ( B e. NN \/ B = 0 ) ) -> ( A + B ) = ( B + A ) ) |
27 |
1 26
|
sylan2b |
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) = ( B + A ) ) |