pythtrip.miz



    begin

    reserve a,b,c,k,k9,m,n,n9,p,p9 for Element of NAT ;

    reserve i,i9 for Integer;

    definition

      let m,n be Nat;

      :: original: are_coprime

      redefine

      :: PYTHTRIP:def1

      pred m,n are_coprime means for k be Nat st k divides m & k divides n holds k = 1;

      compatibility

      proof

        hereby

          assume (m,n) are_coprime ;

          then

           A1: (m gcd n) = 1;

          let k be Nat;

          assume k divides m & k divides n;

          then k divides 1 by A1, NAT_D:def 5;

          hence k = 1 by WSIERP_1: 15;

        end;

        assume for k be Nat st k divides m & k divides n holds k = 1;

        then

         A2: for k be Nat st k divides m & k divides n holds k divides 1;

        1 divides m & 1 divides n by NAT_D: 6;

        hence (m gcd n) = 1 by A2, NAT_D:def 5;

      end;

    end

    definition

      let m,n be Nat;

      :: original: are_coprime

      redefine

      :: PYTHTRIP:def2

      pred m,n are_coprime means for p be prime Nat holds not (p divides m & p divides n);

      compatibility

      proof

        hereby

          assume

           A1: (m,n) are_coprime ;

          let p be prime Nat;

          assume p divides m & p divides n;

          then p = 1 by A1;

          hence contradiction by INT_2:def 4;

        end;

        assume

         A2: for p be prime Nat holds not (p divides m & p divides n);

        let k be Nat;

        assume

         A3: k divides m & k divides n;

        per cases by NAT_1: 25;

          suppose k = 0 ;

          then m = 0 & n = 0 by A3;

          hence thesis by A2, INT_2: 28, NAT_D: 6;

        end;

          suppose k = 1;

          hence thesis;

        end;

          suppose k > 1;

          then k >= (1 + 1) by NAT_1: 13;

          then

          consider p such that

           A4: p is prime and

           A5: p divides k by INT_2: 31;

          reconsider p9 = p as prime Element of NAT by A4;

          p9 divides m & p9 divides n by A3, A5, NAT_D: 4;

          hence thesis by A2;

        end;

      end;

    end

    begin

    definition

      let n be Number;

      :: PYTHTRIP:def3

      attr n is square means

      : Def3: ex m be Nat st n = (m ^2 );

    end

    registration

      cluster square -> natural for Number;

      coherence ;

    end

    registration

      let n be Nat;

      cluster (n ^2 ) -> square;

      coherence ;

    end

    registration

      cluster even square for Element of NAT ;

      existence

      proof

        take 0 ;

         0 = (2 * ( 0 ^2 ));

        hence thesis;

      end;

    end

    registration

      cluster odd square for Element of NAT ;

      existence

      proof

        take 1;

        (1 ^2 ) = ((2 * 0 ) + 1);

        hence thesis;

      end;

    end

    registration

      cluster even square for Integer;

      existence

      proof

        take the even square Element of NAT ;

        thus thesis;

      end;

    end

    registration

      cluster odd square for Integer;

      existence

      proof

        take the odd square Element of NAT ;

        thus thesis;

      end;

    end

    registration

      let m,n be square object;

      cluster (m * n) -> square;

      coherence

      proof

        consider n9 be Nat such that

         A1: n = (n9 ^2 ) by Def3;

        consider m9 be Nat such that

         A2: m = (m9 ^2 ) by Def3;

        (m * n) = ((m9 * n9) ^2 ) by A2, A1;

        hence thesis;

      end;

    end

    theorem :: PYTHTRIP:1

    

     Th1: (m * n) is square & (m,n) are_coprime implies m is square & n is square

    proof

      defpred P[ Nat] means for m, n st (m * n) = $1 & (m * n) is square & (m,n) are_coprime holds m is square & n is square;

      

       A1: for mn be Nat st for k be Nat st k < mn holds P[k] holds P[mn]

      proof

        let mn be Nat;

        assume

         A2: for k be Nat st k < mn holds for m, n st (m * n) = k & (m * n) is square & (m,n) are_coprime holds m is square & n is square;

        let m, n;

        assume

         A3: (m * n) = mn;

        assume (m * n) is square;

        then

        consider mn9 be Nat such that

         A4: mn = (mn9 ^2 ) by A3;

        assume

         A5: (m,n) are_coprime ;

        then

         A6: (m gcd n) = (1 ^2 );

        per cases by A3, NAT_1: 25;

          suppose

           A7: (m * n) = 0 ;

          hereby

            per cases by A7, XCMPLX_1: 6;

              suppose m = ( 0 ^2 );

              hence thesis by A6, NEWTON: 52;

            end;

              suppose n = ( 0 ^2 );

              hence thesis by A6, NEWTON: 52;

            end;

          end;

        end;

          suppose (m * n) = (1 ^2 );

          hence thesis by NAT_1: 15;

        end;

          suppose

           A8: mn > 1;

          then mn >= (1 + 1) by NAT_1: 13;

          then

          consider p9 such that

           A9: p9 is prime and

           A10: p9 divides mn by INT_2: 31;

          reconsider p = p9 as prime Element of NAT by A9;

          p divides mn9 by A4, A10, NEWTON: 80;

          then

          consider mn99 be Nat such that

           A11: mn9 = (p * mn99) by NAT_D:def 3;

          

           A12: p > 1 by INT_2:def 4;

          then (p * p) > p by XREAL_1: 155;

          then

           A13: (p * p) > 1 by A12, XXREAL_0: 2;

          

           A14: n > 0 by A3, A8;

          

           A15: p <> 0 by INT_2:def 4;

          

           A16: m > 0 by A3, A8;

          hereby

            per cases by A3, A10, NEWTON: 80;

              suppose

               A17: p divides m;

              then

               A18: not p divides n by A5;

              consider m9 be Nat such that

               A19: m = (p * m9) by A17, NAT_D:def 3;

              (p * (m9 * n)) = (p * (p * (mn99 * mn99))) by A3, A4, A11, A19;

              then (m9 * n) = (p * (mn99 * mn99)) by A15, XCMPLX_1: 5;

              then p divides (m9 * n);

              then p divides m9 by A18, NEWTON: 80;

              then

              consider m99 be Nat such that

               A20: m9 = (p * m99) by NAT_D:def 3;

              reconsider m99 as Element of NAT by ORDINAL1:def 12;

              

               A21: m99 <> 0 by A3, A8, A19, A20;

              (p * (p * (m99 * n))) = (p * (p * (mn99 * mn99))) by A3, A4, A11, A19, A20;

              then (p * (m99 * n)) = (p * (mn99 * mn99)) by A15, XCMPLX_1: 5;

              then

               A22: (m99 * n) = (mn99 ^2 ) by A15, XCMPLX_1: 5;

              m = ((p * p) * m99) by A19, A20;

              then m99 divides m;

              then (m99 gcd n) = 1 by A6, WSIERP_1: 16;

              then

               A23: (m99,n) are_coprime ;

              m = ((p * p) * m99) by A19, A20;

              then (1 * m99) < m by A13, A21, XREAL_1: 98;

              then

               A24: (m99 * n) < mn by A3, A14, A21, XREAL_1: 98;

              then m99 is square by A2, A22, A23;

              then

              consider m999 be Nat such that

               A25: m99 = (m999 ^2 );

              m = ((p * m999) ^2 ) by A19, A20, A25;

              hence thesis by A2, A24, A22, A23;

            end;

              suppose

               A26: p divides n;

              then

               A27: not p divides m by A5;

              consider n9 be Nat such that

               A28: n = (p * n9) by A26, NAT_D:def 3;

              (p * (m * n9)) = (p * (p * (mn99 * mn99))) by A3, A4, A11, A28;

              then (m * n9) = (p * (mn99 * mn99)) by A15, XCMPLX_1: 5;

              then p divides (m * n9);

              then p divides n9 by A27, NEWTON: 80;

              then

              consider n99 be Nat such that

               A29: n9 = (p * n99) by NAT_D:def 3;

              reconsider n99 as Element of NAT by ORDINAL1:def 12;

              

               A30: n99 <> 0 by A3, A8, A28, A29;

              (p * (p * (m * n99))) = (p * (p * (mn99 * mn99))) by A3, A4, A11, A28, A29;

              then (p * (m * n99)) = (p * (mn99 * mn99)) by A15, XCMPLX_1: 5;

              then

               A31: (m * n99) = (mn99 ^2 ) by A15, XCMPLX_1: 5;

              n = ((p * p) * n99) by A28, A29;

              then n99 divides n;

              then (m gcd n99) = 1 by A6, WSIERP_1: 16;

              then

               A32: (m,n99) are_coprime ;

              n = ((p * p) * n99) by A28, A29;

              then (1 * n99) < n by A13, A30, XREAL_1: 98;

              then

               A33: (m * n99) < mn by A3, A16, A30, XREAL_1: 98;

              then n99 is square by A2, A31, A32;

              then

              consider n999 be Nat such that

               A34: n99 = (n999 ^2 );

              n = ((p * n999) ^2 ) by A28, A29, A34;

              hence thesis by A2, A33, A31, A32;

            end;

          end;

        end;

      end;

      for mn be Nat holds P[mn] from NAT_1:sch 4( A1);

      hence thesis;

    end;

    registration

      let i be Integer;

      cluster (i ^2 ) -> integer;

      coherence ;

    end

    registration

      let i be even Integer;

      cluster (i ^2 ) -> even;

      coherence ;

    end

    registration

      let i be odd Integer;

      cluster (i ^2 ) -> odd;

      coherence ;

    end

    theorem :: PYTHTRIP:2

    i is even iff (i ^2 ) is even;

    theorem :: PYTHTRIP:3

    

     Th3: i is even implies ((i ^2 ) mod 4) = 0

    proof

      given i9 such that

       A1: i = (2 * i9);

      (i ^2 ) = ((4 * (i9 ^2 )) + 0 ) by A1;

      

      hence ((i ^2 ) mod 4) = ( 0 qua Integer mod 4) by EULER_1: 12

      .= 0 by NAT_D: 24;

    end;

    theorem :: PYTHTRIP:4

    

     Th4: i is odd implies ((i ^2 ) mod 4) = 1

    proof

      assume i is odd;

      then

      consider i9 such that

       A1: i = ((2 * i9) + 1) by ABIAN: 1;

      (i ^2 ) = ((4 * ((i9 ^2 ) + i9)) + 1) by A1;

      

      hence ((i ^2 ) mod 4) = (1 qua Integer mod 4) by EULER_1: 12

      .= 1 by NAT_D: 24;

    end;

    registration

      let m,n be odd square Integer;

      cluster (m + n) -> non square;

      coherence

      proof

        reconsider n99 = n as Element of NAT by ORDINAL1:def 12;

        reconsider m99 = m as Element of NAT by ORDINAL1:def 12;

        consider m9 be Nat such that

         A1: m = (m9 ^2 ) by Def3;

        

         A2: m9 is odd by A1;

        consider n9 be Nat such that

         A3: n = (n9 ^2 ) by Def3;

        

         A4: n9 is odd by A3;

        

         A5: ((m99 + n99) mod 4) = (((m99 mod 4) + (n99 mod 4)) mod 4) by EULER_2: 6

        .= ((1 + (n99 mod 4)) mod 4) by A1, A2, Th4

        .= ((1 + 1) mod 4) by A3, A4, Th4

        .= 2 by NAT_D: 24;

        hereby

          assume (m + n) is square;

          then

          consider mn9 be Nat such that

           A6: (m + n) = (mn9 ^2 );

          mn9 is even by A6;

          hence contradiction by A5, A6, Th3;

        end;

      end;

    end

    theorem :: PYTHTRIP:5

    

     Th5: (m ^2 ) = (n ^2 ) implies m = n

    proof

      assume

       A1: (m ^2 ) = (n ^2 );

      per cases by A1, SQUARE_1: 40;

        suppose m = n;

        hence thesis;

      end;

        suppose

         A2: m = ( - n);

        then m = ( - 0 );

        hence thesis by A2;

      end;

    end;

    theorem :: PYTHTRIP:6

    

     Th6: m divides n iff (m ^2 ) divides (n ^2 )

    proof

      defpred P[ Nat] means for n holds $1 divides n iff ($1 ^2 ) divides (n ^2 );

      

       A1: for m be Nat st for k be Nat st k < m holds P[k] holds P[m]

      proof

        let m be Nat;

        assume

         A2: for k be Nat st k < m holds for n holds k divides n iff (k ^2 ) divides (n ^2 );

        let n;

        hereby

          assume m divides n;

          then

          consider k9 be Nat such that

           A3: n = (m * k9) by NAT_D:def 3;

          (n ^2 ) = ((m ^2 ) * (k9 ^2 )) by A3;

          hence (m ^2 ) divides (n ^2 );

        end;

        assume

         A4: (m ^2 ) divides (n ^2 );

        per cases by NAT_1: 25;

          suppose m = 0 ;

          then (n ^2 ) = 0 by A4;

          then n = 0 by XCMPLX_1: 6;

          hence thesis by NAT_D: 6;

        end;

          suppose m = 1;

          hence thesis by NAT_D: 6;

        end;

          suppose

           A5: m > 1;

          consider k9 be Nat such that

           A6: (n ^2 ) = ((m ^2 ) * k9) by A4, NAT_D:def 3;

          m >= (1 + 1) by A5, NAT_1: 13;

          then

          consider p9 such that

           A7: p9 is prime and

           A8: p9 divides m by INT_2: 31;

          reconsider p = p9 as prime Element of NAT by A7;

          consider m9 be Nat such that

           A9: m = (p * m9) by A8, NAT_D:def 3;

          reconsider m9 as Element of NAT by ORDINAL1:def 12;

          (m ^2 ) = ((m * m9) * p) by A9;

          then p divides (m ^2 );

          then p divides (n ^2 ) by A4, NAT_D: 4;

          then p divides n by NEWTON: 80;

          then

          consider n9 be Nat such that

           A10: n = (p * n9) by NAT_D:def 3;

          

           A11: p > 1 by INT_2:def 4;

          then

           A12: (p ^2 ) > 0 by SQUARE_1: 12;

          reconsider n9 as Element of NAT by ORDINAL1:def 12;

          ((p ^2 ) * (n9 ^2 )) = ((p ^2 ) * ((m9 ^2 ) * k9)) by A9, A10, A6;

          then (n9 ^2 ) = ((m9 ^2 ) * k9) by A12, XCMPLX_1: 5;

          then

           A13: (m9 ^2 ) divides (n9 ^2 );

          (p * m9) > (1 * m9) by A5, A9, A11, XREAL_1: 98;

          then m9 divides n9 by A2, A9, A13;

          then

          consider k be Nat such that

           A14: n9 = (m9 * k) by NAT_D:def 3;

          n = (m * k) by A9, A10, A14;

          hence thesis;

        end;

      end;

      for m be Nat holds P[m] from NAT_1:sch 4( A1);

      hence thesis;

    end;

    begin

    theorem :: PYTHTRIP:7

    

     Th7: m divides n or k = 0 iff (k * m) divides (k * n)

    proof

      hereby

        assume

         A1: m divides n or k = 0 ;

        per cases by A1;

          suppose m divides n;

          then

          consider k9 be Nat such that

           A2: n = (m * k9) by NAT_D:def 3;

          (k * n) = ((k * m) * k9) by A2;

          hence (k * m) divides (k * n);

        end;

          suppose k = 0 ;

          hence (k * m) divides (k * n);

        end;

      end;

      assume

       A3: (k * m) divides (k * n);

      now

        consider k9 be Nat such that

         A4: (k * n) = ((k * m) * k9) by A3, NAT_D:def 3;

        assume

         A5: k <> 0 ;

        (k * n) = (k * (m * k9)) by A4;

        then n = (m * k9) by A5, XCMPLX_1: 5;

        hence m divides n;

      end;

      hence thesis;

    end;

    theorem :: PYTHTRIP:8

    

     Th8: ((k * m) gcd (k * n)) = (k * (m gcd n))

    proof

      per cases ;

        suppose

         A1: k <> 0 ;

        k divides (k * m) & k divides (k * n);

        then k divides ((k * m) gcd (k * n)) by NAT_D:def 5;

        then

        consider k9 be Nat such that

         A2: ((k * m) gcd (k * n)) = (k * k9) by NAT_D:def 3;

        reconsider k9 as Element of NAT by ORDINAL1:def 12;

        now

          (k * k9) divides (k * m) by A2, NAT_D:def 5;

          hence k9 divides m by A1, Th7;

          (k * k9) divides (k * n) by A2, NAT_D:def 5;

          hence k9 divides n by A1, Th7;

          let p be Nat;

          reconsider p9 = p as Element of NAT by ORDINAL1:def 12;

          assume p divides m & p divides n;

          then (k * p9) divides (k * m) & (k * p9) divides (k * n) by Th7;

          then (k * p) divides (k * k9) by A2, NAT_D:def 5;

          then p9 divides k9 by A1, Th7;

          hence p divides k9;

        end;

        hence thesis by A2, NAT_D:def 5;

      end;

        suppose k = 0 ;

        hence thesis by NEWTON: 52;

      end;

    end;

    begin

    theorem :: PYTHTRIP:9

    

     Th9: for X be set st for m holds ex n st n >= m & n in X holds X is infinite

    proof

      let X be set;

       A1:

      now

        let f be Function;

        defpred P[ Nat] means ex m st for n st n >= m holds not n in (f .: $1);

        

         A2: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume ex m st for n st n >= m holds not n in (f .: k);

          then

          consider m such that

           A3: for n st n >= m holds not n in (f .: k);

          ( Segm (k + 1)) = (( Segm k) \/ {k}) by AFINSQ_1: 2;

          then

           A4: (f .: (k + 1)) = ((f .: k) \/ ( Im (f,k))) by RELAT_1: 120;

          per cases ;

            suppose

             A5: k in ( dom f) & (f . k) in NAT ;

            then

            reconsider m9 = (f . k) as Element of NAT ;

            take ( max (m,(m9 + 1)));

            let n;

            assume

             A6: n >= ( max (m,(m9 + 1)));

            then

             A7: not n in (f .: k) by A3, XXREAL_0: 30;

            n >= (m9 + 1) by A6, XXREAL_0: 30;

            then n <> m9 by NAT_1: 13;

            then

             A8: not n in {m9} by TARSKI:def 1;

            (f .: (k + 1)) = ((f .: k) \/ {m9}) by A4, A5, FUNCT_1: 59;

            hence thesis by A7, A8, XBOOLE_0:def 3;

          end;

            suppose

             A9: k in ( dom f) & not (f . k) in NAT ;

            take m;

            set m9 = (f . k);

            let n;

            n <> m9 by A9;

            then

             A10: not n in {m9} by TARSKI:def 1;

            assume n >= m;

            then

             A11: not n in (f .: k) by A3;

            (f .: (k + 1)) = ((f .: k) \/ {m9}) by A4, A9, FUNCT_1: 59;

            hence thesis by A11, A10, XBOOLE_0:def 3;

          end;

            suppose not k in ( dom f);

            then

             A12: ( dom f) misses {k} by ZFMISC_1: 50;

            take m;

            let n;

            assume

             A13: n >= m;

            ( Im (f,k)) = (f .: (( dom f) /\ {k})) by RELAT_1: 112

            .= (f .: {} ) by A12, XBOOLE_0:def 7

            .= {} ;

            hence thesis by A3, A4, A13;

          end;

        end;

        

         A14: P[ 0 ]

        proof

          take 0 ;

          let n such that n >= 0 ;

          thus thesis;

        end;

        thus for k be Nat holds P[k] from NAT_1:sch 2( A14, A2);

      end;

      now

        assume X is finite;

        then

        consider f be Function such that

         A15: ( rng f) = X and

         A16: ( dom f) in omega by FINSET_1:def 1;

        reconsider k = ( dom f) as Element of NAT by A16;

        (f .: k) = X by A15, RELAT_1: 113;

        hence ex m st for n st n >= m holds not n in X by A1;

      end;

      hence thesis;

    end;

    begin

    theorem :: PYTHTRIP:10

    (a,b) are_coprime implies a is odd or b is odd;

    theorem :: PYTHTRIP:11

    

     Th11: ((a ^2 ) + (b ^2 )) = (c ^2 ) & (a,b) are_coprime & a is odd implies ex m, n st m <= n & a = ((n ^2 ) - (m ^2 )) & b = ((2 * m) * n) & c = ((n ^2 ) + (m ^2 ))

    proof

      assume

       A1: ((a ^2 ) + (b ^2 )) = (c ^2 );

      assume

       A2: (a,b) are_coprime ;

      assume a is odd;

      then

      reconsider a9 = a as odd Element of NAT ;

      b is even

      proof

        assume b is odd;

        then

        reconsider b9 = b as odd Element of NAT ;

        ((a9 ^2 ) + (b9 ^2 )) = (c ^2 ) by A1;

        hence contradiction;

      end;

      then

      reconsider b9 = b as even Element of NAT ;

      ((a9 ^2 ) + (b9 ^2 )) = (c ^2 ) by A1;

      then

      reconsider c9 = c as odd Element of NAT ;

      2 divides (c9 - a9) by ABIAN:def 1;

      then

      consider i such that

       A3: (c9 - a9) = (2 * i);

      (c ^2 ) >= ((a ^2 ) + 0 ) by A1, XREAL_1: 6;

      then c >= a by SQUARE_1: 16;

      then (2 * i) >= (2 * 0 ) by A3, XREAL_1: 48;

      then i >= 0 by XREAL_1: 68;

      then

      reconsider m9 = i as Element of NAT by INT_1: 3;

      consider n9 be Nat such that

       A4: (c9 + a9) = (2 * n9) by ABIAN:def 2;

      consider k9 be Nat such that

       A5: b9 = (2 * k9) by ABIAN:def 2;

      reconsider n9, k9 as Element of NAT by ORDINAL1:def 12;

      

       A6: (n9 * m9) = (((c + a) / 2) * ((c - a) / 2)) by A4, A3

      .= ((b / 2) ^2 ) by A1

      .= (k9 ^2 ) by A5;

      

       A7: (n9 + m9) = c by A4, A3;

      

       A8: (n9,m9) are_coprime

      proof

        let p be prime Nat;

        assume that

         A9: p divides n9 and

         A10: p divides m9;

        reconsider p as prime Element of NAT by ORDINAL1:def 12;

        p divides c by A7, A9, A10, NAT_D: 8;

        then

         A11: p divides (c * c) by NAT_D: 9;

        p divides ( - m9) by A10, INT_2: 10;

        then

         A12: p divides (n9 + ( - m9)) by A9, WSIERP_1: 4;

        then p divides (a * a) by A4, A3, NAT_D: 9;

        then

         A13: p divides ( - (a * a)) by INT_2: 10;

        (b * b) = ((c * c) + ( - (a * a))) by A1;

        then p divides (b * b) qua Integer by A13, A11, WSIERP_1: 4;

        then p divides b by NEWTON: 80;

        hence contradiction by A2, A4, A3, A12;

      end;

      then n9 is square by A6, Th1;

      then

      consider n be Nat such that

       A14: n9 = (n ^2 );

      m9 is square by A8, A6, Th1;

      then

      consider m be Nat such that

       A15: m9 = (m ^2 );

      reconsider m, n as Element of NAT by ORDINAL1:def 12;

      take m, n;

      (n9 - m9) = a by A4, A3;

      then (m ^2 ) <= (n ^2 ) by A14, A15, XREAL_1: 49;

      hence m <= n by SQUARE_1: 16;

      thus a = ((n ^2 ) - (m ^2 )) by A4, A3, A14, A15;

      (b ^2 ) = ((2 ^2 ) * ((n * m) ^2 )) by A5, A6, A14, A15, SQUARE_1: 9

      .= (((2 * m) * n) ^2 );

      hence b = ((2 * m) * n) by Th5;

      thus thesis by A4, A3, A14, A15;

    end;

    theorem :: PYTHTRIP:12

    a = ((n ^2 ) - (m ^2 )) & b = ((2 * m) * n) & c = ((n ^2 ) + (m ^2 )) implies ((a ^2 ) + (b ^2 )) = (c ^2 );

    definition

      :: PYTHTRIP:def4

      mode Pythagorean_triple -> Subset of NAT means

      : Def4: ex a, b, c st ((a ^2 ) + (b ^2 )) = (c ^2 ) & it = {a, b, c};

      existence

      proof

        take { 0 , 0 , 0 };

        take 0 , 0 , 0 ;

        thus (( 0 ^2 ) + ( 0 ^2 )) = ( 0 ^2 );

        thus thesis;

      end;

    end

    reserve X for Pythagorean_triple;

    registration

      cluster -> finite for Pythagorean_triple;

      coherence

      proof

        let X;

        ex a, b, c st ((a ^2 ) + (b ^2 )) = (c ^2 ) & X = {a, b, c} by Def4;

        hence thesis;

      end;

    end

    definition

      ::$Notion-Name

      :: original: Pythagorean_triple

      redefine

      :: PYTHTRIP:def5

      mode Pythagorean_triple means

      : Def5: ex k, m, n st m <= n & it = {(k * ((n ^2 ) - (m ^2 ))), (k * ((2 * m) * n)), (k * ((n ^2 ) + (m ^2 )))};

      compatibility

      proof

        let X be Subset of NAT ;

        hereby

          assume X is Pythagorean_triple;

          then

          consider a, b, c such that

           A1: ((a ^2 ) + (b ^2 )) = (c ^2 ) and

           A2: X = {a, b, c} by Def4;

          set k = (a gcd b);

          

           A3: k divides a by NAT_D:def 5;

          

           A4: k divides b by NAT_D:def 5;

          per cases ;

            suppose k = 0 ;

            then

             A5: a = 0 & b = 0 by A3, A4;

            thus ex k, m, n st m <= n & X = {(k * ((n ^2 ) - (m ^2 ))), (k * ((2 * m) * n)), (k * ((n ^2 ) + (m ^2 )))}

            proof

              take 0 , 0 , 0 ;

              thus thesis by A1, A2, A5, XCMPLX_1: 6;

            end;

          end;

            suppose

             A6: k <> 0 ;

            then

             A7: (k * k) <> 0 by XCMPLX_1: 6;

            consider a9 be Nat such that

             A8: a = (k * a9) by A3, NAT_D:def 3;

            consider b9 be Nat such that

             A9: b = (k * b9) by A4, NAT_D:def 3;

            reconsider a9, b9 as Element of NAT by ORDINAL1:def 12;

            (k * (a9 gcd b9)) = (k * 1) by A8, A9, Th8;

            then (a9 gcd b9) = 1 by A6, XCMPLX_1: 5;

            then

             A10: (a9,b9) are_coprime ;

            (c ^2 ) = ((k ^2 ) * ((a9 ^2 ) + (b9 ^2 ))) by A1, A8, A9;

            then (k ^2 ) divides (c ^2 );

            then k divides c by Th6;

            then

            consider c9 be Nat such that

             A11: c = (k * c9) by NAT_D:def 3;

            reconsider c9 as Element of NAT by ORDINAL1:def 12;

            ((k ^2 ) * ((a9 ^2 ) + (b9 ^2 ))) = ((k ^2 ) * (c9 ^2 )) by A1, A8, A9, A11;

            then

             A12: ((a9 ^2 ) + (b9 ^2 )) = (c9 ^2 ) by A7, XCMPLX_1: 5;

            thus ex k, m, n st m <= n & X = {(k * ((n ^2 ) - (m ^2 ))), (k * ((2 * m) * n)), (k * ((n ^2 ) + (m ^2 )))}

            proof

              per cases by A10;

                suppose a9 is odd;

                then

                consider m, n such that

                 A13: m <= n & a9 = ((n ^2 ) - (m ^2 )) & b9 = ((2 * m) * n) & c9 = ((n ^2 ) + (m ^2 )) by A12, A10, Th11;

                take k, m, n;

                thus thesis by A2, A8, A9, A11, A13;

              end;

                suppose b9 is odd;

                then

                consider m, n such that

                 A14: m <= n & b9 = ((n ^2 ) - (m ^2 )) & a9 = ((2 * m) * n) & c9 = ((n ^2 ) + (m ^2 )) by A12, A10, Th11;

                take k, m, n;

                thus thesis by A2, A8, A9, A11, A14, ENUMSET1: 58;

              end;

            end;

          end;

        end;

        assume ex k, m, n st m <= n & X = {(k * ((n ^2 ) - (m ^2 ))), (k * ((2 * m) * n)), (k * ((n ^2 ) + (m ^2 )))};

        then

        consider k, m, n such that

         A15: m <= n and

         A16: X = {(k * ((n ^2 ) - (m ^2 ))), (k * ((2 * m) * n)), (k * ((n ^2 ) + (m ^2 )))};

        (m ^2 ) <= (n ^2 ) by A15, SQUARE_1: 15;

        then

        reconsider a9 = ((n ^2 ) - (m ^2 )) as Element of NAT by INT_1: 3, XREAL_1: 48;

        set c9 = ((n ^2 ) + (m ^2 ));

        set b9 = ((2 * m) * n);

        (((k * a9) ^2 ) + ((k * b9) ^2 )) = ((k * c9) ^2 );

        hence thesis by A16, Def4;

      end;

    end

    notation

      let X;

      synonym X is degenerate for X is with_zero;

    end

    theorem :: PYTHTRIP:13

    n > 2 implies ex X st X is non degenerate & n in X

    proof

      assume

       A1: n > 2;

      per cases ;

        suppose n is even;

        then

        consider m be Nat such that

         A2: n = (2 * m);

        reconsider m as Element of NAT by ORDINAL1:def 12;

        set c = (1 * ((m ^2 ) + (1 ^2 )));

        set b = (1 * ((2 * 1) * m));

        (2 * m) > (2 * 1) by A1, A2;

        then

         A3: m > 1 by XREAL_1: 64;

        then (m ^2 ) > (1 ^2 ) by SQUARE_1: 16;

        then ((m ^2 ) - (1 ^2 )) > 0 by XREAL_1: 50;

        then

        reconsider a = (1 * ((m ^2 ) - (1 ^2 ))) as Element of NAT by INT_1: 3;

        reconsider X = {a, b, c} as Pythagorean_triple by A3, Def5;

        take X;

        a <> 0 by A3, SQUARE_1: 16;

        hence not 0 in X by A1, A2, ENUMSET1:def 1;

        thus thesis by A2, ENUMSET1:def 1;

      end;

        suppose n is odd;

        then

        consider i such that

         A4: n = ((2 * i) + 1) by ABIAN: 1;

        

         A5: (2 * i) >= (2 * 1) by A1, A4, INT_1: 7;

        then i >= 1 by XREAL_1: 68;

        then

        reconsider m = i as Element of NAT by INT_1: 3;

        reconsider a = (1 * (((m + 1) ^2 ) - (m ^2 ))) as Element of NAT by A4;

        set b = (1 * ((2 * m) * (m + 1)));

        set c = (1 * (((m + 1) ^2 ) + (m ^2 )));

        m <= (m + 1) by NAT_1: 11;

        then

        reconsider X = {a, b, c} as Pythagorean_triple by Def5;

        take X;

        a = ((2 * m) + 1) & c = ((((m ^2 ) + (2 * m)) + (m ^2 )) + 1);

        hence not 0 in X by A5, ENUMSET1:def 1;

        thus thesis by A4, ENUMSET1:def 1;

      end;

    end;

    definition

      ::$Canceled

      let X;

      :: PYTHTRIP:def7

      attr X is simplified means for k st for n st n in X holds k divides n holds k = 1;

    end

    definition

      let X;

      :: original: simplified

      redefine

      :: PYTHTRIP:def8

      attr X is simplified means

      : Def8: ex m, n st m in X & n in X & (m,n) are_coprime ;

      compatibility

      proof

        hereby

          assume

           A1: X is simplified;

          consider a, b, c such that

           A2: ((a ^2 ) + (b ^2 )) = (c ^2 ) and

           A3: X = {a, b, c} by Def4;

          take a, b;

          thus a in X by A3, ENUMSET1:def 1;

          thus b in X by A3, ENUMSET1:def 1;

          now

            let k be Nat;

            reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

            assume

             A4: k divides a & k divides b;

            then (k1 ^2 ) divides (a ^2 ) & (k1 ^2 ) divides (b ^2 ) by Th6;

            then (k ^2 ) divides (c ^2 ) by A2, NAT_D: 8;

            then k1 divides c by Th6;

            then for n st n in X holds k1 divides n by A3, A4, ENUMSET1:def 1;

            hence k = 1 by A1;

          end;

          hence (a,b) are_coprime ;

        end;

        assume ex m, n st m in X & n in X & (m,n) are_coprime ;

        then

        consider m, n such that

         A5: m in X & n in X and

         A6: (m,n) are_coprime ;

        let k;

        assume for n st n in X holds k divides n;

        then

         A7: k divides m & k divides n by A5;

        (m gcd n) = 1 by A6;

        then k divides 1 by A7, NAT_D:def 5;

        hence thesis by WSIERP_1: 15;

      end;

    end

    theorem :: PYTHTRIP:14

    

     Th14: n > 0 implies ex X st X is non degenerate & X is simplified & (4 * n) in X

    proof

      set b = (1 * ((2 * 1) * (2 * n)));

      set c = (1 * (((2 * n) ^2 ) + (1 ^2 )));

      assume

       A1: n > 0 ;

      then n >= ( 0 + 1) by NAT_1: 13;

      then

       A2: (n + n) > ( 0 + 1) by XREAL_1: 8;

      then ((2 * n) ^2 ) > (1 ^2 ) by SQUARE_1: 16;

      then (((2 * n) ^2 ) - (1 ^2 )) > 0 by XREAL_1: 50;

      then

      reconsider a = (1 * (((2 * n) ^2 ) - (1 ^2 ))) as Element of NAT by INT_1: 3;

      reconsider X = {a, b, c} as Pythagorean_triple by A2, Def5;

      take X;

      a <> 0 & b <> 0 by A1;

      hence not 0 in X by ENUMSET1:def 1;

      (a - c) = ( - 2);

      

      then (a gcd c) = ((1 * (((2 * n) ^2 ) + (1 ^2 ))) gcd ( - 2)) by PREPOWER: 97

      .= ( |.(1 * (((2 * n) ^2 ) + (1 ^2 ))).| gcd |.( - 2).|) by INT_2: 34

      .= ( |.(1 * (((2 * n) ^2 ) + (1 ^2 ))).| gcd |.2.|) by COMPLEX1: 52

      .= (((2 * (2 * (n ^2 ))) + 1) gcd 2) by INT_2: 34

      .= (1 gcd 2) by EULER_1: 16

      .= 1 by WSIERP_1: 8;

      then

       A3: (a,c) are_coprime ;

      a in X & c in X by ENUMSET1:def 1;

      hence X is simplified by A3;

      thus thesis by ENUMSET1:def 1;

    end;

    registration

      cluster non degenerate simplified for Pythagorean_triple;

      existence

      proof

        consider X such that

         A1: X is non degenerate & X is simplified and (4 * 1) in X by Th14;

        take X;

        thus thesis by A1;

      end;

    end

    theorem :: PYTHTRIP:15

     {3, 4, 5} is non degenerate simplified Pythagorean_triple

    proof

      ((3 ^2 ) + (4 ^2 )) = (5 ^2 );

      then

      reconsider X = {3, 4, 5} as Pythagorean_triple by Def4;

      (3 gcd 4) = (3 gcd (4 - 3)) by PREPOWER: 97

      .= 1 by WSIERP_1: 8;

      then

       A1: 4 in X & (3,4) are_coprime by ENUMSET1:def 1;

       not 0 in X & 3 in X by ENUMSET1:def 1;

      hence thesis by A1, Def8, ORDINAL1:def 16;

    end;

    theorem :: PYTHTRIP:16

    { X : X is non degenerate & X is simplified } is infinite

    proof

      set T = { X : X is non degenerate & X is simplified };

      for m holds ex n st n >= m & n in ( union T)

      proof

        let m;

        set m9 = (m + 1);

        set n = (4 * m9);

        take n;

        consider X such that

         A1: X is non degenerate & X is simplified and

         A2: (4 * m9) in X by Th14;

        (n + 0 ) = ((1 * m9) + (3 * m9));

        then

         A3: n >= (m9 + 0 ) by XREAL_1: 6;

        m9 >= m by NAT_1: 11;

        hence n >= m by A3, XXREAL_0: 2;

        X in T by A1;

        hence thesis by A2, TARSKI:def 4;

      end;

      then

       A4: ( union T) is infinite by Th9;

      now

        let X be set;

        assume X in T;

        then ex X9 be Pythagorean_triple st X = X9 & X9 is non degenerate & X9 is simplified;

        hence X is finite;

      end;

      hence thesis by A4, FINSET_1: 7;

    end;