This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 0R <R 𝐴 ∧ 0R <R 𝐵 ) → 0R <R ( 𝐴 +R 𝐵 ) )

Proof

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