Thanks Benoit for the comments on my current branch. I will definitely apply them and submit my mathbox to set.mm!
> This would be a long but automatic derivation. I think mmj2 does this kind of things automatically. But why would you need this ? Wouldn't I need this to go from the substituted rspesbcd.2 (following your naming convention): |- ( ph -> [. 1 / x ]. A. x e. RR ( abs ` ( F ` x ) ) <_ 1 ) to the hypothesis imo72b2lem.6 (following my naming convention): |- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 ) Maybe I'm missing something but my high level goal is to prove: |- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c ) using: |- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 ) Thanks! -stan On Wed, Mar 4, 2020 at 4:36 PM Benoit <[email protected]> wrote: > I started my quest towards IMO 1972 B2 by formalizing a simple >> induction problem (just for fun): `( N e. NN -> 3 || ( ( 4 ^ N ) + 5 ) > > > I think ~ inductionexd (with the caveat below) is a nice instructive > example, and could be moved to main, as the first theorem of the new > subsection > 17.1.5 Examples of proofs by induction > Do the maintainers agree ? Which labeling ? ~ ex-induction0 ? > > Beware that in set.mm, the symbol NN does not denote the natural numbers, > but only the nonzero natural numbers. Therefore, stating ~ inductionexd > with " N e. NN0 " is more... natural. (And its proof might be shorter > since the base case involves smaller numbers.) > > I hope you do a PR with your mathbox. Your eqdivs2d, leeqd and leeq2d > seem to be special cases of oveq2. They are probably not worth stating. > In comments, use " ~ label " to link to other statements. Use > "MM-PA>minimize *" after completing your proofs (maybe you do it already; > and more generally, > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md). > > >> One thing I'm stuck on is the following: In a natural deduction >> setting, how does one demonstrate an existence assuming a witness? >> >> From natded[1] the starting point seems to consist in applying >> spesbcd[2], but I'm unclear on how to breach the difference between >> `E. c ph` and `E. c e. A ph` as it does not seem to exist an >> equivalent for the latter? > > > There should be a theorem in set.mm of the form > ${ > $d x B $. > rspesbcd.1 $e |- ( ph -> A e. B ) $. > rspesbcd.2 $e |- ( ph -> [. A / x ]. ps ) $. > rspesbcd $p |- ( ph -> E. x e. B ps ) $= ? $. > $} > If not, add it: just use spesbcd with the formula "( x e. B /\ ps )". > > >> Even assuming this problem solved, I'm also >> at a loss attempting to prove the following given `imo72b2lem.6`: >> >> ``` >> |- ( ph -> [. 1 / c ]. A. x e. RR ( abs ` ( F ` x ) ) <_ c ) >> ``` >> > > This would be a long but automatic derivation. I think mmj2 does this > kind of things automatically. But why would you need this ? > > 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/99e1a2bd-d406-44ee-a2ef-8fd9739d2df4%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/99e1a2bd-d406-44ee-a2ef-8fd9739d2df4%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_0xPnQdqxhhmGdCfKDYDVcniXS4YxioJLBpAjPxzWVpBrg%40mail.gmail.com.
