Theorem risefall0lem

Description: Lemma for risefac0 and fallfac0 . Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	risefall0lem	$$⊢\left(0\dots 0-1\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-neg	$$⊢-1=0-1$$
2	1	oveq2i	$$⊢\left(0\dots -1\right)=\left(0\dots 0-1\right)$$
3		neg1lt0	$$⊢-1<0$$
4		0z	$$⊢0\in \mathbb{Z}$$
5		neg1z	$$⊢-1\in \mathbb{Z}$$
6		fzn	$$⊢\left(0\in \mathbb{Z}\wedge -1\in \mathbb{Z}\right)\to \left(-1<0\leftrightarrow \left(0\dots -1\right)=\varnothing \right)$$
7	4 5 6	mp2an	$$⊢-1<0\leftrightarrow \left(0\dots -1\right)=\varnothing$$
8	3 7	mpbi	$$⊢\left(0\dots -1\right)=\varnothing$$
9	2 8	eqtr3i	$$⊢\left(0\dots 0-1\right)=\varnothing$$