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