Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> B < ( vol ` A ) ) |
2 |
|
rexr |
|- ( B e. RR -> B e. RR* ) |
3 |
2
|
3ad2ant2 |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> B e. RR* ) |
4 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
5 |
|
volf |
|- vol : dom vol --> ( 0 [,] +oo ) |
6 |
5
|
ffvelrni |
|- ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) ) |
7 |
4 6
|
sselid |
|- ( A e. dom vol -> ( vol ` A ) e. RR* ) |
8 |
7
|
3ad2ant1 |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` A ) e. RR* ) |
9 |
|
xrltnle |
|- ( ( B e. RR* /\ ( vol ` A ) e. RR* ) -> ( B < ( vol ` A ) <-> -. ( vol ` A ) <_ B ) ) |
10 |
3 8 9
|
syl2anc |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( B < ( vol ` A ) <-> -. ( vol ` A ) <_ B ) ) |
11 |
1 10
|
mpbid |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> -. ( vol ` A ) <_ B ) |
12 |
|
negeq |
|- ( m = n -> -u m = -u n ) |
13 |
|
id |
|- ( m = n -> m = n ) |
14 |
12 13
|
oveq12d |
|- ( m = n -> ( -u m [,] m ) = ( -u n [,] n ) ) |
15 |
14
|
ineq2d |
|- ( m = n -> ( A i^i ( -u m [,] m ) ) = ( A i^i ( -u n [,] n ) ) ) |
16 |
|
eqid |
|- ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) = ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) |
17 |
|
ovex |
|- ( -u n [,] n ) e. _V |
18 |
17
|
inex2 |
|- ( A i^i ( -u n [,] n ) ) e. _V |
19 |
15 16 18
|
fvmpt |
|- ( n e. NN -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = ( A i^i ( -u n [,] n ) ) ) |
20 |
19
|
iuneq2i |
|- U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = U_ n e. NN ( A i^i ( -u n [,] n ) ) |
21 |
|
iunin2 |
|- U_ n e. NN ( A i^i ( -u n [,] n ) ) = ( A i^i U_ n e. NN ( -u n [,] n ) ) |
22 |
20 21
|
eqtri |
|- U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = ( A i^i U_ n e. NN ( -u n [,] n ) ) |
23 |
|
simpl1 |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> A e. dom vol ) |
24 |
|
nnre |
|- ( n e. NN -> n e. RR ) |
25 |
24
|
adantl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> n e. RR ) |
26 |
25
|
renegcld |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> -u n e. RR ) |
27 |
|
iccmbl |
|- ( ( -u n e. RR /\ n e. RR ) -> ( -u n [,] n ) e. dom vol ) |
28 |
26 25 27
|
syl2anc |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( -u n [,] n ) e. dom vol ) |
29 |
|
inmbl |
|- ( ( A e. dom vol /\ ( -u n [,] n ) e. dom vol ) -> ( A i^i ( -u n [,] n ) ) e. dom vol ) |
30 |
23 28 29
|
syl2anc |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( A i^i ( -u n [,] n ) ) e. dom vol ) |
31 |
15
|
cbvmptv |
|- ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) = ( n e. NN |-> ( A i^i ( -u n [,] n ) ) ) |
32 |
30 31
|
fmptd |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) : NN --> dom vol ) |
33 |
32
|
ffnd |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) Fn NN ) |
34 |
|
fniunfv |
|- ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) Fn NN -> U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) |
35 |
33 34
|
syl |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) |
36 |
|
mblss |
|- ( A e. dom vol -> A C_ RR ) |
37 |
36
|
3ad2ant1 |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> A C_ RR ) |
38 |
37
|
sselda |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ x e. A ) -> x e. RR ) |
39 |
|
recn |
|- ( x e. RR -> x e. CC ) |
40 |
39
|
abscld |
|- ( x e. RR -> ( abs ` x ) e. RR ) |
41 |
|
arch |
|- ( ( abs ` x ) e. RR -> E. n e. NN ( abs ` x ) < n ) |
42 |
40 41
|
syl |
|- ( x e. RR -> E. n e. NN ( abs ` x ) < n ) |
43 |
|
ltle |
|- ( ( ( abs ` x ) e. RR /\ n e. RR ) -> ( ( abs ` x ) < n -> ( abs ` x ) <_ n ) ) |
44 |
40 24 43
|
syl2an |
|- ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) < n -> ( abs ` x ) <_ n ) ) |
45 |
|
id |
|- ( ( x e. RR /\ -u n <_ x /\ x <_ n ) -> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) |
46 |
45
|
3expib |
|- ( x e. RR -> ( ( -u n <_ x /\ x <_ n ) -> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) ) |
47 |
46
|
adantr |
|- ( ( x e. RR /\ n e. NN ) -> ( ( -u n <_ x /\ x <_ n ) -> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) ) |
48 |
|
absle |
|- ( ( x e. RR /\ n e. RR ) -> ( ( abs ` x ) <_ n <-> ( -u n <_ x /\ x <_ n ) ) ) |
49 |
24 48
|
sylan2 |
|- ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) <_ n <-> ( -u n <_ x /\ x <_ n ) ) ) |
50 |
24
|
adantl |
|- ( ( x e. RR /\ n e. NN ) -> n e. RR ) |
51 |
50
|
renegcld |
|- ( ( x e. RR /\ n e. NN ) -> -u n e. RR ) |
52 |
|
elicc2 |
|- ( ( -u n e. RR /\ n e. RR ) -> ( x e. ( -u n [,] n ) <-> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) ) |
53 |
51 50 52
|
syl2anc |
|- ( ( x e. RR /\ n e. NN ) -> ( x e. ( -u n [,] n ) <-> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) ) |
54 |
47 49 53
|
3imtr4d |
|- ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) <_ n -> x e. ( -u n [,] n ) ) ) |
55 |
44 54
|
syld |
|- ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) < n -> x e. ( -u n [,] n ) ) ) |
56 |
55
|
reximdva |
|- ( x e. RR -> ( E. n e. NN ( abs ` x ) < n -> E. n e. NN x e. ( -u n [,] n ) ) ) |
57 |
42 56
|
mpd |
|- ( x e. RR -> E. n e. NN x e. ( -u n [,] n ) ) |
58 |
38 57
|
syl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ x e. A ) -> E. n e. NN x e. ( -u n [,] n ) ) |
59 |
58
|
ex |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( x e. A -> E. n e. NN x e. ( -u n [,] n ) ) ) |
60 |
|
eliun |
|- ( x e. U_ n e. NN ( -u n [,] n ) <-> E. n e. NN x e. ( -u n [,] n ) ) |
61 |
59 60
|
syl6ibr |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( x e. A -> x e. U_ n e. NN ( -u n [,] n ) ) ) |
62 |
61
|
ssrdv |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> A C_ U_ n e. NN ( -u n [,] n ) ) |
63 |
|
df-ss |
|- ( A C_ U_ n e. NN ( -u n [,] n ) <-> ( A i^i U_ n e. NN ( -u n [,] n ) ) = A ) |
64 |
62 63
|
sylib |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A i^i U_ n e. NN ( -u n [,] n ) ) = A ) |
65 |
22 35 64
|
3eqtr3a |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) = A ) |
66 |
65
|
fveq2d |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) = ( vol ` A ) ) |
67 |
|
peano2re |
|- ( n e. RR -> ( n + 1 ) e. RR ) |
68 |
25 67
|
syl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( n + 1 ) e. RR ) |
69 |
68
|
renegcld |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> -u ( n + 1 ) e. RR ) |
70 |
25
|
lep1d |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> n <_ ( n + 1 ) ) |
71 |
25 68
|
lenegd |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( n <_ ( n + 1 ) <-> -u ( n + 1 ) <_ -u n ) ) |
72 |
70 71
|
mpbid |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> -u ( n + 1 ) <_ -u n ) |
73 |
|
iccss |
|- ( ( ( -u ( n + 1 ) e. RR /\ ( n + 1 ) e. RR ) /\ ( -u ( n + 1 ) <_ -u n /\ n <_ ( n + 1 ) ) ) -> ( -u n [,] n ) C_ ( -u ( n + 1 ) [,] ( n + 1 ) ) ) |
74 |
69 68 72 70 73
|
syl22anc |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( -u n [,] n ) C_ ( -u ( n + 1 ) [,] ( n + 1 ) ) ) |
75 |
|
sslin |
|- ( ( -u n [,] n ) C_ ( -u ( n + 1 ) [,] ( n + 1 ) ) -> ( A i^i ( -u n [,] n ) ) C_ ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) ) |
76 |
74 75
|
syl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( A i^i ( -u n [,] n ) ) C_ ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) ) |
77 |
19
|
adantl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = ( A i^i ( -u n [,] n ) ) ) |
78 |
|
peano2nn |
|- ( n e. NN -> ( n + 1 ) e. NN ) |
79 |
78
|
adantl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( n + 1 ) e. NN ) |
80 |
|
negeq |
|- ( m = ( n + 1 ) -> -u m = -u ( n + 1 ) ) |
81 |
|
id |
|- ( m = ( n + 1 ) -> m = ( n + 1 ) ) |
82 |
80 81
|
oveq12d |
|- ( m = ( n + 1 ) -> ( -u m [,] m ) = ( -u ( n + 1 ) [,] ( n + 1 ) ) ) |
83 |
82
|
ineq2d |
|- ( m = ( n + 1 ) -> ( A i^i ( -u m [,] m ) ) = ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) ) |
84 |
|
ovex |
|- ( -u ( n + 1 ) [,] ( n + 1 ) ) e. _V |
85 |
84
|
inex2 |
|- ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) e. _V |
86 |
83 16 85
|
fvmpt |
|- ( ( n + 1 ) e. NN -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) = ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) ) |
87 |
79 86
|
syl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) = ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) ) |
88 |
76 77 87
|
3sstr4d |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) C_ ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) ) |
89 |
88
|
ralrimiva |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> A. n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) C_ ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) ) |
90 |
|
volsup |
|- ( ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) : NN --> dom vol /\ A. n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) C_ ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) ) -> ( vol ` U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) = sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) ) |
91 |
32 89 90
|
syl2anc |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) = sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) ) |
92 |
66 91
|
eqtr3d |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` A ) = sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) ) |
93 |
92
|
breq1d |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( ( vol ` A ) <_ B <-> sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) <_ B ) ) |
94 |
|
imassrn |
|- ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) C_ ran vol |
95 |
|
frn |
|- ( vol : dom vol --> ( 0 [,] +oo ) -> ran vol C_ ( 0 [,] +oo ) ) |
96 |
5 95
|
ax-mp |
|- ran vol C_ ( 0 [,] +oo ) |
97 |
96 4
|
sstri |
|- ran vol C_ RR* |
98 |
94 97
|
sstri |
|- ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) C_ RR* |
99 |
|
supxrleub |
|- ( ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) C_ RR* /\ B e. RR* ) -> ( sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) <_ B <-> A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B ) ) |
100 |
98 3 99
|
sylancr |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) <_ B <-> A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B ) ) |
101 |
|
ffn |
|- ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol ) |
102 |
5 101
|
ax-mp |
|- vol Fn dom vol |
103 |
32
|
frnd |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) C_ dom vol ) |
104 |
|
breq1 |
|- ( n = ( vol ` z ) -> ( n <_ B <-> ( vol ` z ) <_ B ) ) |
105 |
104
|
ralima |
|- ( ( vol Fn dom vol /\ ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) C_ dom vol ) -> ( A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B <-> A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B ) ) |
106 |
102 103 105
|
sylancr |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B <-> A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B ) ) |
107 |
|
fveq2 |
|- ( z = ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) -> ( vol ` z ) = ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) ) |
108 |
107
|
breq1d |
|- ( z = ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) -> ( ( vol ` z ) <_ B <-> ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B ) ) |
109 |
108
|
ralrn |
|- ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) Fn NN -> ( A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B <-> A. n e. NN ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B ) ) |
110 |
33 109
|
syl |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B <-> A. n e. NN ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B ) ) |
111 |
19
|
fveq2d |
|- ( n e. NN -> ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) = ( vol ` ( A i^i ( -u n [,] n ) ) ) ) |
112 |
111
|
breq1d |
|- ( n e. NN -> ( ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B <-> ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
113 |
112
|
ralbiia |
|- ( A. n e. NN ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) |
114 |
110 113
|
bitrdi |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
115 |
106 114
|
bitrd |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
116 |
93 100 115
|
3bitrd |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( ( vol ` A ) <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
117 |
11 116
|
mtbid |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> -. A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) |
118 |
|
rexnal |
|- ( E. n e. NN -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B <-> -. A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) |
119 |
117 118
|
sylibr |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> E. n e. NN -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) |
120 |
3
|
adantr |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> B e. RR* ) |
121 |
5
|
ffvelrni |
|- ( ( A i^i ( -u n [,] n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. ( 0 [,] +oo ) ) |
122 |
4 121
|
sselid |
|- ( ( A i^i ( -u n [,] n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* ) |
123 |
30 122
|
syl |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* ) |
124 |
|
xrltnle |
|- ( ( B e. RR* /\ ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* ) -> ( B < ( vol ` ( A i^i ( -u n [,] n ) ) ) <-> -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
125 |
120 123 124
|
syl2anc |
|- ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( B < ( vol ` ( A i^i ( -u n [,] n ) ) ) <-> -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
126 |
125
|
rexbidva |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) <-> E. n e. NN -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) ) |
127 |
119 126
|
mpbird |
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) |