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∈𝑷∧B∈𝑷→A+𝑷B=A+𝑷C→B=C

Proof

Step Hyp Ref Expression
1 addclpr ⊢A∈𝑷∧B∈𝑷→A+𝑷B∈𝑷
2 eleq1 ⊢A+𝑷B=A+𝑷C→A+𝑷B∈𝑷↔A+𝑷C∈𝑷
3 dmplp ⊢dom⁡+𝑷=𝑷×𝑷
4 0npr ⊢¬∅∈𝑷
5 3 4 ndmovrcl ⊢A+𝑷C∈𝑷→A∈𝑷∧C∈𝑷
6 2 5 syl6bi ⊢A+𝑷B=A+𝑷C→A+𝑷B∈𝑷→A∈𝑷∧C∈𝑷
7 1 6 syl5com ⊢A∈𝑷∧B∈𝑷→A+𝑷B=A+𝑷C→A∈𝑷∧C∈𝑷
8 ltapr ⊢A∈𝑷→B<𝑷C↔A+𝑷B<𝑷A+𝑷C
9 ltapr ⊢A∈𝑷→C<𝑷B↔A+𝑷C<𝑷A+𝑷B
10 8 9 orbi12d ⊢A∈𝑷→B<𝑷C∨C<𝑷B↔A+𝑷B<𝑷A+𝑷C∨A+𝑷C<𝑷A+𝑷B
11 10 notbid ⊢A∈𝑷→¬B<𝑷C∨C<𝑷B↔¬A+𝑷B<𝑷A+𝑷C∨A+𝑷C<𝑷A+𝑷B
12 11 ad2antrr ⊢A∈𝑷∧B∈𝑷∧A∈𝑷∧C∈𝑷→¬B<𝑷C∨C<𝑷B↔¬A+𝑷B<𝑷A+𝑷C∨A+𝑷C<𝑷A+𝑷B
13 ltsopr ⊢<𝑷Or𝑷
14 sotrieq ⊢<𝑷Or𝑷∧B∈𝑷∧C∈𝑷→B=C↔¬B<𝑷C∨C<𝑷B
15 13 14 mpan ⊢B∈𝑷∧C∈𝑷→B=C↔¬B<𝑷C∨C<𝑷B
16 15 ad2ant2l ⊢A∈𝑷∧B∈𝑷∧A∈𝑷∧C∈𝑷→B=C↔¬B<𝑷C∨C<𝑷B
17 addclpr ⊢A∈𝑷∧C∈𝑷→A+𝑷C∈𝑷
18 sotrieq ⊢<𝑷Or𝑷∧A+𝑷B∈𝑷∧A+𝑷C∈𝑷→A+𝑷B=A+𝑷C↔¬A+𝑷B<𝑷A+𝑷C∨A+𝑷C<𝑷A+𝑷B
19 13 18 mpan ⊢A+𝑷B∈𝑷∧A+𝑷C∈𝑷→A+𝑷B=A+𝑷C↔¬A+𝑷B<𝑷A+𝑷C∨A+𝑷C<𝑷A+𝑷B
20 1 17 19 syl2an ⊢A∈𝑷∧B∈𝑷∧A∈𝑷∧C∈𝑷→A+𝑷B=A+𝑷C↔¬A+𝑷B<𝑷A+𝑷C∨A+𝑷C<𝑷A+𝑷B
21 12 16 20 3bitr4d ⊢A∈𝑷∧B∈𝑷∧A∈𝑷∧C∈𝑷→B=C↔A+𝑷B=A+𝑷C
22 21 exbiri ⊢A∈𝑷∧B∈𝑷→A∈𝑷∧C∈𝑷→A+𝑷B=A+𝑷C→B=C
23 7 22 syld ⊢A∈𝑷∧B∈𝑷→A+𝑷B=A+𝑷C→A+𝑷B=A+𝑷C→B=C
24 23 pm2.43d ⊢A∈𝑷∧B∈𝑷→A+𝑷B=A+𝑷C→B=C