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

Metamath Proof Explorer

Theorem nnnle0

Description: A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020)

		Ref	Expression
	Assertion	nnnle0	$⊢ A \in ℕ \to \neg A \leq 0$

Step	Hyp	Ref	Expression
1		nngt0	$⊢ A \in ℕ \to 0 < A$
2		0re	$⊢ 0 \in ℝ$
3		nnre	$⊢ A \in ℕ \to A \in ℝ$
4		ltnle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \leftrightarrow \neg A \leq 0)$
5	4	bicomd	$⊢ (0 \in ℝ \land A \in ℝ) \to (\neg A \leq 0 \leftrightarrow 0 < A)$
6	2 3 5	sylancr	$⊢ A \in ℕ \to (\neg A \leq 0 \leftrightarrow 0 < A)$
7	1 6	mpbird	$⊢ A \in ℕ \to \neg A \leq 0$