Step |
Hyp |
Ref |
Expression |
1 |
|
reelznn0nn |
|- ( A e. ZZ <-> ( A e. NN0 \/ ( A e. RR /\ ( 0 -R A ) e. NN ) ) ) |
2 |
|
reelznn0nn |
|- ( B e. ZZ <-> ( B e. NN0 \/ ( B e. RR /\ ( 0 -R B ) e. NN ) ) ) |
3 |
|
nn0addcom |
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) = ( B + A ) ) |
4 |
|
zaddcomlem |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( A + B ) = ( B + A ) ) |
5 |
|
zaddcomlem |
|- ( ( ( B e. RR /\ ( 0 -R B ) e. NN ) /\ A e. NN0 ) -> ( B + A ) = ( A + B ) ) |
6 |
5
|
eqcomd |
|- ( ( ( B e. RR /\ ( 0 -R B ) e. NN ) /\ A e. NN0 ) -> ( A + B ) = ( B + A ) ) |
7 |
6
|
ancoms |
|- ( ( A e. NN0 /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( A + B ) = ( B + A ) ) |
8 |
|
renegid2 |
|- ( B e. RR -> ( ( 0 -R B ) + B ) = 0 ) |
9 |
8
|
ad2antrl |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R B ) + B ) = 0 ) |
10 |
|
renegid2 |
|- ( A e. RR -> ( ( 0 -R A ) + A ) = 0 ) |
11 |
10
|
ad2antrr |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R A ) + A ) = 0 ) |
12 |
11
|
oveq1d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R A ) + A ) + B ) = ( 0 + B ) ) |
13 |
|
simplr |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( 0 -R A ) e. NN ) |
14 |
13
|
nncnd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( 0 -R A ) e. CC ) |
15 |
|
simpll |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> A e. RR ) |
16 |
15
|
recnd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> A e. CC ) |
17 |
|
simprl |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> B e. RR ) |
18 |
17
|
recnd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> B e. CC ) |
19 |
14 16 18
|
addassd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R A ) + A ) + B ) = ( ( 0 -R A ) + ( A + B ) ) ) |
20 |
|
readdlid |
|- ( B e. RR -> ( 0 + B ) = B ) |
21 |
20
|
ad2antrl |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( 0 + B ) = B ) |
22 |
12 19 21
|
3eqtr3d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R A ) + ( A + B ) ) = B ) |
23 |
22
|
oveq2d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R B ) + ( ( 0 -R A ) + ( A + B ) ) ) = ( ( 0 -R B ) + B ) ) |
24 |
9 23 11
|
3eqtr4d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R B ) + ( ( 0 -R A ) + ( A + B ) ) ) = ( ( 0 -R A ) + A ) ) |
25 |
|
simprr |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( 0 -R B ) e. NN ) |
26 |
25
|
nncnd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( 0 -R B ) e. CC ) |
27 |
16 18
|
addcld |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( A + B ) e. CC ) |
28 |
26 14 27
|
addassd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R B ) + ( 0 -R A ) ) + ( A + B ) ) = ( ( 0 -R B ) + ( ( 0 -R A ) + ( A + B ) ) ) ) |
29 |
9
|
oveq1d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R B ) + B ) + A ) = ( 0 + A ) ) |
30 |
26 18 16
|
addassd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R B ) + B ) + A ) = ( ( 0 -R B ) + ( B + A ) ) ) |
31 |
|
readdlid |
|- ( A e. RR -> ( 0 + A ) = A ) |
32 |
31
|
ad2antrr |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( 0 + A ) = A ) |
33 |
29 30 32
|
3eqtr3d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R B ) + ( B + A ) ) = A ) |
34 |
33
|
oveq2d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R A ) + ( ( 0 -R B ) + ( B + A ) ) ) = ( ( 0 -R A ) + A ) ) |
35 |
24 28 34
|
3eqtr4d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R B ) + ( 0 -R A ) ) + ( A + B ) ) = ( ( 0 -R A ) + ( ( 0 -R B ) + ( B + A ) ) ) ) |
36 |
|
nnaddcom |
|- ( ( ( 0 -R A ) e. NN /\ ( 0 -R B ) e. NN ) -> ( ( 0 -R A ) + ( 0 -R B ) ) = ( ( 0 -R B ) + ( 0 -R A ) ) ) |
37 |
36
|
ad2ant2l |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R A ) + ( 0 -R B ) ) = ( ( 0 -R B ) + ( 0 -R A ) ) ) |
38 |
37
|
oveq1d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R A ) + ( 0 -R B ) ) + ( A + B ) ) = ( ( ( 0 -R B ) + ( 0 -R A ) ) + ( A + B ) ) ) |
39 |
18 16
|
addcld |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( B + A ) e. CC ) |
40 |
14 26 39
|
addassd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R A ) + ( 0 -R B ) ) + ( B + A ) ) = ( ( 0 -R A ) + ( ( 0 -R B ) + ( B + A ) ) ) ) |
41 |
35 38 40
|
3eqtr4d |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( 0 -R A ) + ( 0 -R B ) ) + ( A + B ) ) = ( ( ( 0 -R A ) + ( 0 -R B ) ) + ( B + A ) ) ) |
42 |
13 25
|
nnaddcld |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R A ) + ( 0 -R B ) ) e. NN ) |
43 |
42
|
nncnd |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( 0 -R A ) + ( 0 -R B ) ) e. CC ) |
44 |
43 27 39
|
sn-addcand |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( ( ( ( 0 -R A ) + ( 0 -R B ) ) + ( A + B ) ) = ( ( ( 0 -R A ) + ( 0 -R B ) ) + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) ) |
45 |
41 44
|
mpbid |
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ ( B e. RR /\ ( 0 -R B ) e. NN ) ) -> ( A + B ) = ( B + A ) ) |
46 |
3 4 7 45
|
ccase |
|- ( ( ( A e. NN0 \/ ( A e. RR /\ ( 0 -R A ) e. NN ) ) /\ ( B e. NN0 \/ ( B e. RR /\ ( 0 -R B ) e. NN ) ) ) -> ( A + B ) = ( B + A ) ) |
47 |
1 2 46
|
syl2anb |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) = ( B + A ) ) |