0nelfz1

Description: 0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020)

		Ref	Expression
	Assertion	0nelfz1	$⊢ 0 \notin (1 \dots N)$

Step	Hyp	Ref	Expression
1		0lt1	$⊢ 0 < 1$
2		0re	$⊢ 0 \in ℝ$
3		1re	$⊢ 1 \in ℝ$
4	2 3	ltnlei	$⊢ 0 < 1 \leftrightarrow \neg 1 \leq 0$
5	1 4	mpbi	$⊢ \neg 1 \leq 0$
6	5	intnanr	$⊢ \neg (1 \leq 0 \land 0 \leq N)$
7	6	intnan	$⊢ \neg ((1 \in ℤ \land N \in ℤ \land 0 \in ℤ) \land (1 \leq 0 \land 0 \leq N))$
8		df-nel	$⊢ 0 \notin (1 \dots N) \leftrightarrow \neg 0 \in (1 \dots N)$
9		elfz2	$⊢ 0 \in (1 \dots N) \leftrightarrow ((1 \in ℤ \land N \in ℤ \land 0 \in ℤ) \land (1 \leq 0 \land 0 \leq N))$
10	8 9	xchbinx	$⊢ 0 \notin (1 \dots N) \leftrightarrow \neg ((1 \in ℤ \land N \in ℤ \land 0 \in ℤ) \land (1 \leq 0 \land 0 \leq N))$
11	7 10	mpbir	$⊢ 0 \notin (1 \dots N)$

Metamath Proof Explorer