Step |
Hyp |
Ref |
Expression |
1 |
|
pnfxr |
|- +oo e. RR* |
2 |
|
icossre |
|- ( ( A e. RR /\ +oo e. RR* ) -> ( A [,) +oo ) C_ RR ) |
3 |
1 2
|
mpan2 |
|- ( A e. RR -> ( A [,) +oo ) C_ RR ) |
4 |
3
|
adantr |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( A [,) +oo ) C_ RR ) |
5 |
|
ovolge0 |
|- ( ( A [,) +oo ) C_ RR -> 0 <_ ( vol* ` ( A [,) +oo ) ) ) |
6 |
4 5
|
syl |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> 0 <_ ( vol* ` ( A [,) +oo ) ) ) |
7 |
|
mnflt0 |
|- -oo < 0 |
8 |
|
mnfxr |
|- -oo e. RR* |
9 |
|
0xr |
|- 0 e. RR* |
10 |
|
ovolcl |
|- ( ( A [,) +oo ) C_ RR -> ( vol* ` ( A [,) +oo ) ) e. RR* ) |
11 |
3 10
|
syl |
|- ( A e. RR -> ( vol* ` ( A [,) +oo ) ) e. RR* ) |
12 |
11
|
adantr |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) e. RR* ) |
13 |
|
xrltletr |
|- ( ( -oo e. RR* /\ 0 e. RR* /\ ( vol* ` ( A [,) +oo ) ) e. RR* ) -> ( ( -oo < 0 /\ 0 <_ ( vol* ` ( A [,) +oo ) ) ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) ) |
14 |
8 9 12 13
|
mp3an12i |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( -oo < 0 /\ 0 <_ ( vol* ` ( A [,) +oo ) ) ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) ) |
15 |
7 14
|
mpani |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( 0 <_ ( vol* ` ( A [,) +oo ) ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) ) |
16 |
6 15
|
mpd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> -oo < ( vol* ` ( A [,) +oo ) ) ) |
17 |
|
simpr |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) < +oo ) |
18 |
|
xrrebnd |
|- ( ( vol* ` ( A [,) +oo ) ) e. RR* -> ( ( vol* ` ( A [,) +oo ) ) e. RR <-> ( -oo < ( vol* ` ( A [,) +oo ) ) /\ ( vol* ` ( A [,) +oo ) ) < +oo ) ) ) |
19 |
12 18
|
syl |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) e. RR <-> ( -oo < ( vol* ` ( A [,) +oo ) ) /\ ( vol* ` ( A [,) +oo ) ) < +oo ) ) ) |
20 |
16 17 19
|
mpbir2and |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) e. RR ) |
21 |
20
|
ltp1d |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) < ( ( vol* ` ( A [,) +oo ) ) + 1 ) ) |
22 |
|
peano2re |
|- ( ( vol* ` ( A [,) +oo ) ) e. RR -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) e. RR ) |
23 |
20 22
|
syl |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) e. RR ) |
24 |
|
simpl |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> A e. RR ) |
25 |
23 24
|
readdcld |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) e. RR ) |
26 |
|
0red |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> 0 e. RR ) |
27 |
20
|
lep1d |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,) +oo ) ) <_ ( ( vol* ` ( A [,) +oo ) ) + 1 ) ) |
28 |
26 20 23 6 27
|
letrd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> 0 <_ ( ( vol* ` ( A [,) +oo ) ) + 1 ) ) |
29 |
24 23
|
addge02d |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( 0 <_ ( ( vol* ` ( A [,) +oo ) ) + 1 ) <-> A <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) |
30 |
28 29
|
mpbid |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> A <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) |
31 |
|
ovolicc |
|- ( ( A e. RR /\ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) e. RR /\ A <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) = ( ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) - A ) ) |
32 |
24 25 30 31
|
syl3anc |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) = ( ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) - A ) ) |
33 |
23
|
recnd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) e. CC ) |
34 |
24
|
recnd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> A e. CC ) |
35 |
33 34
|
pncand |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) - A ) = ( ( vol* ` ( A [,) +oo ) ) + 1 ) ) |
36 |
32 35
|
eqtrd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) = ( ( vol* ` ( A [,) +oo ) ) + 1 ) ) |
37 |
|
elicc2 |
|- ( ( A e. RR /\ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) e. RR ) -> ( x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) <-> ( x e. RR /\ A <_ x /\ x <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) ) |
38 |
24 25 37
|
syl2anc |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) <-> ( x e. RR /\ A <_ x /\ x <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) ) |
39 |
38
|
biimpa |
|- ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> ( x e. RR /\ A <_ x /\ x <_ ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) |
40 |
39
|
simp1d |
|- ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> x e. RR ) |
41 |
39
|
simp2d |
|- ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> A <_ x ) |
42 |
|
elicopnf |
|- ( A e. RR -> ( x e. ( A [,) +oo ) <-> ( x e. RR /\ A <_ x ) ) ) |
43 |
42
|
ad2antrr |
|- ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> ( x e. ( A [,) +oo ) <-> ( x e. RR /\ A <_ x ) ) ) |
44 |
40 41 43
|
mpbir2and |
|- ( ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) /\ x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) -> x e. ( A [,) +oo ) ) |
45 |
44
|
ex |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( x e. ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) -> x e. ( A [,) +oo ) ) ) |
46 |
45
|
ssrdv |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) C_ ( A [,) +oo ) ) |
47 |
|
ovolss |
|- ( ( ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) C_ ( A [,) +oo ) /\ ( A [,) +oo ) C_ RR ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) <_ ( vol* ` ( A [,) +oo ) ) ) |
48 |
46 4 47
|
syl2anc |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( vol* ` ( A [,] ( ( ( vol* ` ( A [,) +oo ) ) + 1 ) + A ) ) ) <_ ( vol* ` ( A [,) +oo ) ) ) |
49 |
36 48
|
eqbrtrrd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> ( ( vol* ` ( A [,) +oo ) ) + 1 ) <_ ( vol* ` ( A [,) +oo ) ) ) |
50 |
23 20 49
|
lensymd |
|- ( ( A e. RR /\ ( vol* ` ( A [,) +oo ) ) < +oo ) -> -. ( vol* ` ( A [,) +oo ) ) < ( ( vol* ` ( A [,) +oo ) ) + 1 ) ) |
51 |
21 50
|
pm2.65da |
|- ( A e. RR -> -. ( vol* ` ( A [,) +oo ) ) < +oo ) |
52 |
|
nltpnft |
|- ( ( vol* ` ( A [,) +oo ) ) e. RR* -> ( ( vol* ` ( A [,) +oo ) ) = +oo <-> -. ( vol* ` ( A [,) +oo ) ) < +oo ) ) |
53 |
11 52
|
syl |
|- ( A e. RR -> ( ( vol* ` ( A [,) +oo ) ) = +oo <-> -. ( vol* ` ( A [,) +oo ) ) < +oo ) ) |
54 |
51 53
|
mpbird |
|- ( A e. RR -> ( vol* ` ( A [,) +oo ) ) = +oo ) |