Metamath Proof Explorer

Theorem itg2seq

Description: Definitional property of the S.2 integral: for any function F there is a countable sequence g of simple functions less than F whose integrals converge to the integral of F . (This theorem is for the most part unnecessary in lieu of itg2i1fseq , but unlike that theorem this one doesn't require F to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014)

Ref Expression
Assertion itg2seq 
|- ( F : RR --> ( 0 [,] +oo ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( g ` n ) oR <_ F /\ ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( n e. NN -> n e. RR )
2 1 ad2antlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ ( S.2 ` F ) = +oo ) -> n e. RR )
3 2 ltpnfd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ ( S.2 ` F ) = +oo ) -> n < +oo )
4 iftrue 
 |-  ( ( S.2 ` F ) = +oo -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) = n )
5 4 adantl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ ( S.2 ` F ) = +oo ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) = n )
6 simpr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ ( S.2 ` F ) = +oo ) -> ( S.2 ` F ) = +oo )
7 3 5 6 3brtr4d 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ ( S.2 ` F ) = +oo ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.2 ` F ) )
8 iffalse 
 |-  ( -. ( S.2 ` F ) = +oo -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) = ( ( S.2 ` F ) - ( 1 / n ) ) )
9 8 adantl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) = ( ( S.2 ` F ) - ( 1 / n ) ) )
10 itg2cl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
11 xrrebnd 
 |-  ( ( S.2 ` F ) e. RR* -> ( ( S.2 ` F ) e. RR <-> ( -oo < ( S.2 ` F ) /\ ( S.2 ` F ) < +oo ) ) )
12 10 11 syl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( S.2 ` F ) e. RR <-> ( -oo < ( S.2 ` F ) /\ ( S.2 ` F ) < +oo ) ) )
13 itg2ge0 
 |-  ( F : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` F ) )
14 mnflt0 
 |-  -oo < 0
15 mnfxr 
 |-  -oo e. RR*
16 0xr 
 |-  0 e. RR*
17 xrltletr 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ ( S.2 ` F ) e. RR* ) -> ( ( -oo < 0 /\ 0 <_ ( S.2 ` F ) ) -> -oo < ( S.2 ` F ) ) )
18 15 16 10 17 mp3an12i 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( -oo < 0 /\ 0 <_ ( S.2 ` F ) ) -> -oo < ( S.2 ` F ) ) )
19 14 18 mpani 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( 0 <_ ( S.2 ` F ) -> -oo < ( S.2 ` F ) ) )
20 13 19 mpd 
 |-  ( F : RR --> ( 0 [,] +oo ) -> -oo < ( S.2 ` F ) )
21 20 biantrurd 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( S.2 ` F ) < +oo <-> ( -oo < ( S.2 ` F ) /\ ( S.2 ` F ) < +oo ) ) )
22 nltpnft 
 |-  ( ( S.2 ` F ) e. RR* -> ( ( S.2 ` F ) = +oo <-> -. ( S.2 ` F ) < +oo ) )
23 10 22 syl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( S.2 ` F ) = +oo <-> -. ( S.2 ` F ) < +oo ) )
24 23 con2bid 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( S.2 ` F ) < +oo <-> -. ( S.2 ` F ) = +oo ) )
25 12 21 24 3bitr2rd 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( -. ( S.2 ` F ) = +oo <-> ( S.2 ` F ) e. RR ) )
26 25 biimpa 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ -. ( S.2 ` F ) = +oo ) -> ( S.2 ` F ) e. RR )
27 26 adantlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> ( S.2 ` F ) e. RR )
28 nnrp 
 |-  ( n e. NN -> n e. RR+ )
29 28 rpreccld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
30 29 ad2antlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> ( 1 / n ) e. RR+ )
31 27 30 ltsubrpd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> ( ( S.2 ` F ) - ( 1 / n ) ) < ( S.2 ` F ) )
32 9 31 eqbrtrd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.2 ` F ) )
33 7 32 pm2.61dan 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.2 ` F ) )
34 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
35 34 ad2antlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> ( 1 / n ) e. RR )
36 27 35 resubcld 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ -. ( S.2 ` F ) = +oo ) -> ( ( S.2 ` F ) - ( 1 / n ) ) e. RR )
37 2 36 ifclda 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR )
38 37 rexrd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* )
39 10 adantr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> ( S.2 ` F ) e. RR* )
40 xrltnle 
 |-  ( ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* /\ ( S.2 ` F ) e. RR* ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.2 ` F ) <-> -. ( S.2 ` F ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
41 38 39 40 syl2anc 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.2 ` F ) <-> -. ( S.2 ` F ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
42 33 41 mpbid 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> -. ( S.2 ` F ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) )
43 itg2leub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* ) -> ( ( S.2 ` F ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) ) )
44 38 43 syldan 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> ( ( S.2 ` F ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) ) )
45 42 44 mtbid 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> -. A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
46 rexanali 
 |-  ( E. f e. dom S.1 ( f oR <_ F /\ -. ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) <-> -. A. f e. dom S.1 ( f oR <_ F -> ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
47 45 46 sylibr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> E. f e. dom S.1 ( f oR <_ F /\ -. ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
48 itg1cl 
 |-  ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
49 ltnle 
 |-  ( ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR /\ ( S.1 ` f ) e. RR ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) <-> -. ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
50 37 48 49 syl2an 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ f e. dom S.1 ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) <-> -. ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
51 50 anbi2d 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) /\ f e. dom S.1 ) -> ( ( f oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) ) <-> ( f oR <_ F /\ -. ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) ) )
52 51 rexbidva 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> ( E. f e. dom S.1 ( f oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) ) <-> E. f e. dom S.1 ( f oR <_ F /\ -. ( S.1 ` f ) <_ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) ) )
53 47 52 mpbird 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ n e. NN ) -> E. f e. dom S.1 ( f oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) ) )
54 53 ralrimiva 
 |-  ( F : RR --> ( 0 [,] +oo ) -> A. n e. NN E. f e. dom S.1 ( f oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) ) )
