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? Also, in general, is it recommended to download the mmj2 program or the content on the Metamath website sufficient enough? Thanks. -Malik. -- 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/c33479d3-9d01-4445-b978-6b1bd9978646n%40googlegroups.com.
