Theorem bndndx

Description: A bounded real sequence A ( k ) is less than or equal to at least one of its indices. (Contributed by NM, 18-Jan-2008)

	Ref	Expression
Assertion	bndndx	|- ( E. x e. RR A. k e. NN ( A e. RR /\ A <_ x ) -> E. k e. NN A <_ k )

Proof

Step	Hyp	Ref	Expression
1		arch	|- ( x e. RR -> E. k e. NN x < k )
2		nnre	|- ( k e. NN -> k e. RR )
3		lelttr	|- ( ( A e. RR /\ x e. RR /\ k e. RR ) -> ( ( A <_ x /\ x < k ) -> A < k ) )
4		ltle	|- ( ( A e. RR /\ k e. RR ) -> ( A < k -> A <_ k ) )
5	4	3adant2	|- ( ( A e. RR /\ x e. RR /\ k e. RR ) -> ( A < k -> A <_ k ) )
6	3 5	syld	|- ( ( A e. RR /\ x e. RR /\ k e. RR ) -> ( ( A <_ x /\ x < k ) -> A <_ k ) )
7	6	exp5o	|- ( A e. RR -> ( x e. RR -> ( k e. RR -> ( A <_ x -> ( x < k -> A <_ k ) ) ) ) )
8	7	com3l	|- ( x e. RR -> ( k e. RR -> ( A e. RR -> ( A <_ x -> ( x < k -> A <_ k ) ) ) ) )
9	8	imp4b	|- ( ( x e. RR /\ k e. RR ) -> ( ( A e. RR /\ A <_ x ) -> ( x < k -> A <_ k ) ) )
10	9	com23	|- ( ( x e. RR /\ k e. RR ) -> ( x < k -> ( ( A e. RR /\ A <_ x ) -> A <_ k ) ) )
11	2 10	sylan2	|- ( ( x e. RR /\ k e. NN ) -> ( x < k -> ( ( A e. RR /\ A <_ x ) -> A <_ k ) ) )
12	11	reximdva	|- ( x e. RR -> ( E. k e. NN x < k -> E. k e. NN ( ( A e. RR /\ A <_ x ) -> A <_ k ) ) )
13	1 12	mpd	|- ( x e. RR -> E. k e. NN ( ( A e. RR /\ A <_ x ) -> A <_ k ) )
14		r19.35	|- ( E. k e. NN ( ( A e. RR /\ A <_ x ) -> A <_ k ) <-> ( A. k e. NN ( A e. RR /\ A <_ x ) -> E. k e. NN A <_ k ) )
15	13 14	sylib	|- ( x e. RR -> ( A. k e. NN ( A e. RR /\ A <_ x ) -> E. k e. NN A <_ k ) )
16	15	rexlimiv	|- ( E. x e. RR A. k e. NN ( A e. RR /\ A <_ x ) -> E. k e. NN A <_ k )