55 ovex 
 |-  ( RR ^m RR ) e. _V
56 i1ff 
 |-  ( x e. dom S.1 -> x : RR --> RR )
57 reex 
 |-  RR e. _V
58 57 57 elmap 
 |-  ( x e. ( RR ^m RR ) <-> x : RR --> RR )
59 56 58 sylibr 
 |-  ( x e. dom S.1 -> x e. ( RR ^m RR ) )
60 59 ssriv 
 |-  dom S.1 C_ ( RR ^m RR )
61 55 60 ssexi 
 |-  dom S.1 e. _V
62 nnenom 
 |-  NN ~~ _om
63 breq1 
 |-  ( f = ( g ` n ) -> ( f oR <_ F <-> ( g ` n ) oR <_ F ) )
64 fveq2 
 |-  ( f = ( g ` n ) -> ( S.1 ` f ) = ( S.1 ` ( g ` n ) ) )
65 64 breq2d 
 |-  ( f = ( g ` n ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) <-> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) )
66 63 65 anbi12d 
 |-  ( f = ( g ` n ) -> ( ( f oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) ) <-> ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) )
67 61 62 66 axcc4 
 |-  ( A. n e. NN E. f e. dom S.1 ( f oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` f ) ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) )
68 54 67 syl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) )
69 simprl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> g : NN --> dom S.1 )
70 simpl 
 |-  ( ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) -> ( g ` n ) oR <_ F )
71 70 ralimi 
 |-  ( A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) -> A. n e. NN ( g ` n ) oR <_ F )
72 71 ad2antll 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> A. n e. NN ( g ` n ) oR <_ F )
73 10 adantr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( S.2 ` F ) e. RR* )
74 ffvelrn 
 |-  ( ( g : NN --> dom S.1 /\ n e. NN ) -> ( g ` n ) e. dom S.1 )
