Metamath Proof Explorer

Theorem itg2monolem3

Description: Lemma for itg2mono . (Contributed by Mario Carneiro, 16-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* , < )
itg2monolem2.7 
|- ( ph -> P e. dom S.1 )
itg2monolem2.8 
|- ( ph -> P oR <_ G )
itg2monolem2.9 
|- ( ph -> -. ( S.1 ` P ) <_ S )
Assertion itg2monolem3 
|- ( ph -> ( S.1 ` P ) <_ 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 itg2monolem2.7 
 |-  ( ph -> P e. dom S.1 )
8 itg2monolem2.8 
 |-  ( ph -> P oR <_ G )
9 itg2monolem2.9 
 |-  ( ph -> -. ( S.1 ` P ) <_ S )
10 1 2 3 4 5 6 7 8 9 itg2monolem2 
 |-  ( ph -> S e. RR )
11 10 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> S e. RR )
12 11 recnd 
 |-  ( ( ph /\ t e. RR+ ) -> S e. CC )
13 7 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> P e. dom S.1 )
14 itg1cl 
 |-  ( P e. dom S.1 -> ( S.1 ` P ) e. RR )
15 13 14 syl 
 |-  ( ( ph /\ t e. RR+ ) -> ( S.1 ` P ) e. RR )
16 15 recnd 
 |-  ( ( ph /\ t e. RR+ ) -> ( S.1 ` P ) e. CC )
17 simpr 
 |-  ( ( ph /\ t e. RR+ ) -> t e. RR+ )
18 17 rpred 
 |-  ( ( ph /\ t e. RR+ ) -> t e. RR )
19 11 18 readdcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( S + t ) e. RR )
20 19 recnd 
 |-  ( ( ph /\ t e. RR+ ) -> ( S + t ) e. CC )
21 0red 
 |-  ( ( ph /\ t e. RR+ ) -> 0 e. RR )
22 0xr 
 |-  0 e. RR*
23 22 a1i 
 |-  ( ph -> 0 e. RR* )
24 fveq2 
 |-  ( n = 1 -> ( F ` n ) = ( F ` 1 ) )
25 24 feq1d 
 |-  ( n = 1 -> ( ( F ` n ) : RR --> ( 0 [,] +oo ) <-> ( F ` 1 ) : RR --> ( 0 [,] +oo ) ) )
26 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
27 fss 
 |-  ( ( ( F ` n ) : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
28 3 26 27 sylancl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,] +oo ) )
29 28 ralrimiva 
 |-  ( ph -> A. n e. NN ( F ` n ) : RR --> ( 0 [,] +oo ) )
30 1nn 
 |-  1 e. NN
31 30 a1i 
 |-  ( ph -> 1 e. NN )
32 25 29 31 rspcdva 
 |-  ( ph -> ( F ` 1 ) : RR --> ( 0 [,] +oo ) )
33 itg2cl 
 |-  ( ( F ` 1 ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` 1 ) ) e. RR* )
34 32 33 syl 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) e. RR* )
35 itg2cl 
 |-  ( ( F ` n ) : RR --> ( 0 [,] +oo ) -> ( S.2 ` ( F ` n ) ) e. RR* )
36 28 35 syl 
 |-  ( ( ph /\ n e. NN ) -> ( S.2 ` ( F ` n ) ) e. RR* )
37 36 fmpttd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) : NN --> RR* )
38 37 frnd 
 |-  ( ph -> ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* )
39 supxrcl 
 |-  ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) e. RR* )
40 38 39 syl 
 |-  ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) e. RR* )
41 6 40 eqeltrid 
 |-  ( ph -> S e. RR* )
