On Sun, Nov 20, 2022 at 9:24 PM M Malik <[email protected]> wrote: > Hello Metamath peeps, > > I am trying to learn advanced math with assistance of Metamath. I > understand a lot of elementary theorems that are in the database. However, > I thought I would jump to (sqrt2irr -Irrationality of square root of 2), > but its proof isn't really making sense to me. > > I am specifically confused about this wff [ For all x e. Z (sqrt2 =/= x/z) > ]. Is this something to be assumed true from the start? >
No, it (more or less) is proved by complete induction on z (which is to say, induction on y e. NN such that x < y) at step 78 of https://us.metamath.org/mpeuni/sqrt2irr.html . > Also, in general, is it recommended to download the mmj2 program or the > content on the Metamath website sufficient enough? > The content of the website should be sufficient for viewing proofs, and indeed is somewhat better than the mmj2 display for many purposes. mmj2 is more if you are interested in writing a proof yourself. Mario -- 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/CAFXXJSv6OxjA-Mz-%2BeYM-tp-RqVSQz0_PP0pE%2BY%2BFgDOX3sPAg%40mail.gmail.com.
