Metamath Proof Explorer

Theorem readdcan

Description: Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 ltadd2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C + A ) < ( C + B ) ) )
2 1 notbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. A < B <-> -. ( C + A ) < ( C + B ) ) )
3 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
4 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
6 3 4 5 ltadd2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < A <-> ( C + B ) < ( C + A ) ) )
7 6 notbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. B < A <-> -. ( C + B ) < ( C + A ) ) )
8 2 7 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( -. A < B /\ -. B < A ) <-> ( -. ( C + A ) < ( C + B ) /\ -. ( C + B ) < ( C + A ) ) ) )
9 4 3 lttri3d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
10 5 4 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + A ) e. RR )
11 5 3 readdcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + B ) e. RR )
12 10 11 lttri3d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) = ( C + B ) <-> ( -. ( C + A ) < ( C + B ) /\ -. ( C + B ) < ( C + A ) ) ) )
13 8 9 12 3bitr4rd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) = ( C + B ) <-> A = B ) )