Metamath Proof Explorer


Theorem suprzcl

Description: The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion suprzcl
|- ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. A )

Proof

Step Hyp Ref Expression
1 zssre
 |-  ZZ C_ RR
2 sstr
 |-  ( ( A C_ ZZ /\ ZZ C_ RR ) -> A C_ RR )
3 1 2 mpan2
 |-  ( A C_ ZZ -> A C_ RR )
4 suprcl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
5 3 4 syl3an1
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
6 5 ltm1d
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR , < ) - 1 ) < sup ( A , RR , < ) )
7 peano2rem
 |-  ( sup ( A , RR , < ) e. RR -> ( sup ( A , RR , < ) - 1 ) e. RR )
8 4 7 syl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( sup ( A , RR , < ) - 1 ) e. RR )
9 suprlub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( sup ( A , RR , < ) - 1 ) e. RR ) -> ( ( sup ( A , RR , < ) - 1 ) < sup ( A , RR , < ) <-> E. z e. A ( sup ( A , RR , < ) - 1 ) < z ) )
10 8 9 mpdan
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( ( sup ( A , RR , < ) - 1 ) < sup ( A , RR , < ) <-> E. z e. A ( sup ( A , RR , < ) - 1 ) < z ) )
11 3 10 syl3an1
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( ( sup ( A , RR , < ) - 1 ) < sup ( A , RR , < ) <-> E. z e. A ( sup ( A , RR , < ) - 1 ) < z ) )
12 6 11 mpbid
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. z e. A ( sup ( A , RR , < ) - 1 ) < z )
13 simpl1
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> A C_ ZZ )
14 13 sselda
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> w e. ZZ )
15 1 14 sselid
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> w e. RR )
16 5 adantr
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> sup ( A , RR , < ) e. RR )
17 16 adantr
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> sup ( A , RR , < ) e. RR )
18 simprl
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> z e. A )
19 13 18 sseldd
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> z e. ZZ )
20 zre
 |-  ( z e. ZZ -> z e. RR )
21 19 20 syl
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> z e. RR )
22 peano2re
 |-  ( z e. RR -> ( z + 1 ) e. RR )
23 21 22 syl
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> ( z + 1 ) e. RR )
24 23 adantr
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> ( z + 1 ) e. RR )
25 suprub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ w e. A ) -> w <_ sup ( A , RR , < ) )
26 3 25 syl3anl1
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ w e. A ) -> w <_ sup ( A , RR , < ) )
27 26 adantlr
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> w <_ sup ( A , RR , < ) )
28 simprr
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> ( sup ( A , RR , < ) - 1 ) < z )
29 1red
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> 1 e. RR )
30 16 29 21 ltsubaddd
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> ( ( sup ( A , RR , < ) - 1 ) < z <-> sup ( A , RR , < ) < ( z + 1 ) ) )
31 28 30 mpbid
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> sup ( A , RR , < ) < ( z + 1 ) )
32 31 adantr
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> sup ( A , RR , < ) < ( z + 1 ) )
33 15 17 24 27 32 lelttrd
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> w < ( z + 1 ) )
34 19 adantr
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> z e. ZZ )
35 zleltp1
 |-  ( ( w e. ZZ /\ z e. ZZ ) -> ( w <_ z <-> w < ( z + 1 ) ) )
36 14 34 35 syl2anc
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> ( w <_ z <-> w < ( z + 1 ) ) )
37 33 36 mpbird
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) /\ w e. A ) -> w <_ z )
38 37 ralrimiva
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> A. w e. A w <_ z )
39 suprleub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. RR ) -> ( sup ( A , RR , < ) <_ z <-> A. w e. A w <_ z ) )
40 3 39 syl3anl1
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. RR ) -> ( sup ( A , RR , < ) <_ z <-> A. w e. A w <_ z ) )
41 21 40 syldan
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> ( sup ( A , RR , < ) <_ z <-> A. w e. A w <_ z ) )
42 38 41 mpbird
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> sup ( A , RR , < ) <_ z )
43 suprub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> z <_ sup ( A , RR , < ) )
44 3 43 syl3anl1
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ z e. A ) -> z <_ sup ( A , RR , < ) )
45 44 adantrr
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> z <_ sup ( A , RR , < ) )
46 16 21 letri3d
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> ( sup ( A , RR , < ) = z <-> ( sup ( A , RR , < ) <_ z /\ z <_ sup ( A , RR , < ) ) ) )
47 42 45 46 mpbir2and
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> sup ( A , RR , < ) = z )
48 47 18 eqeltrd
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( z e. A /\ ( sup ( A , RR , < ) - 1 ) < z ) ) -> sup ( A , RR , < ) e. A )
49 12 48 rexlimddv
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. A )