As an example, I believe the following are all valid but presumably
drastically influence the proof strategy?
$e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.
$e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $.
$e |- ( ph -> C e. RR )
$e |- ( 0 < ( abs ` ( F ` C ) ) ) $.
$e |- ( ph -> C e. RR )
$e |- ( ( F ` C ) =/= 0 ) $.
I'm very curious to better understand how do people go about making
these choices?
I believe it is partly a matter of taste, and partly depends about how
you plan to use the theorem. If you know you'll already have a non-zero
value, then the last two versions may be of advantage.
In any case, it's actually fairly easy to swap from one formulation to
the other, so they will actually not drastically impact the proof strategy.
* between 1 and 2 using ~ rexnal (and df-ne)
* from 4 to 2, using ~ rspcev
* from 2 to 4, using ~ r19.29a for example
* between 3 and 4, using ~ absgt0
In your last two formulations, however, I would have used the deduction
style ( ph -> ( F ` C ) =/= 0 ) , it is weaker and therefore easier to use.
My preference usually goes to limiting the number of free variables, so
I would used the last solution.
Good luck!
_
Thierry
--
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/68f8963e-bd53-3e3c-0bed-e4a4bb6cafad%40gmx.net.
