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

Metamath Proof Explorer

Theorem nnm1ge0

Description: A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018)

		Ref	Expression
	Assertion	nnm1ge0	$⊢ N \in ℕ \to 0 \leq N - 1$

Step	Hyp	Ref	Expression
1		nngt0	$⊢ N \in ℕ \to 0 < N$
2		0z	$⊢ 0 \in ℤ$
3		nnz	$⊢ N \in ℕ \to N \in ℤ$
4		zltlem1	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 < N \leftrightarrow 0 \leq N - 1)$
5	2 3 4	sylancr	$⊢ N \in ℕ \to (0 < N \leftrightarrow 0 \leq N - 1)$
6	1 5	mpbid	$⊢ N \in ℕ \to 0 \leq N - 1$