zgt0ge1

Description: An integer greater than 0 is greater than or equal to 1 . (Contributed by AV, 14-Oct-2018)

		Ref	Expression
	Assertion	zgt0ge1	$⊢ Z \in ℤ \to (0 < Z \leftrightarrow 1 \leq Z)$

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		zltp1le	$⊢ (0 \in ℤ \land Z \in ℤ) \to (0 < Z \leftrightarrow 0 + 1 \leq Z)$
3	1 2	mpan	$⊢ Z \in ℤ \to (0 < Z \leftrightarrow 0 + 1 \leq Z)$
4		0p1e1	$⊢ 0 + 1 = 1$
5	4	a1i	$⊢ Z \in ℤ \to 0 + 1 = 1$
6	5	breq1d	$⊢ Z \in ℤ \to (0 + 1 \leq Z \leftrightarrow 1 \leq Z)$
7	3 6	bitrd	$⊢ Z \in ℤ \to (0 < Z \leftrightarrow 1 \leq Z)$

Metamath Proof Explorer