This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )