Step |
Hyp |
Ref |
Expression |
1 |
|
infrpge.xph |
|- F/ x ph |
2 |
|
infrpge.a |
|- ( ph -> A C_ RR* ) |
3 |
|
infrpge.an0 |
|- ( ph -> A =/= (/) ) |
4 |
|
infrpge.bnd |
|- ( ph -> E. x e. RR A. y e. A x <_ y ) |
5 |
|
infrpge.b |
|- ( ph -> B e. RR+ ) |
6 |
|
n0 |
|- ( A =/= (/) <-> E. z z e. A ) |
7 |
6
|
biimpi |
|- ( A =/= (/) -> E. z z e. A ) |
8 |
3 7
|
syl |
|- ( ph -> E. z z e. A ) |
9 |
8
|
adantr |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> E. z z e. A ) |
10 |
|
nfv |
|- F/ z ( ph /\ inf ( A , RR* , < ) = +oo ) |
11 |
|
simpr |
|- ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> z e. A ) |
12 |
2
|
adantr |
|- ( ( ph /\ z e. A ) -> A C_ RR* ) |
13 |
|
simpr |
|- ( ( ph /\ z e. A ) -> z e. A ) |
14 |
12 13
|
sseldd |
|- ( ( ph /\ z e. A ) -> z e. RR* ) |
15 |
|
pnfge |
|- ( z e. RR* -> z <_ +oo ) |
16 |
14 15
|
syl |
|- ( ( ph /\ z e. A ) -> z <_ +oo ) |
17 |
16
|
adantlr |
|- ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> z <_ +oo ) |
18 |
|
oveq1 |
|- ( inf ( A , RR* , < ) = +oo -> ( inf ( A , RR* , < ) +e B ) = ( +oo +e B ) ) |
19 |
18
|
adantl |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( inf ( A , RR* , < ) +e B ) = ( +oo +e B ) ) |
20 |
5
|
rpxrd |
|- ( ph -> B e. RR* ) |
21 |
5
|
rpred |
|- ( ph -> B e. RR ) |
22 |
|
renemnf |
|- ( B e. RR -> B =/= -oo ) |
23 |
21 22
|
syl |
|- ( ph -> B =/= -oo ) |
24 |
|
xaddpnf2 |
|- ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo ) |
25 |
20 23 24
|
syl2anc |
|- ( ph -> ( +oo +e B ) = +oo ) |
26 |
25
|
adantr |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( +oo +e B ) = +oo ) |
27 |
19 26
|
eqtr2d |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> +oo = ( inf ( A , RR* , < ) +e B ) ) |
28 |
27
|
adantr |
|- ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> +oo = ( inf ( A , RR* , < ) +e B ) ) |
29 |
17 28
|
breqtrd |
|- ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> z <_ ( inf ( A , RR* , < ) +e B ) ) |
30 |
11 29
|
jca |
|- ( ( ( ph /\ inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) |
31 |
30
|
ex |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( z e. A -> ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) ) |
32 |
10 31
|
eximd |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> ( E. z z e. A -> E. z ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) ) |
33 |
9 32
|
mpd |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> E. z ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) |
34 |
|
df-rex |
|- ( E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) <-> E. z ( z e. A /\ z <_ ( inf ( A , RR* , < ) +e B ) ) ) |
35 |
33 34
|
sylibr |
|- ( ( ph /\ inf ( A , RR* , < ) = +oo ) -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) ) |
36 |
|
simpl |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ph ) |
37 |
|
nfv |
|- F/ x -oo < inf ( A , RR* , < ) |
38 |
|
mnfxr |
|- -oo e. RR* |
39 |
38
|
a1i |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> -oo e. RR* ) |
40 |
|
rexr |
|- ( x e. RR -> x e. RR* ) |
41 |
40
|
3ad2ant2 |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> x e. RR* ) |
42 |
|
infxrcl |
|- ( A C_ RR* -> inf ( A , RR* , < ) e. RR* ) |
43 |
2 42
|
syl |
|- ( ph -> inf ( A , RR* , < ) e. RR* ) |
44 |
43
|
3ad2ant1 |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> inf ( A , RR* , < ) e. RR* ) |
45 |
|
mnflt |
|- ( x e. RR -> -oo < x ) |
46 |
45
|
3ad2ant2 |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> -oo < x ) |
47 |
|
simp3 |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> A. y e. A x <_ y ) |
48 |
2
|
adantr |
|- ( ( ph /\ x e. RR ) -> A C_ RR* ) |
49 |
40
|
adantl |
|- ( ( ph /\ x e. RR ) -> x e. RR* ) |
50 |
|
infxrgelb |
|- ( ( A C_ RR* /\ x e. RR* ) -> ( x <_ inf ( A , RR* , < ) <-> A. y e. A x <_ y ) ) |
51 |
48 49 50
|
syl2anc |
|- ( ( ph /\ x e. RR ) -> ( x <_ inf ( A , RR* , < ) <-> A. y e. A x <_ y ) ) |
52 |
51
|
3adant3 |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> ( x <_ inf ( A , RR* , < ) <-> A. y e. A x <_ y ) ) |
53 |
47 52
|
mpbird |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> x <_ inf ( A , RR* , < ) ) |
54 |
39 41 44 46 53
|
xrltletrd |
|- ( ( ph /\ x e. RR /\ A. y e. A x <_ y ) -> -oo < inf ( A , RR* , < ) ) |
55 |
54
|
3exp |
|- ( ph -> ( x e. RR -> ( A. y e. A x <_ y -> -oo < inf ( A , RR* , < ) ) ) ) |
56 |
1 37 55
|
rexlimd |
|- ( ph -> ( E. x e. RR A. y e. A x <_ y -> -oo < inf ( A , RR* , < ) ) ) |
57 |
4 56
|
mpd |
|- ( ph -> -oo < inf ( A , RR* , < ) ) |
58 |
57
|
adantr |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> -oo < inf ( A , RR* , < ) ) |
59 |
|
neqne |
|- ( -. inf ( A , RR* , < ) = +oo -> inf ( A , RR* , < ) =/= +oo ) |
60 |
59
|
adantl |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) =/= +oo ) |
61 |
43
|
adantr |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) e. RR* ) |
62 |
60 61
|
nepnfltpnf |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) < +oo ) |
63 |
58 62
|
jca |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) |
64 |
|
xrrebnd |
|- ( inf ( A , RR* , < ) e. RR* -> ( inf ( A , RR* , < ) e. RR <-> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) ) |
65 |
43 64
|
syl |
|- ( ph -> ( inf ( A , RR* , < ) e. RR <-> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) ) |
66 |
65
|
adantr |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ( inf ( A , RR* , < ) e. RR <-> ( -oo < inf ( A , RR* , < ) /\ inf ( A , RR* , < ) < +oo ) ) ) |
67 |
63 66
|
mpbird |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> inf ( A , RR* , < ) e. RR ) |
68 |
|
simpr |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) e. RR ) |
69 |
5
|
adantr |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> B e. RR+ ) |
70 |
68 69
|
ltaddrpd |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) < ( inf ( A , RR* , < ) + B ) ) |
71 |
21
|
adantr |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> B e. RR ) |
72 |
|
rexadd |
|- ( ( inf ( A , RR* , < ) e. RR /\ B e. RR ) -> ( inf ( A , RR* , < ) +e B ) = ( inf ( A , RR* , < ) + B ) ) |
73 |
68 71 72
|
syl2anc |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) +e B ) = ( inf ( A , RR* , < ) + B ) ) |
74 |
73
|
eqcomd |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) + B ) = ( inf ( A , RR* , < ) +e B ) ) |
75 |
70 74
|
breqtrd |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) < ( inf ( A , RR* , < ) +e B ) ) |
76 |
43
|
adantr |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> inf ( A , RR* , < ) e. RR* ) |
77 |
43 20
|
xaddcld |
|- ( ph -> ( inf ( A , RR* , < ) +e B ) e. RR* ) |
78 |
77
|
adantr |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) +e B ) e. RR* ) |
79 |
|
xrltnle |
|- ( ( inf ( A , RR* , < ) e. RR* /\ ( inf ( A , RR* , < ) +e B ) e. RR* ) -> ( inf ( A , RR* , < ) < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) ) |
80 |
76 78 79
|
syl2anc |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> ( inf ( A , RR* , < ) < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) ) |
81 |
75 80
|
mpbid |
|- ( ( ph /\ inf ( A , RR* , < ) e. RR ) -> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) |
82 |
36 67 81
|
syl2anc |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) |
83 |
|
simpr |
|- ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) |
84 |
|
simpl |
|- ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> ph ) |
85 |
|
infxrgelb |
|- ( ( A C_ RR* /\ ( inf ( A , RR* , < ) +e B ) e. RR* ) -> ( ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) <-> A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) ) |
86 |
2 77 85
|
syl2anc |
|- ( ph -> ( ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) <-> A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) ) |
87 |
84 86
|
syl |
|- ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> ( ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) <-> A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) ) |
88 |
83 87
|
mtbid |
|- ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> -. A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) |
89 |
|
rexnal |
|- ( E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z <-> -. A. z e. A ( inf ( A , RR* , < ) +e B ) <_ z ) |
90 |
88 89
|
sylibr |
|- ( ( ph /\ -. ( inf ( A , RR* , < ) +e B ) <_ inf ( A , RR* , < ) ) -> E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z ) |
91 |
36 82 90
|
syl2anc |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z ) |
92 |
14
|
adantr |
|- ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> z e. RR* ) |
93 |
77
|
ad2antrr |
|- ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> ( inf ( A , RR* , < ) +e B ) e. RR* ) |
94 |
|
simpr |
|- ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> -. ( inf ( A , RR* , < ) +e B ) <_ z ) |
95 |
|
xrltnle |
|- ( ( z e. RR* /\ ( inf ( A , RR* , < ) +e B ) e. RR* ) -> ( z < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ z ) ) |
96 |
92 93 95
|
syl2anc |
|- ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> ( z < ( inf ( A , RR* , < ) +e B ) <-> -. ( inf ( A , RR* , < ) +e B ) <_ z ) ) |
97 |
94 96
|
mpbird |
|- ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> z < ( inf ( A , RR* , < ) +e B ) ) |
98 |
92 93 97
|
xrltled |
|- ( ( ( ph /\ z e. A ) /\ -. ( inf ( A , RR* , < ) +e B ) <_ z ) -> z <_ ( inf ( A , RR* , < ) +e B ) ) |
99 |
98
|
ex |
|- ( ( ph /\ z e. A ) -> ( -. ( inf ( A , RR* , < ) +e B ) <_ z -> z <_ ( inf ( A , RR* , < ) +e B ) ) ) |
100 |
99
|
adantlr |
|- ( ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) /\ z e. A ) -> ( -. ( inf ( A , RR* , < ) +e B ) <_ z -> z <_ ( inf ( A , RR* , < ) +e B ) ) ) |
101 |
100
|
reximdva |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> ( E. z e. A -. ( inf ( A , RR* , < ) +e B ) <_ z -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) ) ) |
102 |
91 101
|
mpd |
|- ( ( ph /\ -. inf ( A , RR* , < ) = +oo ) -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) ) |
103 |
35 102
|
pm2.61dan |
|- ( ph -> E. z e. A z <_ ( inf ( A , RR* , < ) +e B ) ) |