newton05.miz



    begin

    registration

      let a be Integer;

      cluster (a mod a) -> zero;

      coherence by INT_1: 50;

      cluster (a mod 2) -> natural;

      coherence by INT_1: 57, INT_1: 3;

    end

    registration

      let a,b be Integer;

      reduce ((a * b) gcd |.a.|) to |.a.|;

      reducibility

      proof

         |.a.| in NAT by INT_1: 3;

        then

        reconsider k = |.a.| as Nat;

        ((a * b) gcd |.a.|) = ( |.(a * b).| gcd |. |.a.|.|) by INT_2: 34

        .= (( 0 + ( |.a.| * |.b.|)) gcd |.a.|) by COMPLEX1: 65

        .= ( 0 gcd k) by NEWTON02: 5;

        hence thesis;

      end;

    end

    registration

      let a be odd Nat;

      cluster (a mod 2) -> non zero;

      coherence

      proof

         not 2 divides a;

        hence thesis by INT_1: 62;

      end;

    end

    registration

      let a be even Integer;

      cluster (a mod 2) -> zero;

      coherence

      proof

        2 divides a by ABIAN:def 1;

        hence thesis by INT_1: 62;

      end;

      reduce ((a + 1) mod 2) to 1;

      reducibility

      proof

        reconsider b = (a / 2) as Integer;

        (((2 * b) + 1) mod 2) = (1 mod 2) by NAT_D: 61;

        hence thesis by NAT_D: 14;

      end;

    end

    registration

      let a,b be Real;

      cluster (( max (a,b)) - ( min (a,b))) -> non negative;

      coherence

      proof

        ( max (a,b)) >= a & a >= ( min (a,b)) by XXREAL_0: 17, XXREAL_0: 25;

        then ( max (a,b)) >= ( min (a,b)) by XXREAL_0: 2;

        then (( max (a,b)) - ( min (a,b))) >= (( max (a,b)) - ( max (a,b))) by XREAL_1: 10;

        hence thesis;

      end;

    end

    registration

      let a be Nat, b be non zero Nat;

      reduce (a mod (a + b)) to a;

      reducibility

      proof

        (a + b) > (a + 0 ) by XREAL_1: 6;

        hence thesis by NAT_D: 63;

      end;

      cluster (a div (a + b)) -> zero;

      coherence

      proof

        (a + b) > (a + 0 ) by XREAL_1: 6;

        hence thesis by NAT_D: 27;

      end;

    end

    registration

      let a be non trivial Nat;

      cluster (a |-count 1) -> zero;

      coherence

      proof

         not a divides 1 by NAT_D: 7, NEWTON03:def 1;

        hence thesis by NEWTON03: 77;

      end;

      cluster (a |-count ( - 1)) -> zero;

      coherence

      proof

        a <> 1 by NAT_2:def 1;

        then not a divides ( - 1) by INT_2: 13;

        hence thesis by NEWTON03: 77;

      end;

    end

    registration

      let a be non trivial Nat, b be Nat;

      reduce (a |-count (a |^ b)) to b;

      reducibility

      proof

        (a |-count ((a |^ b) * 1)) = (b + (a |-count 1)) by NEWTON03: 105;

        hence thesis;

      end;

      reduce (a |-count ( - (a |^ b))) to b;

      reducibility

      proof

        (a |-count ((a |^ b) * ( - 1))) = (b + (a |-count ( - 1))) by NEWTON03: 105;

        hence thesis;

      end;

    end

    theorem :: NEWTON05:1

    

     Th1: for a,b be Integer holds a divides b implies (b / a) is integer

    proof

      let a,b be Integer;

      a = 0 or thesis by WSIERP_1: 17;

      hence thesis;

    end;

    registration

      cluster non zero for even Integer;

      existence

      proof

        2 is non zero & 2 is even;

        hence thesis;

      end;

      cluster non zero trivial -> odd for Nat;

      coherence

      proof

        ((2 * 0 ) + 1) is odd;

        hence thesis by NAT_2:def 1;

      end;

    end

    registration

      cluster non trivial for odd Nat;

      existence

      proof

        3 is non trivial & ((2 * 1) + 1) is odd;

        hence thesis;

      end;

    end

    registration

      let a be Integer, b be even Integer;

      cluster (a lcm b) -> even;

      coherence

      proof

        2 divides b & b divides (a lcm b) by INT_2:def 1, ABIAN:def 1;

        hence thesis;

      end;

    end

    registration

      let a,b be odd Integer;

      cluster (a lcm b) -> odd;

      coherence

      proof

        a divides (a * b) & b divides (a * b);

        then (a lcm b) divides (a * b) by INT_2: 19;

        hence thesis;

      end;

    end

    registration

      let a,b be Integer;

      cluster ((a + b) / (a gcd b)) -> integer;

      coherence

      proof

        (a gcd b) divides a & (a gcd b) divides b by INT_2:def 2;

        hence thesis by Th1, WSIERP_1: 4;

      end;

      cluster ((a - b) / (a gcd b)) -> integer;

      coherence

      proof

        reconsider c = ( - b) as Integer;

        ((a + c) / (a gcd c)) is Integer;

        hence thesis by NEWTON02: 1;

      end;

    end

    theorem :: NEWTON05:2

    

     ABS: for a,b be Real holds |.(a + b).| = ( |.a.| + |.b.|) or |.(a - b).| = ( |.a.| + |.b.|)

    proof

      let a,b be Real;

      per cases ;

        suppose (a >= 0 & b >= 0 ) or (a <= 0 & b <= 0 );

        then (a * b) >= 0 ;

        hence thesis by ABSVALUE: 11;

      end;

        suppose (a > 0 & b < 0 ) or (a < 0 & b > 0 );

        then (a * ( - b)) >= 0 ;

        then |.(a + ( - b)).| = ( |.a.| + |.( - b).|) by ABSVALUE: 11;

        hence thesis by COMPLEX1: 52;

      end;

    end;

    theorem :: NEWTON05:3

    

     ABS1: for a,b be Real holds |.( |.a.| - |.b.|).| = |.(a + b).| or |.( |.a.| - |.b.|).| = |.(a - b).|

    proof

      let a,b be Real;

      per cases ;

        suppose

         A1: a >= 0 ;

        per cases ;

          suppose b >= 0 ;

          then |.a.| = a & |.b.| = b by A1, ABSVALUE:def 1;

          hence thesis;

        end;

          suppose b < 0 ;

          then |.a.| = a & |.b.| = ( - b) by A1, ABSVALUE:def 1;

          hence thesis;

        end;

      end;

        suppose

         A1: a < 0 ;

        per cases ;

          suppose b >= 0 ;

          then |.a.| = ( - a) & |.b.| = b by A1, ABSVALUE:def 1;

          then |.( |.a.| - |.b.|).| = |.( - (a + b)).|;

          hence thesis by COMPLEX1: 52;

        end;

          suppose b < 0 ;

          then |.a.| = ( - a) & |.b.| = ( - b) by A1, ABSVALUE:def 1;

          then |.( |.a.| - |.b.|).| = |.( - (a - b)).|;

          hence thesis by COMPLEX1: 52;

        end;

      end;

    end;

    theorem :: NEWTON05:4

    

     LmABS: for a,b be Real holds |.( |.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = ( |.a.| + |.b.|)

    proof

      let a,b be Real;

      per cases ;

        suppose

         B1: a >= 0 ;

        per cases ;

          suppose b >= 0 ;

          then |.a.| = a & |.b.| = b by B1, ABSVALUE:def 1;

          hence thesis;

        end;

          suppose b < 0 ;

          then |.a.| = a & |.b.| = ( - b) by B1, ABSVALUE:def 1;

          hence thesis;

        end;

      end;

        suppose

         B1: a < 0 ;

        per cases ;

          suppose b >= 0 ;

          then

           C1: |.a.| = ( - a) & |.b.| = b by B1, ABSVALUE:def 1;

          then

           C2: |.( |.a.| - |.b.|).| = |.( - (a + b)).|;

           |.(a - b).| = |.( - ( |.a.| + |.b.|)).| by C1

          .= |.( |.a.| + |.b.|).| by COMPLEX1: 52;

          hence thesis by C2, COMPLEX1: 52;

        end;

          suppose b < 0 ;

          then

           C1: |.a.| = ( - a) & |.b.| = ( - b) by B1, ABSVALUE:def 1;

          then

           C2: |.( |.a.| - |.b.|).| = |.( - (a - b)).|;

           |.(a + b).| = |.( - ( |.a.| + |.b.|)).| by C1

          .= |.( |.a.| + |.b.|).| by COMPLEX1: 52;

          hence thesis by COMPLEX1: 52, C2;

        end;

      end;

    end;

    theorem :: NEWTON05:5

    

     LABS: for a,b be Real holds |.(a + b).| = ( |.a.| + |.b.|) iff |.(a - b).| = |.( |.a.| - |.b.|).|

    proof

      let a,b be Real;

      reconsider c = ( - b) as Real;

       |.( |.a.| - |.c.|).| = |.(a + c).| iff |.(a - c).| = ( |.a.| + |.c.|) by LmABS;

      hence thesis by COMPLEX1: 52;

    end;

    theorem :: NEWTON05:6

    for a,b be non zero Real holds ( |.( |.a.| - |.b.|).| = |.(a + b).| & |.(a - b).| = ( |.a.| + |.b.|)) iff not ( |.( |.a.| - |.b.|).| = |.(a - b).| & |.(a + b).| = ( |.a.| + |.b.|))

    proof

      let a,b be non zero Real;

      

       A1: |.( |.a.| - |.b.|).| = |.(a + b).| iff |.(a - b).| = ( |.a.| + |.b.|) by LmABS;

      

       A2: |.( |.a.| - |.b.|).| = |.(a - b).| iff |.(a + b).| = ( |.a.| + |.b.|)

      proof

        reconsider c = ( - b) as non zero Real;

         |.( |.a.| - |.c.|).| = |.(a + c).| iff |.(a - c).| = ( |.a.| + |.c.|) by LmABS;

        hence thesis by COMPLEX1: 52;

      end;

       |.(a + b).| = ( |.a.| + |.b.|) iff not |.(a - b).| = ( |.a.| + |.b.|)

      proof

        (( |.a.| - |.b.|) + 0 ) < (( |.a.| - |.b.|) + (2 * |.b.|)) & (( |.b.| - |.a.|) + 0 ) < (( |.b.| - |.a.|) + (2 * |.a.|)) by XREAL_1: 6;

        then

         B0: ( |.a.| + |.b.|) > ( |.a.| - |.b.|) & ( |.a.| + |.b.|) > ( - ( |.a.| - |.b.|));

        per cases by ABS;

          suppose |.(a + b).| = ( |.a.| + |.b.|);

          hence thesis by A2, B0, ABSVALUE: 1;

        end;

          suppose |.(a - b).| = ( |.a.| + |.b.|);

          hence thesis by A1, B0, ABSVALUE: 1;

        end;

      end;

      hence thesis by LmABS, A2;

    end;

    theorem :: NEWTON05:7

    for a,b be positive Real, n be Nat holds ( min ((a |^ n),(b |^ n))) = (( min (a,b)) |^ n)

    proof

      let a,b be positive Real, n be Nat;

      per cases ;

        suppose

         A1: a >= b;

        then ( min (a,b)) = b by XXREAL_0:def 9;

        hence thesis by A1, NEWTON02: 41, XXREAL_0:def 9;

      end;

        suppose

         A1: b >= a;

        then ( min (a,b)) = a by XXREAL_0:def 9;

        hence thesis by A1, NEWTON02: 41, XXREAL_0:def 9;

      end;

    end;

    theorem :: NEWTON05:8

    for a,b be positive Real, n be Nat holds ( max ((a |^ n),(b |^ n))) = (( max (a,b)) |^ n)

    proof

      let a,b be positive Real, n be Nat;

      per cases ;

        suppose

         A1: a >= b;

        then ( max (a,b)) = a by XXREAL_0:def 10;

        hence thesis by A1, NEWTON02: 41, XXREAL_0:def 10;

      end;

        suppose

         A1: b >= a;

        then ( max (a,b)) = b by XXREAL_0:def 10;

        hence thesis by A1, NEWTON02: 41, XXREAL_0:def 10;

      end;

    end;

    theorem :: NEWTON05:9

    

     MIN1: for a be non zero Nat, m,n be Nat holds ( min ((a |^ n),(a |^ m))) = (a |^ ( min (n,m)))

    proof

      let a be non zero Nat, m,n be Nat;

      per cases ;

        suppose

         A1: m >= n;

        then

         A2: ( min (m,n)) = n by XXREAL_0:def 9;

        (a |^ n) divides (a |^ m) by A1, NEWTON: 89;

        then (a |^ m) >= (a |^ n) by NAT_D: 7;

        hence thesis by A2, XXREAL_0:def 9;

      end;

        suppose

         A1: n >= m;

        then

         A2: ( min (m,n)) = m by XXREAL_0:def 9;

        (a |^ m) divides (a |^ n) by A1, NEWTON: 89;

        then (a |^ n) >= (a |^ m) by NAT_D: 7;

        hence thesis by A2, XXREAL_0:def 9;

      end;

    end;

    theorem :: NEWTON05:10

    for a be non zero Nat, m,n be Nat holds ( max ((a |^ n),(a |^ m))) = (a |^ ( max (n,m)))

    proof

      let a be non zero Nat, m,n be Nat;

      per cases ;

        suppose

         A1: m <= n;

        then

         A2: ( max (m,n)) = n by XXREAL_0:def 10;

        (a |^ m) divides (a |^ n) by A1, NEWTON: 89;

        then (a |^ m) <= (a |^ n) by NAT_D: 7;

        hence thesis by A2, XXREAL_0:def 10;

      end;

        suppose

         A1: m >= n;

        then

         A2: ( max (m,n)) = m by XXREAL_0:def 10;

        (a |^ n) divides (a |^ m) by A1, NEWTON: 89;

        then (a |^ m) >= (a |^ n) by NAT_D: 7;

        hence thesis by A2, XXREAL_0:def 10;

      end;

    end;

    theorem :: NEWTON05:11

    

     AMB: for a,b be Nat holds (a mod b) <= a

    proof

      let a,b be Nat;

      per cases ;

        suppose b = 0 ;

        hence thesis;

      end;

        suppose b <> 0 ;

        then

        reconsider b as non zero Nat;

        (((a div b) * b) + (a mod b)) >= ( 0 + (a mod b)) by XREAL_1: 6;

        hence thesis by NAT_D: 2;

      end;

    end;

    theorem :: NEWTON05:12

    for a be Nat, b,c be non zero Nat holds ((a mod c) + (b mod c)) >= ((a + b) mod c)

    proof

      let a be Nat, b,c be non zero Nat;

      (((a mod c) + (b mod c)) mod c) <= ((a mod c) + (b mod c)) by AMB;

      hence thesis by NAT_D: 66;

    end;

    theorem :: NEWTON05:13

    for a be Nat, b,c be non zero Nat holds ((a mod c) * (b mod c)) >= ((a * b) mod c)

    proof

      let a be Nat, b,c be non zero Nat;

      (((a mod c) * (b mod c)) mod c) <= ((a mod c) * (b mod c)) by AMB;

      hence thesis by NAT_D: 67;

    end;

    theorem :: NEWTON05:14

    for a be Nat, b,n be non zero Nat holds ((a mod b) |^ n) >= ((a |^ n) mod b)

    proof

      let a be Nat, b,n be non zero Nat;

      reconsider m = (n - 1) as Nat;

      

       A1: ((a mod b) * ((a mod b) |^ m)) = ((a mod b) |^ (m + 1)) by NEWTON: 6;

      (((a mod b) * ((a mod b) |^ m)) mod b) <= ((a mod b) * ((a mod b) |^ m)) by AMB;

      hence thesis by A1, GR_CY_3: 30;

    end;

    theorem :: NEWTON05:15

    for a be Nat, b,n be non zero Nat holds (a mod b) = 1 implies ((a |^ n) mod b) = 1

    proof

      let a be Nat, b,n be non zero Nat;

      assume (a mod b) = 1;

      then 1 = (((a mod b) |^ n) mod b);

      hence thesis by GR_CY_3: 30;

    end;

    theorem :: NEWTON05:16

    for a,b be Nat, c be non zero Nat holds ((a mod c) * (b mod c)) < c iff ((a * b) mod c) = ((a mod c) * (b mod c))

    proof

      let a,b be Nat, c be non zero Nat;

      ((a mod c) * (b mod c)) < c implies ((a * b) mod c) = ((a mod c) * (b mod c))

      proof

        assume ((a mod c) * (b mod c)) < c;

        then (((a mod c) * (b mod c)) mod c) = ((a mod c) * (b mod c)) by NAT_D: 24;

        hence thesis by NAT_D: 67;

      end;

      hence thesis by INT_1: 58;

    end;

    theorem :: NEWTON05:17

    for a,b,c be Nat holds ((a mod c) * (b mod c)) = c implies ((a * b) mod c) = 0

    proof

      let a,b,c be Nat;

      assume ((a mod c) * (b mod c)) = c;

      then (c mod c) = (((a mod c) * (b mod c)) mod c);

      hence thesis by NAT_D: 67;

    end;

    theorem :: NEWTON05:18

    for a,b be Nat, c be non zero Nat holds ((a mod c) * (b mod c)) >= c implies (a mod c) > 1

    proof

      let a,b be Nat, c be non zero Nat;

      assume

       A1: ((a mod c) * (b mod c)) >= c;

      (a mod c) > 1 or ((a mod c) * (b mod c)) <= (1 * (b mod c)) by XREAL_1: 64;

      then (a mod c) > 1 or (b mod c) >= c by A1, XXREAL_0: 2;

      hence thesis by INT_1: 58;

    end;

    theorem :: NEWTON05:19

    

     MAB: for a,b be Integer, c be non zero Nat holds (((a + b) mod c) = (b mod c) implies (a mod c) = 0 ) & (((a + b) mod c) <> (b mod c) implies (a mod c) > 0 )

    proof

      let a,b be Integer, c be non zero Nat;

      

       L1: ((a + b) mod c) = (b mod c) implies (a mod c) = 0

      proof

        assume ((a + b) mod c) = (b mod c);

        

        then 0 = ((((a + b) mod c) - (b mod c)) mod c)

        .= (((a + b) - b) mod c) by INT_6: 7;

        hence thesis;

      end;

      ((a + b) mod c) = (((a mod c) + (b mod c)) mod c) by NAT_D: 66;

      then (a mod c) = 0 implies ((a + b) mod c) = (b mod c);

      hence thesis by L1, INT_1: 57;

    end;

    theorem :: NEWTON05:20

    for a be Nat, b,c be non zero Nat holds ((a * b) mod c) = b implies ((a * (b gcd c)) mod c) = (b gcd c)

    proof

      let a be Nat, b,c be non zero Nat;

      assume

       A1: ((a * b) mod c) = b;

      reconsider a as non zero Nat by A1;

      consider k,l be Integer such that

       A4: b = ((b gcd c) * k) & c = ((b gcd c) * l) & (k,l) are_coprime by INT_2: 23;

      k >= 0 by A4;

      then k in NAT by INT_1: 3;

      then

      reconsider k as non zero Nat by A4;

      l >= 0 by A4;

      then l in NAT by INT_1: 3;

      then

      reconsider l as non zero Nat by A4;

      

       A5: ((a * k) mod l) = (((b gcd c) * ((a * k) mod l)) / (b gcd c)) by XCMPLX_1: 89

      .= ((((a * k) * (b gcd c)) mod (l * (b gcd c))) / (b gcd c)) by INT_4: 20

      .= k by A1, A4, XCMPLX_1: 89;

      then

       A6: (k mod l) = k;

      l > k & k >= 1 by A5, INT_1: 58, NAT_1: 14;

      then l > 1 by XXREAL_0: 2;

      then 1 = (a mod l) by A4, A5, A6, PEPIN: 11;

      then ((b gcd c) * 1) = ((a * (b gcd c)) mod c) by A4, INT_4: 20;

      hence thesis;

    end;

    theorem :: NEWTON05:21

    for a,b be Integer holds (a,b) are_congruent_mod (a gcd b)

    proof

      let a,b be Integer;

      (a gcd b) divides a & (a gcd b) divides b by INT_2:def 2;

      hence thesis by INT_5: 1;

    end;

    theorem :: NEWTON05:22

    

     N0319: for k,l be odd square Integer holds ((k - l) mod 8) = 0

    proof

      let k,l be odd square Integer;

      reconsider k, l as odd Element of NAT by INT_1: 3;

      8 divides (k - l) by NEWTON03: 19;

      hence thesis by INT_1: 62;

    end;

    theorem :: NEWTON05:23

    for k,l be odd square Integer holds ((k + l) mod 8) = 2

    proof

      let k,l be odd square Integer;

      (1 |^ 2) is square & ((2 * 0 ) + 1) is odd & 1 is integer;

      then

       A1: ((k - 1) mod 8) = 0 & ((l - 1) mod 8) = 0 by N0319;

      ((k + l) mod 8) = (((k - 1) + ((l - 1) + 2)) mod 8)

      .= ((((k - 1) mod 8) + (((l - 1) + 2) mod 8)) mod 8) by NAT_D: 66

      .= ((((l - 1) mod 8) + (2 mod 8)) mod 8) by NAT_D: 66, A1

      .= (2 mod (2 + 6)) by A1

      .= 2;

      hence thesis;

    end;

    definition

      let a be Integer;

      :: NEWTON05:def1

      func parity a -> trivial Nat equals (a mod 2);

      coherence

      proof

        (a mod 2) = 0 or (a mod 2) = 1 by NAT_1: 23, INT_1: 58;

        hence thesis by NAT_2:def 1;

      end;

    end

    definition

      let a be Integer;

      :: original: parity

      redefine

      :: NEWTON05:def2

      func parity a -> trivial Nat equals (2 - (a gcd 2));

      coherence ;

      compatibility

      proof

        per cases ;

          suppose

           A1: a is odd;

          then (a mod 2) <> 0 by INT_1: 62;

          hence thesis by A1, PRE_FF: 6;

        end;

          suppose a is even;

          hence thesis by INT_1: 62;

        end;

      end;

    end

    registration

      let a be even Integer;

      cluster ( parity a) -> zero;

      coherence ;

    end

    registration

      let a be odd Integer;

      cluster ( parity a) -> non zero;

      coherence

      proof

        a is odd;

        hence thesis;

      end;

    end

    definition

      let a be Integer;

      :: NEWTON05:def3

      func Parity a -> Nat equals

      : Def1: 0 if a = 0

      otherwise (2 |^ (2 |-count a));

      coherence ;

      consistency ;

    end

    registration

      let a be non zero Integer;

      cluster ( Parity a) -> non zero;

      coherence

      proof

        ( Parity a) = (2 |^ (2 |-count a)) by Def1;

        hence thesis;

      end;

    end

    registration

      let a be non zero even Integer;

      cluster ( Parity a) -> non trivial;

      coherence

      proof

        2 is non trivial & 2 divides a by ABIAN:def 1;

        then (2 |-count a) >= 1 by NAT_1: 14, NEWTON03: 89;

        then (2 |^ (2 |-count a)) >= (2 |^ 1) & (1 + 1) > (1 + 0 ) by PREPOWER: 12;

        then (2 |^ (2 |-count a)) > 1 by XXREAL_0: 2;

        hence thesis by Def1;

      end;

      cluster ( Parity a) -> even;

      coherence

      proof

        2 is non trivial & 2 divides a by ABIAN:def 1;

        then (2 |-count a) >= 1 by NAT_1: 14, NEWTON03: 89;

        then (2 |^ 1) divides (2 |^ (2 |-count a)) by NEWTON: 89;

        hence thesis by Def1;

      end;

    end

    registration

      let a be even Integer;

      cluster ( Parity a) -> even;

      coherence

      proof

        (a = 0 or a is non zero even Integer) & ( Parity 0 ) is even by Def1;

        hence thesis;

      end;

      cluster ( Parity (a + 1)) -> odd;

      coherence

      proof

        (2 |-count (a + 1)) = 0 ;

        then ( Parity (a + 1)) = (1 * (2 |^ 0 )) by Def1;

        hence thesis;

      end;

    end

    registration

      let a be odd Integer;

      cluster ( Parity a) -> trivial;

      coherence

      proof

        (2 |-count a) = 0 ;

        then ( Parity a) = (1 * (2 |^ 0 )) by Def1;

        hence thesis;

      end;

    end

    reconsider dwa = 2 as prime Nat by INT_2: 28;

    registration

      let n be Nat;

      reduce ( Parity (2 |^ n)) to (2 |^ n);

      reducibility

      proof

        ( Parity (dwa |^ n)) = (dwa |^ (dwa |-count (dwa |^ n))) by Def1;

        hence thesis;

      end;

    end

    registration

      reduce ( Parity 1) to 1;

      reducibility

      proof

        ( Parity ((2 * 0 ) + 1)) = 1 by NAT_2:def 1;

        hence thesis;

      end;

      reduce ( Parity 2) to 2;

      reducibility

      proof

        ( Parity (2 |^ 1)) = (2 |^ 1);

        hence thesis;

      end;

    end

    theorem :: NEWTON05:24

    

     Th3: for a be Integer holds ( Parity a) divides a

    proof

      let a be Integer;

      per cases ;

        suppose a = 0 ;

        hence thesis by Def1;

      end;

        suppose

         A1: a <> 0 ;

         |.2.| > 1;

        then (2 |^ (2 |-count a)) divides a by A1, NEWTON03:def 7;

        hence thesis by A1, Def1;

      end;

    end;

    theorem :: NEWTON05:25

    

     ILP: for a,b be Integer holds ( Parity (a * b)) = (( Parity a) * ( Parity b))

    proof

      let a,b be Integer;

      per cases ;

        suppose a = 0 or b = 0 ;

        then (( Parity a) = 0 or ( Parity b) = 0 ) & ( Parity (a * b)) = 0 by Def1;

        hence thesis;

      end;

        suppose

         B1: a <> 0 & b <> 0 ;

        then

         B2: ( Parity b) = (2 |^ (2 |-count b)) & ( Parity a) = (2 |^ (2 |-count a)) by Def1;

        ( Parity (a * b)) = (2 |^ (2 |-count (a * b))) by B1, Def1

        .= (2 |^ ((2 |-count a) + (2 |-count b))) by B1, NEWTON03: 57, INT_2: 28

        .= ((2 |^ (2 |-count a)) * (2 |^ (2 |-count b))) by NEWTON: 8;

        hence thesis by B2;

      end;

    end;

    definition

      let a be Integer;

      :: NEWTON05:def4

      func Oddity a -> Integer equals (a / ( Parity a));

      coherence by Th1, Th3;

    end

    theorem :: NEWTON05:26

    

     ADI: for a be non zero Integer holds (a / ( Parity a)) = (a div ( Parity a))

    proof

      let a be non zero Integer;

      ( Parity a) > 0 & ( Parity a) divides a by Th3;

      then

       A1: (a mod ( Parity a)) = 0 by INT_1: 62;

      (a / ( Parity a)) = ((((a div ( Parity a)) * ( Parity a)) + (a mod ( Parity a))) / ( Parity a)) by INT_1: 59

      .= (((a div ( Parity a)) * ( Parity a)) / ( Parity a)) by A1;

      hence thesis by XCMPLX_1: 89;

    end;

    registration

      let a be Integer;

      reduce (( Parity a) * ( Oddity a)) to a;

      reducibility

      proof

        per cases ;

          suppose a = 0 ;

          hence thesis;

        end;

          suppose a <> 0 ;

          hence thesis by XCMPLX_1: 87;

        end;

      end;

      reduce ( Parity ( Parity a)) to ( Parity a);

      reducibility

      proof

        per cases ;

          suppose a is zero;

          hence thesis by Def1;

        end;

          suppose not a is zero;

          then

          reconsider a as non zero Integer;

          (2 |^ (2 |-count a)) = ( Parity (2 |^ (2 |-count a)))

          .= ( Parity ( Parity a)) by Def1;

          hence thesis by Def1;

        end;

      end;

      reduce ( Oddity ( Oddity a)) to ( Oddity a);

      reducibility

      proof

        per cases ;

          suppose a is zero;

          hence thesis;

        end;

          suppose a <> 0 ;

          then

          reconsider a as non zero Integer;

          (( Oddity a) * ( Parity a)) = ((( Parity ( Oddity a)) * ( Oddity ( Oddity a))) * ( Parity ( Parity a)))

          .= (( Oddity ( Oddity a)) * (( Parity ( Oddity a)) * ( Parity ( Parity a))))

          .= (( Oddity ( Oddity a)) * ( Parity (( Oddity a) * ( Parity a)))) by ILP

          .= (( Oddity ( Oddity a)) * ( Parity a));

          hence thesis by XCMPLX_1: 5;

        end;

      end;

      cluster ( Parity ( Oddity a)) -> trivial;

      coherence

      proof

        per cases ;

          suppose a is zero;

          hence thesis by Def1;

        end;

          suppose a is non zero;

          then

          reconsider a as non zero Integer;

          ( Oddity ( Oddity a)) = ( Oddity a) & (( Oddity ( Oddity a)) * ( Parity ( Oddity a))) = ( Oddity a);

          hence thesis by XCMPLX_1: 7;

        end;

      end;

      cluster (a + ( Parity a)) -> even;

      coherence

      proof

        per cases ;

          suppose a is odd;

          hence thesis;

        end;

          suppose a is even;

          hence thesis;

        end;

      end;

      cluster (a - ( Parity a)) -> even;

      coherence

      proof

        per cases ;

          suppose a is odd;

          hence thesis;

        end;

          suppose a is even;

          hence thesis;

        end;

      end;

      cluster (a / ( Parity a)) -> integer;

      coherence by Th1, Th3;

    end

    theorem :: NEWTON05:27

    

     OPA: for a be non zero Integer holds ( Oddity ( Parity a)) = 1

    proof

      let a be non zero Integer;

      ( Parity ( Parity a)) = ( Parity a) & (( Parity ( Parity a)) * ( Oddity ( Parity a))) = ( Parity a);

      hence thesis by XCMPLX_1: 7;

    end;

    theorem :: NEWTON05:28

    

     ILO: for a,b be Integer holds ( Oddity (a * b)) = (( Oddity a) * ( Oddity b))

    proof

      let a,b be Integer;

      per cases ;

        suppose a = 0 or b = 0 ;

        hence thesis;

      end;

        suppose

         B1: a <> 0 & b <> 0 ;

        then

        reconsider a as non zero Integer;

        reconsider b as non zero Integer by B1;

        ((( Oddity a) * ( Oddity b)) * ( Parity (a * b))) = ((( Oddity a) * ( Oddity b)) * (( Parity a) * ( Parity b))) by ILP

        .= ((( Oddity a) * ( Parity a)) * (( Oddity b) * ( Parity b)))

        .= (( Oddity (a * b)) * ( Parity (a * b)));

        hence thesis by XCMPLX_1: 5;

      end;

    end;

    registration

      let a be non zero Integer;

      cluster (a / ( Parity a)) -> odd;

      coherence

      proof

        ( Parity a) = (2 |^ (2 |-count a)) by Def1;

        hence thesis;

      end;

      cluster (a div ( Parity a)) -> odd;

      coherence

      proof

        (a / ( Parity a)) is odd;

        hence thesis by ADI;

      end;

    end

    theorem :: NEWTON05:29

    

     Th4: for a,b be Integer holds ( Parity a) divides ( Parity b) or ( Parity b) divides ( Parity a)

    proof

      let a,b be Integer;

      per cases ;

        suppose a = 0 or b = 0 ;

        then ( Parity a) = 0 or ( Parity b) = 0 by Def1;

        hence thesis by INT_2: 12;

      end;

        suppose

         B1: a <> 0 & b <> 0 ;

        then

        reconsider a as non zero Integer;

        reconsider b as non zero Integer by B1;

        

         B2: ( Parity a) = (2 |^ (2 |-count a)) & ( Parity b) = (2 |^ (2 |-count b)) by Def1;

        per cases ;

          suppose (2 |-count a) >= (2 |-count b);

          hence thesis by B2, NEWTON: 89;

        end;

          suppose (2 |-count b) >= (2 |-count a);

          hence thesis by B2, NEWTON: 89;

        end;

      end;

    end;

    theorem :: NEWTON05:30

    

     PEPIN31: for a,b be non zero Integer holds ( Parity a) divides ( Parity b) iff ( Parity b) >= ( Parity a)

    proof

      let a,b be non zero Integer;

      

       A1: ( Parity a) = (2 |^ (2 |-count a)) & ( Parity b) = (2 |^ (2 |-count b)) by Def1;

      ( Parity b) >= ( Parity a) implies ( Parity a) divides ( Parity b)

      proof

        assume ( Parity b) >= ( Parity a);

        then (2 |-count b) >= (2 |-count a) by A1, PEPIN: 66;

        hence thesis by A1, NEWTON: 89;

      end;

      hence thesis by NAT_D: 7;

    end;

    theorem :: NEWTON05:31

    

     P2P: for a,b be non zero Integer st ( Parity a) > ( Parity b) holds (2 * ( Parity b)) divides ( Parity a)

    proof

      let a,b be non zero Integer such that

       A1: ( Parity a) > ( Parity b);

      

       A2: ( Parity a) = (2 |^ (2 |-count a)) & ( Parity b) = (2 |^ (2 |-count b)) by Def1;

      then (2 |-count a) > (2 |-count b) by A1, PREPOWER: 93;

      then (2 |-count a) >= ((2 |-count b) + 1) by NAT_1: 13;

      then (2 |^ ((2 |-count b) + 1)) divides (2 |^ (2 |-count a)) by NEWTON: 89;

      hence thesis by A2, NEWTON: 6;

    end;

    theorem :: NEWTON05:32

    

     PM: for a be Integer holds ( Parity a) = ( Parity ( - a))

    proof

      let a be Integer;

      per cases ;

        suppose a <> 0 ;

        then

        reconsider a as non zero Integer;

        

         B1: 2 is non trivial Nat by NAT_2:def 1;

        ( Parity ( - a)) = (2 |^ (2 |-count (a * ( - 1)))) by Def1

        .= (2 |^ ((2 |-count a) + (2 |-count ( - 1)))) by NEWTON03: 57, INT_2: 28

        .= (2 |^ ((2 |-count a) + 0 )) by B1;

        hence thesis by Def1;

      end;

        suppose a = 0 ;

        hence thesis;

      end;

    end;

    theorem :: NEWTON05:33

    

     PMP: for a be Integer holds ( Parity a) = ( Parity |.a.|)

    proof

      let a be Integer;

      per cases by ABSVALUE: 1;

        suppose |.a.| = a;

        hence thesis;

      end;

        suppose |.a.| = ( - a);

        hence thesis by PM;

      end;

    end;

    theorem :: NEWTON05:34

    for a be Integer holds ( Parity a) <= |.a.|

    proof

      let a be Integer;

      per cases ;

        suppose a = 0 ;

        hence thesis by Def1;

      end;

        suppose a <> 0 ;

        then ( Parity |.a.|) <= |.a.| by Th3, NAT_D: 7;

        hence thesis by PMP;

      end;

    end;

    theorem :: NEWTON05:35

    

     PYTHTRIP10: for a,b be Integer st (a,b) are_coprime holds a is odd or b is odd

    proof

      let a,b be Integer such that

       A1: (a,b) are_coprime ;

      assume not thesis;

      then (a gcd b) is even;

      hence contradiction by A1;

    end;

    theorem :: NEWTON05:36

    

     MPO: for a,b be odd Integer st |.a.| <> |.b.| holds ( min (( Parity (a - b)),( Parity (a + b)))) = 2

    proof

      let a,b be odd Integer such that

       A1: |.a.| <> |.b.|;

      

       A0: |.a.| in NAT & |.b.| in NAT by INT_1: 3;

      then

      reconsider k = |.a.| as odd Nat;

      reconsider l = |.b.| as odd Nat by A0;

      (k - l) <> 0 & (k + l) <> 0 by A1;

      then

       A2: ( Parity (k - l)) = (2 |^ (2 |-count (k - l))) & ( Parity (k + l)) = (2 |^ (2 |-count (k + l))) by Def1;

      

       A3: ( Parity (k - l)) = ( Parity |.(k - l).|) & ( Parity (a + b)) = ( Parity |.(a + b).|) & ( Parity (a - b)) = ( Parity |.(a - b).|) by PMP;

      ( min ((2 |-count (k - l)),(2 |-count (k + l)))) = 1 by A1, NEWTON03: 82;

      then

       A4: ( min (( Parity (k - l)),( Parity (k + l)))) = (2 |^ 1) by A2, MIN1;

      per cases by ABS;

        suppose |.(a + b).| = ( |.a.| + |.b.|);

        then |.(a - ( - b)).| = ( |.a.| + |.( - b).|) by COMPLEX1: 52;

        then |.(a - ( - b)).| = ( |.a.| + |.( - b).|) & |.(a + ( - b)).| = |.( |.a.| - |.( - b).|).| by LmABS;

        then ( Parity |.(a + b).|) = ( Parity ( |.a.| + |.b.|)) & ( Parity |.(a - b).|) = ( Parity |.( |.a.| - |.b.|).|) by COMPLEX1: 52;

        hence thesis by A4, A3;

      end;

        suppose |.(a - b).| = ( |.a.| + |.b.|);

        hence thesis by A4, A3, LmABS;

      end;

    end;

    theorem :: NEWTON05:37

    

     ODP: for a,b be odd Integer holds ( min (( Parity (a - b)),( Parity (a + b)))) <= 2

    proof

      let a,b be odd Integer;

      

       A0: |.a.| in NAT & |.b.| in NAT by INT_1: 3;

      then

      reconsider k = |.a.| as odd Nat;

      reconsider l = |.b.| as odd Nat by A0;

      per cases ;

        suppose k = l;

        then ( Parity |.( |.a.| - |.b.|).|) = 0 by Def1;

        then ( Parity |.(a - b).|) = 0 or ( Parity |.(a + b).|) = 0 by ABS1;

        then ( Parity (a - b)) = 0 or ( Parity (a + b)) = 0 by PMP;

        hence thesis by XXREAL_0:def 9;

      end;

        suppose k <> l;

        hence thesis by MPO;

      end;

    end;

    theorem :: NEWTON05:38

    for a,b be Integer st (a,b) are_coprime holds ( min (( Parity (a - b)),( Parity (a + b)))) <= 2

    proof

      let a,b be Integer such that

       A1: (a,b) are_coprime ;

      per cases ;

        suppose

         B1: a is even;

        then b is odd by A1, PYTHTRIP10;

        then ( Parity (a + b)) = 1 & ( Parity (a - b)) = 1 by B1, NAT_2:def 1;

        hence thesis;

      end;

        suppose

         B1: b is even;

        then a is odd by A1, PYTHTRIP10;

        then ( Parity (a + b)) = 1 & ( Parity (a - b)) = 1 by B1, NAT_2:def 1;

        hence thesis;

      end;

        suppose a is odd & b is odd;

        hence thesis by ODP;

      end;

    end;

    theorem :: NEWTON05:39

    

     CCM: for a,b be non zero Integer, c be non trivial Nat holds (c |-count (a gcd b)) = ( min ((c |-count a),(c |-count b)))

    proof

      let a,b be non zero Integer, c be non trivial Nat;

      

       A1: |.c.| > 1 by NEWTON03:def 1;

      then

       A3: (c |^ (c |-count a)) divides a & not (c |^ ((c |-count a) + 1)) divides a by NEWTON03:def 7;

      

       A4: (c |^ (c |-count b)) divides b & not (c |^ ((c |-count b) + 1)) divides b by A1, NEWTON03:def 7;

      

       A5: |.(c |^ ((c |-count b) + 1)).| in NAT & |.a.| in NAT & |.b.| in NAT by INT_1: 3;

      per cases ;

        suppose

         B1: (c |-count a) >= (c |-count b);

        then

         B2: ( min ((c |-count a),(c |-count b))) = (c |-count b) by XXREAL_0:def 9;

        (c |^ (c |-count b)) divides (c |^ (c |-count a)) by B1, NEWTON: 89;

        then (c |^ (c |-count b)) divides a by A3, INT_2: 9;

        then

         B3: (c |^ (c |-count b)) divides (a gcd b) by A4, INT_2:def 2;

         not |.(c |^ ((c |-count b) + 1)).| divides |.b.| by A4, INT_2: 16;

        then not |.(c |^ ((c |-count b) + 1)).| divides ( |.a.| gcd |.b.|) by A5, NEWTON: 50;

        then not (c |^ ((c |-count b) + 1)) divides (a gcd b) by INT_2: 34;

        hence thesis by A1, B2, B3, NEWTON03:def 7;

      end;

        suppose

         B1: (c |-count b) > (c |-count a);

        then

         B2: ( min ((c |-count b),(c |-count a))) = (c |-count a) by XXREAL_0:def 9;

        (c |^ (c |-count a)) divides (c |^ (c |-count b)) by B1, NEWTON: 89;

        then (c |^ (c |-count a)) divides b by A4, INT_2: 9;

        then

         B3: (c |^ (c |-count a)) divides (a gcd b) by A3, INT_2:def 2;

         not |.(c |^ ((c |-count a) + 1)).| divides |.a.| by A3, INT_2: 16;

        then not |.(c |^ ((c |-count a) + 1)).| divides ( |.a.| gcd |.b.|) by A5, NEWTON: 50;

        then not (c |^ ((c |-count a) + 1)) divides (a gcd b) by INT_2: 34;

        hence thesis by A1, B2, B3, NEWTON03:def 7;

      end;

    end;

    theorem :: NEWTON05:40

    

     PGC: for a,b be non zero Integer holds ( Parity (a gcd b)) = ( min (( Parity a),( Parity b)))

    proof

      let a,b be non zero Integer;

      reconsider c = (a gcd b) as non zero Nat;

      

       A1: ( Parity c) = (2 |^ (2 |-count (a gcd b))) & ( Parity b) = (2 |^ (2 |-count b)) & ( Parity a) = (2 |^ (2 |-count a)) by Def1;

      2 is non trivial;

      

      then (2 |^ (2 |-count (a gcd b))) = (2 |^ ( min ((2 |-count a),(2 |-count b)))) by CCM

      .= ( min ((2 |^ (2 |-count a)),(2 |^ (2 |-count b)))) by MIN1;

      hence thesis by A1;

    end;

    theorem :: NEWTON05:41

    

     PGG: for a,b be Integer holds (( Parity a) gcd ( Parity b)) = ( Parity (a gcd b))

    proof

      let a,b be Integer;

       |.a.| in NAT by INT_1: 3;

      then

      reconsider k = |.a.| as Nat;

       |.b.| in NAT by INT_1: 3;

      then

      reconsider l = |.b.| as Nat;

      per cases ;

        suppose

         A1: a = 0 ;

        then ( Parity a) = 0 by Def1;

        then (( Parity a) gcd ( Parity b)) = ( Parity (k gcd l)) by A1, PMP;

        hence thesis by INT_2: 34;

      end;

        suppose

         A1: b = 0 ;

        then ( Parity b) = 0 by Def1;

        then (( Parity a) gcd ( Parity b)) = ( Parity (k gcd l)) by A1, PMP;

        hence thesis by INT_2: 34;

      end;

        suppose

         A0: a <> 0 & b <> 0 ;

        reconsider a as non zero Integer by A0;

        reconsider b as non zero Integer by A0;

        per cases by Th4;

          suppose

           B1: ( Parity a) divides ( Parity b);

          then

           B2: ( Parity a) <= ( Parity b) by NAT_D: 7;

          (( Parity a) gcd ( Parity b)) = |.( Parity a).| by B1

          .= ( min (( Parity a),( Parity b))) by B2, XXREAL_0:def 9

          .= ( Parity (a gcd b)) by PGC;

          hence thesis;

        end;

          suppose

           B1: ( Parity b) divides ( Parity a);

          then

           B2: ( Parity a) >= ( Parity b) by NAT_D: 7;

          (( Parity a) gcd ( Parity b)) = |.( Parity b).| by B1

          .= ( min (( Parity a),( Parity b))) by B2, XXREAL_0:def 9

          .= ( Parity (a gcd b)) by PGC;

          hence thesis;

        end;

      end;

    end;

    theorem :: NEWTON05:42

    for a be Nat holds ( Parity (2 * a)) = (2 * ( Parity a))

    proof

      let a be Nat;

      ( Parity (2 * a)) = (( Parity 2) * ( Parity a)) by ILP;

      hence thesis;

    end;

    theorem :: NEWTON05:43

    

     PLG: for a,b be Integer holds (( Parity a) lcm ( Parity b)) = ( Parity (a lcm b))

    proof

      let a,b be Integer;

       |.a.| in NAT by INT_1: 3;

      then

      reconsider k = |.a.| as Nat;

       |.b.| in NAT by INT_1: 3;

      then

      reconsider l = |.b.| as Nat;

      per cases ;

        suppose

         A1: a = 0 or b = 0 ;

        then ( Parity a) = 0 or ( Parity b) = 0 by Def1;

        hence thesis by A1;

      end;

        suppose

         A0: a <> 0 & b <> 0 ;

        reconsider a as non zero Integer by A0;

        reconsider b as non zero Integer by A0;

        ((( Parity a) lcm ( Parity b)) * (( Parity a) gcd ( Parity b))) = (( Parity a) * ( Parity b)) by NAT_D: 29

        .= ( Parity (a * b)) by ILP

        .= ( Parity |.(a * b).|) by PMP

        .= ( Parity (k * l)) by COMPLEX1: 65

        .= ( Parity ((k gcd l) * (k lcm l))) by NAT_D: 29

        .= (( Parity (k gcd l)) * ( Parity (k lcm l))) by ILP

        .= (( Parity (a gcd b)) * ( Parity (k lcm l))) by INT_2: 34

        .= (( Parity (a gcd b)) * ( Parity (a lcm b))) by INT_2: 33

        .= ((( Parity a) gcd ( Parity b)) * ( Parity (a lcm b))) by PGG;

        hence thesis by XCMPLX_1: 5;

      end;

    end;

    theorem :: NEWTON05:44

    for a,b be non zero Integer holds ( Parity (a lcm b)) = ( max (( Parity a),( Parity b)))

    proof

      let a,b be non zero Integer;

      (( min (( Parity a),( Parity b))) * ( max (( Parity a),( Parity b)))) = (( Parity a) * ( Parity b)) by NEWTON04: 18

      .= ((( Parity a) gcd ( Parity b)) * (( Parity a) lcm ( Parity b))) by NAT_D: 29

      .= (( Parity (a gcd b)) * (( Parity a) lcm ( Parity b))) by PGG

      .= (( min (( Parity a),( Parity b))) * (( Parity a) lcm ( Parity b))) by PGC

      .= (( min (( Parity a),( Parity b))) * ( Parity (a lcm b))) by PLG;

      hence thesis by XCMPLX_1: 5;

    end;

    theorem :: NEWTON05:45

    for a,b be Integer holds ( Parity (a + b)) = (( Parity (a gcd b)) * ( Parity ((a + b) / (a gcd b))))

    proof

      let a,b be Integer;

      per cases ;

        suppose a = 0 & b = 0 ;

        then ( Parity (a gcd b)) = 0 & ( Parity (a + b)) = 0 by Def1;

        hence thesis;

      end;

        suppose

         A1: a <> 0 or b <> 0 ;

        ( Parity (((a + b) / (a gcd b)) * (a gcd b))) = (( Parity ((a + b) / (a gcd b))) * ( Parity (a gcd b))) by ILP;

        hence thesis by A1, XCMPLX_1: 87;

      end;

    end;

    theorem :: NEWTON05:46

    

     PAN: for a be Integer, n be Nat holds ( Parity (a |^ n)) = (( Parity a) |^ n)

    proof

      let a be Integer, n be Nat;

      defpred P[ Nat] means ( Parity (a |^ $1)) = (( Parity a) |^ $1);

      

       A1: P[ 0 ]

      proof

        ( Parity (1 * (a |^ 0 ))) = (1 * (( Parity a) |^ 0 ));

        hence thesis;

      end;

      

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

      proof

        let k be Nat;

        assume

         B1: ( Parity (a |^ k)) = (( Parity a) |^ k);

        ( Parity (a |^ (k + 1))) = ( Parity (a * (a |^ k))) by NEWTON: 6

        .= (( Parity a) * (( Parity a) |^ k)) by B1, ILP;

        hence thesis by NEWTON: 6;

      end;

      for x be Nat holds P[x] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: NEWTON05:47

    for a,b be non zero Integer, n be Nat holds ( min (( Parity (a |^ n)),( Parity (b |^ n)))) = (( min (( Parity a),( Parity b))) |^ n)

    proof

      let a,b be non zero Integer, n be Nat;

      ( min (( Parity (a |^ n)),( Parity (b |^ n)))) = ( Parity ((a |^ n) gcd (b |^ n))) by PGC

      .= ( Parity ((a gcd b) |^ n)) by NEWTON03: 4

      .= (( Parity (a gcd b)) |^ n) by PAN;

      hence thesis by PGC;

    end;

    registration

      let a be odd Integer;

      identify parity a with Parity a;

      correctness

      proof

        

        thus ( Parity a) = 1 by NAT_2:def 1

        .= ( parity a) by NAT_2:def 1;

      end;

      identify Parity a with parity a;

      correctness ;

      reduce (a |^ ( parity a)) to a;

      reducibility

      proof

        (a |^ ( parity a)) = (a |^ 1) by NAT_2:def 1;

        hence thesis;

      end;

    end

    registration

      let a be even Integer;

      cluster (a |^ ( parity a)) -> trivial non zero;

      coherence

      proof

        (a |^ ( parity a)) = (1 * (a |^ 0 ));

        hence thesis by NAT_2:def 1;

      end;

    end

    registration

      let a be Integer;

      reduce ( parity ( parity a)) to ( parity a);

      reducibility ;

      reduce ( Parity ( parity a)) to ( parity a);

      reducibility

      proof

        per cases ;

          suppose a is odd;

          hence thesis;

        end;

          suppose a is even;

          hence thesis by Def1;

        end;

      end;

    end

    theorem :: NEWTON05:48

    

     PIP: for a be Integer holds (a is even iff ( parity a) is even) & (( parity a) is even iff ( Parity a) is even)

    proof

      let a be Integer;

      per cases ;

        suppose a is even;

        hence thesis;

      end;

        suppose a is odd;

        hence thesis;

      end;

    end;

    registration

      let a be Integer;

      cluster (( parity a) + ( Parity a)) -> even;

      coherence

      proof

        ( Parity a) is even iff ( parity a) is even by PIP;

        hence thesis;

      end;

      cluster (( Parity a) - ( parity a)) -> even;

      coherence

      proof

        ( Parity a) is even iff ( parity a) is even by PIP;

        hence thesis;

      end;

      cluster (( Parity a) - ( parity a)) -> natural;

      coherence

      proof

        per cases ;

          suppose a = 0 ;

          hence thesis;

        end;

          suppose a <> 0 ;

          then ( Parity a) >= 1 & ( parity a) <= 1 by NAT_1: 14, NEWTON03:def 1;

          then (( Parity a) - ( parity a)) >= (1 - 1) by XREAL_1: 13;

          hence thesis;

        end;

      end;

      cluster (a + ( parity a)) -> even;

      coherence

      proof

        a is even iff ( parity a) is even;

        hence thesis;

      end;

      cluster (a - ( parity a)) -> even;

      coherence

      proof

        a is odd iff ( parity a) is odd;

        hence thesis;

      end;

    end

    theorem :: NEWTON05:49

    for a be Integer holds ( parity ( Parity a)) = ( parity a)

    proof

      let a be Integer;

      per cases ;

        suppose

         A1: a is even;

        then ( Parity a) is even;

        hence thesis by A1;

      end;

        suppose

         A1: a is odd;

        then ( Parity a) is odd;

        hence thesis by A1;

      end;

    end;

    theorem :: NEWTON05:50

    

     P1: for a be Integer holds ( parity a) = ( parity ( - a))

    proof

      let a be Integer;

      per cases ;

        suppose

         A1: a is even;

         0 is even;

        then ( 0 - a) is even by A1;

        hence thesis by A1;

      end;

        suppose

         A1: a is odd;

        then ( - a) is odd;

        hence thesis by A1;

      end;

    end;

    theorem :: NEWTON05:51

    

     PMI: for a,b be Integer holds ( parity (a - b)) = |.(( parity a) - ( parity b)).|

    proof

      let a,b be Integer;

      per cases ;

        suppose

         A1: a is even;

        per cases ;

          suppose b is even;

          then ( parity (a - b)) = 0 & |.(( parity a) - ( parity b)).| = 0 by A1;

          hence thesis;

        end;

          suppose

           B1: b is odd;

          then

           B2: (a - b) is odd by A1;

           |.(( parity a) - ( parity b)).| = ( - ( - 1)) by A1, B1

          .= ( parity (a - b)) by B2;

          hence thesis;

        end;

      end;

        suppose

         A1: a is odd;

        per cases ;

          suppose b is odd;

          then ( parity (a - b)) = 0 & |.(( parity a) - ( parity b)).| = 0 by A1;

          hence thesis;

        end;

          suppose

           B1: b is even;

          then (a - b) is odd by A1;

          hence thesis by A1, B1;

        end;

      end;

    end;

    theorem :: NEWTON05:52

    for a,b be Integer holds ( parity (a + b)) = ( parity (( parity a) + ( parity b))) by NAT_D: 66;

    theorem :: NEWTON05:53

    

     PPM: for a,b be Integer holds ( parity (a + b)) = ( parity (a - b))

    proof

      let a,b be Integer;

      ( parity (a + b)) = ( parity (( parity a) + ( parity b))) by NAT_D: 66

      .= ( parity (( parity a) + ( parity ( - b)))) by P1

      .= ( parity (a + ( - b))) by NAT_D: 66;

      hence thesis;

    end;

    theorem :: NEWTON05:54

    

     ABP: for a,b be Integer holds ( parity (a + b)) = |.(( parity a) - ( parity b)).|

    proof

      let a,b be Integer;

      

      thus ( parity (a + b)) = ( parity (a - b)) by PPM

      .= |.(( parity a) - ( parity b)).| by PMI;

    end;

    theorem :: NEWTON05:55

    for a,b be Nat holds (( parity (a + b)) = ( parity b) implies ( parity a) = 0 ) & (( parity (a + b)) <> ( parity b) implies ( parity a) = 1)

    proof

      let a,b be Nat;

      (((a + b) mod 2) = (b mod 2) implies (a mod 2) = 0 ) & (((a + b) mod 2) <> (b mod 2) implies (a mod 2) <> 0 ) by MAB;

      hence thesis by NAT_2:def 1;

    end;

    theorem :: NEWTON05:56

    for a,b be Integer holds ( parity (a + b)) = ((( parity a) + ( parity b)) - ((2 * ( parity a)) * ( parity b))) & (( parity a) - ( parity b)) = (( parity (a + b)) - ((2 * ( parity (a + b))) * ( parity b))) & (( parity a) - ( parity b)) = (((2 * ( parity a)) * ( parity (a + b))) - ( parity (a + b)))

    proof

      let a,b be Integer;

      per cases ;

        suppose a is even & b is even;

        then ( parity a) = 0 & ( parity b) = 0 & ( parity (a + b)) = 0 ;

        hence thesis;

      end;

        suppose a is odd & b is odd;

        then ( parity a) = 1 & ( parity b) = 1 & ( parity (a + b)) = 0 ;

        hence thesis;

      end;

        suppose

         A1: a is even & b is odd;

        then (a + b) is odd;

        hence thesis by A1;

      end;

        suppose

         A1: a is odd & b is even;

        then (a + b) is odd;

        hence thesis by A1;

      end;

    end;

    theorem :: NEWTON05:57

    

     EVP: for a,b be Integer holds (a + b) is even iff ( parity a) = ( parity b)

    proof

      let a,b be Integer;

      thus (a + b) is even implies ( parity a) = ( parity b)

      proof

        assume (a + b) is even;

        

        then 0 = ( parity (a + b))

        .= |.(( parity a) - ( parity b)).| by ABP;

        then (( parity a) - ( parity b)) = 0 ;

        hence thesis;

      end;

      assume ( parity a) = ( parity b);

      

      then 0 = |.(( parity a) - ( parity b)).|

      .= ( parity (a + b)) by ABP;

      hence thesis;

    end;

    theorem :: NEWTON05:58

    for a,b be Integer holds ( parity (a * b)) = (( parity a) * ( parity b))

    proof

      let a,b be Integer;

      per cases ;

        suppose a is even;

        then ( parity a) = 0 & ( parity (a * b)) = 0 ;

        hence thesis;

      end;

        suppose a is odd;

        then ( parity a) = 1 & (b is even iff (a * b) is even);

        hence thesis;

      end;

    end;

    theorem :: NEWTON05:59

    for a,b be Integer holds ( parity (a lcm b)) = ( parity (a * b))

    proof

      let a,b be Integer;

      per cases ;

        suppose

         A1: (a * b) is odd;

        then a is odd & b is odd;

        then (a lcm b) is odd;

        hence thesis by A1;

      end;

        suppose

         A1: (a * b) is even;

        then a is even or b is even;

        then (a lcm b) is even;

        hence thesis by A1;

      end;

    end;

    theorem :: NEWTON05:60

    for a,b be Integer holds ( parity (a gcd b)) = ( max (( parity a),( parity b)))

    proof

      let a,b be Integer;

      per cases ;

        suppose

         A1: a is odd;

        then (a gcd b) is odd;

        hence thesis by A1, XXREAL_0:def 10, NEWTON03:def 1;

      end;

        suppose

         A1: a is even;

        per cases ;

          suppose

           B1: b is odd;

          then (a gcd b) is odd;

          hence thesis by B1, A1, XXREAL_0:def 10;

        end;

          suppose

           B1: b is even;

          then (a gcd b) is even by A1;

          hence thesis by B1, A1;

        end;

      end;

    end;

    theorem :: NEWTON05:61

    for a,b be Integer holds ( parity (a * b)) = ( min (( parity a),( parity b)))

    proof

      let a,b be Integer;

      ( min (( parity a),( parity b))) = ( parity a) or ( min (( parity a),( parity b))) = ( parity b) by XXREAL_0:def 9;

      per cases by NAT_2:def 1;

        suppose

         B1: ( min (( parity a),( parity b))) = 0 ;

        then a is even or b is even;

        hence thesis by B1;

      end;

        suppose

         B1: ( min (( parity a),( parity b))) = 1;

        then a is odd & b is odd by XXREAL_0:def 9;

        then (a * b) is odd;

        hence thesis by B1;

      end;

    end;

    theorem :: NEWTON05:62

    for a be Integer, n be non zero Nat holds ( parity (a |^ n)) = ( parity a)

    proof

      let a be Integer, n be non zero Nat;

      per cases ;

        suppose

         A1: a is even;

        then (a |^ n) is even;

        hence thesis by A1;

      end;

        suppose

         A1: a is odd;

        then (a |^ n) is odd;

        hence thesis by A1;

      end;

    end;

    

     PAP: for a,b be non zero Integer holds ( Parity a) > ( Parity b) implies ( Parity (a + b)) = ( Parity b)

    proof

      let a,b be non zero Integer;

      assume

       A1: ( Parity a) > ( Parity b);

      then

       A1a: not ( Parity a) divides ( Parity b) by NAT_D: 7;

      

       A2: |.2.| > 1;

      a <> ( - b) by A1, PM;

      then

       A3: (a + b) <> 0 ;

      reconsider k = (2 |-count a) as Nat;

      reconsider l = (2 |-count b) as Nat;

      

       A2a: ( Parity a) = (2 |^ k) & ( Parity b) = (2 |^ l) by Def1;

      then

       A2b: k > l by A1a, PEPIN: 31;

      then (2 |^ l) divides ( Parity a) & ( Parity a) divides a & ( Parity b) divides b by PEPIN: 31, A2a, Th3;

      then (2 |^ l) divides a & (2 |^ l) divides b by Def1, INT_2: 9;

      then

       A4: (2 |^ l) divides (a + b) by WSIERP_1: 4;

       not (2 |^ (l + 1)) divides (a + b)

      proof

        (l + 1) <= k by A2b, NAT_1: 13;

        then

         B1: (2 |^ (l + 1)) divides (2 |^ k) by PEPIN: 31;

        (2 |^ k) divides a by A2, NEWTON03:def 7;

        then

         B2: (2 |^ (l + 1)) divides a by INT_2: 9, B1;

         not (2 |^ (l + 1)) divides b by A2, NEWTON03:def 7;

        hence thesis by INT_2: 1, B2;

      end;

      then (2 |-count (a + b)) = l by A2, A3, A4, NEWTON03:def 7;

      then ( Parity (a + b)) = (2 |^ l) by A3, Def1;

      hence thesis by Def1;

    end;

    theorem :: NEWTON05:63

    

     LEQ: for a,b be non zero Integer holds ( Parity (a + b)) >= (( Parity a) + ( Parity b)) implies ( Parity a) = ( Parity b)

    proof

      let a,b be non zero Integer;

      assume

       A1: ( Parity (a + b)) >= (( Parity a) + ( Parity b));

      (( Parity a) + ( Parity b)) > (( Parity b) + 0 ) & (( Parity a) + ( Parity b)) > (( Parity a) + 0 ) by XREAL_1: 6;

      then ( Parity a) <= ( Parity b) & ( Parity b) <= ( Parity a) by A1, PAP;

      hence thesis by XXREAL_0: 1;

    end;

    theorem :: NEWTON05:64

    for a,b be Integer holds ( Parity (a + b)) > (( Parity a) + ( Parity b)) implies ( Parity a) = ( Parity b)

    proof

      let a,b be Integer;

      per cases ;

        suppose a is zero;

        then ( Parity (a + b)) = ( Parity b) & ( Parity a) = 0 by Def1;

        hence thesis;

      end;

        suppose b is zero;

        then ( Parity (a + b)) = ( Parity a) & ( Parity b) = 0 by Def1;

        hence thesis;

      end;

        suppose not a is zero & not b is zero;

        hence thesis by LEQ;

      end;

    end;

    theorem :: NEWTON05:65

    for a,b be odd Integer, m be odd Nat holds ( Parity ((a |^ m) + (b |^ m))) = ( Parity (a + b))

    proof

      let a,b be odd Integer, m be odd Nat;

      per cases ;

        suppose

         A1: (a + b) = 0 ;

        then a = ( - b);

        then (a |^ m) = ( - (b |^ m)) by POWER: 2;

        hence thesis by A1;

      end;

        suppose

         A1: (a + b) <> 0 ;

        then a <> ( - b);

        then (a |^ m) <> (( - b) |^ m) by NEWTON03: 13;

        then (a |^ m) <> ( - (b |^ m)) by POWER: 2;

        then ((a |^ m) + (b |^ m)) <> 0 ;

        then ( Parity ((a |^ m) + (b |^ m))) = (2 |^ (2 |-count ((a |^ m) + (b |^ m)))) & ( Parity (a + b)) = (2 |^ (2 |-count (a + b))) by A1, Def1;

        hence thesis by NEWTON03: 81;

      end;

    end;

    theorem :: NEWTON05:66

    for a,b be odd Integer, m be even Nat holds ( Parity ((a |^ m) + (b |^ m))) = 2

    proof

      let a,b be odd Integer, m be even Nat;

      reconsider n = (m / 2) as Nat;

      

       A1: ((a |^ n) |^ 2) = (a |^ (2 * n)) & ((b |^ n) |^ 2) = (b |^ (2 * n)) by NEWTON: 9;

      (2 |^ (2 |-count (((a |^ n) |^ 2) + ((b |^ n) |^ 2)))) = (2 |^ 1) by NEWTON03: 74;

      hence thesis by A1, Def1;

    end;

    theorem :: NEWTON05:67

    

     PEQ: for a,b be non zero Integer st (a + b) <> 0 holds ( Parity a) = ( Parity b) implies ( Parity (a + b)) >= (( Parity a) + ( Parity b))

    proof

      let a,b be non zero Integer such that

       A0: (a + b) <> 0 ;

      reconsider k = (2 |-count a) as Nat;

      assume

       A1: ( Parity a) = ( Parity b);

      reconsider l = ((a / ( Parity a)) + (b / ( Parity b))) as even Integer;

      

       A2: (l * ( Parity a)) = (((a / ( Parity a)) * ( Parity a)) + ((b / ( Parity b)) * ( Parity b))) by A1

      .= (((a / ( Parity a)) * ( Parity a)) + b) by XCMPLX_1: 87

      .= (a + b) by XCMPLX_1: 87;

      

       A3: (2 * ( Parity a)) = (2 * (2 |^ k)) by Def1

      .= (2 |^ (k + 1)) by NEWTON: 6;

      2 divides l by ABIAN:def 1;

      then 2 is non trivial & (2 |^ (k + 1)) divides (a + b) by NEWTON03: 5, A2, A3;

      then (2 |-count (a + b)) >= (k + 1) by A0, NEWTON03: 59;

      then (2 |^ (k + 1)) divides (2 |^ (2 |-count (a + b))) by PEPIN: 31;

      then (2 |^ (k + 1)) divides ( Parity (a + b)) by A0, Def1;

      hence thesis by A0, A1, A3, NAT_D: 7;

    end;

    theorem :: NEWTON05:68

    for a,b be non zero Integer holds ( Parity (a + b)) = ( Parity b) iff ( Parity a) > ( Parity b)

    proof

      let a,b be non zero Integer;

      thus ( Parity (a + b)) = ( Parity b) implies ( Parity a) > ( Parity b)

      proof

        assume

         A1: ( Parity (a + b)) = ( Parity b);

        then

         A2: (( Parity (a + b)) + 0 ) < (( Parity a) + ( Parity b)) by XREAL_1: 6;

        per cases by XXREAL_0: 1;

          suppose ( Parity a) = ( Parity b);

          hence thesis by A1, A2, Def1, PEQ;

        end;

          suppose ( Parity b) > ( Parity a);

          hence thesis by A1, PAP;

        end;

          suppose ( Parity b) < ( Parity a);

          hence thesis;

        end;

      end;

      thus thesis by PAP;

    end;

    theorem :: NEWTON05:69

    for a,b be non zero Nat holds ( Parity (a + b)) < (( Parity a) + ( Parity b)) implies ( Parity (a + b)) = ( min (( Parity a),( Parity b)))

    proof

      let a,b be non zero Nat;

      assume ( Parity (a + b)) < (( Parity a) + ( Parity b));

      then ( Parity a) <> ( Parity b) by PEQ;

      per cases by XXREAL_0: 1;

        suppose

         B1: ( Parity a) > ( Parity b);

        then ( Parity (a + b)) = ( Parity b) by PAP;

        hence thesis by B1, XXREAL_0:def 9;

      end;

        suppose

         B1: ( Parity a) < ( Parity b);

        then ( Parity (a + b)) = ( Parity a) by PAP;

        hence thesis by B1, XXREAL_0:def 9;

      end;

    end;

    theorem :: NEWTON05:70

    for a,b be non zero Integer st (a + b) <> 0 holds ( Parity (a + b)) = ( Parity a) implies ( Parity a) < ( Parity b)

    proof

      let a,b be non zero Integer such that

       A0: (a + b) <> 0 ;

      assume

       A1: ( Parity (a + b)) = ( Parity a);

      (( Parity a) + ( Parity b)) > (( Parity a) + 0 ) by XREAL_1: 6;

      then ( Parity a) <> ( Parity b) by A0, A1, PEQ;

      then ( Parity a) > ( Parity b) or ( Parity a) < ( Parity b) by XXREAL_0: 1;

      hence thesis by PAP, A1;

    end;

    theorem :: NEWTON05:71

    

     PGP: for a be Integer holds ( Parity (a + ( Parity a))) = (( Parity (( Oddity a) + 1)) * ( Parity a)) & ( Parity (a - ( Parity a))) = (( Parity (( Oddity a) - 1)) * ( Parity a))

    proof

      let a be Integer;

      per cases ;

        suppose a is non zero;

        then

        reconsider a as non zero Integer;

        

         A1: ( Parity (a - ( Parity a))) = ( Parity ((( Oddity a) * ( Parity a)) - (1 * ( Parity a))))

        .= ( Parity ((( Oddity a) - 1) * ( Parity a)))

        .= (( Parity (( Oddity a) - 1)) * ( Parity ( Parity a))) by ILP

        .= (( Parity (( Oddity a) - 1)) * ( Parity a));

        ( Parity (a + ( Parity a))) = ( Parity ((( Oddity a) * ( Parity a)) + ( Parity a)))

        .= ( Parity ((( Oddity a) + 1) * ( Parity a)))

        .= (( Parity (( Oddity a) + 1)) * ( Parity ( Parity a))) by ILP

        .= (( Parity (( Oddity a) + 1)) * ( Parity a));

        hence thesis by A1;

      end;

        suppose a is zero;

        then ( Parity (a + ( Parity a))) = ( Parity 0 ) & ( Parity a) = 0 by Def1;

        hence thesis;

      end;

    end;

    theorem :: NEWTON05:72

    

     ADA: for a be Integer holds (2 * ( Parity a)) divides ( Parity (a + ( Parity a))) & (2 * ( Parity a)) divides ( Parity (a - ( Parity a)))

    proof

      let a be Integer;

      per cases ;

        suppose a is zero;

        then ( Parity a) = 0 by Def1;

        hence thesis;

      end;

        suppose not a is zero;

        then

        reconsider a as non zero Integer;

        2 divides ( Parity (( Oddity a) + 1)) & 2 divides ( Parity (( Oddity a) - 1)) by ABIAN:def 1;

        then (2 * ( Parity a)) divides (( Parity a) * ( Parity (( Oddity a) + 1))) & (2 * ( Parity a)) divides (( Parity a) * ( Parity (( Oddity a) - 1))) by NEWTON03: 5;

        hence thesis by PGP;

      end;

    end;

    theorem :: NEWTON05:73

    for a,b be Integer st ( Parity a) = ( Parity b) holds ( Parity (a + b)) = ( Parity ((a + ( Parity a)) + (b - ( Parity b))));

    theorem :: NEWTON05:74

    for a be Nat holds ( Parity (a + ( Parity a))) >= (2 * ( Parity a))

    proof

      let a be Nat;

      per cases ;

        suppose a = 0 ;

        then ( Parity a) = 0 by Def1;

        hence thesis;

      end;

        suppose a <> 0 ;

        hence thesis by ADA, NAT_D: 7;

      end;

    end;

    theorem :: NEWTON05:75

    for a be Nat holds ( Parity (a - ( Parity a))) >= (2 * ( Parity a)) or a = ( Parity a)

    proof

      let a be Nat;

      per cases ;

        suppose a = ( Parity a);

        hence thesis;

      end;

        suppose

         A0: a <> ( Parity a);

        then

        reconsider a as non zero Nat by Def1;

        

         A1: ( Parity (a - ( Parity a))) = (( Parity (( Oddity a) - 1)) * ( Parity a)) by PGP;

        a = (( Oddity a) * ( Parity a));

        then

         A2: (( Oddity a) - 1) <> 0 by A0;

        ( Parity (( Oddity a) - 1)) <> 1;

        hence thesis by A1, A2, XREAL_1: 64, NAT_1: 23;

      end;

    end;

    theorem :: NEWTON05:76

    

     PSD: for a,b be odd Integer holds ( Parity (a + b)) <> ( Parity (a - b))

    proof

      let a,b be odd Integer;

      per cases ;

        suppose

         B1: (a + b) is zero;

        

        then ( Parity (a - b)) = ( Parity (2 * a))

        .= (( Parity 2) * ( Parity a)) by ILP;

        hence thesis by B1, Def1;

      end;

        suppose

         B1: (a - b) is zero;

        

        then ( Parity (a + b)) = ( Parity (2 * a))

        .= (( Parity 2) * ( Parity a)) by ILP;

        hence thesis by B1, Def1;

      end;

        suppose

         B0: (a + b) <> 0 & (a - b) <> 0 ;

        then

         B1: (2 |^ (2 |-count (a + b))) = ( Parity (a + b)) & (2 |^ (2 |-count (a - b))) = ( Parity (a - b)) by Def1;

        (2 * 2) = (2 |^ 2) by NEWTON: 81;

        then

         B2: (2 |^ 2) divides (a + b) iff not (2 |^ 2) divides (a - b) by NEWTON03: 73;

        2 is non trivial;

        then (2 |-count (a + b)) >= 2 iff (2 |-count (a - b)) < 2 by B0, B2, NEWTON03: 59;

        per cases by XXREAL_0: 1;

          suppose (2 |-count (a + b)) > (2 |-count (a - b));

          hence thesis by B1, PEPIN: 66;

        end;

          suppose (2 |-count (a + b)) < (2 |-count (a - b));

          hence thesis by B1, PEPIN: 66;

        end;

      end;

    end;

    theorem :: NEWTON05:77

    for a,b be odd Integer holds ( Parity (a + 1)) = ( Parity (b - 1)) implies a <> b

    proof

      let a,b be odd Integer;

      1 is odd;

      hence thesis by PSD;

    end;

    theorem :: NEWTON05:78

    

     PMG: for a be odd Nat, b be non trivial odd Nat holds ( Parity (a + b)) = ( min (( Parity (a + 1)),( Parity (b - 1)))) or ( Parity (a + b)) >= (2 * ( Parity (a + 1)))

    proof

      let a be odd Nat, b be non trivial odd Nat;

      per cases by XXREAL_0: 1;

        suppose

         A1: ( Parity (a + 1)) = ( Parity (b - 1));

        then ( Parity ((a + 1) + (b - 1))) >= (( Parity (a + 1)) + ( Parity (b - 1))) by PEQ;

        hence thesis by A1;

      end;

        suppose

         B1: ( Parity (a + 1)) > ( Parity (b - 1));

        then ( Parity ((a + 1) + (b - 1))) = ( Parity (b - 1)) by PAP;

        hence thesis by B1, XXREAL_0:def 9;

      end;

        suppose

         B1: ( Parity (a + 1)) < ( Parity (b - 1));

        then ( Parity ((a + 1) + (b - 1))) = ( Parity (a + 1)) by PAP;

        hence thesis by B1, XXREAL_0:def 9;

      end;

    end;

    theorem :: NEWTON05:79

    for a,b be non zero Integer holds ( Parity a) > ( Parity b) implies (a div ( Parity b)) is even

    proof

      let a,b be non zero Integer;

      assume ( Parity a) > ( Parity b);

      then

       A0: (2 * ( Parity b)) divides ( Parity a) by P2P;

      ( Parity a) divides a by Th3;

      then (2 * ( Parity b)) divides a by INT_2: 9, A0;

      then

      consider c be Integer such that

       A1: a = ((2 * ( Parity b)) * c);

      (( 0 + ((2 * c) * ( Parity b))) div ( Parity b)) = (( 0 div ( Parity b)) + (2 * c)) by NAT_D: 61;

      hence thesis by A1;

    end;

    theorem :: NEWTON05:80

    for a,b be non zero Integer holds ( Parity a) > ( Parity b) iff (( Parity a) div ( Parity b)) is non zero even

    proof

      let a,b be non zero Integer;

      thus ( Parity a) > ( Parity b) implies (( Parity a) div ( Parity b)) is non zero even

      proof

        assume ( Parity a) > ( Parity b);

        then (2 * ( Parity b)) divides ( Parity a) by P2P;

        then

        consider c be Integer such that

         A1: ( Parity a) = ((2 * ( Parity b)) * c);

        (( 0 + ((2 * c) * ( Parity b))) div ( Parity b)) = (( 0 div ( Parity b)) + (2 * c)) by NAT_D: 61;

        hence thesis by A1;

      end;

      assume (( Parity a) div ( Parity b)) is non zero even;

      then

       B1: (( Parity b) * (( Parity a) div ( Parity b))) >= (2 * ( Parity b)) by NAT_D: 7, NEWTON02: 2;

      

       B2: (2 * ( Parity b)) > (1 * ( Parity b)) by XREAL_1: 68;

      ((( Parity b) * (( Parity a) div ( Parity b))) + (( Parity a) mod ( Parity b))) >= ((( Parity b) * (( Parity a) div ( Parity b))) + 0 ) by XREAL_1: 6;

      then ( Parity a) >= ((( Parity b) * (( Parity a) div ( Parity b))) + 0 ) by INT_1: 59;

      then ( Parity a) >= (2 * ( Parity b)) by B1, XXREAL_0: 2;

      hence thesis by B2, XXREAL_0: 2;

    end;

    theorem :: NEWTON05:81

    for a be odd Nat holds ( Parity (a - 1)) = (2 * ( Parity (a div 2)))

    proof

      let a be odd Nat;

      a = (((a div 2) * 2) + (a mod 2)) by INT_1: 59

      .= (((a div 2) * 2) + 1) by NAT_D: 12;

      then ( Parity (a - 1)) = (( Parity (a div 2)) * ( Parity 2)) by ILP;

      hence thesis;

    end;

    theorem :: NEWTON05:82

    

     MPA: for a,b be non zero Integer holds ( min (( Parity a),( Parity b))) divides a & ( min (( Parity a),( Parity b))) divides b

    proof

      let a,b be non zero Integer;

      ( min (( Parity a),( Parity b))) = ( Parity a) or ( min (( Parity a),( Parity b))) = ( Parity b) by XXREAL_0:def 9;

      then

       A1: ( min (( Parity a),( Parity b))) divides ( Parity a) & ( min (( Parity a),( Parity b))) divides ( Parity b) by XXREAL_0:def 9, PEPIN31;

      ( Parity a) divides a & ( Parity b) divides b by Th3;

      hence thesis by A1, INT_2: 9;

    end;

    registration

      let a,b be non zero Integer;

      cluster ((a + b) / ( min (( Parity a),( Parity b)))) -> integer;

      coherence

      proof

        ( min (( Parity a),( Parity b))) divides a & ( min (( Parity a),( Parity b))) divides b by MPA;

        hence thesis by Th1, WSIERP_1: 4;

      end;

    end

    registration

      let p be non square Integer;

      let n be odd Nat;

      cluster (p |^ n) -> non square;

      coherence

      proof

        per cases ;

          suppose p >= 0 ;

          then p in NAT by INT_1: 3;

          hence thesis;

        end;

          suppose p < 0 ;

          hence thesis;

        end;

      end;

    end

    registration

      let a be Integer;

      let n be even Nat;

      cluster (a |^ n) -> square;

      coherence

      proof

        reconsider k = |.a.| as Element of NAT by INT_1: 3;

        (k |^ n) = |.(a |^ n).| by TAYLOR_2: 1;

        hence thesis;

      end;

    end

    registration

      let p be prime Nat;

      let a be non zero square Integer;

      cluster (p |-count a) -> even;

      coherence

      proof

        reconsider a as non zero square Element of NAT by INT_1: 3;

         |.p.| > 1 by NEWTON03:def 1;

        then (p |^ (p |-count a)) divides a by NEWTON03:def 7;

        then

        consider k be Nat such that

         A0: a = ((p |^ (p |-count a)) * k) by NAT_D:def 3;

         not p divides k by A0, NEWTON03: 76;

        then not (k gcd p) = p by INT_2:def 2;

        then (k,p) are_coprime by PEPIN: 2;

        then

         A1: (k,(p |^ (p |-count a))) are_coprime by WSIERP_1: 10;

        assume

         A2: not thesis;

        

         A3: not (2 -root (p |^ (p |-count a))) in NAT

        proof

          assume not thesis;

          then ((2 -root (p |^ (p |-count a))) |^ 2) is square Nat;

          hence contradiction by A2;

        end;

         not ex c be Nat st (k * (p |^ (p |-count a))) = (c ^2 )

        proof

          assume not thesis;

          then

          consider c be Nat such that

           B1: (c ^2 ) = (k * (p |^ (p |-count a)));

          (k * (p |^ (p |-count a))) = (c |^ 2) by B1, NEWTON: 81;

          hence contradiction by NEWTON03: 14, A1, A3;

        end;

        hence contradiction by A0, PYTHTRIP:def 3;

      end;

    end

    registration

      let a be odd Integer;

      cluster (2 * a) -> non square;

      coherence

      proof

        per cases ;

          suppose a >= 0 ;

          then a in NAT by INT_1: 3;

          then

          reconsider a as odd Nat;

          

           A1: (a,2) are_coprime by NEWTON03:def 5;

           not ((2 -root 2) |^ 2) is square by INT_2: 28;

          then

           A2: not (2 -root 2) in NAT ;

           not ex c be Nat st (2 * a) = (c ^2 )

          proof

            assume not thesis;

            then

            consider c be Nat such that

             B1: (2 * a) = (c ^2 );

            (2 * a) = (c |^ 2) by B1, NEWTON: 81;

            hence contradiction by A1, A2, NEWTON03: 14;

          end;

          hence thesis by PYTHTRIP:def 3;

        end;

          suppose a < 0 ;

          hence thesis;

        end;

      end;

    end

    registration

      let a be square Integer;

      cluster ( Parity a) -> square;

      coherence

      proof

        per cases ;

          suppose a = 0 ;

          hence thesis by Def1;

        end;

          suppose a <> 0 ;

          then

          reconsider a as non zero Integer;

          ( Parity a) = (2 |^ (dwa |-count a)) by Def1;

          hence thesis;

        end;

      end;

      cluster ( Oddity a) -> square;

      coherence

      proof

        per cases ;

          suppose a = 0 ;

          hence thesis;

        end;

          suppose a <> 0 ;

          then

          reconsider a as non zero Integer;

          a = (( Parity a) * ( Oddity a));

          hence thesis;

        end;

      end;

    end

    registration

      let a be non zero square Integer;

      cluster (2 |-count a) -> even;

      coherence by INT_2: 28;

    end

    theorem :: NEWTON05:83

    

     MMD: for a,b be non negative Real holds (( max (a,b)) - ( min (a,b))) = |.(a - b).|

    proof

      let a,b be non negative Real;

      per cases ;

        suppose a >= b;

        then ( max (a,b)) = a & ( min (a,b)) = b by XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis;

      end;

        suppose a < b;

        then ( max (a,b)) = b & ( min (a,b)) = a by XXREAL_0:def 9, XXREAL_0:def 10;

        then |.(( max (a,b)) - ( min (a,b))).| = |.( - (b - a)).| by COMPLEX1: 52;

        hence thesis;

      end;

    end;

    theorem :: NEWTON05:84

    

     A4I: for a be even Integer st not 4 divides a holds a is non square

    proof

      let a be even Integer such that

       A1: not 4 divides a;

       not 2 divides (a / 2)

      proof

        assume not thesis;

        then (2 * 2) divides ((a / 2) * 2) by NEWTON02: 2;

        hence contradiction by A1;

      end;

      then

      reconsider b = (a / 2) as odd Integer by ABIAN:def 1;

      (2 * b) is non square;

      hence thesis;

    end;

    theorem :: NEWTON05:85

    for a,b be odd Integer holds (a - b) is square implies not (a + b) is square

    proof

      let a,b be odd Integer;

      assume (a - b) is square;

      then

      consider c be Nat such that

       A1: (c ^2 ) = (a - b) by PYTHTRIP:def 3;

      reconsider c as even Nat by A1;

      

       A2: |.a.| in NAT & |.b.| in NAT by INT_1: 3;

      then

      reconsider k = ( max ( |.a.|, |.b.|)) as odd Nat by XXREAL_0:def 10;

      reconsider l = ( min ( |.a.|, |.b.|)) as odd Nat by A2, XXREAL_0:def 9;

      

       A3: ( |.a.| + |.b.|) = (k + l) by NEWTON03: 41;

      2 divides c by ABIAN:def 1;

      then (2 * 2) divides (c * c) by NEWTON02: 2;

      then

       A5: (2 * 2) divides (c ^2 ) by SQUARE_1:def 1;

      per cases by ABS;

        suppose

         B1: |.(a + b).| = ( |.a.| + |.b.|);

        

        then

         B2: |.(a - b).| = |.( |.a.| - |.b.|).| by LABS

        .= (k - l) by MMD;

         not 4 divides ((k |^ 1) + (l |^ 1)) by A1, A5, B2, NEWTON03: 20;

        hence thesis by B1, A3, A4I;

      end;

        suppose

         B1: |.(a - b).| = ( |.a.| + |.b.|);

        

        then

         B2: |.(a + b).| = |.( |.a.| - |.b.|).| by LmABS

        .= (k - l) by MMD;

        4 divides ((k |^ 1) + (l |^ 1)) by B1, A1, NEWTON03: 41, A5;

        then not 4 divides (k - l) by NEWTON03: 20;

        hence thesis by B2, A4I;

      end;

    end;

    theorem :: NEWTON05:86

    for a,b be non zero Integer holds ( Parity (a + b)) = (( min (( Parity a),( Parity b))) * ( Parity ((a + b) / ( min (( Parity a),( Parity b))))))

    proof

      let a,b be non zero Integer;

      

       A1: ( min (( Parity a),( Parity b))) = ( Parity a) or ( min (( Parity a),( Parity b))) = ( Parity b) by XXREAL_0:def 9;

      ( min (( Parity a),( Parity b))) divides ( Parity a) by A1, XXREAL_0:def 9, PEPIN31;

      then

      consider c be Nat such that

       A2: ( Parity a) = (( min (( Parity a),( Parity b))) * c) by NAT_D:def 3;

      ( min (( Parity a),( Parity b))) divides ( Parity b) by A1, XXREAL_0:def 9, PEPIN31;

      then

      consider d be Nat such that

       A3: ( Parity b) = (( min (( Parity a),( Parity b))) * d) by NAT_D:def 3;

      (( Parity a) / ( min (( Parity a),( Parity b)))) = c & (( Parity b) / ( min (( Parity a),( Parity b)))) = d by A2, A3, XCMPLX_1: 89;

      then

       A4: (( Oddity a) * c) = (a / ( min (( Parity a),( Parity b)))) & (( Oddity b) * d) = (b / ( min (( Parity a),( Parity b)))) by XCMPLX_1: 98;

      (a + b) = ((( Oddity a) * (( min (( Parity a),( Parity b))) * c)) + (( Oddity b) * (( min (( Parity a),( Parity b))) * d))) by A2, A3

      .= (( min (( Parity a),( Parity b))) * ((( Oddity a) * c) + (( Oddity b) * d)));

      

      then ( Parity (a + b)) = (( Parity ( min (( Parity a),( Parity b)))) * ( Parity ((( Oddity a) * c) + (( Oddity b) * d)))) by ILP

      .= (( min (( Parity a),( Parity b))) * ( Parity ((( Oddity a) * c) + (( Oddity b) * d)))) by A1;

      hence thesis by A4, XCMPLX_1: 62;

    end;

    theorem :: NEWTON05:87

    

     OPC: for a,b be non zero Integer holds (( Parity a),( Oddity b)) are_coprime & (( Parity a) gcd ( Oddity b)) = 1

    proof

      let a,b be non zero Integer;

      (( Oddity b) gcd 2) = 1 by NEWTON03:def 5;

      then (( Oddity b) gcd (2 |^ (2 |-count a))) = 1 by WSIERP_1: 12;

      hence thesis by Def1;

    end;

    theorem :: NEWTON05:88

    

     OMO: for a be Integer holds |.( Oddity a).| = ( Oddity |.a.|)

    proof

      let a be Integer;

      per cases ;

        suppose a = 0 ;

        hence thesis;

      end;

        suppose a <> 0 ;

        then

        reconsider a as non zero Integer;

        ( |.( Oddity a).| * |.( Parity a).|) = |.(( Oddity a) * ( Parity a)).| by COMPLEX1: 65

        .= (( Oddity |.a.|) * ( Parity |.a.|))

        .= (( Oddity |.a.|) * |.( Parity a).|) by PMP;

        hence thesis by XCMPLX_1: 5;

      end;

    end;

    theorem :: NEWTON05:89

    for a,b be Integer holds (( Oddity a) gcd ( Oddity b)) = ( Oddity (a gcd b))

    proof

      let a,b be Integer;

      per cases ;

        suppose

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

        then

        reconsider a as non zero Integer;

        reconsider b as non zero Integer by A1;

        

         A2: ( Parity (( Oddity a) gcd ( Oddity b))) = (1 gcd 1) by NAT_2:def 1;

        ( Oddity (a gcd b)) = ( Oddity ((( Parity a) * ( Oddity a)) gcd (( Parity b) * ( Oddity b))))

        .= ( Oddity ((( Parity a) gcd (( Parity b) * ( Oddity b))) * (( Oddity a) gcd (( Parity b) * ( Oddity b))))) by OPC, NEWTON03: 35

        .= ( Oddity (((( Parity a) gcd ( Parity b)) * (( Parity a) gcd ( Oddity b))) * (( Oddity a) gcd (( Parity b) * ( Oddity b))))) by OPC, NEWTON03: 35

        .= ( Oddity (((( Parity a) gcd ( Parity b)) * 1) * (( Oddity a) gcd (( Parity b) * ( Oddity b))))) by OPC

        .= ( Oddity ((( Parity a) gcd ( Parity b)) * ((( Oddity a) gcd ( Parity b)) * (( Oddity a) gcd ( Oddity b))))) by OPC, NEWTON03: 35

        .= ( Oddity ((( Parity a) gcd ( Parity b)) * (1 * (( Oddity a) gcd ( Oddity b))))) by OPC

        .= (( Oddity (( Parity a) gcd ( Parity b))) * ( Oddity (( Oddity a) gcd ( Oddity b)))) by ILO

        .= (( Oddity ( Parity (a gcd b))) * ( Oddity (( Oddity a) gcd ( Oddity b)))) by PGG

        .= (1 * ( Oddity (( Oddity a) gcd ( Oddity b)))) by OPA;

        hence thesis by A2;

      end;

        suppose a = 0 ;

        then ( Oddity (a gcd b)) = ( Oddity |.b.|) & (( Oddity a) gcd ( Oddity b)) = |.( Oddity b).| by INT_2: 12, NEWTON02: 3;

        hence thesis by OMO;

      end;

        suppose b = 0 ;

        then ( Oddity (a gcd b)) = ( Oddity |.a.|) & (( Oddity a) gcd ( Oddity b)) = |.( Oddity a).| by INT_2: 12, NEWTON02: 3;

        hence thesis by OMO;

      end;

    end;

    theorem :: NEWTON05:90

    for a,b be non zero Integer holds (a gcd b) = ((( Parity a) gcd ( Parity b)) * (( Oddity a) gcd ( Oddity b)))

    proof

      let a,b be non zero Integer;

      (a gcd b) = ((( Parity a) * ( Oddity a)) gcd b)

      .= ((( Parity a) gcd (( Parity b) * ( Oddity b))) * (( Oddity a) gcd b)) by NEWTON03: 35, OPC

      .= (((( Parity a) gcd ( Parity b)) * (( Parity a) gcd ( Oddity b))) * (( Oddity a) gcd b)) by NEWTON03: 35, OPC

      .= (((( Parity a) gcd ( Parity b)) * 1) * (( Oddity a) gcd b)) by OPC

      .= ((( Parity a) gcd ( Parity b)) * (( Oddity a) gcd (( Parity b) * ( Oddity b))))

      .= ((( Parity a) gcd ( Parity b)) * ((( Oddity a) gcd ( Parity b)) * (( Oddity a) gcd ( Oddity b)))) by NEWTON03: 35, OPC

      .= ((( Parity a) gcd ( Parity b)) * (1 * (( Oddity a) gcd ( Oddity b)))) by OPC;

      hence thesis;

    end;

    theorem :: NEWTON05:91

    for a be odd Nat holds ( Parity (a + 1)) = 2 iff ( parity (a div 2)) = 0

    proof

      let a be odd Nat;

      a >= 1 by NAT_1: 14;

      per cases by XXREAL_0: 1;

        suppose

         B0: a = 1;

        ( parity (1 div (1 + 1))) = ( parity 0 );

        hence thesis by B0;

      end;

        suppose a > 1;

        then

        reconsider a as non trivial odd Nat by NAT_2:def 1;

        reconsider l = ((2 * 0 ) + 1) as odd Nat;

        

         L1: ( Parity (a + 1)) = 2 implies ( parity (a div 2)) = 0

        proof

          assume

           A1: ( Parity (a + 1)) = 2;

          per cases by PMG;

            suppose 2 = ( min (( Parity (l + 1)),( Parity (a - 1))));

            then ( Parity (a - 1)) > 2 by A1, PSD, XXREAL_0:def 9;

            then (2 |^ (2 |-count (a - 1))) > (2 |^ 1) by Def1;

            then (2 |-count (a - 1)) > 1 by PREPOWER: 93;

            then (2 |-count (a - 1)) >= (1 + 1) by NAT_1: 13;

            then (2 |^ 2) divides (a - 1) by NEWTON03: 59;

            then (2 * 2) divides (a - 1) by NEWTON: 81;

            

            then (((a - 1) div 4) * 4) = (a - 1) by NAT_D: 3

            .= ((((a div 2) * 2) + (a mod 2)) - 1) by INT_1: 59

            .= ((((a div 2) * 2) + 1) - 1) by NAT_D: 12;

            then (((a - 1) div 4) * 2) = (a div 2);

            hence thesis;

          end;

            suppose 2 >= (2 * ( Parity (l + 1)));

            hence thesis;

          end;

        end;

        ( parity (a div 2)) = 0 implies ( Parity (a + 1)) = 2

        proof

          assume ( parity (a div 2)) = 0 ;

          then

          reconsider k = (a div 2) as even Nat;

          (a + 1) = ((((a div 2) * 2) + (a mod 2)) + 1) by INT_1: 59

          .= ((((a div 2) * 2) + 1) + 1) by NAT_D: 12

          .= (2 * (k + 1));

          

          then ( Parity (a + 1)) = (( Parity 2) * ( Parity (k + 1))) by ILP

          .= (2 * 1);

          hence thesis;

        end;

        hence thesis by L1;

      end;

    end;

    theorem :: NEWTON05:92

    for a be even Integer holds (a div 2) = ((a + 1) div 2)

    proof

      let a be even Integer;

      ((((a + 1) div 2) * 2) + ((a + 1) mod 2)) = (a + 1) by INT_1: 59

      .= ((((a div 2) * 2) + (a mod 2)) + 1) by INT_1: 59

      .= (((a div 2) * 2) + ((a + 1) mod 2));

      hence thesis;

    end;

    theorem :: NEWTON05:93

    

     SAB: for a,b be Integer holds (a + b) = (((2 * ((a div 2) + (b div 2))) + ( parity a)) + ( parity b))

    proof

      let a,b be Integer;

      a = (((a div 2) * 2) + (a mod 2)) & b = (((b div 2) * 2) + (b mod 2)) by INT_1: 59;

      hence thesis;

    end;

    theorem :: NEWTON05:94

    

     SPA: for a,b be odd Integer holds ( Parity (a + b)) = (2 * ( Parity (((a div 2) + (b div 2)) + 1)))

    proof

      let a,b be odd Integer;

      ( parity a) = 1 & ( parity b) = 1 by NAT_2:def 1;

      

      then ( Parity (a + b)) = ( Parity (((2 * ((a div 2) + (b div 2))) + 1) + 1)) by SAB

      .= ( Parity (2 * (((a div 2) + (b div 2)) + 1)))

      .= (( Parity 2) * ( Parity (((a div 2) + (b div 2)) + 1))) by ILP;

      hence thesis;

    end;

    theorem :: NEWTON05:95

    

     PPD: for a,b be odd Integer holds ( Parity (a + b)) = 2 iff ( parity (a div 2)) = ( parity (b div 2))

    proof

      let a,b be odd Integer;

      thus ( Parity (a + b)) = 2 implies ( parity (a div 2)) = ( parity (b div 2))

      proof

        assume ( Parity (a + b)) = 2;

        then (2 * ( Parity (((a div 2) + (b div 2)) + 1))) = (2 * 1) by SPA;

        then ((a div 2) + (b div 2)) is even;

        hence thesis by EVP;

      end;

      assume ( parity (a div 2)) = ( parity (b div 2));

      then (a div 2) is odd iff (b div 2) is odd;

      then (2 * ( Parity (((a div 2) + (b div 2)) + 1))) = (2 * 1) by NAT_2:def 1;

      hence thesis by SPA;

    end;

    theorem :: NEWTON05:96

    

     PSU: for a,b be non zero Integer holds ( Parity (a + b)) = (( Parity a) + ( Parity b)) iff (( Parity a) = ( Parity b)) & ( parity (( Oddity a) div 2)) = ( parity (( Oddity b) div 2))

    proof

      let a,b be non zero Integer;

      thus ( Parity (a + b)) = (( Parity a) + ( Parity b)) implies (( Parity a) = ( Parity b)) & ( parity (( Oddity a) div 2)) = ( parity (( Oddity b) div 2))

      proof

        assume

         A1: ( Parity (a + b)) = (( Parity a) + ( Parity b));

        then

         A2: ( Parity a) = ( Parity b) by LEQ;

        

        then (2 * ( Parity a)) = ( Parity ((( Parity a) * ( Oddity a)) + (( Parity b) * ( Oddity b)))) by A1

        .= ( Parity (( Parity a) * (( Oddity a) + ( Oddity b)))) by A2

        .= (( Parity ( Parity a)) * ( Parity (( Oddity a) + ( Oddity b)))) by ILP

        .= (( Parity a) * ( Parity (( Oddity a) + ( Oddity b))));

        hence thesis by A1, LEQ, PPD, XCMPLX_1: 5;

      end;

      assume

       A1: (( Parity a) = ( Parity b)) & ( parity (( Oddity a) div 2)) = ( parity (( Oddity b) div 2));

      ( Parity (a + b)) = ( Parity ((( Parity a) * ( Oddity a)) + (( Parity b) * ( Oddity b))))

      .= ( Parity (( Parity a) * (( Oddity a) + ( Oddity b)))) by A1

      .= (( Parity ( Parity a)) * ( Parity (( Oddity a) + ( Oddity b)))) by ILP

      .= (2 * ( Parity a)) by A1, PPD;

      hence thesis by A1;

    end;

    theorem :: NEWTON05:97

    for a,b be non zero Integer st (a + b) <> 0 & ( Parity a) = ( Parity b) & ( parity (( Oddity a) div 2)) <> ( parity (( Oddity b) div 2)) holds ( Parity (a + b)) > (( Parity a) + ( Parity b))

    proof

      let a,b be non zero Integer such that

       A1: (a + b) <> 0 & ( Parity a) = ( Parity b) & ( parity (( Oddity a) div 2)) <> ( parity (( Oddity b) div 2));

      

       A2: ( Parity (a + b)) >= (( Parity a) + ( Parity b)) by A1, PEQ;

      ( Parity (a + b)) <> (( Parity a) + ( Parity b)) by A1, PSU;

      hence thesis by A2, XXREAL_0: 1;

    end;