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 𝐵 ) )