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