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

Metamath Proof Explorer

Theorem addge01d

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	leidd.1	$⊢ φ \to A \in ℝ$
	ltnegd.2	$⊢ φ \to B \in ℝ$
Assertion	addge01d	$⊢ φ \to (0 \leq B \leftrightarrow A \leq A + B)$

Step	Hyp	Ref	Expression
1		leidd.1	$⊢ φ \to A \in ℝ$
2		ltnegd.2	$⊢ φ \to B \in ℝ$
3		addge01	$⊢ (A \in ℝ \land B \in ℝ) \to (0 \leq B \leftrightarrow A \leq A + B)$
4	1 2 3	syl2anc	$⊢ φ \to (0 \leq B \leftrightarrow A \leq A + B)$