Prove that the square root of two is irrational in iset.mm

[jkingdon]

That is, formalize https://en.wikipedia.org/wiki/Square_root_of_2#Constructive_proof or some other proof that the square root of two is apart from any rational number (as described at http://us.metamath.org/ileuni/sqrt2irr.html this is different from "the square root of two is not rational").

Assuming we stick with that proof, the steps are

• given positive integers a and b , ( 2 x. ( b ^ 2 ) ) =/= ( a ^ 2 )
  • use http://us.metamath.org/mpeuni/oddpwdc.html to decompose ( 2 x. ( b ^ 2 ) ) and ( a ^ 2 ) each into a power of two times an odd number and apply the logic that the exponents are odd and even respectively
  • To prove oddpwdc, the set.mm proof uses oddpwdc is now proved at http://us2.metamath.org/ileuni/oddpwdc.html
    • The sup notation, including uzsupss , supcl , and supub to express the idea "the largest power of two which divides a natural number". There might be a way to express this via induction or something but supremum as used in the set.mm proof runs immediately afoul of http://us.metamath.org/ileuni/nnregexmid.html . Induction indeed works as seen at Add pw2dvds to iset.mm (largest power of two which divides a natural number) #2319
    • ssfi to show that "the set of powers of two which divide a natural number" is finite. Although we can't have ssfi ( see http://us.metamath.org/ileuni/ssfiexmid.html ), we probably could show this set is finite if we need to. We didn't end up needing this
    • A number of theorems using http://us.metamath.org/mpeuni/df-dvds.html notation. Presumably intuitionizable I assume these are now in iset.mm. At least, most of the theorems in the df-dvds section and the next one are.
    • Some of the usual intuitionizing as described in the Metamath Proof Explorer cross reference at http://us.metamath.org/ileuni/mmil.html#setmm done
    • Some other theorems from set.mm which aren't in iset.mm yet: http://us.metamath.org/mpeuni/nexple.html , http://us.metamath.org/mpeuni/f1od2.html , http://us.metamath.org/mpeuni/cnvoprab.html , and http://us.metamath.org/mpeuni/spc2ed.html . The first one is handled by http://us.metamath.org/ileuni/bernneq3.html and the others are in Add pw2dvds to iset.mm (largest power of two which divides a natural number) #2319
  • We need something like ( ( A e. NN /\ B e. NN ) -> ( A ^ 2 ) =/= ( 2 x. ( B ^ 2 ) ) ) this is proved at http://us.metamath.org/ileuni/sqne2sq.html
• If two integers are unequal, then the absolute value of their difference is at least one. Although this seems easy, I'm not sure what set.mm theorems are closest or whether we are talking about starting with http://us.metamath.org/ileuni/ztri3or.html , http://us.metamath.org/ileuni/zltp1le.html , etc
• The calculations shown on the wikipedia page which seem straightforward given various theorems such as http://us.metamath.org/ileuni/lediv1dd.html
• Using http://us.metamath.org/ileuni/zletric.html for the "otherwise the quantitative apartness can be trivially established" step
• Once we have established that 1 / ( 3 x. ( B ^ 2 ) ) is a lower bound for the distance between A / B and ( sqrt ` 2 ), do some fairly simple steps including http://us.metamath.org/ileuni/elq.html , establishing that 0 < ( sqrt ` 2 ) , etc, to turn that into Q e. QQ -> ( sqrt ` 2 ) # Q ,

[jkingdon]

As discussed above, I didn't figure out how to formalize the "otherwise the quantitative apartness can be trivially established" part of the wikipedia proof. Perhaps more importantly, I found that ( sqrt ` 2 ) # ( A / B ) could be proved more directly from http://us.metamath.org/ileuni/sqne2sq.html with the key step being http://us.metamath.org/ileuni/sqrt11ap.html .