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	⊢ ( 0 ... ( 0 − 1 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 1 = ( 0 − 1 )
2	1	oveq2i	⊢ ( 0 ... - 1 ) = ( 0 ... ( 0 − 1 ) )
3		neg1lt0	⊢ - 1 < 0
4		0z	⊢ 0 ∈ ℤ
5		neg1z	⊢ - 1 ∈ ℤ
6		fzn	⊢ ( ( 0 ∈ ℤ ∧ - 1 ∈ ℤ ) → ( - 1 < 0 ↔ ( 0 ... - 1 ) = ∅ ) )
7	4 5 6	mp2an	⊢ ( - 1 < 0 ↔ ( 0 ... - 1 ) = ∅ )
8	3 7	mpbi	⊢ ( 0 ... - 1 ) = ∅
9	2 8	eqtr3i	⊢ ( 0 ... ( 0 − 1 ) ) = ∅