Metamath Proof Explorer

Theorem elunitge0

Description: An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016)

		Ref	Expression
	Assertion	elunitge0	$⊢ A \in [0, 1] \to 0 \leq A$

Proof

Step	Hyp	Ref	Expression
1		elicc01	$⊢ A \in [0, 1] \leftrightarrow (A \in ℝ \land 0 \leq A \land A \leq 1)$
2	1	simp2bi	$⊢ A \in [0, 1] \to 0 \leq A$