75 itg1cl 
 |-  ( ( g ` n ) e. dom S.1 -> ( S.1 ` ( g ` n ) ) e. RR )
76 74 75 syl 
 |-  ( ( g : NN --> dom S.1 /\ n e. NN ) -> ( S.1 ` ( g ` n ) ) e. RR )
77 76 fmpttd 
 |-  ( g : NN --> dom S.1 -> ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) : NN --> RR )
78 77 ad2antrl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) : NN --> RR )
79 78 frnd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR )
80 ressxr 
 |-  RR C_ RR*
81 79 80 sstrdi 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR* )
82 supxrcl 
 |-  ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR* -> sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) e. RR* )
83 81 82 syl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) e. RR* )
84 38 adantlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* )
85 76 adantll 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( S.1 ` ( g ` n ) ) e. RR )
86 85 rexrd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( S.1 ` ( g ` n ) ) e. RR* )
87 xrltle 
 |-  ( ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* /\ ( S.1 ` ( g ` n ) ) e. RR* ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ ( S.1 ` ( g ` n ) ) ) )
88 84 86 87 syl2anc 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ ( S.1 ` ( g ` n ) ) ) )
89 2fveq3 
 |-  ( n = m -> ( S.1 ` ( g ` n ) ) = ( S.1 ` ( g ` m ) ) )
90 89 cbvmptv 
 |-  ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) = ( m e. NN |-> ( S.1 ` ( g ` m ) ) )
91 90 rneqi 
 |-  ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) = ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) )
92 77 adantl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) -> ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) : NN --> RR )
93 92 frnd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) -> ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR )
94 93 80 sstrdi 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) -> ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR* )
95 94 adantr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR* )
96 91 95 eqsstrrid 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) C_ RR* )
97 2fveq3 
 |-  ( m = n -> ( S.1 ` ( g ` m ) ) = ( S.1 ` ( g ` n ) ) )
98 eqid 
 |-  ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) = ( m e. NN |-> ( S.1 ` ( g ` m ) ) )
99 fvex 
 |-  ( S.1 ` ( g ` n ) ) e. _V
100 97 98 99 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) ` n ) = ( S.1 ` ( g ` n ) ) )
101 fvex 
 |-  ( S.1 ` ( g ` m ) ) e. _V
102 101 98 fnmpti 
 |-  ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) Fn NN
103 fnfvelrn 
 |-  ( ( ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) Fn NN /\ n e. NN ) -> ( ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) ` n ) e. ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) )
104 102 103 mpan 
 |-  ( n e. NN -> ( ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) ` n ) e. ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) )
105 100 104 eqeltrrd 
 |-  ( n e. NN -> ( S.1 ` ( g ` n ) ) e. ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) )
106 105 adantl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( S.1 ` ( g ` n ) ) e. ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) )
107 supxrub 
 |-  ( ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) C_ RR* /\ ( S.1 ` ( g ` n ) ) e. ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) ) -> ( S.1 ` ( g ` n ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) )
108 96 106 107 syl2anc 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( S.1 ` ( g ` n ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) )
109 91 supeq1i 
 |-  sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) = sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < )
110 95 82 syl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) e. RR* )
111 109 110 eqeltrrid 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) e. RR* )
112 xrletr 
 |-  ( ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* /\ ( S.1 ` ( g ` n ) ) e. RR* /\ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) e. RR* ) -> ( ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ ( S.1 ` ( g ` n ) ) /\ ( S.1 ` ( g ` n ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
113 84 86 111 112 syl3anc 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ ( S.1 ` ( g ` n ) ) /\ ( S.1 ` ( g ` n ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
114 108 113 mpan2d 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ ( S.1 ` ( g ` n ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
115 88 114 syld 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
116 115 adantld 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
117 116 ralimdva 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) -> ( A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) -> A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
118 117 impr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) )
119 breq2 
 |-  ( x = sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x <-> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
120 119 ralbidv 
 |-  ( x = sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x <-> A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
121 breq2 
 |-  ( x = sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) -> ( ( S.2 ` F ) <_ x <-> ( S.2 ` F ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
122 120 121 imbi12d 
 |-  ( x = sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) -> ( ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) <-> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) -> ( S.2 ` F ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) ) )
123 elxr 
 |-  ( x e. RR* <-> ( x e. RR \/ x = +oo \/ x = -oo ) )
124 simplrl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ ( S.2 ` F ) = +oo ) -> x e. RR )
125 arch 
 |-  ( x e. RR -> E. n e. NN x < n )
126 124 125 syl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ ( S.2 ` F ) = +oo ) -> E. n e. NN x < n )
127 4 adantl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ ( S.2 ` F ) = +oo ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) = n )
128 127 breq2d 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ ( S.2 ` F ) = +oo ) -> ( x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> x < n ) )
129 128 rexbidv 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ ( S.2 ` F ) = +oo ) -> ( E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> E. n e. NN x < n ) )
130 126 129 mpbird 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ ( S.2 ` F ) = +oo ) -> E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) )
131 26 adantlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> ( S.2 ` F ) e. RR )
132 simplrl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> x e. RR )
133 131 132 resubcld 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> ( ( S.2 ` F ) - x ) e. RR )
134 simplrr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> x < ( S.2 ` F ) )
135 132 131 posdifd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> ( x < ( S.2 ` F ) <-> 0 < ( ( S.2 ` F ) - x ) ) )
136 134 135 mpbid 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> 0 < ( ( S.2 ` F ) - x ) )
137 nnrecl 
 |-  ( ( ( ( S.2 ` F ) - x ) e. RR /\ 0 < ( ( S.2 ` F ) - x ) ) -> E. n e. NN ( 1 / n ) < ( ( S.2 ` F ) - x ) )
