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

Metamath Proof Explorer

Theorem ltaddrp

Description: Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007)

		Ref	Expression
	Assertion	ltaddrp	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A < A + B$

Step	Hyp	Ref	Expression
1		elrp	$⊢ B \in ℝ^{+} \leftrightarrow (B \in ℝ \land 0 < B)$
2		ltaddpos	$⊢ (B \in ℝ \land A \in ℝ) \to (0 < B \leftrightarrow A < A + B)$
3	2	biimpd	$⊢ (B \in ℝ \land A \in ℝ) \to (0 < B \to A < A + B)$
4	3	expcom	$⊢ A \in ℝ \to (B \in ℝ \to (0 < B \to A < A + B))$
5	4	imp32	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to A < A + B$
6	1 5	sylan2b	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A < A + B$