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