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

Metamath Proof Explorer

Theorem xle0neg2

Description: Extended real version of le0neg2 . (Contributed by Mario Carneiro, 9-Sep-2015)

		Ref	Expression
	Assertion	xle0neg2	$⊢ A \in ℝ^{*} \to (0 \leq A \leftrightarrow - A \leq 0)$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		xleneg	$⊢ (0 \in ℝ^{} \land A \in ℝ^{}) \to (0 \leq A \leftrightarrow - A \leq - 0)$
3	1 2	mpan	$⊢ A \in ℝ^{*} \to (0 \leq A \leftrightarrow - A \leq - 0)$
4		xneg0	$⊢ - 0 = 0$
5	4	breq2i	$⊢ - A \leq - 0 \leftrightarrow - A \leq 0$
6	3 5	bitrdi	$⊢ A \in ℝ^{*} \to (0 \leq A \leftrightarrow - A \leq 0)$