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 ) |