Metamath Proof Explorer


Theorem zaddcom

Description: Addition is commutative for integers. Proven without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion zaddcom
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) = ( B + A ) )

Proof

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