UWB Informatyka - Nieoficjalne Forum Studentów

::::::::::::::::::::::::::::::::::::::::::::::::::::
scheme Sch1{P[Nat]}:
    for n holds P[n]
provided
  A1:P[0] and
  A2:P[1] and
  A3:for n st n>=1 & P[n] holds P[n+1]
proof
A4: for n st P[n] holds P[n+1]
proof
   let n such that A5: P[n];
   n=0 or n>=1 by NAT_1: 14;
   hence thesis by A2,A3,A5;
end;
for n holds  P[n]  from NAT_1: sch 2(A1,A4);
hence thesis;
end;

scheme
    NatInd2 { P[Nat] } : for k being non empty Nat holds P[k]
    provided
      E: P[1] and
      D1: for k be non empty Nat st P[k] holds P[k + 1]
  proof
    defpred Q[Nat] means $1 is non empty implies P[$1];
    A: Q[0];
    B: for i be Nat st Q[i] holds Q[i+1]
      proof
        let i be Nat such that C1: Q[i];
        i is non empty implies P[i] by C1;
        per cases;
          suppose i is non empty;
            hence thesis by D1,C1;
          end;
          suppose i is empty;
            hence thesis by E;
          end;
      end;
    for i be Nat holds Q[i] from NAT_1:sch 2 (A,B);
    hence thesis;
  end;

lm1: for n  st n>=1 holds 2*n>=n+1
proof
defpred P[Nat] means 2*$1 >= $1 +1;
A: P[1];
B: for i be non empty  Nat st P[i] holds P[i + 1]
proof
let n be non empty Nat;
assume C1: P[n]; ::czyli 2*n>=n+1;
then 2*n+1 >=n+1 by NAT_1:12;   ::Jezeli a>=b to a+1>=b
then 2*n+1+1>= n+1+1 by XREAL_1:8; :: Jezeli a>=b to a+1>=b+1
hence thesis;
end;
for k being non empty Nat holds P[k] from   NatInd2(A,B);
hence thesis;
end;

theorem
2|^n >= n
proof
defpred P[Nat] means 2|^$1>=$1;
A: P[0];
2|^1=2 by  NEWTON: 10;
then B: P[1] ;
C: for n st n>=1 & P[n] holds P[n+1]
proof
let n such that C1: n>=1 & P[n];
2|^n>=n by C1;                                        :: z zalozenia wiemy, ze to zachodzi;
then 2* 2|^n >=2*n by NAT_1:4; :               :Jezeli a>=b to c*a>=c*b;
then 2|^(n+1)>= 2*n by NEWTON:11;
then 2|^(n+1)>= 2*n & 2*n>=n+1 by C1,lm1 ; ::wziete z wczesniej
:: udowodnionego
hence thesis by XXREAL_0:2;                     ::Jezeli a>=b & b>=c to a>=c
end;
for n holds P[n] from Sch1(A,B,C);
hence thesis;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem
for n  holds 4|^n>=2|^n;

::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem
  9 divides 10 |^ n - 1;
proof
  defpred Q[Nat] means 9 divides 10|^$1 -1;
  p1: Q[0]
  proof
    n: 10|^0 = 1 by NEWTON:9;
    10|^0 - 1 = 0 by n .= 1-1 .= 9*0;
    hence thesis by INT_1: def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: 10|^n-1 = 9*i by a1, INT_1:def 9;
    10|^(n+1) -1 = 10*10|^n -1 by NEWTON: 11
    .= 10*(10|^n-1) + 9
    .= 10*9*i + 9 by z
    .= 9*(10*i + 1);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem
  9 divides 4 |^ n + 15 * n - 1;
proof
  defpred Q[Nat] means 9 divides 4|^$1 + 15*$1 -1;
  p1: Q[0]
  proof
    4|^0 = 1 by NEWTON:9;
    then 4|^0 + 15*0 -1 = 0 .= 9*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: 4|^n + 15*n -1 = 9*i by a1, INT_1:def 9;
    4|^(n+1) + 15*(n+1) -1
    = 4*4|^n + 15*(n+1) -1 by NEWTON: 11
    .= 4*4|^n + 15*n + 14
    .= 4*(4|^n + 15*n - 1) - 3*15*n + 18
    .= 4*9*i - 3*15*n + 18 by z
    .= 9*(4*i - 5*n +2);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;


::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem
  6 divides n |^ 3 - n;

::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem
  6 divides n |^ 3 + 5 * n;
proof
  defpred Q[Nat] means 6 divides $1|^3 + 5*$1;
  p1: Q[0]
  proof
    0|^3 = 0 by NEWTON: 16;
    then 0|^3 + 5*0 = 0 .= 6*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    s1: n|^2 = n|^(1+1) .= n*n|^1 by NEWTON:11 .=n*n by NEWTON:10;
    s2: 2 divides n*(n+1) by Th1;
    consider i being Integer such that z: n|^3 + 5*n = 6*i by a1, INT_1:def 9;
    consider j being Integer such that x: n*(n + 1) = 2*j by s2, INT_1:def 9;
    (n+1)|^3 + 5*(n+1)
    = n|^3 + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5*(n+1) by SERIES_4: 2
    .= n|^3 + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5*n + 5
    .= (n|^3 + 5*n) + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5
    .= 6*i + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5 by z
    .= 6*i + 3*n|^2 + 3*1|^2*n + 1 + 5 by NEWTON: 15
    .= 6*i + 3*n|^2 + 3*1*n + 1 + 5 by NEWTON: 15
    .= 6*i + 3*n|^2 + 3*n + 6
    .= 6*i + 3*n*n + 3*n + 6 by s1
    .= 6*i + 3*n*(n + 1) + 6
    .= 6*i + 3*2*j +6 by x
    .= 6*(i + j + 1);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::::::::::::::
powinno działać niech ktoś sprawdzi

Ostatnio edytowany przez Darrjus (2009-11-15 12:46:48)