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