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