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 ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → 𝐵 = 𝐶 ) )

Proof

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