Metamath Proof Explorer


Theorem itg2monolem1

Description: Lemma for itg2mono . We show that for any constant t less than one, t x. S.1 H is less than S , and so S.1 H <_ S , which is one half of the equality in itg2mono . Consider the sequence A ( n ) = { x | t x. H <_ F ( n ) } . This is an increasing sequence of measurable sets whose union is RR , and so ` H |`A ( n ) has an integral which equals S.1 H in the limit, by itg1climres . Then by taking the limit in ` ( t x. H ) |`A ( n ) <_ F ( n ) , we get t x. S.1 H <_ S as desired. (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itg2mono.1
|- G = ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( F ` n ) ` x ) ) , RR , < ) )
itg2mono.2
|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. MblFn )
itg2mono.3
|- ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
itg2mono.4
|- ( ( ph /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
itg2mono.5
|- ( ( ph /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
itg2mono.6
|- S = sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < )
itg2mono.7
|- ( ph -> T e. ( 0 (,) 1 ) )
itg2mono.8
|- ( ph -> H e. dom S.1 )
itg2mono.9
|- ( ph -> H oR <_ G )
itg2mono.10
|- ( ph -> S e. RR )
itg2mono.11
|- A = ( n e. NN |-> { x e. RR | ( T x. ( H ` x ) ) <_ ( ( F ` n ) ` x ) } )
Assertion itg2monolem1
|- ( ph -> ( T x. ( S.1 ` H ) ) <_ S )

Proof

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 )