Metamath Proof Explorer

Theorem fsequb

Description: The values of a finite real sequence have an upper bound. (Contributed by NM, 19-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fsequb 
|- ( A. k e. ( M ... N ) ( F ` k ) e. RR -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x )

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( M ... N ) e. Fin
2 fimaxre3 
 |-  ( ( ( M ... N ) e. Fin /\ A. k e. ( M ... N ) ( F ` k ) e. RR ) -> E. y e. RR A. k e. ( M ... N ) ( F ` k ) <_ y )
3 1 2 mpan 
 |-  ( A. k e. ( M ... N ) ( F ` k ) e. RR -> E. y e. RR A. k e. ( M ... N ) ( F ` k ) <_ y )
4 r19.26 
 |-  ( A. k e. ( M ... N ) ( ( F ` k ) e. RR /\ ( F ` k ) <_ y ) <-> ( A. k e. ( M ... N ) ( F ` k ) e. RR /\ A. k e. ( M ... N ) ( F ` k ) <_ y ) )
5 peano2re 
 |-  ( y e. RR -> ( y + 1 ) e. RR )
6 ltp1 
 |-  ( y e. RR -> y < ( y + 1 ) )
7 6 adantr 
 |-  ( ( y e. RR /\ ( F ` k ) e. RR ) -> y < ( y + 1 ) )
8 simpr 
 |-  ( ( y e. RR /\ ( F ` k ) e. RR ) -> ( F ` k ) e. RR )
9 simpl 
 |-  ( ( y e. RR /\ ( F ` k ) e. RR ) -> y e. RR )
10 5 adantr 
 |-  ( ( y e. RR /\ ( F ` k ) e. RR ) -> ( y + 1 ) e. RR )
11 lelttr 
 |-  ( ( ( F ` k ) e. RR /\ y e. RR /\ ( y + 1 ) e. RR ) -> ( ( ( F ` k ) <_ y /\ y < ( y + 1 ) ) -> ( F ` k ) < ( y + 1 ) ) )
12 8 9 10 11 syl3anc 
 |-  ( ( y e. RR /\ ( F ` k ) e. RR ) -> ( ( ( F ` k ) <_ y /\ y < ( y + 1 ) ) -> ( F ` k ) < ( y + 1 ) ) )
13 7 12 mpan2d 
 |-  ( ( y e. RR /\ ( F ` k ) e. RR ) -> ( ( F ` k ) <_ y -> ( F ` k ) < ( y + 1 ) ) )
14 13 expimpd 
 |-  ( y e. RR -> ( ( ( F ` k ) e. RR /\ ( F ` k ) <_ y ) -> ( F ` k ) < ( y + 1 ) ) )
15 14 ralimdv 
 |-  ( y e. RR -> ( A. k e. ( M ... N ) ( ( F ` k ) e. RR /\ ( F ` k ) <_ y ) -> A. k e. ( M ... N ) ( F ` k ) < ( y + 1 ) ) )
16 brralrspcev 
 |-  ( ( ( y + 1 ) e. RR /\ A. k e. ( M ... N ) ( F ` k ) < ( y + 1 ) ) -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x )
17 5 15 16 syl6an 
 |-  ( y e. RR -> ( A. k e. ( M ... N ) ( ( F ` k ) e. RR /\ ( F ` k ) <_ y ) -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x ) )
18 4 17 syl5bir 
 |-  ( y e. RR -> ( ( A. k e. ( M ... N ) ( F ` k ) e. RR /\ A. k e. ( M ... N ) ( F ` k ) <_ y ) -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x ) )
19 18 expd 
 |-  ( y e. RR -> ( A. k e. ( M ... N ) ( F ` k ) e. RR -> ( A. k e. ( M ... N ) ( F ` k ) <_ y -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x ) ) )
20 19 impcom 
 |-  ( ( A. k e. ( M ... N ) ( F ` k ) e. RR /\ y e. RR ) -> ( A. k e. ( M ... N ) ( F ` k ) <_ y -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x ) )
21 20 rexlimdva 
 |-  ( A. k e. ( M ... N ) ( F ` k ) e. RR -> ( E. y e. RR A. k e. ( M ... N ) ( F ` k ) <_ y -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x ) )
22 3 21 mpd 
 |-  ( A. k e. ( M ... N ) ( F ` k ) e. RR -> E. x e. RR A. k e. ( M ... N ) ( F ` k ) < x )