Hello Mario, Sorry if this is too trivial of a question. Where does this statement [ z < 1 -> A. x e. ZZ ( sqrt ` 2 ) =/= ( x / z ) ] come from? I understand it's associated to ( n = 1 ) case for strong induction, but I am not sure what makes it true.
Also, is there a way to know what book this theorem was referenced from? I apologize since these questions aren't really related to Metamath but math in general. Let me know if I need to stop posting these kind of questions here. Appreciate your time. -Malik. On Sunday, November 20, 2022 at 9:53:03 PM UTC-5 [email protected] wrote: > 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/b31cd4ce-0dff-496f-9892-b1a714987710n%40googlegroups.com.