42 itg2ge0 
 |-  ( ( F ` 1 ) : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` ( F ` 1 ) ) )
43 32 42 syl 
 |-  ( ph -> 0 <_ ( S.2 ` ( F ` 1 ) ) )
44 2fveq3 
 |-  ( n = 1 -> ( S.2 ` ( F ` n ) ) = ( S.2 ` ( F ` 1 ) ) )
45 eqid 
 |-  ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) = ( n e. NN |-> ( S.2 ` ( F ` n ) ) )
46 fvex 
 |-  ( S.2 ` ( F ` 1 ) ) e. _V
47 44 45 46 fvmpt 
 |-  ( 1 e. NN -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) = ( S.2 ` ( F ` 1 ) ) )
48 30 47 ax-mp 
 |-  ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) = ( S.2 ` ( F ` 1 ) )
49 37 ffnd 
 |-  ( ph -> ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN )
50 fnfvelrn 
 |-  ( ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) Fn NN /\ 1 e. NN ) -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
51 49 30 50 sylancl 
 |-  ( ph -> ( ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ` 1 ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
52 48 51 eqeltrrid 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) )
53 supxrub 
 |-  ( ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) C_ RR* /\ ( S.2 ` ( F ` 1 ) ) e. ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) ) -> ( S.2 ` ( F ` 1 ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) )
54 38 52 53 syl2anc 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) <_ sup ( ran ( n e. NN |-> ( S.2 ` ( F ` n ) ) ) , RR* , < ) )
55 54 6 breqtrrdi 
 |-  ( ph -> ( S.2 ` ( F ` 1 ) ) <_ S )
56 23 34 41 43 55 xrletrd 
 |-  ( ph -> 0 <_ S )
57 56 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> 0 <_ S )
58 11 17 ltaddrpd 
 |-  ( ( ph /\ t e. RR+ ) -> S < ( S + t ) )
59 21 11 19 57 58 lelttrd 
 |-  ( ( ph /\ t e. RR+ ) -> 0 < ( S + t ) )
60 59 gt0ne0d 
 |-  ( ( ph /\ t e. RR+ ) -> ( S + t ) =/= 0 )
61 12 16 20 60 div23d 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S x. ( S.1 ` P ) ) / ( S + t ) ) = ( ( S / ( S + t ) ) x. ( S.1 ` P ) ) )
62 11 19 60 redivcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( S / ( S + t ) ) e. RR )
63 62 15 remulcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S / ( S + t ) ) x. ( S.1 ` P ) ) e. RR )
64 halfre 
 |-  ( 1 / 2 ) e. RR
65 ifcl 
 |-  ( ( ( S / ( S + t ) ) e. RR /\ ( 1 / 2 ) e. RR ) -> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. RR )
66 62 64 65 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. RR )
67 66 15 remulcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( S.1 ` P ) ) e. RR )
68 max2 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( S / ( S + t ) ) e. RR ) -> ( S / ( S + t ) ) <_ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) )
69 64 62 68 sylancr 
 |-  ( ( ph /\ t e. RR+ ) -> ( S / ( S + t ) ) <_ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) )
70 7 14 syl 
 |-  ( ph -> ( S.1 ` P ) e. RR )
71 70 rexrd 
 |-  ( ph -> ( S.1 ` P ) e. RR* )
72 xrltnle 
 |-  ( ( S e. RR* /\ ( S.1 ` P ) e. RR* ) -> ( S < ( S.1 ` P ) <-> -. ( S.1 ` P ) <_ S ) )
73 41 71 72 syl2anc 
 |-  ( ph -> ( S < ( S.1 ` P ) <-> -. ( S.1 ` P ) <_ S ) )
74 9 73 mpbird 
 |-  ( ph -> S < ( S.1 ` P ) )
75 74 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> S < ( S.1 ` P ) )
76 21 11 15 57 75 lelttrd 
 |-  ( ( ph /\ t e. RR+ ) -> 0 < ( S.1 ` P ) )
77 lemul1 
 |-  ( ( ( S / ( S + t ) ) e. RR /\ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. RR /\ ( ( S.1 ` P ) e. RR /\ 0 < ( S.1 ` P ) ) ) -> ( ( S / ( S + t ) ) <_ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) <-> ( ( S / ( S + t ) ) x. ( S.1 ` P ) ) <_ ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( S.1 ` P ) ) ) )
