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 eqtrid 
 |-  ( ( 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 )