Metamath Proof Explorer

Theorem addgt0sr

Description: The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

Ref Expression
Assertion addgt0sr ⊢ 0 𝑹 < 𝑹 A ∧ 0 𝑹 < 𝑹 B → 0 𝑹 < 𝑹 A + 𝑹 B

Proof

Step Hyp Ref Expression
1 ltrelsr ⊢ < 𝑹 ⊆ 𝑹 × 𝑹
2 1 brel ⊢ 0 𝑹 < 𝑹 A → 0 𝑹 ∈ 𝑹 ∧ A ∈ 𝑹
3 ltasr ⊢ A ∈ 𝑹 → 0 𝑹 < 𝑹 B ↔ A + 𝑹 0 𝑹 < 𝑹 A + 𝑹 B
4 0idsr ⊢ A ∈ 𝑹 → A + 𝑹 0 𝑹 = A
5 4 breq1d ⊢ A ∈ 𝑹 → A + 𝑹 0 𝑹 < 𝑹 A + 𝑹 B ↔ A < 𝑹 A + 𝑹 B
6 3 5 bitrd ⊢ A ∈ 𝑹 → 0 𝑹 < 𝑹 B ↔ A < 𝑹 A + 𝑹 B
7 2 6 simpl2im ⊢ 0 𝑹 < 𝑹 A → 0 𝑹 < 𝑹 B ↔ A < 𝑹 A + 𝑹 B
8 7 biimpa ⊢ 0 𝑹 < 𝑹 A ∧ 0 𝑹 < 𝑹 B → A < 𝑹 A + 𝑹 B
9 ltsosr ⊢ < 𝑹 Or 𝑹
10 9 1 sotri ⊢ 0 𝑹 < 𝑹 A ∧ A < 𝑹 A + 𝑹 B → 0 𝑹 < 𝑹 A + 𝑹 B
11 8 10 syldan ⊢ 0 𝑹 < 𝑹 A ∧ 0 𝑹 < 𝑹 B → 0 𝑹 < 𝑹 A + 𝑹 B