Metamath Proof Explorer

Theorem readdsub

Description: Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023)

Ref Expression
Assertion readdsub 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R C ) = ( ( A -R C ) + B ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
2 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
3 2 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) e. RR )
4 repncan3 
 |-  ( ( C e. RR /\ ( A + B ) e. RR ) -> ( C + ( ( A + B ) -R C ) ) = ( A + B ) )
5 1 3 4 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( ( A + B ) -R C ) ) = ( A + B ) )
6 repncan3 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C + ( A -R C ) ) = A )
7 6 ancoms 
 |-  ( ( A e. RR /\ C e. RR ) -> ( C + ( A -R C ) ) = A )
8 7 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( A -R C ) ) = A )
9 8 oveq1d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + ( A -R C ) ) + B ) = ( A + B ) )
10 1 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
11 rersubcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A -R C ) e. RR )
12 11 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A -R C ) e. RR )
13 12 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A -R C ) e. CC )
14 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
15 14 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
16 10 13 15 addassd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + ( A -R C ) ) + B ) = ( C + ( ( A -R C ) + B ) ) )
17 5 9 16 3eqtr2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( ( A + B ) -R C ) ) = ( C + ( ( A -R C ) + B ) ) )
18 rersubcl 
 |-  ( ( ( A + B ) e. RR /\ C e. RR ) -> ( ( A + B ) -R C ) e. RR )
19 3 1 18 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R C ) e. RR )
20 12 14 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R C ) + B ) e. RR )
21 readdcan 
 |-  ( ( ( ( A + B ) -R C ) e. RR /\ ( ( A -R C ) + B ) e. RR /\ C e. RR ) -> ( ( C + ( ( A + B ) -R C ) ) = ( C + ( ( A -R C ) + B ) ) <-> ( ( A + B ) -R C ) = ( ( A -R C ) + B ) ) )
22 19 20 1 21 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + ( ( A + B ) -R C ) ) = ( C + ( ( A -R C ) + B ) ) <-> ( ( A + B ) -R C ) = ( ( A -R C ) + B ) ) )
23 17 22 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R C ) = ( ( A -R C ) + B ) )