78 62 66 15 76 77 syl112anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S / ( S + t ) ) <_ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) <-> ( ( S / ( S + t ) ) x. ( S.1 ` P ) ) <_ ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( S.1 ` P ) ) ) )
79 69 78 mpbid 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S / ( S + t ) ) x. ( S.1 ` P ) ) <_ ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( S.1 ` P ) ) )
80 2 adantlr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ n e. NN ) -> ( F ` n ) e. MblFn )
81 3 adantlr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ n e. NN ) -> ( F ` n ) : RR --> ( 0 [,) +oo ) )
82 4 adantlr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ n e. NN ) -> ( F ` n ) oR <_ ( F ` ( n + 1 ) ) )
83 5 adantlr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ x e. RR ) -> E. y e. RR A. n e. NN ( ( F ` n ) ` x ) <_ y )
84 64 a1i 
 |-  ( ( ph /\ t e. RR+ ) -> ( 1 / 2 ) e. RR )
85 halfgt0 
 |-  0 < ( 1 / 2 )
86 85 a1i 
 |-  ( ( ph /\ t e. RR+ ) -> 0 < ( 1 / 2 ) )
87 max1 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( S / ( S + t ) ) e. RR ) -> ( 1 / 2 ) <_ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) )
88 64 62 87 sylancr 
 |-  ( ( ph /\ t e. RR+ ) -> ( 1 / 2 ) <_ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) )
89 21 84 66 86 88 ltletrd 
 |-  ( ( ph /\ t e. RR+ ) -> 0 < if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) )
90 20 mulid1d 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S + t ) x. 1 ) = ( S + t ) )
91 58 90 breqtrrd 
 |-  ( ( ph /\ t e. RR+ ) -> S < ( ( S + t ) x. 1 ) )
92 1red 
 |-  ( ( ph /\ t e. RR+ ) -> 1 e. RR )
93 ltdivmul 
 |-  ( ( S e. RR /\ 1 e. RR /\ ( ( S + t ) e. RR /\ 0 < ( S + t ) ) ) -> ( ( S / ( S + t ) ) < 1 <-> S < ( ( S + t ) x. 1 ) ) )
94 11 92 19 59 93 syl112anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S / ( S + t ) ) < 1 <-> S < ( ( S + t ) x. 1 ) ) )
95 91 94 mpbird 
 |-  ( ( ph /\ t e. RR+ ) -> ( S / ( S + t ) ) < 1 )
96 halflt1 
 |-  ( 1 / 2 ) < 1
97 breq1 
 |-  ( ( S / ( S + t ) ) = if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) -> ( ( S / ( S + t ) ) < 1 <-> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) < 1 ) )
98 breq1 
 |-  ( ( 1 / 2 ) = if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) -> ( ( 1 / 2 ) < 1 <-> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) < 1 ) )
99 97 98 ifboth 
 |-  ( ( ( S / ( S + t ) ) < 1 /\ ( 1 / 2 ) < 1 ) -> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) < 1 )
100 95 96 99 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) < 1 )
101 1xr 
 |-  1 e. RR*
102 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. ( 0 (,) 1 ) <-> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. RR /\ 0 < if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) /\ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) < 1 ) ) )
103 22 101 102 mp2an 
 |-  ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. ( 0 (,) 1 ) <-> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. RR /\ 0 < if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) /\ if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) < 1 ) )
104 66 89 100 103 syl3anbrc 
 |-  ( ( ph /\ t e. RR+ ) -> if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) e. ( 0 (,) 1 ) )
105 8 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> P oR <_ G )
106 fveq2 
 |-  ( y = x -> ( P ` y ) = ( P ` x ) )
107 106 oveq2d 
 |-  ( y = x -> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` y ) ) = ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` x ) ) )
