> > 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.
