environ

vocabularies INTEGRA1, NUMBERS, ARYTM_1, CARD_1, FUNCT_1, ARYTM_3, XXREAL_0,
  XREAL_0, ORDINAL1, POWER, RELAT_1, SIN_COS, XXREAL_1, PREPOWER, ORDINAL4,
  SUBSET_1, INTEGRA5, SEQ_4, NEWTON;
notations NUMBERS, XXREAL_0, SQUARE_1, INTEGRA5, TAYLOR_1, XREAL_0, ORDINAL1,
  FUNCT_1, FUNCT_2, POWER, XCMPLX_0, SIN_COS, XXREAL_1, PREPOWER, IRRAT_1,
  SUBSET_1, SEQ_4, NEWTON;
constructors TAYLOR_1, SQUARE_1, INTEGRA5, POWER, NEWTON, SIN_COS, SEQ_1,
  PREPOWER, REAL_1, SEQ_4, RCOMP_1;
registrations MEMBERED, VALUED_0, RELSET_1, XREAL_0, SIN_COS, XXREAL_0, INT_1,
  XBOOLE_0, NUMBERS, NAT_1, XXREAL_1, NEWTON;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
theorems XXREAL_0, XREAL_1, TAYLOR_1, SIN_COS,  POWER, FUNCT_2, INTEGRA5,
  INTEGRA9, ORDINAL1, JORDAN5A, XCMPLX_1;

begin

reserve n for natural number;
reserve x,y,t,a,b for real number;
reserve f for Function of REAL,REAL;

Lm1:
  x > 0 implies exp_R x > 1
proof
A1: number_e > 1 by TAYLOR_1:11,XXREAL_0:2;
  assume
A2: x > 0;
  then exp_R.x >= 1 by SIN_COS:52;
  then
A3: exp_R x >= 1 by SIN_COS:def 23;
  log(number_e,1) = 0 by A1,POWER:51;
  then exp_R x <> 1 by A2,TAYLOR_1:12;
  hence thesis by A3,XXREAL_0:1;
end;

theorem Th1:
  x < y implies exp_R x < exp_R y
proof
  assume x < y;
  then y - x > 0 & x + (y - x) = y by XREAL_1:50;
  then  exp_R x > 0 & exp_R (y - x) > 1 & exp_R x * exp_R (y - x) = exp_R y
    by Lm1,SIN_COS:50,SIN_COS:55;
  then exp_R x * 1 < exp_R y by XREAL_1:68;
  hence thesis;
end;

theorem Th2:
  (for t holds f.t = t^n) implies
    integral(f,a,b) = b^(n + 1)/(n + 1) - a^(n + 1)/(n + 1)
proof
  reconsider nn = n as Element of NAT by ORDINAL1:def 12;
  assume
A1: for t holds f.t = t^n;
  now
    let t be Element of REAL;
    thus f.t = t^n by A1
      .= t #Z n by POWER:43
      .= ( #Z n).t by TAYLOR_1:def 1;
  end;
  then
A2: f = #Z n by FUNCT_2:def 7;
A3: ((1/(n + 1))*(b|^(n + 1))) - ((1/(n + 1))*(a|^(n + 1)))
     = ((1/(n + 1))*(b^(n + 1))) - ((1/(n + 1))*(a|^(n + 1))) by POWER:41
    .= ((1/(n + 1))*(b^(n + 1))) - ((1/(n + 1))*(a^(n + 1))) by POWER:41
    .= (b^(n + 1))/(n + 1) - ((1/(n + 1))*(a^(n + 1))) by XCMPLX_1:99
    .= (b^(n + 1))/(n + 1) - (a^(n + 1))/(n + 1) by XCMPLX_1:99;
  per cases;
  suppose
A4:   a <= b;
A5:  ['a,b'] = [.a,b.] & lower_bound [.a,b.] = a & upper_bound [.a,b.] = b
      by A4,INTEGRA5:def 3,JORDAN5A:19;
    integral(f,a,b) = integral( #Z nn,['a,b']) by A2,A4,INTEGRA5:def 4
      .= ((1/(n + 1))*(b|^(n + 1))) - ((1/(n + 1))*(a|^(n + 1)))
        by A5,INTEGRA9:19;
    hence thesis by A3;
  end;
  suppose
A6:   b < a;
A7:  ['b,a'] = [.b,a.] & lower_bound [.b,a.] = b & upper_bound [.b,a.] = a
      by A6,INTEGRA5:def 3,JORDAN5A:19;
    integral(f,a,b) = -integral( #Z nn,['b,a']) by A2,A6,INTEGRA5:def 4
      .= -(((1/(n + 1))*(a|^(n + 1))) - ((1/(n + 1))*(b|^(n + 1))))
        by A7,INTEGRA9:19;
    hence thesis by A3;
  end;
end;