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 \land 0_{𝑹} <_{𝑹} B) \to 0_{𝑹} <_{𝑹} (A +_{𝑹} B)$

Step	Hyp	Ref	Expression
1		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
2	1	brel	$⊢ 0_{𝑹} <_{𝑹} A \to (0_{𝑹} \in 𝑹 \land A \in 𝑹)$
3		ltasr	$⊢ A \in 𝑹 \to (0_{𝑹} <_{𝑹} B \leftrightarrow (A +_{𝑹} 0_{𝑹}) <_{𝑹} (A +_{𝑹} B))$
4		0idsr	$⊢ A \in 𝑹 \to A +_{𝑹} 0_{𝑹} = A$
5	4	breq1d	$⊢ A \in 𝑹 \to ((A +_{𝑹} 0_{𝑹}) <_{𝑹} (A +_{𝑹} B) \leftrightarrow A <_{𝑹} (A +_{𝑹} B))$
6	3 5	bitrd	$⊢ A \in 𝑹 \to (0_{𝑹} <_{𝑹} B \leftrightarrow A <_{𝑹} (A +_{𝑹} B))$
7	2 6	simpl2im	$⊢ 0_{𝑹} <_{𝑹} A \to (0_{𝑹} <_{𝑹} B \leftrightarrow A <_{𝑹} (A +_{𝑹} B))$
8	7	biimpa	$⊢ (0_{𝑹} <_{𝑹} A \land 0_{𝑹} <_{𝑹} B) \to A <_{𝑹} (A +_{𝑹} B)$
9		ltsosr	$⊢ <_{𝑹} Or 𝑹$
10	9 1	sotri	$⊢ (0_{𝑹} <_{𝑹} A \land A <_{𝑹} (A +_{𝑹} B)) \to 0_{𝑹} <_{𝑹} (A +_{𝑹} B)$
11	8 10	syldan	$⊢ (0_{𝑹} <_{𝑹} A \land 0_{𝑹} <_{𝑹} B) \to 0_{𝑹} <_{𝑹} (A +_{𝑹} B)$

Metamath Proof Explorer