Step |
Hyp |
Ref |
Expression |
1 |
|
itg2mono.1 |
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) ) |
2 |
|
itg2mono.2 |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn ) |
3 |
|
itg2mono.3 |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) ) |
4 |
|
itg2mono.4 |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) ) |
5 |
|
itg2mono.5 |
|- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y ) |
6 |
|
itg2mono.6 |
|- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) |
7 |
|
itg2mono.7 |
|- ( ph -> T e. ( 0 (,) 1 ) ) |
8 |
|
itg2mono.8 |
|- ( ph -> H e. dom S.1 ) |
9 |
|
itg2mono.9 |
|- ( ph -> H oR <_ G ) |
10 |
|
itg2mono.10 |
|- ( ph -> S e. RR ) |
11 |
|
itg2mono.11 |
|- A = ( n e. NN |-> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } ) |
12 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
13 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
14 |
|
simpr |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> x e. RR ) |
15 |
|
readdcl |
|- ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR ) |
16 |
15
|
adantl |
|- ( ( ( ph /\ n e. NN ) /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR ) |
17 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
18 |
|
fss |
|- ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` n ) : RR --> RR ) |
19 |
3 17 18
|
sylancl |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> RR ) |
20 |
|
0xr |
|- 0 e. RR* |
21 |
|
1xr |
|- 1 e. RR* |
22 |
|
elioo2 |
|- ( ( 0 e. RR* /\ 1 e. RR* ) -> ( T e. ( 0 (,) 1 ) <-> ( T e. RR /\ 0 < T /\ T < 1 ) ) ) |
23 |
20 21 22
|
mp2an |
|- ( T e. ( 0 (,) 1 ) <-> ( T e. RR /\ 0 < T /\ T < 1 ) ) |
24 |
7 23
|
sylib |
|- ( ph -> ( T e. RR /\ 0 < T /\ T < 1 ) ) |
25 |
24
|
simp1d |
|- ( ph -> T e. RR ) |
26 |
25
|
renegcld |
|- ( ph -> -u T e. RR ) |
27 |
8 26
|
i1fmulc |
|- ( ph -> ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 ) |
28 |
27
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 ) |
29 |
|
i1ff |
|- ( ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 -> ( ( RR X. { -u T } ) oF x. H ) : RR --> RR ) |
30 |
28 29
|
syl |
|- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) : RR --> RR ) |
31 |
|
reex |
|- RR e. _V |
32 |
31
|
a1i |
|- ( ( ph /\ n e. NN ) -> RR e. _V ) |
33 |
|
inidm |
|- ( RR i^i RR ) = RR |
34 |
16 19 30 32 32 33
|
off |
|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR ) |
35 |
34
|
adantr |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR ) |
36 |
35
|
ffnd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) Fn RR ) |
37 |
|
elpreima |
|- ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) Fn RR -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( x e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) ) ) |
38 |
36 37
|
syl |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( x e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) ) ) |
39 |
14 38
|
mpbirand |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) ) ) |
40 |
|
elioomnf |
|- ( 0 e. RR* -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) ) ) |
41 |
20 40
|
ax-mp |
|- ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) ) |
42 |
34
|
ffvelrnda |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR ) |
43 |
42
|
biantrurd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 <-> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. RR /\ ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) ) ) |
44 |
41 43
|
bitr4id |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) e. ( -oo (,) 0 ) <-> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 ) ) |
45 |
3
|
ffnd |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) Fn RR ) |
46 |
30
|
ffnd |
|- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) Fn RR ) |
47 |
|
eqidd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` x ) ) |
48 |
26
|
adantr |
|- ( ( ph /\ n e. NN ) -> -u T e. RR ) |
49 |
|
i1ff |
|- ( H e. dom S.1 -> H : RR --> RR ) |
50 |
8 49
|
syl |
|- ( ph -> H : RR --> RR ) |
51 |
50
|
ffnd |
|- ( ph -> H Fn RR ) |
52 |
51
|
adantr |
|- ( ( ph /\ n e. NN ) -> H Fn RR ) |
53 |
|
eqidd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( H ` x ) = ( H ` x ) ) |
54 |
32 48 52 53
|
ofc1 |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( RR X. { -u T } ) oF x. H ) ` x ) = ( -u T x. ( H ` x ) ) ) |
55 |
25
|
recnd |
|- ( ph -> T e. CC ) |
56 |
55
|
ad2antrr |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> T e. CC ) |
57 |
50
|
ffvelrnda |
|- ( ( ph /\ x e. RR ) -> ( H ` x ) e. RR ) |
58 |
57
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( H ` x ) e. RR ) |
59 |
58
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( H ` x ) e. CC ) |
60 |
56 59
|
mulneg1d |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( -u T x. ( H ` x ) ) = -u ( T x. ( H ` x ) ) ) |
61 |
54 60
|
eqtrd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( RR X. { -u T } ) oF x. H ) ` x ) = -u ( T x. ( H ` x ) ) ) |
62 |
45 46 32 32 33 47 61
|
ofval |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) = ( ( ( F ` n ) ` x ) + -u ( T x. ( H ` x ) ) ) ) |
63 |
19
|
ffvelrnda |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) e. RR ) |
64 |
63
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` n ) ` x ) e. CC ) |
65 |
25
|
adantr |
|- ( ( ph /\ x e. RR ) -> T e. RR ) |
66 |
65 57
|
remulcld |
|- ( ( ph /\ x e. RR ) -> ( T x. ( H ` x ) ) e. RR ) |
67 |
66
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( T x. ( H ` x ) ) e. RR ) |
68 |
67
|
recnd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( T x. ( H ` x ) ) e. CC ) |
69 |
64 68
|
negsubd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) ` x ) + -u ( T x. ( H ` x ) ) ) = ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) ) |
70 |
62 69
|
eqtrd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) = ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) ) |
71 |
70
|
breq1d |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 <-> ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) < 0 ) ) |
72 |
|
0red |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> 0 e. RR ) |
73 |
63 67 72
|
ltsubaddd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) ` x ) - ( T x. ( H ` x ) ) ) < 0 <-> ( ( F ` n ) ` x ) < ( 0 + ( T x. ( H ` x ) ) ) ) ) |
74 |
68
|
addid2d |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( 0 + ( T x. ( H ` x ) ) ) = ( T x. ( H ` x ) ) ) |
75 |
74
|
breq2d |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( F ` n ) ` x ) < ( 0 + ( T x. ( H ` x ) ) ) <-> ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) ) |
76 |
71 73 75
|
3bitrd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) ` x ) < 0 <-> ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) ) |
77 |
39 44 76
|
3bitrd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) ) |
78 |
77
|
notbid |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) <-> -. ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) ) |
79 |
|
eldif |
|- ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> ( x e. RR /\ -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) |
80 |
79
|
baib |
|- ( x e. RR -> ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) |
81 |
80
|
adantl |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> -. x e. ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) |
82 |
67 63
|
lenltd |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> -. ( ( F ` n ) ` x ) < ( T x. ( H ` x ) ) ) ) |
83 |
78 81 82
|
3bitr4d |
|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x e. ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) ) ) |
84 |
83
|
rabbi2dva |
|- ( ( ph /\ n e. NN ) -> ( RR i^i ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } ) |
85 |
|
rembl |
|- RR e. dom vol |
86 |
|
i1fmbf |
|- ( ( ( RR X. { -u T } ) oF x. H ) e. dom S.1 -> ( ( RR X. { -u T } ) oF x. H ) e. MblFn ) |
87 |
28 86
|
syl |
|- ( ( ph /\ n e. NN ) -> ( ( RR X. { -u T } ) oF x. H ) e. MblFn ) |
88 |
2 87
|
mbfadd |
|- ( ( ph /\ n e. NN ) -> ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) e. MblFn ) |
89 |
|
mbfima |
|- ( ( ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) e. MblFn /\ ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) : RR --> RR ) -> ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) e. dom vol ) |
90 |
88 34 89
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) e. dom vol ) |
91 |
|
cmmbl |
|- ( ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) e. dom vol -> ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) e. dom vol ) |
92 |
90 91
|
syl |
|- ( ( ph /\ n e. NN ) -> ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) e. dom vol ) |
93 |
|
inmbl |
|- ( ( RR e. dom vol /\ ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) e. dom vol ) -> ( RR i^i ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) e. dom vol ) |
94 |
85 92 93
|
sylancr |
|- ( ( ph /\ n e. NN ) -> ( RR i^i ( RR \ ( `' ( ( F ` n ) oF + ( ( RR X. { -u T } ) oF x. H ) ) " ( -oo (,) 0 ) ) ) ) e. dom vol ) |
95 |
84 94
|
eqeltrrd |
|- ( ( ph /\ n e. NN ) -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } e. dom vol ) |
96 |
95 11
|
fmptd |
|- ( ph -> A : NN --> dom vol ) |
97 |
4
|
ralrimiva |
|- ( ph -> A. n e. NN ( F ` n ) oR <_ ( F ` ( n + 1 ) ) ) |
98 |
|
fveq2 |
|- ( n = j -> ( F ` n ) = ( F ` j ) ) |
99 |
|
fvoveq1 |
|- ( n = j -> ( F ` ( n + 1 ) ) = ( F ` ( j + 1 ) ) ) |
100 |
98 99
|
breq12d |
|- ( n = j -> ( ( F ` n ) oR <_ ( F ` ( n + 1 ) ) <-> ( F ` j ) oR <_ ( F ` ( j + 1 ) ) ) ) |
101 |
100
|
cbvralvw |
|- ( A. n e. NN ( F ` n ) oR <_ ( F ` ( n + 1 ) ) <-> A. j e. NN ( F ` j ) oR <_ ( F ` ( j + 1 ) ) ) |
102 |
97 101
|
sylib |
|- ( ph -> A. j e. NN ( F ` j ) oR <_ ( F ` ( j + 1 ) ) ) |
103 |
102
|
r19.21bi |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) oR <_ ( F ` ( j + 1 ) ) ) |
104 |
3
|
ralrimiva |
|- ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) ) |
105 |
98
|
feq1d |
|- ( n = j -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` j ) : RR --> ( 0 [,) +oo ) ) ) |
106 |
105
|
cbvralvw |
|- ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) <-> A. j e. NN ( F ` j ) : RR --> ( 0 [,) +oo ) ) |
107 |
104 106
|
sylib |
|- ( ph -> A. j e. NN ( F ` j ) : RR --> ( 0 [,) +oo ) ) |
108 |
107
|
r19.21bi |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) : RR --> ( 0 [,) +oo ) ) |
109 |
108
|
ffnd |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) Fn RR ) |
110 |
|
peano2nn |
|- ( j e. NN -> ( j + 1 ) e. NN ) |
111 |
|
fveq2 |
|- ( n = ( j + 1 ) -> ( F ` n ) = ( F ` ( j + 1 ) ) ) |
112 |
111
|
feq1d |
|- ( n = ( j + 1 ) -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) ) ) |
113 |
112
|
rspccva |
|- ( ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( j + 1 ) e. NN ) -> ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) ) |
114 |
104 110 113
|
syl2an |
|- ( ( ph /\ j e. NN ) -> ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) ) |
115 |
114
|
ffnd |
|- ( ( ph /\ j e. NN ) -> ( F ` ( j + 1 ) ) Fn RR ) |
116 |
31
|
a1i |
|- ( ( ph /\ j e. NN ) -> RR e. _V ) |
117 |
|
eqidd |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` j ) ` x ) = ( ( F ` j ) ` x ) ) |
118 |
|
eqidd |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` ( j + 1 ) ) ` x ) = ( ( F ` ( j + 1 ) ) ` x ) ) |
119 |
109 115 116 116 33 117 118
|
ofrfval |
|- ( ( ph /\ j e. NN ) -> ( ( F ` j ) oR <_ ( F ` ( j + 1 ) ) <-> A. x e. RR ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) ) |
120 |
103 119
|
mpbid |
|- ( ( ph /\ j e. NN ) -> A. x e. RR ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) |
121 |
120
|
r19.21bi |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) |
122 |
25
|
ad2antrr |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> T e. RR ) |
123 |
50
|
adantr |
|- ( ( ph /\ j e. NN ) -> H : RR --> RR ) |
124 |
123
|
ffvelrnda |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( H ` x ) e. RR ) |
125 |
122 124
|
remulcld |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( T x. ( H ` x ) ) e. RR ) |
126 |
|
fss |
|- ( ( ( F ` j ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` j ) : RR --> RR ) |
127 |
108 17 126
|
sylancl |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) : RR --> RR ) |
128 |
127
|
ffvelrnda |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` j ) ` x ) e. RR ) |
129 |
|
fss |
|- ( ( ( F ` ( j + 1 ) ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> ( F ` ( j + 1 ) ) : RR --> RR ) |
130 |
114 17 129
|
sylancl |
|- ( ( ph /\ j e. NN ) -> ( F ` ( j + 1 ) ) : RR --> RR ) |
131 |
130
|
ffvelrnda |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( F ` ( j + 1 ) ) ` x ) e. RR ) |
132 |
|
letr |
|- ( ( ( T x. ( H ` x ) ) e. RR /\ ( ( F ` j ) ` x ) e. RR /\ ( ( F ` ( j + 1 ) ) ` x ) e. RR ) -> ( ( ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) /\ ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) -> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) ) |
133 |
125 128 131 132
|
syl3anc |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) /\ ( ( F ` j ) ` x ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) -> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) ) |
134 |
121 133
|
mpan2d |
|- ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) -> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) ) |
135 |
134
|
ss2rabdv |
|- ( ( ph /\ j e. NN ) -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } C_ { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } ) |
136 |
98
|
fveq1d |
|- ( n = j -> ( ( F ` n ) ` x ) = ( ( F ` j ) ` x ) ) |
137 |
136
|
breq2d |
|- ( n = j -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) ) |
138 |
137
|
rabbidv |
|- ( n = j -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } ) |
139 |
31
|
rabex |
|- { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } e. _V |
140 |
138 11 139
|
fvmpt |
|- ( j e. NN -> ( A ` j ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } ) |
141 |
140
|
adantl |
|- ( ( ph /\ j e. NN ) -> ( A ` j ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } ) |
142 |
110
|
adantl |
|- ( ( ph /\ j e. NN ) -> ( j + 1 ) e. NN ) |
143 |
111
|
fveq1d |
|- ( n = ( j + 1 ) -> ( ( F ` n ) ` x ) = ( ( F ` ( j + 1 ) ) ` x ) ) |
144 |
143
|
breq2d |
|- ( n = ( j + 1 ) -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) ) ) |
145 |
144
|
rabbidv |
|- ( n = ( j + 1 ) -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } ) |
146 |
31
|
rabex |
|- { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } e. _V |
147 |
145 11 146
|
fvmpt |
|- ( ( j + 1 ) e. NN -> ( A ` ( j + 1 ) ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } ) |
148 |
142 147
|
syl |
|- ( ( ph /\ j e. NN ) -> ( A ` ( j + 1 ) ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` ( j + 1 ) ) ` x ) } ) |
149 |
135 141 148
|
3sstr4d |
|- ( ( ph /\ j e. NN ) -> ( A ` j ) C_ ( A ` ( j + 1 ) ) ) |
150 |
66
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) e. RR ) |
151 |
57
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( H ` x ) e. RR ) |
152 |
63
|
an32s |
|- ( ( ( ph /\ x e. RR ) /\ n e. NN ) -> ( ( F ` n ) ` x ) e. RR ) |
153 |
152
|
fmpttd |
|- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) : NN --> RR ) |
154 |
153
|
frnd |
|- ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR ) |
155 |
|
1nn |
|- 1 e. NN |
156 |
|
eqid |
|- ( n e. NN |-> ( ( F ` n ) ` x ) ) = ( n e. NN |-> ( ( F ` n ) ` x ) ) |
157 |
156 152
|
dmmptd |
|- ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) = NN ) |
158 |
155 157
|
eleqtrrid |
|- ( ( ph /\ x e. RR ) -> 1 e. dom ( n e. NN |-> ( ( F ` n ) ` x ) ) ) |
159 |
158
|
ne0d |
|- ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) ) |
160 |
|
dm0rn0 |
|- ( dom ( n e. NN |-> ( ( F ` n ) ` x ) ) = (/) <-> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) = (/) ) |
161 |
160
|
necon3bii |
|- ( dom ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) <-> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) ) |
162 |
159 161
|
sylib |
|- ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) ) |
163 |
153
|
ffnd |
|- ( ( ph /\ x e. RR ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN ) |
164 |
|
breq1 |
|- ( z = ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) -> ( z <_ y <-> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) ) |
165 |
164
|
ralrn |
|- ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) ) |
166 |
163 165
|
syl |
|- ( ( ph /\ x e. RR ) -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y ) ) |
167 |
|
fveq2 |
|- ( n = m -> ( F ` n ) = ( F ` m ) ) |
168 |
167
|
fveq1d |
|- ( n = m -> ( ( F ` n ) ` x ) = ( ( F ` m ) ` x ) ) |
169 |
|
fvex |
|- ( ( F ` m ) ` x ) e. _V |
170 |
168 156 169
|
fvmpt |
|- ( m e. NN -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) ) |
171 |
170
|
breq1d |
|- ( m e. NN -> ( ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> ( ( F ` m ) ` x ) <_ y ) ) |
172 |
171
|
ralbiia |
|- ( A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> A. m e. NN ( ( F ` m ) ` x ) <_ y ) |
173 |
168
|
breq1d |
|- ( n = m -> ( ( ( F ` n ) ` x ) <_ y <-> ( ( F ` m ) ` x ) <_ y ) ) |
174 |
173
|
cbvralvw |
|- ( A. n e. NN ( ( F ` n ) ` x ) <_ y <-> A. m e. NN ( ( F ` m ) ` x ) <_ y ) |
175 |
172 174
|
bitr4i |
|- ( A. m e. NN ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` m ) <_ y <-> A. n e. NN ( ( F ` n ) ` x ) <_ y ) |
176 |
166 175
|
bitrdi |
|- ( ( ph /\ x e. RR ) -> ( A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> A. n e. NN ( ( F ` n ) ` x ) <_ y ) ) |
177 |
176
|
rexbidv |
|- ( ( ph /\ x e. RR ) -> ( E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y <-> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y ) ) |
178 |
5 177
|
mpbird |
|- ( ( ph /\ x e. RR ) -> E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) |
179 |
154 162 178
|
suprcld |
|- ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR ) |
180 |
179
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR ) |
181 |
24
|
simp3d |
|- ( ph -> T < 1 ) |
182 |
181
|
adantr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> T < 1 ) |
183 |
25
|
adantr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> T e. RR ) |
184 |
|
1red |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> 1 e. RR ) |
185 |
|
simprr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> 0 < ( H ` x ) ) |
186 |
|
ltmul1 |
|- ( ( T e. RR /\ 1 e. RR /\ ( ( H ` x ) e. RR /\ 0 < ( H ` x ) ) ) -> ( T < 1 <-> ( T x. ( H ` x ) ) < ( 1 x. ( H ` x ) ) ) ) |
187 |
183 184 151 185 186
|
syl112anc |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T < 1 <-> ( T x. ( H ` x ) ) < ( 1 x. ( H ` x ) ) ) ) |
188 |
182 187
|
mpbid |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) < ( 1 x. ( H ` x ) ) ) |
189 |
151
|
recnd |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( H ` x ) e. CC ) |
190 |
189
|
mulid2d |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( 1 x. ( H ` x ) ) = ( H ` x ) ) |
191 |
188 190
|
breqtrd |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) < ( H ` x ) ) |
192 |
179 1
|
fmptd |
|- ( ph -> G : RR --> RR ) |
193 |
192
|
ffnd |
|- ( ph -> G Fn RR ) |
194 |
31
|
a1i |
|- ( ph -> RR e. _V ) |
195 |
|
eqidd |
|- ( ( ph /\ y e. RR ) -> ( H ` y ) = ( H ` y ) ) |
196 |
|
fveq2 |
|- ( x = y -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` y ) ) |
197 |
196
|
mpteq2dv |
|- ( x = y -> ( n e. NN |-> ( ( F ` n ) ` x ) ) = ( n e. NN |-> ( ( F ` n ) ` y ) ) ) |
198 |
197
|
rneqd |
|- ( x = y -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) = ran ( n e. NN |-> ( ( F ` n ) ` y ) ) ) |
199 |
198
|
supeq1d |
|- ( x = y -> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) |
200 |
|
ltso |
|- < Or RR |
201 |
200
|
supex |
|- sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) e. _V |
202 |
199 1 201
|
fvmpt |
|- ( y e. RR -> ( G ` y ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) |
203 |
202
|
adantl |
|- ( ( ph /\ y e. RR ) -> ( G ` y ) = sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) |
204 |
51 193 194 194 33 195 203
|
ofrfval |
|- ( ph -> ( H oR <_ G <-> A. y e. RR ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) ) |
205 |
9 204
|
mpbid |
|- ( ph -> A. y e. RR ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) |
206 |
|
fveq2 |
|- ( x = y -> ( H ` x ) = ( H ` y ) ) |
207 |
206 199
|
breq12d |
|- ( x = y -> ( ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) ) |
208 |
207
|
cbvralvw |
|- ( A. x e. RR ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> A. y e. RR ( H ` y ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` y ) ) , RR , < ) ) |
209 |
205 208
|
sylibr |
|- ( ph -> A. x e. RR ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) ) |
210 |
209
|
r19.21bi |
|- ( ( ph /\ x e. RR ) -> ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) ) |
211 |
210
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( H ` x ) <_ sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) ) |
212 |
150 151 180 191 211
|
ltletrd |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) < sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) ) |
213 |
154
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR ) |
214 |
162
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) ) |
215 |
178
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) |
216 |
|
suprlub |
|- ( ( ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) C_ RR /\ ran ( n e. NN |-> ( ( F ` n ) ` x ) ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) z <_ y ) /\ ( T x. ( H ` x ) ) e. RR ) -> ( ( T x. ( H ` x ) ) < sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w ) ) |
217 |
213 214 215 150 216
|
syl31anc |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( ( T x. ( H ` x ) ) < sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) <-> E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w ) ) |
218 |
212 217
|
mpbid |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w ) |
219 |
163
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN ) |
220 |
|
breq2 |
|- ( w = ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) -> ( ( T x. ( H ` x ) ) < w <-> ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) ) ) |
221 |
220
|
rexrn |
|- ( ( n e. NN |-> ( ( F ` n ) ` x ) ) Fn NN -> ( E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) ) ) |
222 |
219 221
|
syl |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) ) ) |
223 |
|
fvex |
|- ( ( F ` j ) ` x ) e. _V |
224 |
136 156 223
|
fvmpt |
|- ( j e. NN -> ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) = ( ( F ` j ) ` x ) ) |
225 |
224
|
breq2d |
|- ( j e. NN -> ( ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) <-> ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) ) ) |
226 |
225
|
rexbiia |
|- ( E. j e. NN ( T x. ( H ` x ) ) < ( ( n e. NN |-> ( ( F ` n ) ` x ) ) ` j ) <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) ) |
227 |
222 226
|
bitrdi |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( E. w e. ran ( n e. NN |-> ( ( F ` n ) ` x ) ) ( T x. ( H ` x ) ) < w <-> E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) ) ) |
228 |
218 227
|
mpbid |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) ) |
229 |
183 151
|
remulcld |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( T x. ( H ` x ) ) e. RR ) |
230 |
108
|
adantlr |
|- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( F ` j ) : RR --> ( 0 [,) +oo ) ) |
231 |
|
simplr |
|- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> x e. RR ) |
232 |
230 231
|
ffvelrnd |
|- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. ( 0 [,) +oo ) ) |
233 |
|
elrege0 |
|- ( ( ( F ` j ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( F ` j ) ` x ) e. RR /\ 0 <_ ( ( F ` j ) ` x ) ) ) |
234 |
232 233
|
sylib |
|- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( ( F ` j ) ` x ) e. RR /\ 0 <_ ( ( F ` j ) ` x ) ) ) |
235 |
234
|
simpld |
|- ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. RR ) |
236 |
235
|
adantlrr |
|- ( ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. RR ) |
237 |
|
ltle |
|- ( ( ( T x. ( H ` x ) ) e. RR /\ ( ( F ` j ) ` x ) e. RR ) -> ( ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) -> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) ) |
238 |
229 236 237
|
syl2an2r |
|- ( ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) /\ j e. NN ) -> ( ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) -> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) ) |
239 |
238
|
reximdva |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> ( E. j e. NN ( T x. ( H ` x ) ) < ( ( F ` j ) ` x ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) ) |
240 |
228 239
|
mpd |
|- ( ( ph /\ ( x e. RR /\ 0 < ( H ` x ) ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
241 |
240
|
anassrs |
|- ( ( ( ph /\ x e. RR ) /\ 0 < ( H ` x ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
242 |
155
|
ne0ii |
|- NN =/= (/) |
243 |
66
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> ( T x. ( H ` x ) ) e. RR ) |
244 |
243
|
adantr |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) e. RR ) |
245 |
|
0red |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> 0 e. RR ) |
246 |
234
|
adantlrr |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( ( ( F ` j ) ` x ) e. RR /\ 0 <_ ( ( F ` j ) ` x ) ) ) |
247 |
246
|
simpld |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( ( F ` j ) ` x ) e. RR ) |
248 |
|
simplrr |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( H ` x ) <_ 0 ) |
249 |
57
|
adantrr |
|- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> ( H ` x ) e. RR ) |
250 |
249
|
adantr |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( H ` x ) e. RR ) |
251 |
25
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> T e. RR ) |
252 |
24
|
simp2d |
|- ( ph -> 0 < T ) |
253 |
252
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> 0 < T ) |
254 |
|
lemul2 |
|- ( ( ( H ` x ) e. RR /\ 0 e. RR /\ ( T e. RR /\ 0 < T ) ) -> ( ( H ` x ) <_ 0 <-> ( T x. ( H ` x ) ) <_ ( T x. 0 ) ) ) |
255 |
250 245 251 253 254
|
syl112anc |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( ( H ` x ) <_ 0 <-> ( T x. ( H ` x ) ) <_ ( T x. 0 ) ) ) |
256 |
248 255
|
mpbid |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) <_ ( T x. 0 ) ) |
257 |
251
|
recnd |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> T e. CC ) |
258 |
257
|
mul01d |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. 0 ) = 0 ) |
259 |
256 258
|
breqtrd |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) <_ 0 ) |
260 |
246
|
simprd |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> 0 <_ ( ( F ` j ) ` x ) ) |
261 |
244 245 247 259 260
|
letrd |
|- ( ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) /\ j e. NN ) -> ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
262 |
261
|
ralrimiva |
|- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> A. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
263 |
|
r19.2z |
|- ( ( NN =/= (/) /\ A. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
264 |
242 262 263
|
sylancr |
|- ( ( ph /\ ( x e. RR /\ ( H ` x ) <_ 0 ) ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
265 |
264
|
anassrs |
|- ( ( ( ph /\ x e. RR ) /\ ( H ` x ) <_ 0 ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
266 |
|
0red |
|- ( ( ph /\ x e. RR ) -> 0 e. RR ) |
267 |
241 265 266 57
|
ltlecasei |
|- ( ( ph /\ x e. RR ) -> E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
268 |
267
|
ralrimiva |
|- ( ph -> A. x e. RR E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
269 |
|
rabid2 |
|- ( RR = { x e. RR | E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } <-> A. x e. RR E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) ) |
270 |
268 269
|
sylibr |
|- ( ph -> RR = { x e. RR | E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } ) |
271 |
|
iunrab |
|- U_ j e. NN { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } = { x e. RR | E. j e. NN ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } |
272 |
270 271
|
eqtr4di |
|- ( ph -> RR = U_ j e. NN { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } ) |
273 |
141
|
iuneq2dv |
|- ( ph -> U_ j e. NN ( A ` j ) = U_ j e. NN { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` j ) ` x ) } ) |
274 |
96
|
ffnd |
|- ( ph -> A Fn NN ) |
275 |
|
fniunfv |
|- ( A Fn NN -> U_ j e. NN ( A ` j ) = U. ran A ) |
276 |
274 275
|
syl |
|- ( ph -> U_ j e. NN ( A ` j ) = U. ran A ) |
277 |
272 273 276
|
3eqtr2rd |
|- ( ph -> U. ran A = RR ) |
278 |
|
eqid |
|- ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) |
279 |
96 149 277 8 278
|
itg1climres |
|- ( ph -> ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ~~> ( S.1 ` H ) ) |
280 |
|
nnex |
|- NN e. _V |
281 |
280
|
mptex |
|- ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) e. _V |
282 |
281
|
a1i |
|- ( ph -> ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) e. _V ) |
283 |
|
fveq2 |
|- ( j = k -> ( A ` j ) = ( A ` k ) ) |
284 |
283
|
eleq2d |
|- ( j = k -> ( x e. ( A ` j ) <-> x e. ( A ` k ) ) ) |
285 |
284
|
ifbid |
|- ( j = k -> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) = if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) |
286 |
285
|
mpteq2dv |
|- ( j = k -> ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) |
287 |
286
|
fveq2d |
|- ( j = k -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) |
288 |
|
eqid |
|- ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) = ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) |
289 |
|
fvex |
|- ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. _V |
290 |
287 288 289
|
fvmpt |
|- ( k e. NN -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) |
291 |
290
|
adantl |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) |
292 |
96
|
ffvelrnda |
|- ( ( ph /\ k e. NN ) -> ( A ` k ) e. dom vol ) |
293 |
|
eqid |
|- ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) |
294 |
293
|
i1fres |
|- ( ( H e. dom S.1 /\ ( A ` k ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) e. dom S.1 ) |
295 |
8 292 294
|
syl2an2r |
|- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) e. dom S.1 ) |
296 |
|
itg1cl |
|- ( ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. RR ) |
297 |
295 296
|
syl |
|- ( ( ph /\ k e. NN ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. RR ) |
298 |
291 297
|
eqeltrd |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) e. RR ) |
299 |
298
|
recnd |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) e. CC ) |
300 |
287
|
oveq2d |
|- ( j = k -> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) ) |
301 |
|
eqid |
|- ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) = ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) |
302 |
|
ovex |
|- ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) e. _V |
303 |
300 301 302
|
fvmpt |
|- ( k e. NN -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) ) |
304 |
290
|
oveq2d |
|- ( k e. NN -> ( T x. ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) ) |
305 |
303 304
|
eqtr4d |
|- ( k e. NN -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) ) ) |
306 |
305
|
adantl |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( ( j e. NN |-> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ` k ) ) ) |
307 |
12 13 279 55 282 299 306
|
climmulc2 |
|- ( ph -> ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ~~> ( T x. ( S.1 ` H ) ) ) |
308 |
|
icossicc |
|- ( 0 [,) +oo ) C_ ( 0 [,] +oo ) |
309 |
|
fss |
|- ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) ) |
310 |
3 308 309
|
sylancl |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) ) |
311 |
10
|
adantr |
|- ( ( ph /\ n e. NN ) -> S e. RR ) |
312 |
|
itg2cl |
|- ( ( F ` n ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` n ) ) e. RR* ) |
313 |
310 312
|
syl |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR* ) |
314 |
313
|
fmpttd |
|- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR* ) |
315 |
314
|
frnd |
|- ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* ) |
316 |
|
fvex |
|- ( S.2 ` ( F ` n ) ) e. _V |
317 |
316
|
elabrex |
|- ( n e. NN -> ( S.2 ` ( F ` n ) ) e. { x | E. n e. NN x = ( S.2 ` ( F ` n ) ) } ) |
318 |
317
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. { x | E. n e. NN x = ( S.2 ` ( F ` n ) ) } ) |
319 |
|
eqid |
|- ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) |
320 |
319
|
rnmpt |
|- ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = { x | E. n e. NN x = ( S.2 ` ( F ` n ) ) } |
321 |
318 320
|
eleqtrrdi |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ) |
322 |
|
supxrub |
|- ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* /\ ( S.2 ` ( F ` n ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ) -> ( S.2 ` ( F ` n ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) ) |
323 |
315 321 322
|
syl2an2r |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) ) |
324 |
323 6
|
breqtrrdi |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) <_ S ) |
325 |
|
itg2lecl |
|- ( ( ( F ` n ) : RR --> ( 0 [,] +oo ) /\ S e. RR /\ ( S.2 ` ( F ` n ) ) <_ S ) -> ( S.2 ` ( F ` n ) ) e. RR ) |
326 |
310 311 324 325
|
syl3anc |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR ) |
327 |
326
|
fmpttd |
|- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR ) |
328 |
310
|
ralrimiva |
|- ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,] +oo ) ) |
329 |
|
fveq2 |
|- ( n = k -> ( F ` n ) = ( F ` k ) ) |
330 |
329
|
feq1d |
|- ( n = k -> ( ( F ` n ) : RR --> ( 0 [,] +oo ) <-> ( F ` k ) : RR --> ( 0 [,] +oo ) ) ) |
331 |
330
|
cbvralvw |
|- ( A. n e. NN ( F ` n ) : RR --> ( 0 [,] +oo ) <-> A. k e. NN ( F ` k ) : RR --> ( 0 [,] +oo ) ) |
332 |
328 331
|
sylib |
|- ( ph -> A. k e. NN ( F ` k ) : RR --> ( 0 [,] +oo ) ) |
333 |
|
peano2nn |
|- ( n e. NN -> ( n + 1 ) e. NN ) |
334 |
|
fveq2 |
|- ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) ) |
335 |
334
|
feq1d |
|- ( k = ( n + 1 ) -> ( ( F ` k ) : RR --> ( 0 [,] +oo ) <-> ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) ) ) |
336 |
335
|
rspccva |
|- ( ( A. k e. NN ( F ` k ) : RR --> ( 0 [,] +oo ) /\ ( n + 1 ) e. NN ) -> ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) ) |
337 |
332 333 336
|
syl2an |
|- ( ( ph /\ n e. NN ) -> ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) ) |
338 |
|
itg2le |
|- ( ( ( F ` n ) : RR --> ( 0 [,] +oo ) /\ ( F ` ( n + 1 ) ) : RR --> ( 0 [,] +oo ) /\ ( F ` n ) oR <_ ( F ` ( n + 1 ) ) ) -> ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) ) |
339 |
310 337 4 338
|
syl3anc |
|- ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) ) |
340 |
339
|
ralrimiva |
|- ( ph -> A. n e. NN ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) ) |
341 |
|
2fveq3 |
|- ( n = k -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` k ) ) ) |
342 |
|
fvex |
|- ( S.2 ` ( F ` k ) ) e. _V |
343 |
341 319 342
|
fvmpt |
|- ( k e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) = ( S.2 ` ( F ` k ) ) ) |
344 |
|
peano2nn |
|- ( k e. NN -> ( k + 1 ) e. NN ) |
345 |
|
2fveq3 |
|- ( n = ( k + 1 ) -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) ) |
346 |
|
fvex |
|- ( S.2 ` ( F ` ( k + 1 ) ) ) e. _V |
347 |
345 319 346
|
fvmpt |
|- ( ( k + 1 ) e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) ) |
348 |
344 347
|
syl |
|- ( k e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) ) |
349 |
343 348
|
breq12d |
|- ( k e. NN -> ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) <-> ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) ) ) |
350 |
349
|
ralbiia |
|- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) ) |
351 |
|
fvoveq1 |
|- ( n = k -> ( F ` ( n + 1 ) ) = ( F ` ( k + 1 ) ) ) |
352 |
351
|
fveq2d |
|- ( n = k -> ( S.2 ` ( F ` ( n + 1 ) ) ) = ( S.2 ` ( F ` ( k + 1 ) ) ) ) |
353 |
341 352
|
breq12d |
|- ( n = k -> ( ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) <-> ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) ) ) |
354 |
353
|
cbvralvw |
|- ( A. n e. NN ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ ( S.2 ` ( F ` ( k + 1 ) ) ) ) |
355 |
350 354
|
bitr4i |
|- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ ( S.2 ` ( F ` ( n + 1 ) ) ) ) |
356 |
340 355
|
sylibr |
|- ( ph -> A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) ) |
357 |
356
|
r19.21bi |
|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` ( k + 1 ) ) ) |
358 |
324
|
ralrimiva |
|- ( ph -> A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) |
359 |
343
|
breq1d |
|- ( k e. NN -> ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> ( S.2 ` ( F ` k ) ) <_ x ) ) |
360 |
359
|
ralbiia |
|- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ x ) |
361 |
341
|
breq1d |
|- ( n = k -> ( ( S.2 ` ( F ` n ) ) <_ x <-> ( S.2 ` ( F ` k ) ) <_ x ) ) |
362 |
361
|
cbvralvw |
|- ( A. n e. NN ( S.2 ` ( F ` n ) ) <_ x <-> A. k e. NN ( S.2 ` ( F ` k ) ) <_ x ) |
363 |
360 362
|
bitr4i |
|- ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ x ) |
364 |
|
breq2 |
|- ( x = S -> ( ( S.2 ` ( F ` n ) ) <_ x <-> ( S.2 ` ( F ` n ) ) <_ S ) ) |
365 |
364
|
ralbidv |
|- ( x = S -> ( A. n e. NN ( S.2 ` ( F ` n ) ) <_ x <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) ) |
366 |
363 365
|
syl5bb |
|- ( x = S -> ( A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x <-> A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) ) |
367 |
366
|
rspcev |
|- ( ( S e. RR /\ A. n e. NN ( S.2 ` ( F ` n ) ) <_ S ) -> E. x e. RR A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) |
368 |
10 358 367
|
syl2anc |
|- ( ph -> E. x e. RR A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) |
369 |
12 13 327 357 368
|
climsup |
|- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ~~> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) ) |
370 |
327
|
frnd |
|- ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR ) |
371 |
319 313
|
dmmptd |
|- ( ph -> dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = NN ) |
372 |
242
|
a1i |
|- ( ph -> NN =/= (/) ) |
373 |
371 372
|
eqnetrd |
|- ( ph -> dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) ) |
374 |
|
dm0rn0 |
|- ( dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = (/) <-> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = (/) ) |
375 |
374
|
necon3bii |
|- ( dom ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) <-> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) ) |
376 |
373 375
|
sylib |
|- ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) ) |
377 |
316 319
|
fnmpti |
|- ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN |
378 |
|
breq1 |
|- ( z = ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) -> ( z <_ x <-> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) ) |
379 |
378
|
ralrn |
|- ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x <-> A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) ) |
380 |
377 379
|
mp1i |
|- ( ph -> ( A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x <-> A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) ) |
381 |
380
|
rexbidv |
|- ( ph -> ( E. x e. RR A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x <-> E. x e. RR A. k e. NN ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) <_ x ) ) |
382 |
368 381
|
mpbird |
|- ( ph -> E. x e. RR A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x ) |
383 |
|
supxrre |
|- ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR /\ ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) =/= (/) /\ E. x e. RR A. z e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) z <_ x ) -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) ) |
384 |
370 376 382 383
|
syl3anc |
|- ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) ) |
385 |
6 384
|
eqtr2id |
|- ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR , < ) = S ) |
386 |
369 385
|
breqtrd |
|- ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ~~> S ) |
387 |
25
|
adantr |
|- ( ( ph /\ j e. NN ) -> T e. RR ) |
388 |
96
|
ffvelrnda |
|- ( ( ph /\ j e. NN ) -> ( A ` j ) e. dom vol ) |
389 |
278
|
i1fres |
|- ( ( H e. dom S.1 /\ ( A ` j ) e. dom vol ) -> ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) e. dom S.1 ) |
390 |
8 388 389
|
syl2an2r |
|- ( ( ph /\ j e. NN ) -> ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) e. dom S.1 ) |
391 |
|
itg1cl |
|- ( ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) e. RR ) |
392 |
390 391
|
syl |
|- ( ( ph /\ j e. NN ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) e. RR ) |
393 |
387 392
|
remulcld |
|- ( ( ph /\ j e. NN ) -> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) e. RR ) |
394 |
393
|
fmpttd |
|- ( ph -> ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) : NN --> RR ) |
395 |
394
|
ffvelrnda |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) e. RR ) |
396 |
327
|
ffvelrnda |
|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) e. RR ) |
397 |
329
|
feq1d |
|- ( n = k -> ( ( F ` n ) : RR --> ( 0 [,) +oo ) <-> ( F ` k ) : RR --> ( 0 [,) +oo ) ) ) |
398 |
397
|
cbvralvw |
|- ( A. n e. NN ( F ` n ) : RR --> ( 0 [,) +oo ) <-> A. k e. NN ( F ` k ) : RR --> ( 0 [,) +oo ) ) |
399 |
104 398
|
sylib |
|- ( ph -> A. k e. NN ( F ` k ) : RR --> ( 0 [,) +oo ) ) |
400 |
399
|
r19.21bi |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) : RR --> ( 0 [,) +oo ) ) |
401 |
|
fss |
|- ( ( ( F ` k ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` k ) : RR --> ( 0 [,] +oo ) ) |
402 |
400 308 401
|
sylancl |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) : RR --> ( 0 [,] +oo ) ) |
403 |
31
|
a1i |
|- ( ( ph /\ k e. NN ) -> RR e. _V ) |
404 |
25
|
adantr |
|- ( ( ph /\ k e. NN ) -> T e. RR ) |
405 |
404
|
adantr |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> T e. RR ) |
406 |
|
fvex |
|- ( H ` x ) e. _V |
407 |
|
c0ex |
|- 0 e. _V |
408 |
406 407
|
ifex |
|- if ( x e. ( A ` k ) , ( H ` x ) , 0 ) e. _V |
409 |
408
|
a1i |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) e. _V ) |
410 |
|
fconstmpt |
|- ( RR X. { T } ) = ( x e. RR |-> T ) |
411 |
410
|
a1i |
|- ( ( ph /\ k e. NN ) -> ( RR X. { T } ) = ( x e. RR |-> T ) ) |
412 |
|
eqidd |
|- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) |
413 |
403 405 409 411 412
|
offval2 |
|- ( ( ph /\ k e. NN ) -> ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) = ( x e. RR |-> ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) |
414 |
|
ovif2 |
|- ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , ( T x. 0 ) ) |
415 |
55
|
adantr |
|- ( ( ph /\ k e. NN ) -> T e. CC ) |
416 |
415
|
mul01d |
|- ( ( ph /\ k e. NN ) -> ( T x. 0 ) = 0 ) |
417 |
416
|
ifeq2d |
|- ( ( ph /\ k e. NN ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , ( T x. 0 ) ) = if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) |
418 |
414 417
|
syl5eq |
|- ( ( ph /\ k e. NN ) -> ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) = if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) |
419 |
418
|
mpteq2dv |
|- ( ( ph /\ k e. NN ) -> ( x e. RR |-> ( T x. if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) |
420 |
413 419
|
eqtrd |
|- ( ( ph /\ k e. NN ) -> ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) |
421 |
295 404
|
i1fmulc |
|- ( ( ph /\ k e. NN ) -> ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) e. dom S.1 ) |
422 |
420 421
|
eqeltrrd |
|- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) e. dom S.1 ) |
423 |
|
iftrue |
|- ( x e. ( A ` k ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = ( T x. ( H ` x ) ) ) |
424 |
423
|
adantl |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = ( T x. ( H ` x ) ) ) |
425 |
329
|
fveq1d |
|- ( n = k -> ( ( F ` n ) ` x ) = ( ( F ` k ) ` x ) ) |
426 |
425
|
breq2d |
|- ( n = k -> ( ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) <-> ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) ) ) |
427 |
426
|
rabbidv |
|- ( n = k -> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } ) |
428 |
31
|
rabex |
|- { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } e. _V |
429 |
427 11 428
|
fvmpt |
|- ( k e. NN -> ( A ` k ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } ) |
430 |
429
|
ad2antlr |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( A ` k ) = { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } ) |
431 |
430
|
eleq2d |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( x e. ( A ` k ) <-> x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } ) ) |
432 |
431
|
biimpa |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } ) |
433 |
|
rabid |
|- ( x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } <-> ( x e. RR /\ ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) ) ) |
434 |
433
|
simprbi |
|- ( x e. { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) } -> ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) ) |
435 |
432 434
|
syl |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> ( T x. ( H ` x ) ) <_ ( ( F ` k ) ` x ) ) |
436 |
424 435
|
eqbrtrd |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) ) |
437 |
|
iffalse |
|- ( -. x e. ( A ` k ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = 0 ) |
438 |
437
|
adantl |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) = 0 ) |
439 |
400
|
ffvelrnda |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( ( F ` k ) ` x ) e. ( 0 [,) +oo ) ) |
440 |
|
elrege0 |
|- ( ( ( F ` k ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( F ` k ) ` x ) e. RR /\ 0 <_ ( ( F ` k ) ` x ) ) ) |
441 |
440
|
simprbi |
|- ( ( ( F ` k ) ` x ) e. ( 0 [,) +oo ) -> 0 <_ ( ( F ` k ) ` x ) ) |
442 |
439 441
|
syl |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> 0 <_ ( ( F ` k ) ` x ) ) |
443 |
442
|
adantr |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( A ` k ) ) -> 0 <_ ( ( F ` k ) ` x ) ) |
444 |
438 443
|
eqbrtrd |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ -. x e. ( A ` k ) ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) ) |
445 |
436 444
|
pm2.61dan |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) ) |
446 |
445
|
ralrimiva |
|- ( ( ph /\ k e. NN ) -> A. x e. RR if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) ) |
447 |
|
ovex |
|- ( T x. ( H ` x ) ) e. _V |
448 |
447 407
|
ifex |
|- if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) e. _V |
449 |
448
|
a1i |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) e. _V ) |
450 |
|
fvexd |
|- ( ( ( ph /\ k e. NN ) /\ x e. RR ) -> ( ( F ` k ) ` x ) e. _V ) |
451 |
|
eqidd |
|- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) = ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) |
452 |
400
|
feqmptd |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( x e. RR |-> ( ( F ` k ) ` x ) ) ) |
453 |
403 449 450 451 452
|
ofrfval2 |
|- ( ( ph /\ k e. NN ) -> ( ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) oR <_ ( F ` k ) <-> A. x e. RR if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) <_ ( ( F ` k ) ` x ) ) ) |
454 |
446 453
|
mpbird |
|- ( ( ph /\ k e. NN ) -> ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) oR <_ ( F ` k ) ) |
455 |
|
itg2ub |
|- ( ( ( F ` k ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) e. dom S.1 /\ ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) oR <_ ( F ` k ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) <_ ( S.2 ` ( F ` k ) ) ) |
456 |
402 422 454 455
|
syl3anc |
|- ( ( ph /\ k e. NN ) -> ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) <_ ( S.2 ` ( F ` k ) ) ) |
457 |
303
|
adantl |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) ) |
458 |
295 404
|
itg1mulc |
|- ( ( ph /\ k e. NN ) -> ( S.1 ` ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) = ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) ) |
459 |
420
|
fveq2d |
|- ( ( ph /\ k e. NN ) -> ( S.1 ` ( ( RR X. { T } ) oF x. ( x e. RR |-> if ( x e. ( A ` k ) , ( H ` x ) , 0 ) ) ) ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) ) |
460 |
457 458 459
|
3eqtr2d |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) = ( S.1 ` ( x e. RR |-> if ( x e. ( A ` k ) , ( T x. ( H ` x ) ) , 0 ) ) ) ) |
461 |
343
|
adantl |
|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) = ( S.2 ` ( F ` k ) ) ) |
462 |
456 460 461
|
3brtr4d |
|- ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( T x. ( S.1 ` ( x e. RR |-> if ( x e. ( A ` j ) , ( H ` x ) , 0 ) ) ) ) ) ` k ) <_ ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` k ) ) |
463 |
12 13 307 386 395 396 462
|
climle |
|- ( ph -> ( T x. ( S.1 ` H ) ) <_ S ) |