Theorem nn0p1elfzo

Description: A nonnegative integer increased by 1 which is less than or equal to another integer is an element of a half-open range of integers. (Contributed by AV, 27-Feb-2021)

	Ref	Expression
Assertion	nn0p1elfzo	|- ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) -> K e. ( 0 ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		nn0ltp1le	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( K < N <-> ( K + 1 ) <_ N ) )
2	1	biimp3ar	|- ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) -> K < N )
3		simpl1	|- ( ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) /\ K < N ) -> K e. NN0 )
4		simpr	|- ( ( K e. NN0 /\ N e. NN0 ) -> N e. NN0 )
5	4	adantr	|- ( ( ( K e. NN0 /\ N e. NN0 ) /\ K < N ) -> N e. NN0 )
6		nn0ge0	|- ( K e. NN0 -> 0 <_ K )
7	6	adantr	|- ( ( K e. NN0 /\ N e. NN0 ) -> 0 <_ K )
8		0re	|- 0 e. RR
9		nn0re	|- ( K e. NN0 -> K e. RR )
10		nn0re	|- ( N e. NN0 -> N e. RR )
11		lelttr	|- ( ( 0 e. RR /\ K e. RR /\ N e. RR ) -> ( ( 0 <_ K /\ K < N ) -> 0 < N ) )
12	8 9 10 11	mp3an3an	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( ( 0 <_ K /\ K < N ) -> 0 < N ) )
13	7 12	mpand	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( K < N -> 0 < N ) )
14	13	imp	|- ( ( ( K e. NN0 /\ N e. NN0 ) /\ K < N ) -> 0 < N )
15		elnnnn0b	|- ( N e. NN <-> ( N e. NN0 /\ 0 < N ) )
16	5 14 15	sylanbrc	|- ( ( ( K e. NN0 /\ N e. NN0 ) /\ K < N ) -> N e. NN )
17	16	3adantl3	|- ( ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) /\ K < N ) -> N e. NN )
18		simpr	|- ( ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) /\ K < N ) -> K < N )
19	3 17 18	3jca	|- ( ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) /\ K < N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
20	2 19	mpdan	|- ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) -> ( K e. NN0 /\ N e. NN /\ K < N ) )
21		elfzo0	|- ( K e. ( 0 ..^ N ) <-> ( K e. NN0 /\ N e. NN /\ K < N ) )
22	20 21	sylibr	|- ( ( K e. NN0 /\ N e. NN0 /\ ( K + 1 ) <_ N ) -> K e. ( 0 ..^ N ) )