Metamath Proof Explorer


Theorem zaddcomlem

Description: Lemma for zaddcom . (Contributed by SN, 1-Feb-2025)

Ref Expression
Assertion zaddcomlem
|- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( A + B ) = ( B + A ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> B e. NN0 )
2 1 nn0cnd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> B e. CC )
3 rernegcl
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
4 3 ad2antrr
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( 0 -R A ) e. RR )
5 4 recnd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( 0 -R A ) e. CC )
6 simpll
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> A e. RR )
7 6 recnd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> A e. CC )
8 2 5 7 addassd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( B + ( 0 -R A ) ) + A ) = ( B + ( ( 0 -R A ) + A ) ) )
9 renegid2
 |-  ( A e. RR -> ( ( 0 -R A ) + A ) = 0 )
10 9 ad2antrr
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( 0 -R A ) + A ) = 0 )
11 10 oveq2d
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( B + ( ( 0 -R A ) + A ) ) = ( B + 0 ) )
12 nn0re
 |-  ( B e. NN0 -> B e. RR )
13 readdrid
 |-  ( B e. RR -> ( B + 0 ) = B )
14 12 13 syl
 |-  ( B e. NN0 -> ( B + 0 ) = B )
15 14 adantl
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( B + 0 ) = B )
16 8 11 15 3eqtrrd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> B = ( ( B + ( 0 -R A ) ) + A ) )
17 9 oveq1d
 |-  ( A e. RR -> ( ( ( 0 -R A ) + A ) + B ) = ( 0 + B ) )
18 17 adantr
 |-  ( ( A e. RR /\ ( 0 -R A ) e. NN ) -> ( ( ( 0 -R A ) + A ) + B ) = ( 0 + B ) )
19 readdlid
 |-  ( B e. RR -> ( 0 + B ) = B )
20 12 19 syl
 |-  ( B e. NN0 -> ( 0 + B ) = B )
21 18 20 sylan9eq
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( ( 0 -R A ) + A ) + B ) = B )
22 nnnn0
 |-  ( ( 0 -R A ) e. NN -> ( 0 -R A ) e. NN0 )
23 nn0addcom
 |-  ( ( ( 0 -R A ) e. NN0 /\ B e. NN0 ) -> ( ( 0 -R A ) + B ) = ( B + ( 0 -R A ) ) )
24 22 23 sylan
 |-  ( ( ( 0 -R A ) e. NN /\ B e. NN0 ) -> ( ( 0 -R A ) + B ) = ( B + ( 0 -R A ) ) )
25 24 adantll
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( 0 -R A ) + B ) = ( B + ( 0 -R A ) ) )
26 25 oveq1d
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( ( 0 -R A ) + B ) + A ) = ( ( B + ( 0 -R A ) ) + A ) )
27 16 21 26 3eqtr4d
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( ( 0 -R A ) + A ) + B ) = ( ( ( 0 -R A ) + B ) + A ) )
28 5 7 2 addassd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( ( 0 -R A ) + A ) + B ) = ( ( 0 -R A ) + ( A + B ) ) )
29 5 2 7 addassd
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( ( 0 -R A ) + B ) + A ) = ( ( 0 -R A ) + ( B + A ) ) )
30 27 28 29 3eqtr3d
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( 0 -R A ) + ( A + B ) ) = ( ( 0 -R A ) + ( B + A ) ) )
31 7 2 addcld
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( A + B ) e. CC )
32 2 7 addcld
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( B + A ) e. CC )
33 5 31 32 sn-addcand
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( ( ( 0 -R A ) + ( A + B ) ) = ( ( 0 -R A ) + ( B + A ) ) <-> ( A + B ) = ( B + A ) ) )
34 30 33 mpbid
 |-  ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) -> ( A + B ) = ( B + A ) )