Theorem elfzouz2

Description: The upper bound of a half-open range is greater than or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	elfzouz2	|- ( K e. ( M ..^ N ) -> N e. ( ZZ>= ` K ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	|- ( K e. ( M ..^ N ) -> K e. ZZ )
2		elfzoel2	|- ( K e. ( M ..^ N ) -> N e. ZZ )
3		elfzolt2	|- ( K e. ( M ..^ N ) -> K < N )
4		zre	|- ( K e. ZZ -> K e. RR )
5		zre	|- ( N e. ZZ -> N e. RR )
6		ltle	|- ( ( K e. RR /\ N e. RR ) -> ( K < N -> K <_ N ) )
7	4 5 6	syl2an	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N -> K <_ N ) )
8	1 2 7	syl2anc	|- ( K e. ( M ..^ N ) -> ( K < N -> K <_ N ) )
9	3 8	mpd	|- ( K e. ( M ..^ N ) -> K <_ N )
10		eluz2	|- ( N e. ( ZZ>= ` K ) <-> ( K e. ZZ /\ N e. ZZ /\ K <_ N ) )
11	1 2 9 10	syl3anbrc	|- ( K e. ( M ..^ N ) -> N e. ( ZZ>= ` K ) )