Thanks Mario!
I just finished formalizing the following lemma (which is a good chunk of
the proof \o/):
```
$d F c x $. $d c ph x $.
imo72b2lem.1 $e |- ( ph -> F : RR --> RR ) $.
imo72b2lem.2 $e |- ( ph -> G : RR --> RR ) $.
imo72b2lem.3 $e |- ( ph -> A e. RR ) $.
imo72b2lem.4 $e |- ( ph -> B e. RR ) $.
imo72b2lem.5 $e |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) =
( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) $.
imo72b2lem.6 $e |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) $.
imo72b2lem.7 $e |- ( ph -> E. x e. RR ( F ` x ) =/= 0 ) $.
imo72b2lem $p |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) )
<_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) $=
```
Proof here:
https://github.com/spolu/set.mm/commit/454132a35254c17c4e54353b5c2c772eeb2ebb65
One thing I'm quite dissatisfied with is the shape of `imo72b2lem.6`. I'd
much rather have the more natural/intuitive expression `|- ( ph -> A. x e.
RR ( abs ` ( F `x ) ) <_ 1 )` but I completely failed to prove imo72b2lem.6
from it. Any help on this would be greatly appreciated!
-stan
On Wed, Mar 4, 2020 at 8:45 PM Mario Carneiro <[email protected]> wrote:
> Can't look right now, but you should search for a theorem of the form A =
> (/) <-> ( F " A ) = (/) .
>
> On Wed, Mar 4, 2020, 11:30 AM 'Stanislas Polu' via Metamath <
> [email protected]> wrote:
>
>> I'm now looking to prove that `( abs " ( F " RR ) ) =/= (/)` given `F :
>> RR --> RR`. From my exploration of the definition of --> I believe this
>> should be enough but I don't see an easy path towards that? Would anybody
>> have an example in mind that could give me a little bit of inspiration?
>>
>> Thanks for the continued support!
>>
>> -stan
>>
>> On Wed, Mar 4, 2020 at 6:29 PM Benoit <[email protected]> wrote:
>>
>>> Stan: you're right about the need to prove this (if using explicit
>>> substitution): look for the utility theorems exchanging [. / ]. with other
>>> symbols (quantifiers, operations). As said by Jim and Thierry, who are
>>> more experienced in proof building, implicit substitution might be easier
>>> to use. I think it is instructive to compare the details of both proving
>>> styles on a specific example (e.g. ralbidv, suggested by Thierry, would be
>>> analogous to exchanging [. / ]. with A.).
>>>
>>> Still, I think adding what I called rspesbcd could prove useful (if it
>>> is not already in set.mm under another label; I cannot search now, but
>>> it probably is already somewhere).
>>>
>>> Benoît
>>>
>>> --
>>> You received this message because you are subscribed to the Google
>>> Groups "Metamath" group.
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to [email protected].
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com
>>> <https://groups.google.com/d/msgid/metamath/ebdd296f-6bcd-49e0-88c8-c7fef3628cdd%40googlegroups.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Metamath" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to [email protected].
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com
>> <https://groups.google.com/d/msgid/metamath/CACZd_0zFiVT5n-7%2BYh-YL2mDCLMom6R66gq7gbMT7tgJzTzadQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com
> <https://groups.google.com/d/msgid/metamath/CAFXXJStosWZ0BEO7zjpeW90VMNT3pf-Kr6nUaqLefJyA%3Dgwa2Q%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CACZd_0zgFkBD0kOaAXNGyB3PL18Qt06uSHV%3DEmwOjh6Rk5j3OQ%40mail.gmail.com.
