Metamath Proof Explorer

Theorem fseqsupcl

Description: The values of a finite real sequence have a supremum. (Contributed by NM, 20-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fseqsupcl 
|- ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> sup ( ran F , RR , < ) e. RR )

Proof

Step Hyp Ref Expression
1 frn 
 |-  ( F : ( M ... N ) --> RR -> ran F C_ RR )
2 1 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> ran F C_ RR )
3 fzfi 
 |-  ( M ... N ) e. Fin
4 ffn 
 |-  ( F : ( M ... N ) --> RR -> F Fn ( M ... N ) )
5 4 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> F Fn ( M ... N ) )
6 dffn4 
 |-  ( F Fn ( M ... N ) <-> F : ( M ... N ) -onto-> ran F )
7 5 6 sylib 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> F : ( M ... N ) -onto-> ran F )
8 fofi 
 |-  ( ( ( M ... N ) e. Fin /\ F : ( M ... N ) -onto-> ran F ) -> ran F e. Fin )
9 3 7 8 sylancr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> ran F e. Fin )
10 fdm 
 |-  ( F : ( M ... N ) --> RR -> dom F = ( M ... N ) )
11 10 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> dom F = ( M ... N ) )
12 simpl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> N e. ( ZZ>= ` M ) )
13 fzn0 
 |-  ( ( M ... N ) =/= (/) <-> N e. ( ZZ>= ` M ) )
14 12 13 sylibr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> ( M ... N ) =/= (/) )
15 11 14 eqnetrd 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> dom F =/= (/) )
16 dm0rn0 
 |-  ( dom F = (/) <-> ran F = (/) )
17 16 necon3bii 
 |-  ( dom F =/= (/) <-> ran F =/= (/) )
18 15 17 sylib 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> ran F =/= (/) )
19 ltso 
 |-  < Or RR
20 fisupcl 
 |-  ( ( < Or RR /\ ( ran F e. Fin /\ ran F =/= (/) /\ ran F C_ RR ) ) -> sup ( ran F , RR , < ) e. ran F )
21 19 20 mpan 
 |-  ( ( ran F e. Fin /\ ran F =/= (/) /\ ran F C_ RR ) -> sup ( ran F , RR , < ) e. ran F )
22 9 18 2 21 syl3anc 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> sup ( ran F , RR , < ) e. ran F )
23 2 22 sseldd 
 |-  ( ( N e. ( ZZ>= ` M ) /\ F : ( M ... N ) --> RR ) -> sup ( ran F , RR , < ) e. RR )