Metamath Proof Explorer

Theorem readdcan2

Description: Commuted version of readdcan without ax-mulcom . (Contributed by SN, 21-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( ( A + C ) = ( B + C ) -> ( ( A + C ) + ( 0 -R C ) ) = ( ( B + C ) + ( 0 -R C ) ) )
2 1 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A + C ) = ( B + C ) ) -> ( ( A + C ) + ( 0 -R C ) ) = ( ( B + C ) + ( 0 -R C ) ) )
3 simpl 
 |-  ( ( A e. RR /\ C e. RR ) -> A e. RR )
4 3 recnd 
 |-  ( ( A e. RR /\ C e. RR ) -> A e. CC )
5 simpr 
 |-  ( ( A e. RR /\ C e. RR ) -> C e. RR )
6 5 recnd 
 |-  ( ( A e. RR /\ C e. RR ) -> C e. CC )
7 rernegcl 
 |-  ( C e. RR -> ( 0 -R C ) e. RR )
8 7 adantl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( 0 -R C ) e. RR )
9 8 recnd 
 |-  ( ( A e. RR /\ C e. RR ) -> ( 0 -R C ) e. CC )
10 4 6 9 addassd 
 |-  ( ( A e. RR /\ C e. RR ) -> ( ( A + C ) + ( 0 -R C ) ) = ( A + ( C + ( 0 -R C ) ) ) )
11 renegid 
 |-  ( C e. RR -> ( C + ( 0 -R C ) ) = 0 )
12 11 oveq2d 
 |-  ( C e. RR -> ( A + ( C + ( 0 -R C ) ) ) = ( A + 0 ) )
13 12 adantl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + ( C + ( 0 -R C ) ) ) = ( A + 0 ) )
14 readdid1 
 |-  ( A e. RR -> ( A + 0 ) = A )
15 14 adantr 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + 0 ) = A )
16 10 13 15 3eqtrd 
 |-  ( ( A e. RR /\ C e. RR ) -> ( ( A + C ) + ( 0 -R C ) ) = A )
17 16 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) + ( 0 -R C ) ) = A )
18 17 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A + C ) = ( B + C ) ) -> ( ( A + C ) + ( 0 -R C ) ) = A )
19 simpl 
 |-  ( ( B e. RR /\ C e. RR ) -> B e. RR )
20 19 recnd 
 |-  ( ( B e. RR /\ C e. RR ) -> B e. CC )
21 simpr 
 |-  ( ( B e. RR /\ C e. RR ) -> C e. RR )
22 21 recnd 
 |-  ( ( B e. RR /\ C e. RR ) -> C e. CC )
23 7 adantl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( 0 -R C ) e. RR )
24 23 recnd 
 |-  ( ( B e. RR /\ C e. RR ) -> ( 0 -R C ) e. CC )
25 20 22 24 addassd 
 |-  ( ( B e. RR /\ C e. RR ) -> ( ( B + C ) + ( 0 -R C ) ) = ( B + ( C + ( 0 -R C ) ) ) )
26 11 oveq2d 
 |-  ( C e. RR -> ( B + ( C + ( 0 -R C ) ) ) = ( B + 0 ) )
27 26 adantl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + ( C + ( 0 -R C ) ) ) = ( B + 0 ) )
28 readdid1 
 |-  ( B e. RR -> ( B + 0 ) = B )
29 28 adantr 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + 0 ) = B )
30 25 27 29 3eqtrd 
 |-  ( ( B e. RR /\ C e. RR ) -> ( ( B + C ) + ( 0 -R C ) ) = B )
31 30 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) + ( 0 -R C ) ) = B )
32 31 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A + C ) = ( B + C ) ) -> ( ( B + C ) + ( 0 -R C ) ) = B )
33 2 18 32 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A + C ) = ( B + C ) ) -> A = B )
34 33 ex 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) = ( B + C ) -> A = B ) )
35 oveq1 
 |-  ( A = B -> ( A + C ) = ( B + C ) )
36 34 35 impbid1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) = ( B + C ) <-> A = B ) )