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

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 )