138 133 136 137 syl2anc 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> E. n e. NN ( 1 / n ) < ( ( S.2 ` F ) - x ) )
139 34 adantl 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> ( 1 / n ) e. RR )
140 131 adantr 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> ( S.2 ` F ) e. RR )
141 132 adantr 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> x e. RR )
142 ltsub13 
 |-  ( ( ( 1 / n ) e. RR /\ ( S.2 ` F ) e. RR /\ x e. RR ) -> ( ( 1 / n ) < ( ( S.2 ` F ) - x ) <-> x < ( ( S.2 ` F ) - ( 1 / n ) ) ) )
143 139 140 141 142 syl3anc 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> ( ( 1 / n ) < ( ( S.2 ` F ) - x ) <-> x < ( ( S.2 ` F ) - ( 1 / n ) ) ) )
144 8 ad2antlr 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) = ( ( S.2 ` F ) - ( 1 / n ) ) )
145 144 breq2d 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> ( x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> x < ( ( S.2 ` F ) - ( 1 / n ) ) ) )
146 143 145 bitr4d 
 |-  ( ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) /\ n e. NN ) -> ( ( 1 / n ) < ( ( S.2 ` F ) - x ) <-> x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
147 146 rexbidva 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> ( E. n e. NN ( 1 / n ) < ( ( S.2 ` F ) - x ) <-> E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
148 138 147 mpbid 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) /\ -. ( S.2 ` F ) = +oo ) -> E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) )
149 130 148 pm2.61dan 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR /\ x < ( S.2 ` F ) ) ) -> E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) )
150 149 expr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( x < ( S.2 ` F ) -> E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) ) )
151 rexr 
 |-  ( x e. RR -> x e. RR* )
152 xrltnle 
 |-  ( ( x e. RR* /\ ( S.2 ` F ) e. RR* ) -> ( x < ( S.2 ` F ) <-> -. ( S.2 ` F ) <_ x ) )
153 151 10 152 syl2anr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( x < ( S.2 ` F ) <-> -. ( S.2 ` F ) <_ x ) )
154 151 ad2antlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) /\ n e. NN ) -> x e. RR* )
155 38 adantlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* )
156 xrltnle 
 |-  ( ( x e. RR* /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* ) -> ( x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x ) )
157 154 155 156 syl2anc 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) /\ n e. NN ) -> ( x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x ) )
158 157 rexbidva 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> E. n e. NN -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x ) )
159 rexnal 
 |-  ( E. n e. NN -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x <-> -. A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x )
160 158 159 bitrdi 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( E. n e. NN x < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> -. A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x ) )
161 150 153 160 3imtr3d 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( -. ( S.2 ` F ) <_ x -> -. A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x ) )
162 161 con4d 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
163 10 adantr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = +oo ) -> ( S.2 ` F ) e. RR* )
164 pnfge 
 |-  ( ( S.2 ` F ) e. RR* -> ( S.2 ` F ) <_ +oo )
165 163 164 syl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = +oo ) -> ( S.2 ` F ) <_ +oo )
166 simpr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = +oo ) -> x = +oo )
167 165 166 breqtrrd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = +oo ) -> ( S.2 ` F ) <_ x )
168 167 a1d 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = +oo ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
169 1nn 
 |-  1 e. NN
170 169 ne0ii 
 |-  NN =/= (/)
171 r19.2z 
 |-  ( ( NN =/= (/) /\ A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x ) -> E. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x )
172 170 171 mpan 
 |-  ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> E. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x )
173 37 adantlr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) /\ n e. NN ) -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR )
174 mnflt 
 |-  ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR -> -oo < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) )
175 rexr 
 |-  ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR -> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* )
176 xrltnle 
 |-  ( ( -oo e. RR* /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR* ) -> ( -oo < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ -oo ) )
177 15 175 176 sylancr 
 |-  ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR -> ( -oo < if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <-> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ -oo ) )
178 174 177 mpbid 
 |-  ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) e. RR -> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ -oo )
179 173 178 syl 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) /\ n e. NN ) -> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ -oo )
180 simplr 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) /\ n e. NN ) -> x = -oo )
181 180 breq2d 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) /\ n e. NN ) -> ( if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x <-> if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ -oo ) )
182 179 181 mtbird 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) /\ n e. NN ) -> -. if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x )
183 182 nrexdv 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) -> -. E. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x )
184 183 pm2.21d 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) -> ( E. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
185 172 184 syl5 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x = -oo ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
186 162 168 185 3jaodan 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR \/ x = +oo \/ x = -oo ) ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
187 123 186 sylan2b 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ x e. RR* ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
188 187 ralrimiva 
 |-  ( F : RR --> ( 0 [,] +oo ) -> A. x e. RR* ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
189 188 adantr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> A. x e. RR* ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ x -> ( S.2 ` F ) <_ x ) )
190 109 83 eqeltrrid 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) e. RR* )
191 122 189 190 rspcdva 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( A. n e. NN if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) -> ( S.2 ` F ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) ) )
192 118 191 mpd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( S.2 ` F ) <_ sup ( ran ( m e. NN |-> ( S.1 ` ( g ` m ) ) ) , RR* , < ) )
193 192 109 breqtrrdi 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( S.2 ` F ) <_ sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) )
194 itg2ub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g ` n ) e. dom S.1 /\ ( g ` n ) oR <_ F ) -> ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) )
195 194 3expia 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g ` n ) e. dom S.1 ) -> ( ( g ` n ) oR <_ F -> ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) ) )
196 74 195 sylan2 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ n e. NN ) ) -> ( ( g ` n ) oR <_ F -> ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) ) )
197 196 anassrs 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( ( g ` n ) oR <_ F -> ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) ) )
198 197 adantrd 
 |-  ( ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) /\ n e. NN ) -> ( ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) -> ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) ) )
199 198 ralimdva 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ g : NN --> dom S.1 ) -> ( A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) -> A. n e. NN ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) ) )
200 199 impr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> A. n e. NN ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) )
201 eqid 
 |-  ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) = ( n e. NN |-> ( S.1 ` ( g ` n ) ) )
202 89 201 101 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) = ( S.1 ` ( g ` m ) ) )
203 202 breq1d 
 |-  ( m e. NN -> ( ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) <-> ( S.1 ` ( g ` m ) ) <_ ( S.2 ` F ) ) )
204 203 ralbiia 
 |-  ( A. m e. NN ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) <-> A. m e. NN ( S.1 ` ( g ` m ) ) <_ ( S.2 ` F ) )
205 89 breq1d 
 |-  ( n = m -> ( ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) <-> ( S.1 ` ( g ` m ) ) <_ ( S.2 ` F ) ) )
