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 0R

Proof

Step	Hyp	Ref	Expression
1		ltrelsr	|-
2	1	brel	|- ( 0R ( 0R e. R. /\ A e. R. ) )
3		ltasr	|- ( A e. R. -> ( 0R ( A +R 0R )
4		0idsr	|- ( A e. R. -> ( A +R 0R ) = A )
5	4	breq1d	|- ( A e. R. -> ( ( A +R 0R ) A
6	3 5	bitrd	|- ( A e. R. -> ( 0R A
7	2 6	simpl2im	|- ( 0R ( 0R A
8	7	biimpa	|- ( ( 0R A
9		ltsosr	|-
10	9 1	sotri	|- ( ( 0R 0R
11	8 10	syldan	|- ( ( 0R 0R