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 ) )

Metamath Proof Explorer

Theorem nn0p1elfzo

Proof