206 205 cbvralvw 
 |-  ( A. n e. NN ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) <-> A. m e. NN ( S.1 ` ( g ` m ) ) <_ ( S.2 ` F ) )
207 204 206 bitr4i 
 |-  ( A. m e. NN ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) <-> A. n e. NN ( S.1 ` ( g ` n ) ) <_ ( S.2 ` F ) )
208 200 207 sylibr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> A. m e. NN ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) )
209 ffn 
 |-  ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) : NN --> RR -> ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) Fn NN )
210 breq1 
 |-  ( z = ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) -> ( z <_ ( S.2 ` F ) <-> ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) ) )
211 210 ralrn 
 |-  ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) Fn NN -> ( A. z e. ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) z <_ ( S.2 ` F ) <-> A. m e. NN ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) ) )
212 78 209 211 3syl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( A. z e. ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) z <_ ( S.2 ` F ) <-> A. m e. NN ( ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) ` m ) <_ ( S.2 ` F ) ) )
213 208 212 mpbird 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> A. z e. ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) z <_ ( S.2 ` F ) )
214 supxrleub 
 |-  ( ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) C_ RR* /\ ( S.2 ` F ) e. RR* ) -> ( sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) <_ ( S.2 ` F ) <-> A. z e. ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) z <_ ( S.2 ` F ) ) )
215 81 73 214 syl2anc 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) <_ ( S.2 ` F ) <-> A. z e. ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) z <_ ( S.2 ` F ) ) )
216 213 215 mpbird 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) <_ ( S.2 ` F ) )
217 73 83 193 216 xrletrid 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) )
218 69 72 217 3jca 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) ) -> ( g : NN --> dom S.1 /\ A. n e. NN ( g ` n ) oR <_ F /\ ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) ) )
219 218 ex 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) -> ( g : NN --> dom S.1 /\ A. n e. NN ( g ` n ) oR <_ F /\ ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) ) ) )
220 219 eximdv 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( E. g ( g : NN --> dom S.1 /\ A. n e. NN ( ( g ` n ) oR <_ F /\ if ( ( S.2 ` F ) = +oo , n , ( ( S.2 ` F ) - ( 1 / n ) ) ) < ( S.1 ` ( g ` n ) ) ) ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( g ` n ) oR <_ F /\ ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) ) ) )
221 68 220 mpd 
 |-  ( F : RR --> ( 0 [,] +oo ) -> E. g ( g : NN --> dom S.1 /\ A. n e. NN ( g ` n ) oR <_ F /\ ( S.2 ` F ) = sup ( ran ( n e. NN |-> ( S.1 ` ( g ` n ) ) ) , RR* , < ) ) )