$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
        Irrationality of square root of 2
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

  ${
    sqr2irrlem1.1 $e |- A e. NN $.
    sqr2irrlem1.2 $e |- B e. NN $.
    $( Lemma for irrationality of square root of 2.  Technical lemma used
       to simplify the main induction step. $)
    sqr2irrlem1 $p |- ( ( A ^ 2 ) = ( 2 x. ( B ^ 2 ) ) ->
                      ( ( B < A /\ ( A / 2 ) e. NN ) /\
                     ( B ^ 2 ) = ( 2 x. ( ( A / 2 ) ^ 2 ) ) ) ) $=
      ( c2 cexp co cmulc wceq clt wbr cdiv cn wcel wa c1 nnre sqrecl recn
      mulid2 caddc ax1re ltplus1 df-2 breqtrr 2re nnsqcl nngt0 ltmul1i mpbi
      eqbrtrr breq2 mpbiri cc0 cle wb ax0re ltlei lt2sqe mp2an sylibr 2cn 2pos
      gt0ne0i divmul eleq1 nnesq sylbir eqcoms jca redivcl remulcl mulcan nncn
      sqdiv sqval opreq2i eqtr mulass mulcl muln0 divcan2 3eqtr3 eqeq1i bitr3
      biimpr eqcomd ) AEFGZEBEFGZHGZIZBAJKZAELGZMNZOWIEWMEFGZHGZIWKWLWNWKWIWHJK
      ZWLWKWQWIWJJKPWIHGZWIWJJWIWIBBDQZRZSZTPEJKWRWJJKPPPUAGEJPUBUCUDUEPEWIUBUF
      WTWIBDUGZUHUIUJUKWHWJWIJULUMUNBUOKUNAUOKWLWQUPUNBUQWSBDUHURUNAUQACQZACUHU
      RBAWSXCUSUTVAWNWJWHWJWHIWHELGZWIIZWNWHEWIWHAXCRSZVBXAEUFVCVDZVEXEXDMNZWNX
      EXHWIMNXBXDWIMVFUMACVGVAVHVIVJWKWPWIWPWIIZWKXIEWPHGZWJIWKEWPWIVBWPEWOUFWM
      AEXCUFXGVKRZVLSXAXGVMXJWHWJEEHGZWOHGXLWHXLLGZHGXJWHWOXMXLHWOWHEEFGZLGXMAE
      ACVNVBXGVOXNXLWHLEVBVPVQVRVQEEWOVBVBWOXKSVSXLWHEEVBVBVTXFEEVBVBXGXGWAWBWC
      WDWEWFWGVJ $.
      $( [20-Aug-01] $)
  $}

  $( Lemma for irrationality of square root of 2.  Eliminates hypotheses with
     weak deduction theorem. $)
  sqr2irrlem2 $p |- ( ( A e. NN /\ B e. NN ) ->
                   ( ( A ^ 2 ) = ( 2 x. ( B ^ 2 ) ) ->
                    ( ( B < A /\ ( A / 2 ) e. NN ) /\
                   ( B ^ 2 ) = ( 2 x. ( ( A / 2 ) ^ 2 ) ) ) ) ) $=
    ( cn wcel c2 cexp co cmulc wceq clt wbr cdiv wa wi cif opreq1 eqeq1d breq2
    eleq1d anbi12d opreq1d opreq2d eqeq2d imbi12d breq1 anbi1d 2nn elimel
    sqr2irrlem1 dedth2h ) ACDZBCDZAEFGZEBEFGZHGZIZBAJKZAELGZCDZMZUNEUREFGZHGZIZ
    MZNUKAEOZEFGZUOIZBVEJKZVEELGZCDZMZUNEVIEFGZHGZIZMZNVFEULBEOZEFGZHGZIZVPVEJK
    ZVJMZVQVMIZMZNABEEAVEIZUPVGVDVOWDUMVFUOAVEEFPQWDUTVKVCVNWDUQVHUSVJAVEBJRWDU
    RVICAVEELPZSTWDVBVMUNWDVAVLEHWDURVIEFWEUAUBUCTUDBVPIZVGVSVOWCWFUOVRVFWFUNVQ
    EHBVPEFPZUBUCWFVKWAVNWBWFVHVTVJBVPVEJUEUFWFUNVQVMWGQTUDVEVPAECUGUHBECUGUHUI
    UJ $.
    $( [20-Aug-01] $)

  ${
    $d x y z w $.
    $( Main theorem for irrationality of square root of 2.  There are no
       natural numbers such that the square of one is twice the square of the
       other.  Uses strong induction. $)
    sqr2irrlem3 $p |- -. E. x e. NN E. y e. NN
                            ( x ^ 2 ) = ( 2 x. ( y ^ 2 ) ) $=
      ( vz vw cv c2 cexp co cmulc wceq cn wrex wn wral wcel weq opreq1 eqeq1d
      negbid biraldv opreq2d eqeq2d cbvralv syl6bb clt wbr wi wa cdiv breq1
      imbi12d rcla4v imp syl6 imp3a imnan sylib adantll sqr2irrlem2 adantlr
      mtod exp31 r19.21adv indstr ralnex rgen mpbi ) AEZFGHZFBEZFGHZIHZJZBKLZMZ
      AKNVNAKLMVOAKVHKOZVMMZBKNZVOVRCEZFGHZFDEZFGHZIHZJZMZDKNZACACPZVRVTVLJZMZB
      KNWFWGVQWIBKWGVMWHWGVIVTVLVHVSFGQRSTWIWEBDKBDPZWHWDWJVLWCVTWJVKWBFIVJWAFG
      QUAUBSUCUDVPVSVHUEUFZWFUGZCKNZVQBKVPWMVJKOZVQVPWMUHWNUHVMVJVHUEUFZVHFUIHZ
      KOZUHZVKFWPFGHZIHZJZUHZWMWNXBMZVPWMWNUHZWRXAMZUGXCXDWOWQXEXDWOVKWCJZMZDKN
      ZWQXEUGWMWNWOXHUGZWLXICVJKCBPZWKWOWFXHVSVJVHUEUJXJWEXGDKXJWDXFXJVTVKWCVSV
      JFGQRSTUKULUMXGXEDWPKWAWPJZXFXAXKWCWTVKXKWBWSFIWAWPFGQUAUBSULUNUOWRXAUPUQ
      URVPWNVMXBUGWMVHVJUSUTVAVBVCVDVMBKVEUQVFVNAKVEVG $.
      $( [20-Aug-01] $)
  $}

  ${
    sqr2irrlem4.1 $e |- A e. NN $.
    sqr2irrlem4.2 $e |- B e. NN $.
    $( Lemma for irrationality of square root of 2. $)
    sqr2irrlem4 $p |- ( ( sqr ` 2 ) = ( A / B ) <->
                      ( A ^ 2 ) = ( 2 x. ( B ^ 2 ) ) ) $=
      ( c2 cexp co cmulc wceq csqr cfv cdiv nncn nnne0 sqdiv eqcomi nnsqcl 2cn
      divcan4 eqeq12i nnre sqrecl recn 2re remulcl div11 eqcom 3bitr3 cc0 cle
      wbr wb ax0re 2pos ltlei redivcl sqege0 sqr11 mp2an bitr4 nngt0 divgt0i
      sqrsqe ax-mp eqeq2i bitr2 ) AEFGZEBEFGZHGZIZEJKZABLGZEFGZJKZIZVKVLIVJEVMI
      ZVOVGVHLGZVIVHLGZIVMEIVJVPVQVMVREVMVQABACMBDMBDNZOPVHEVHBDQZMZRVHVTNZSTVG
      VIVHVGAACUAZUBUCVIEVHUDVHVTUAUEUCWAWBUFVMEUGUHUIEUJUKUIVMUJUKVOVPULUIEUMU
      DUNUOVLABWCBDUAZVSUPZUQEVMUDVLWEUBURUSUTVNVLVKUIVLUJUKVNVLIUIVLUMWEABWCWD
      ACVABDVAVBUOVLWEVCVDVEVF $.
      $( [20-Aug-01] $)
  $}

  $( Lemma for irrationality of square root of 2.  Eliminates hypotheses with
     weak deduction theorem. $)
  sqr2irrlem5 $p |- ( ( A e. NN /\ B e. NN ) -> ( ( sqr ` 2 ) = ( A / B )
                     <-> ( A ^ 2 ) = ( 2 x. ( B ^ 2 ) ) ) ) $=
    ( cn wcel c2 csqr cfv cdiv co wceq cexp cmulc wb cif opreq1 eqeq2d eqeq1d
    bibi12d opreq2 opreq2d 2nn elimel sqr2irrlem4 dedth2h ) ACDZBCDZEFGZABHIZJZ
    AEKIZEBEKIZLIZJZMUGUEAENZBHIZJZUNEKIZULJZMUGUNUFBENZHIZJZUQEUSEKIZLIZJZMABE
    EAUNJZUIUPUMURVEUHUOUGAUNBHOPVEUJUQULAUNEKOQRBUSJZUPVAURVDVFUOUTUGBUSUNHSPV
    FULVCUQVFUKVBELBUSEKOTPRUNUSAECUAUBBECUAUBUCUD $.
    $( [20-Aug-01] $)

  ${
    $d x y $.
    $( The square root of 2 is irrational. $)
    sqr2irr $p |- ( sqr ` 2 ) e/ QQ $=
      ( vx vy c2 csqr cfv cq wnel wcel wn cv cdiv co wceq cn wrex cz cexp
      cmulc sqr2irrlem3 sqr2irrlem5 bi2rexa mtbir cc0 clt wbr wa wi wb nngt0t
      adantr cr ax0re ltmuldivt mp3an1 nnret zret syl2an mpd ancoms 2re 2pos
      sqrgt0i breq2 mpbii syl5bir cc nncnt mulzer2t syl breq1d adantl sylibd
      exp r19.23adv anc2li elnnz syl6ibr impac r19.22i2 mto elq df-nel mpbir )
      CDEZFGWDFHZIWEWDAJZBJZKLZMZBNOZAPOZWKWJANOZWLWFCQLCWGCQLRLMZBNOANOABSWIWM
      ABNNWFWGTUAUBWJWJAPNWFPHZWJWFNHZWNWJWNUCWFUDUEZUFWOWNWJWPWNWIWPBNWNWGNHZW
      IWPUGWNWQUFZWIUCWGRLZWFUDUEZWPWRWTUCWHUDUEZWIWQWNWTXAUHZWQWNUFUCWGUDUEZXB
      WQXCWNWGUIUJWGUKHZWFUKHZXCXBUGZWQWNUCUKHXDXEXFULUCWGWFUMUNWGUOWFUPUQURUSW
      IUCWDUDUEXACUTVAVBWDWHUCUDVCVDVEWQWTWPUHWNWQWSUCWFUDWQWGVFHWSUCMWGVGWGVHV
      IVJVKVLVMVNVOWFVPVQVRVSVTABWDWAUBWDFWBWC $.
      $( [8-Jan-02] $)
  $}