These kinds of questions are fine, although you are asking questions about statements rather than proofs. "where does this proposition come from" is not a very targeted question. I assume you are referring to step 13 of https://us.metamath.org/mpeuni/sqrt2irr.html , in which case we can check the proof that leads up to it:
11 nnnlt1 <https://us.metamath.org/mpeuni/nnnlt1.html> 11302 . . . . . . . . 9 β’ (π§ β β β Β¬ π§ < 1) 12 11 <https://us.metamath.org/mpeuni/sqrt2irr.html#11> pm2.21d <https://us.metamath.org/mpeuni/pm2.21d.html> 119 . . . . . . . 8 β’ (π§ β β β (π§ < 1 β βπ₯ β β€ (ββ2) β (π₯ / π§))) 13 12 <https://us.metamath.org/mpeuni/sqrt2irr.html#12> rgen <https://us.metamath.org/mpeuni/rgen.html> 3066 . . . . . . 7 β’ βπ§ β β (π§ < 1 β βπ₯ β β€ (ββ2) β (π₯ / π§)) That is, it is true that every natural number z less than 1 satisfies A. x e. ZZ (sqrt`2) =/= (x/z) simply because there are no natural numbers less than 1. (In metamath the set NN denotes the strictly positive integers, i.e. 1, 2, 3, ... and all of these are greater or equal to 1.) I don't have a particular book to reference for this proof (it would be mentioned in the head comment if there was), but it is a classical proof, by "infinite descent" (I think Fermat is credited for it). The proof in sqrt2irr itself is merely the setup work, the core of the proof is in sqrt2irrlem, where we show that if sqrt(2) = A/B then A/2 and B/2 are both integers, in which case (A/2)/(B/2) is a smaller expression for sqrt(2). So we are doing induction on B here, with the observation that B/2 is a natural number less than B so that we can assume by induction that sqrt(2) is not a fraction with denominator B/2 and hence also not a fraction with denominator B. On Mon, Nov 21, 2022 at 4:41 PM M Malik <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/b31cd4ce-0dff-496f-9892-b1a714987710n%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/CAFXXJSsx4YO_taRjjJAes5sO%3DQJAEsv6%3DykSYjT4ZxfZQ_Qugw%40mail.gmail.com.
