Metamath Proof Explorer


Theorem addcanpr

Description: Addition cancellation law for positive reals. Proposition 9-3.5(vi) of Gleason p. 123. (Contributed by NM, 9-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion addcanpr
|- ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) )

Proof

Step Hyp Ref Expression
1 addclpr
 |-  ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )
2 eleq1
 |-  ( ( A +P. B ) = ( A +P. C ) -> ( ( A +P. B ) e. P. <-> ( A +P. C ) e. P. ) )
3 dmplp
 |-  dom +P. = ( P. X. P. )
4 0npr
 |-  -. (/) e. P.
5 3 4 ndmovrcl
 |-  ( ( A +P. C ) e. P. -> ( A e. P. /\ C e. P. ) )
6 2 5 syl6bi
 |-  ( ( A +P. B ) = ( A +P. C ) -> ( ( A +P. B ) e. P. -> ( A e. P. /\ C e. P. ) ) )
7 1 6 syl5com
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> ( A e. P. /\ C e. P. ) ) )
8 ltapr
 |-  ( A e. P. -> ( B 

( A +P. B )

9 ltapr
 |-  ( A e. P. -> ( C 

( A +P. C )

10 8 9 orbi12d
 |-  ( A e. P. -> ( ( B 

( ( A +P. B )

11 10 notbid
 |-  ( A e. P. -> ( -. ( B 

-. ( ( A +P. B )

12 11 ad2antrr
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( -. ( B 

-. ( ( A +P. B )

13 ltsopr
 |-  

14 sotrieq
 |-  ( ( 

( B = C <-> -. ( B

15 13 14 mpan
 |-  ( ( B e. P. /\ C e. P. ) -> ( B = C <-> -. ( B 

16 15 ad2ant2l
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( B = C <-> -. ( B 

17 addclpr
 |-  ( ( A e. P. /\ C e. P. ) -> ( A +P. C ) e. P. )
18 sotrieq
 |-  ( ( 

( ( A +P. B ) = ( A +P. C ) <-> -. ( ( A +P. B )

19 13 18 mpan
 |-  ( ( ( A +P. B ) e. P. /\ ( A +P. C ) e. P. ) -> ( ( A +P. B ) = ( A +P. C ) <-> -. ( ( A +P. B ) 

20 1 17 19 syl2an
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( ( A +P. B ) = ( A +P. C ) <-> -. ( ( A +P. B ) 

21 12 16 20 3bitr4d
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( A e. P. /\ C e. P. ) ) -> ( B = C <-> ( A +P. B ) = ( A +P. C ) ) )
22 21 exbiri
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( A e. P. /\ C e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) ) )
23 7 22 syld
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) ) )
24 23 pm2.43d
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) )