108 fveq2 
 |-  ( y = x -> ( ( F ` n ) ` y ) = ( ( F ` n ) ` x ) )
109 107 108 breq12d 
 |-  ( y = x -> ( ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` y ) ) <_ ( ( F ` n ) ` y ) <-> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` x ) ) <_ ( ( F ` n ) ` x ) ) )
110 109 cbvrabv 
 |-  { y e. RR | ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` y ) ) <_ ( ( F ` n ) ` y ) } = { x e. RR | ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` x ) ) <_ ( ( F ` n ) ` x ) }
111 110 mpteq2i 
 |-  ( n e. NN |-> { y e. RR | ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` y ) ) <_ ( ( F ` n ) ` y ) } ) = ( n e. NN |-> { x e. RR | ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( P ` x ) ) <_ ( ( F ` n ) ` x ) } )
112 1 80 81 82 83 6 104 13 105 11 111 itg2monolem1 
 |-  ( ( ph /\ t e. RR+ ) -> ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( S.1 ` P ) ) <_ S )
113 63 67 11 79 112 letrd 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S / ( S + t ) ) x. ( S.1 ` P ) ) <_ S )
114 61 113 eqbrtrd 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S x. ( S.1 ` P ) ) / ( S + t ) ) <_ S )
115 11 15 remulcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( S x. ( S.1 ` P ) ) e. RR )
116 ledivmul2 
 |-  ( ( ( S x. ( S.1 ` P ) ) e. RR /\ S e. RR /\ ( ( S + t ) e. RR /\ 0 < ( S + t ) ) ) -> ( ( ( S x. ( S.1 ` P ) ) / ( S + t ) ) <_ S <-> ( S x. ( S.1 ` P ) ) <_ ( S x. ( S + t ) ) ) )
117 115 11 19 59 116 syl112anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( ( S x. ( S.1 ` P ) ) / ( S + t ) ) <_ S <-> ( S x. ( S.1 ` P ) ) <_ ( S x. ( S + t ) ) ) )
118 114 117 mpbid 
 |-  ( ( ph /\ t e. RR+ ) -> ( S x. ( S.1 ` P ) ) <_ ( S x. ( S + t ) ) )
119 66 15 89 76 mulgt0d 
 |-  ( ( ph /\ t e. RR+ ) -> 0 < ( if ( ( 1 / 2 ) <_ ( S / ( S + t ) ) , ( S / ( S + t ) ) , ( 1 / 2 ) ) x. ( S.1 ` P ) ) )
120 21 67 11 119 112 ltletrd 
 |-  ( ( ph /\ t e. RR+ ) -> 0 < S )
121 lemul2 
 |-  ( ( ( S.1 ` P ) e. RR /\ ( S + t ) e. RR /\ ( S e. RR /\ 0 < S ) ) -> ( ( S.1 ` P ) <_ ( S + t ) <-> ( S x. ( S.1 ` P ) ) <_ ( S x. ( S + t ) ) ) )
122 15 19 11 120 121 syl112anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( S.1 ` P ) <_ ( S + t ) <-> ( S x. ( S.1 ` P ) ) <_ ( S x. ( S + t ) ) ) )
123 118 122 mpbird 
 |-  ( ( ph /\ t e. RR+ ) -> ( S.1 ` P ) <_ ( S + t ) )
124 123 ralrimiva 
 |-  ( ph -> A. t e. RR+ ( S.1 ` P ) <_ ( S + t ) )
125 alrple 
 |-  ( ( ( S.1 ` P ) e. RR /\ S e. RR ) -> ( ( S.1 ` P ) <_ S <-> A. t e. RR+ ( S.1 ` P ) <_ ( S + t ) ) )
126 70 10 125 syl2anc 
 |-  ( ph -> ( ( S.1 ` P ) <_ S <-> A. t e. RR+ ( S.1 ` P ) <_ ( S + t ) ) )
127 124 126 mpbird 
 |-  ( ph -> ( S.1 ` P ) <_ S )