Description: |- ( ( ph /\ n e. NN ) -> <. ( ( 1st( Fn ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd( Fn ) ) >. e. ( RR X. RR ) ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ovolval5lem2.q | |
|
ovolval5lem2.y | |
||
ovolval5lem2.z | |
||
ovolval5lem2.f | |
||
ovolval5lem2.s | |
||
ovolval5lem2.w | |
||
ovolval5lem2.g | |
||
Assertion | ovolval5lem2 | |