:: TAYLOR_1 semantic presentation begin definition let q be Integer; func #Z q -> Function of REAL,REAL means :Def1: :: TAYLOR_1:def 1 for x being real number holds it . x = x #Z q; existence ex b1 being Function of REAL,REAL st for x being real number holds b1 . x = x #Z q proof deffunc H1( Real) -> Element of REAL = \$1 #Z q; consider f being Function of REAL,REAL such that A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4(); take f ; ::_thesis: for x being real number holds f . x = x #Z q let d be real number ; ::_thesis: f . d = d #Z q d is Real by XREAL_0:def_1; hence f . d = d #Z q by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of REAL,REAL st ( for x being real number holds b1 . x = x #Z q ) & ( for x being real number holds b2 . x = x #Z q ) holds b1 = b2 proof let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for x being real number holds f1 . x = x #Z q ) & ( for x being real number holds f2 . x = x #Z q ) implies f1 = f2 ) assume that A2: for d being real number holds f1 . d = d #Z q and A3: for d being real number holds f2 . d = d #Z q ; ::_thesis: f1 = f2 for d being Element of REAL holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: f1 . d = f2 . d thus f1 . d = d #Z q by A2 .= f2 . d by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines #Z TAYLOR_1:def_1_:_ for q being Integer for b2 being Function of REAL,REAL holds ( b2 = #Z q iff for x being real number holds b2 . x = x #Z q ); theorem Th1: :: TAYLOR_1:1 for x being real number for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m) proof let x be real number ; ::_thesis: for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m) let m, n be Nat; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m) percases ( x <> 0 or x = 0 ) ; suppose x <> 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m) hence x #Z (n + m) = (x #Z n) * (x #Z m) by PREPOWER:44; ::_thesis: verum end; supposeA1: x = 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m) thus x #Z (n + m) = (x #Z n) * (x #Z m) ::_thesis: verum proof A2: 0 #Z (n + m) = 0 |^ (abs (n + m)) by PREPOWER:def_3 .= 0 |^ (n + m) by ABSVALUE:def_1 .= (0 |^ n) * (0 |^ m) by NEWTON:8 ; percases ( ( n = 0 & m = 0 ) or n <> 0 or m <> 0 ) ; supposeA3: ( n = 0 & m = 0 ) ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m) x #Z (0 + 0) = 1 * (x #Z 0) .= (x #Z 0) * (x #Z 0) by PREPOWER:34 ; hence x #Z (n + m) = (x #Z n) * (x #Z m) by A3; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m) then A4: 0 + 1 <= n by NAT_1:13; A5: (0 #Z n) * (0 #Z m) = (0 |^ (abs n)) * (0 #Z m) by PREPOWER:def_3 .= (0 |^ n) * (0 #Z m) by ABSVALUE:def_1 .= 0 * (0 #Z m) by A4, NEWTON:11 ; 0 #Z (n + m) = 0 * (0 |^ m) by A2, A4, NEWTON:11; hence x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A5; ::_thesis: verum end; suppose m <> 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m) then A6: 0 + 1 <= m by NAT_1:13; A7: (0 #Z n) * (0 #Z m) = (0 |^ (abs m)) * (0 #Z n) by PREPOWER:def_3 .= (0 |^ m) * (0 #Z n) by ABSVALUE:def_1 .= 0 * (0 #Z n) by A6, NEWTON:11 ; 0 #Z (n + m) = 0 * (0 |^ n) by A2, A6, NEWTON:11; hence x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A7; ::_thesis: verum end; end; end; end; end; end; theorem Th2: :: TAYLOR_1:2 for n being Nat for x being real number holds ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) proof let n be Nat; ::_thesis: for x being real number holds ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) let x be real number ; ::_thesis: ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) defpred S1[ Nat] means for x being real number holds ( #Z \$1 is_differentiable_in x & diff ((#Z \$1),x) = \$1 * (x #Z (\$1 - 1)) ); A1: for k being Nat st S1[k] holds S1[k + 1] proof A2: now__::_thesis:_for_x_being_Real_st_x_in_REAL_holds_ (#Z_1)_._x_=_(1_*_x)_+_0 let x be Real; ::_thesis: ( x in REAL implies (#Z 1) . x = (1 * x) + 0 ) assume x in REAL ; ::_thesis: (#Z 1) . x = (1 * x) + 0 thus (#Z 1) . x = x #Z 1 by Def1 .= (1 * x) + 0 by PREPOWER:35 ; ::_thesis: verum end; A3: [#] REAL is open Subset of REAL ; A4: REAL c= dom (#Z 1) by FUNCT_2:def_1; then A5: #Z 1 is_differentiable_on REAL by A2, A3, FDIFF_1:23; A6: for x being real number holds ( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 ) proof let x be real number ; ::_thesis: ( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 ) A7: x is Real by XREAL_0:def_1; hence #Z 1 is_differentiable_in x by A3, A5, FDIFF_1:9; ::_thesis: diff ((#Z 1),x) = 1 thus diff ((#Z 1),x) = ((#Z 1) `| REAL) . x by A5, A7, FDIFF_1:def_7 .= 1 by A2, A4, A3, A7, FDIFF_1:23 ; ::_thesis: verum end; let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_(_k_=_0_&_S1[k_+_1]_)_or_(_k_<>_0_&_(_for_x_being_real_number_holds_ (_#Z_(k_+_1)_is_differentiable_in_x_&_diff_((#Z_(k_+_1)),x)_=_(k_+_1)_*_(x_#Z_((k_+_1)_-_1))_)_)_)_) percases ( k = 0 or k <> 0 ) ; caseA9: k = 0 ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let x be real number ; ::_thesis: ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) ) thus #Z (k + 1) is_differentiable_in x by A6, A9; ::_thesis: diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) thus diff ((#Z (k + 1)),x) = 1 by A6, A9 .= (k + 1) * (x #Z ((k + 1) - 1)) by A9, PREPOWER:34 ; ::_thesis: verum end; end; case k <> 0 ; ::_thesis: for x being real number holds ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) ) then 1 <= k by NAT_1:14; then 1 - 1 <= k - 1 by XREAL_1:13; then reconsider k1 = k - 1 as Element of NAT by INT_1:3; let x be real number ; ::_thesis: ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) ) A10: REAL = dom (#Z (k + 1)) by FUNCT_2:def_1; A11: ( x is Real & #Z k is_differentiable_in x ) by A8, XREAL_0:def_1; A12: for x being set st x in dom (#Z (k + 1)) holds (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x) proof let x be set ; ::_thesis: ( x in dom (#Z (k + 1)) implies (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x) ) assume x in dom (#Z (k + 1)) ; ::_thesis: (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x) then reconsider x1 = x as Real ; thus (#Z (k + 1)) . x = x1 #Z (k + 1) by Def1 .= (x1 #Z k) * (x1 #Z 1) by Th1 .= ((#Z k) . x) * (x1 #Z 1) by Def1 .= ((#Z k) . x) * ((#Z 1) . x) by Def1 ; ::_thesis: verum end; A13: #Z 1 is_differentiable_in x by A6; A14: (dom (#Z k)) /\ (dom (#Z 1)) = ([#] REAL) /\ (dom (#Z 1)) by FUNCT_2:def_1 .= ([#] REAL) /\ REAL by FUNCT_2:def_1 ; then #Z (k + 1) = (#Z k) (#) (#Z 1) by A10, A12, VALUED_1:def_4; hence #Z (k + 1) is_differentiable_in x by A11, A13, FDIFF_1:16; ::_thesis: diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) thus diff ((#Z (k + 1)),x) = diff (((#Z k) (#) (#Z 1)),x) by A14, A10, A12, VALUED_1:def_4 .= (((#Z k) . x) * (diff ((#Z 1),x))) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by A11, A13, FDIFF_1:16 .= (((#Z k) . x) * 1) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by A6 .= ((x #Z k) * 1) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by Def1 .= ((x #Z k) * 1) + ((diff ((#Z k),x)) * (x #Z 1)) by Def1 .= (x #Z k) + ((k * (x #Z k1)) * (x #Z 1)) by A8 .= (x #Z k) + (k * ((x #Z k1) * (x #Z 1))) .= (x #Z k) + (k * (x #Z (k1 + 1))) by Th1 .= (k + 1) * (x #Z ((k + 1) - 1)) ; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A15: S1[ 0 ] proof let x be real number ; ::_thesis: ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) ) set f = #Z 0; now__::_thesis:_for_y_being_set_st_y_in_{1}_holds_ y_in_rng_(#Z_0) dom (#Z 0) = REAL by FUNCT_2:def_1; then consider x being set such that A16: x in dom (#Z 0) ; reconsider x1 = x as Real by A16; let y be set ; ::_thesis: ( y in {1} implies y in rng (#Z 0) ) assume A17: y in {1} ; ::_thesis: y in rng (#Z 0) (#Z 0) . x = x1 #Z 0 by Def1 .= 1 by PREPOWER:34 .= y by A17, TARSKI:def_1 ; hence y in rng (#Z 0) by A16, FUNCT_1:def_3; ::_thesis: verum end; then A18: {1} c= rng (#Z 0) by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_rng_(#Z_0)_holds_ y_in_{1} let y be set ; ::_thesis: ( y in rng (#Z 0) implies y in {1} ) assume y in rng (#Z 0) ; ::_thesis: y in {1} then consider x being set such that A19: x in dom (#Z 0) and A20: y = (#Z 0) . x by FUNCT_1:def_3; reconsider x = x as Real by A19; (#Z 0) . x = x #Z 0 by Def1 .= 1 by PREPOWER:34 ; hence y in {1} by A20, TARSKI:def_1; ::_thesis: verum end; then rng (#Z 0) c= {1} by TARSKI:def_3; then A21: rng (#Z 0) = {1} by A18, XBOOLE_0:def_10; A22: dom (#Z 0) = [#] REAL by FUNCT_2:def_1; then A23: #Z 0 is_differentiable_on dom (#Z 0) by A21, FDIFF_1:11; A24: x is Real by XREAL_0:def_1; then ((#Z 0) `| (dom (#Z 0))) . x = 0 by A21, A22, FDIFF_1:11; hence ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) ) by A24, A23, A22, FDIFF_1:9, FDIFF_1:def_7; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A15, A1); hence ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) ; ::_thesis: verum end; theorem :: TAYLOR_1:3 for n being Nat for x0 being real number for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) proof let n be Nat; ::_thesis: for x0 being real number for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 implies ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) ) assume A1: f is_differentiable_in x0 ; ::_thesis: ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) A2: ( #Z n is_differentiable_in f . x0 & x0 is Real ) by Th2, XREAL_0:def_1; hence (#Z n) * f is_differentiable_in x0 by A1, FDIFF_2:13; ::_thesis: diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) thus diff (((#Z n) * f),x0) = (diff ((#Z n),(f . x0))) * (diff (f,x0)) by A1, A2, FDIFF_2:13 .= (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) by Th2 ; ::_thesis: verum end; Lm1: for n being Nat for x being real number holds (exp_R x) #R n = exp_R (n * x) proof let n be Nat; ::_thesis: for x being real number holds (exp_R x) #R n = exp_R (n * x) let x be real number ; ::_thesis: (exp_R x) #R n = exp_R (n * x) reconsider x = x as Real by XREAL_0:def_1; defpred S1[ Nat] means (exp_R x) #R \$1 = exp_R (\$1 * x); A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] reconsider k1 = k as Element of NAT by ORDINAL1:def_12; thus (exp_R x) #R (k + 1) = ((exp_R x) #R k) * ((exp_R x) #R 1) by PREPOWER:75, SIN_COS:55 .= ((exp_R x) #R k) * (exp_R x) by PREPOWER:72, SIN_COS:55 .= exp_R ((k1 * x) + x) by A2, SIN_COS:50 .= exp_R ((k + 1) * x) ; ::_thesis: verum end; A3: S1[ 0 ] by PREPOWER:71, SIN_COS:51, SIN_COS:55; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence (exp_R x) #R n = exp_R (n * x) ; ::_thesis: verum end; theorem Th4: :: TAYLOR_1:4 for x being real number holds exp_R (- x) = 1 / (exp_R x) proof let x be real number ; ::_thesis: exp_R (- x) = 1 / (exp_R x) reconsider x = x as Real by XREAL_0:def_1; (exp_R (- x)) * (exp_R x) = exp_R ((- x) + x) by SIN_COS:50 .= 1 by SIN_COS:51 ; hence exp_R (- x) = 1 / (exp_R x) by XCMPLX_1:73; ::_thesis: verum end; Lm2: for i being Integer for x being real number holds (exp_R x) #R i = exp_R (i * x) proof let i be Integer; ::_thesis: for x being real number holds (exp_R x) #R i = exp_R (i * x) let x be real number ; ::_thesis: (exp_R x) #R i = exp_R (i * x) consider n being Element of NAT such that A1: ( i = n or i = - n ) by INT_1:2; now__::_thesis:_(_(_i_=_n_&_(exp_R_x)_#R_i_=_exp_R_(i_*_x)_)_or_(_i_=_-_n_&_exp_R_(i_*_x)_=_(exp_R_x)_#R_i_)_) percases ( i = n or i = - n ) by A1; case i = n ; ::_thesis: (exp_R x) #R i = exp_R (i * x) hence (exp_R x) #R i = exp_R (i * x) by Lm1; ::_thesis: verum end; caseA2: i = - n ; ::_thesis: exp_R (i * x) = (exp_R x) #R i hence exp_R (i * x) = exp_R (- (n * x)) .= 1 / (exp_R (n * x)) by Th4 .= 1 / ((exp_R x) #R n) by Lm1 .= (exp_R x) #R i by A2, PREPOWER:76, SIN_COS:55 ; ::_thesis: verum end; end; end; hence (exp_R x) #R i = exp_R (i * x) ; ::_thesis: verum end; theorem Th5: :: TAYLOR_1:5 for i being Integer for x being real number holds (exp_R x) #R (1 / i) = exp_R (x / i) proof let i be Integer; ::_thesis: for x being real number holds (exp_R x) #R (1 / i) = exp_R (x / i) let x be real number ; ::_thesis: (exp_R x) #R (1 / i) = exp_R (x / i) set n = i; percases ( i <> 0 or i = 0 ) ; supposeA1: i <> 0 ; ::_thesis: (exp_R x) #R (1 / i) = exp_R (x / i) then exp_R x = exp_R ((x / i) * i) by XCMPLX_1:87 .= (exp_R (x / i)) #R i by Lm2 ; hence (exp_R x) #R (1 / i) = (exp_R (x / i)) #R (i * (1 / i)) by PREPOWER:91, SIN_COS:55 .= (exp_R (x / i)) #R 1 by A1, XCMPLX_1:106 .= exp_R (x / i) by PREPOWER:72, SIN_COS:55 ; ::_thesis: verum end; supposeA2: i = 0 ; ::_thesis: (exp_R x) #R (1 / i) = exp_R (x / i) (exp_R x) #R (1 / 0) = exp_R 0 by PREPOWER:71, SIN_COS:51, SIN_COS:55 .= exp_R (x / 0) by XCMPLX_1:49 ; hence (exp_R x) #R (1 / i) = exp_R (x / i) by A2; ::_thesis: verum end; end; end; theorem Th6: :: TAYLOR_1:6 for x being real number for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x) proof let x be real number ; ::_thesis: for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x) let m, n be Integer; ::_thesis: (exp_R x) #R (m / n) = exp_R ((m / n) * x) thus exp_R ((m / n) * x) = exp_R ((x / n) * m) by XCMPLX_1:75 .= (exp_R (x / n)) #R m by Lm2 .= ((exp_R x) #R (1 / n)) #R m by Th5 .= (exp_R x) #R ((1 / n) * m) by PREPOWER:91, SIN_COS:55 .= (exp_R x) #R ((m / n) * 1) by XCMPLX_1:75 .= (exp_R x) #R (m / n) ; ::_thesis: verum end; Lm3: for x being real number for q being Rational holds (exp_R x) #R q = exp_R (q * x) proof let x be real number ; ::_thesis: for q being Rational holds (exp_R x) #R q = exp_R (q * x) let q be Rational; ::_thesis: (exp_R x) #R q = exp_R (q * x) ex m being Integer ex n being Element of NAT st ( n <> 0 & q = m / n ) by RAT_1:8; hence (exp_R x) #R q = exp_R (q * x) by Th6; ::_thesis: verum end; theorem Th7: :: TAYLOR_1:7 for x being real number for q being Rational holds (exp_R x) #Q q = exp_R (q * x) proof let x be real number ; ::_thesis: for q being Rational holds (exp_R x) #Q q = exp_R (q * x) let q be Rational; ::_thesis: (exp_R x) #Q q = exp_R (q * x) thus (exp_R x) #Q q = (exp_R x) #R q by PREPOWER:74, SIN_COS:55 .= exp_R (q * x) by Lm3 ; ::_thesis: verum end; theorem Th8: :: TAYLOR_1:8 for x, p being real number holds (exp_R x) #R p = exp_R (p * x) proof let x, p be real number ; ::_thesis: (exp_R x) #R p = exp_R (p * x) exp_R x > 0 by SIN_COS:55; then consider s being Rational_Sequence such that A1: ( s is convergent & lim s = p ) and (exp_R x) #Q s is convergent and A2: lim ((exp_R x) #Q s) = (exp_R x) #R p by PREPOWER:def_7; A3: ( exp_R is_continuous_in x * p & rng (x (#) s) c= dom exp_R ) by FDIFF_1:24, SIN_COS:47, SIN_COS:65; A4: now__::_thesis:_for_ii_being_set_st_ii_in_NAT_holds_ ((exp_R_x)_#Q_s)_._ii_=_(exp_R_/*_(x_(#)_s))_._ii let ii be set ; ::_thesis: ( ii in NAT implies ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii ) assume ii in NAT ; ::_thesis: ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii then reconsider i = ii as Element of NAT ; A5: rng (x (#) s) c= dom exp_R by SIN_COS:47; thus ((exp_R x) #Q s) . ii = (exp_R x) #Q (s . i) by PREPOWER:def_6 .= exp_R ((s . i) * x) by Th7 .= exp_R ((x (#) s) . i) by SEQ_1:9 .= exp_R . ((x (#) s) . i) by SIN_COS:def_23 .= (exp_R /* (x (#) s)) . ii by A5, FUNCT_2:108 ; ::_thesis: verum end; ( x (#) s is convergent & lim (x (#) s) = x * p ) by A1, SEQ_2:7, SEQ_2:8; then lim (exp_R /* (x (#) s)) = exp_R . (x * p) by A3, FCONT_1:def_1 .= exp_R (p * x) by SIN_COS:def_23 ; hence (exp_R x) #R p = exp_R (p * x) by A2, A4, FUNCT_2:12; ::_thesis: verum end; theorem Th9: :: TAYLOR_1:9 for x being real number holds ( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x ) proof let x be real number ; ::_thesis: ( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x ) thus A1: exp_R x = exp_R (x * 1) .= (exp_R 1) #R x by Th8 ; ::_thesis: ( (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x ) exp_R 1 > 0 by SIN_COS:55; hence ( (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x ) by A1, IRRAT_1:def_7, POWER:def_2; ::_thesis: verum end; theorem :: TAYLOR_1:10 for x being real number holds ( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x ) proof let x be real number ; ::_thesis: ( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x ) thus (exp_R . 1) #R x = (exp_R 1) #R x by SIN_COS:def_23 .= exp_R x by Th9 .= exp_R . x by SIN_COS:def_23 ; ::_thesis: ( (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x ) thus (exp_R . 1) to_power x = (exp_R 1) to_power x by SIN_COS:def_23 .= exp_R x by Th9 .= exp_R . x by SIN_COS:def_23 ; ::_thesis: ( number_e to_power x = exp_R . x & number_e #R x = exp_R . x ) thus number_e to_power x = exp_R x by Th9 .= exp_R . x by SIN_COS:def_23 ; ::_thesis: number_e #R x = exp_R . x thus number_e #R x = exp_R x by Th9 .= exp_R . x by SIN_COS:def_23 ; ::_thesis: verum end; theorem :: TAYLOR_1:11 number_e > 2 proof A1: number_e is irrational by IRRAT_1:41; A2: for th, th1, th2, th3 being real number for n being Element of NAT holds ( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) proof let th, th1, th2, th3 be real number ; ::_thesis: for n being Element of NAT holds ( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) let n be Element of NAT ; ::_thesis: ( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) thus th |^ 0 = (th GeoSeq) . 0 by PREPOWER:def_1 .= 1 by PREPOWER:3 ; ::_thesis: ( th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) thus th |^ (2 * n) = (th |^ n) |^ 2 by NEWTON:9; ::_thesis: ( th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) thus A3: th |^ 1 = (th GeoSeq) . (0 + 1) by PREPOWER:def_1 .= ((th GeoSeq) . 0) * th by PREPOWER:3 .= 1 * th by PREPOWER:3 .= th ; ::_thesis: ( th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) thus th |^ 2 = th |^ (1 + 1) .= th * th by A3, NEWTON:8 ; ::_thesis: ( (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) thus A4: (- 1) |^ (2 * n) = 1 |^ (2 * n) by POWER:1 .= 1 by NEWTON:10 ; ::_thesis: (- 1) |^ ((2 * n) + 1) = - 1 thus (- 1) |^ ((2 * n) + 1) = ((- 1) |^ (2 * n)) * (- 1) by NEWTON:6 .= - 1 by A4 ; ::_thesis: verum end; A5: for n being Element of NAT st 1 <= n holds (Partial_Sums (1 rExpSeq)) . n >= 2 proof defpred S1[ Integer] means (Partial_Sums (1 rExpSeq)) . \$1 >= 2; A6: for ni being Integer st 1 <= ni & S1[ni] holds S1[ni + 1] proof let ni be Integer; ::_thesis: ( 1 <= ni & S1[ni] implies S1[ni + 1] ) assume 1 <= ni ; ::_thesis: ( not S1[ni] or S1[ni + 1] ) then reconsider n = ni as Element of NAT by INT_1:3; A7: (Partial_Sums (1 rExpSeq)) . (n + 1) = ((Partial_Sums (1 rExpSeq)) . n) + ((1 rExpSeq) . (n + 1)) by SERIES_1:def_1 .= ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) by SIN_COS:def_5 ; ( 1 |^ (n + 1) > 0 & (n + 1) ! > 0 ) by PREPOWER:6; then A8: ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) > (Partial_Sums (1 rExpSeq)) . n by XREAL_1:29, XREAL_1:139; assume (Partial_Sums (1 rExpSeq)) . ni >= 2 ; ::_thesis: S1[ni + 1] hence S1[ni + 1] by A7, A8, XXREAL_0:2; ::_thesis: verum end; (Partial_Sums (1 rExpSeq)) . 1 = ((Partial_Sums (1 rExpSeq)) . 0) + ((1 rExpSeq) . (0 + 1)) by SERIES_1:def_1 .= ((1 rExpSeq) . 0) + ((1 rExpSeq) . 1) by SERIES_1:def_1 .= ((1 rExpSeq) . 0) + ((1 |^ 1) / (1 !)) by SIN_COS:def_5 .= ((1 |^ 0) / (0 !)) + ((1 |^ 1) / (1 !)) by SIN_COS:def_5 .= 1 + ((1 |^ 1) / (1 !)) by A2, NEWTON:12 .= 1 + (1 / 1) by A2, NEWTON:13 .= 2 ; then A9: S1[1] ; for n being Integer st 1 <= n holds S1[n] from INT_1:sch_2(A9, A6); hence for n being Element of NAT st 1 <= n holds (Partial_Sums (1 rExpSeq)) . n >= 2 ; ::_thesis: verum end; A10: for n being Element of NAT holds ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2 proof let n be Element of NAT ; ::_thesis: ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2 ((Partial_Sums (1 rExpSeq)) ^\ 1) . n = (Partial_Sums (1 rExpSeq)) . (n + 1) by NAT_1:def_3; hence ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2 by A5, NAT_1:11; ::_thesis: verum end; 1 rExpSeq is summable by SIN_COS:45; then A11: Partial_Sums (1 rExpSeq) is convergent by SERIES_1:def_2; lim (Partial_Sums (1 rExpSeq)) = Sum (1 rExpSeq) by SERIES_1:def_3; then lim ((Partial_Sums (1 rExpSeq)) ^\ 1) = Sum (1 rExpSeq) by A11, SEQ_4:20; then Sum (1 rExpSeq) >= 2 by A10, A11, SIN_COS:38; then exp_R . 1 >= 2 by SIN_COS:def_22; then number_e >= 2 by IRRAT_1:def_7, SIN_COS:def_23; then ( number_e > 2 or number_e = 2 ) by XXREAL_0:1; hence number_e > 2 by A1; ::_thesis: verum end; then Lm4: number_e > 1 by XXREAL_0:2; theorem Th12: :: TAYLOR_1:12 for x being real number holds log (number_e,(exp_R x)) = x proof let x be real number ; ::_thesis: log (number_e,(exp_R x)) = x ( exp_R x > 0 & number_e to_power x = exp_R x ) by Th9, SIN_COS:55; hence log (number_e,(exp_R x)) = x by Lm4, POWER:def_3; ::_thesis: verum end; theorem Th13: :: TAYLOR_1:13 for x being real number holds log (number_e,(exp_R . x)) = x proof let x be real number ; ::_thesis: log (number_e,(exp_R . x)) = x thus log (number_e,(exp_R . x)) = log (number_e,(exp_R x)) by SIN_COS:def_23 .= x by Th12 ; ::_thesis: verum end; theorem Th14: :: TAYLOR_1:14 for y being real number st y > 0 holds exp_R (log (number_e,y)) = y proof let y be real number ; ::_thesis: ( y > 0 implies exp_R (log (number_e,y)) = y ) assume y > 0 ; ::_thesis: exp_R (log (number_e,y)) = y then number_e to_power (log (number_e,y)) = y by Lm4, POWER:def_3; hence exp_R (log (number_e,y)) = y by Th9; ::_thesis: verum end; theorem Th15: :: TAYLOR_1:15 for y being real number st y > 0 holds exp_R . (log (number_e,y)) = y proof let y be real number ; ::_thesis: ( y > 0 implies exp_R . (log (number_e,y)) = y ) assume A1: y > 0 ; ::_thesis: exp_R . (log (number_e,y)) = y thus exp_R . (log (number_e,y)) = exp_R (log (number_e,y)) by SIN_COS:def_23 .= y by A1, Th14 ; ::_thesis: verum end; theorem Th16: :: TAYLOR_1:16 ( exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 ) proof now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_exp_R_&_x2_in_dom_exp_R_&_exp_R_._x1_=_exp_R_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom exp_R & x2 in dom exp_R & exp_R . x1 = exp_R . x2 implies x1 = x2 ) assume that A1: x1 in dom exp_R and A2: x2 in dom exp_R and A3: exp_R . x1 = exp_R . x2 ; ::_thesis: x1 = x2 reconsider p2 = x2 as Real by A2; reconsider p1 = x1 as Real by A1; thus x1 = log (number_e,(exp_R . p1)) by Th13 .= log (number_e,(exp_R . p2)) by A3 .= x2 by Th13 ; ::_thesis: verum end; hence exp_R is one-to-one by FUNCT_1:def_4; ::_thesis: ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 ) thus ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL ) by SIN_COS:66; ::_thesis: ( ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 ) thus for x being Real holds diff (exp_R,x) = exp_R . x by SIN_COS:66; ::_thesis: ( ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 ) hereby ::_thesis: ( dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 ) let x be Real; ::_thesis: diff (exp_R,x) > 0 diff (exp_R,x) = exp_R . x by SIN_COS:66; hence diff (exp_R,x) > 0 by SIN_COS:54; ::_thesis: verum end; thus ( dom exp_R = [#] REAL & dom exp_R = [#] REAL ) by SIN_COS:47; ::_thesis: rng exp_R = right_open_halfline 0 now__::_thesis:_for_y_being_set_st_y_in_rng_exp_R_holds_ y_in_right_open_halfline_0 let y be set ; ::_thesis: ( y in rng exp_R implies y in right_open_halfline 0 ) assume y in rng exp_R ; ::_thesis: y in right_open_halfline 0 then consider x being set such that A4: x in dom exp_R and A5: y = exp_R . x by FUNCT_1:def_3; reconsider y1 = y as Real by A5; reconsider x = x as Real by A4; exp_R . x > 0 by SIN_COS:54; then y1 in { g where g is Real : 0 < g } by A5; hence y in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; then A6: rng exp_R c= right_open_halfline 0 by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_right_open_halfline_0_holds_ y_in_rng_exp_R let y be set ; ::_thesis: ( y in right_open_halfline 0 implies y in rng exp_R ) assume y in right_open_halfline 0 ; ::_thesis: y in rng exp_R then y in { g where g is Real : 0 < g } by XXREAL_1:230; then A7: ex g being Real st ( y = g & 0 < g ) ; then reconsider y1 = y as Real ; y1 = exp_R . (log (number_e,y1)) by A7, Th15; hence y in rng exp_R by FUNCT_1:def_3, SIN_COS:47; ::_thesis: verum end; then right_open_halfline 0 c= rng exp_R by TARSKI:def_3; hence rng exp_R = right_open_halfline 0 by A6, XBOOLE_0:def_10; ::_thesis: verum end; registration cluster exp_R -> one-to-one ; coherence exp_R is one-to-one by Th16; end; theorem Th17: :: TAYLOR_1:17 ( exp_R " is_differentiable_on dom (exp_R ") & ( for x being real number st x in dom (exp_R ") holds diff ((exp_R "),x) = 1 / x ) ) proof thus exp_R " is_differentiable_on dom (exp_R ") by Th16, FDIFF_2:45; ::_thesis: for x being real number st x in dom (exp_R ") holds diff ((exp_R "),x) = 1 / x let x be real number ; ::_thesis: ( x in dom (exp_R ") implies diff ((exp_R "),x) = 1 / x ) assume A1: x in dom (exp_R ") ; ::_thesis: diff ((exp_R "),x) = 1 / x A2: x in rng exp_R by A1, FUNCT_1:33; diff (exp_R,((exp_R ") . x)) = exp_R . ((exp_R ") . x) by Th16 .= x by A2, FUNCT_1:35 ; hence diff ((exp_R "),x) = 1 / x by A1, Th16, FDIFF_2:45; ::_thesis: verum end; registration cluster right_open_halfline 0 -> non empty ; coherence not right_open_halfline 0 is empty proof 1 in { g where g is Real : 0 < g } ; hence not right_open_halfline 0 is empty by XXREAL_1:230; ::_thesis: verum end; end; definition let a be real number ; func log_ a -> PartFunc of REAL,REAL means :Def2: :: TAYLOR_1:def 2 ( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = log (a,d) ) ); existence ex b1 being PartFunc of REAL,REAL st ( dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = log (a,d) ) ) proof defpred S1[ set ] means \$1 in right_open_halfline 0; reconsider a = a as Real by XREAL_0:def_1; deffunc H1( Real) -> Element of REAL = log (a,\$1); consider f being PartFunc of REAL,REAL such that A1: for d being Element of REAL holds ( d in dom f iff S1[d] ) and A2: for d being Element of REAL st d in dom f holds f /. d = H1(d) from PARTFUN2:sch_2(); take f ; ::_thesis: ( dom f = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f . d = log (a,d) ) ) for x being set st x in right_open_halfline 0 holds x in dom f by A1; then A3: right_open_halfline 0 c= dom f by TARSKI:def_3; for x being set st x in dom f holds x in right_open_halfline 0 by A1; then dom f c= right_open_halfline 0 by TARSKI:def_3; hence A4: dom f = right_open_halfline 0 by A3, XBOOLE_0:def_10; ::_thesis: for d being Element of right_open_halfline 0 holds f . d = log (a,d) let d be Element of right_open_halfline 0; ::_thesis: f . d = log (a,d) f /. d = log (a,d) by A2, A4; hence f . d = log (a,d) by A4, PARTFUN1:def_6; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = log (a,d) ) & dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = log (a,d) ) holds b1 = b2 proof let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f1 . d = log (a,d) ) & dom f2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f2 . d = log (a,d) ) implies f1 = f2 ) assume that A5: dom f1 = right_open_halfline 0 and A6: for d being Element of right_open_halfline 0 holds f1 . d = log (a,d) and A7: dom f2 = right_open_halfline 0 and A8: for d being Element of right_open_halfline 0 holds f2 . d = log (a,d) ; ::_thesis: f1 = f2 for d being Element of REAL st d in right_open_halfline 0 holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies f1 . d = f2 . d ) assume A9: d in right_open_halfline 0 ; ::_thesis: f1 . d = f2 . d thus f1 . d = log (a,d) by A6, A9 .= f2 . d by A8, A9 ; ::_thesis: verum end; hence f1 = f2 by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def2 defines log_ TAYLOR_1:def_2_:_ for a being real number for b2 being PartFunc of REAL,REAL holds ( b2 = log_ a iff ( dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = log (a,d) ) ) ); definition func ln -> PartFunc of REAL,REAL equals :: TAYLOR_1:def 3 log_ number_e; correctness coherence log_ number_e is PartFunc of REAL,REAL; ; end; :: deftheorem defines ln TAYLOR_1:def_3_:_ ln = log_ number_e; theorem Th18: :: TAYLOR_1:18 ( ln = exp_R " & ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) ) proof A1: for d being Element of REAL st d in right_open_halfline 0 holds (exp_R ") . d = ln . d proof let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies (exp_R ") . d = ln . d ) assume A2: d in right_open_halfline 0 ; ::_thesis: (exp_R ") . d = ln . d (exp_R ") . d = log (number_e,d) proof d in { g where g is Real : 0 < g } by A2, XXREAL_1:230; then ex g being Real st ( g = d & g > 0 ) ; then d = exp_R . (log (number_e,d)) by Th15; hence (exp_R ") . d = log (number_e,d) by Th16, FUNCT_1:32; ::_thesis: verum end; hence (exp_R ") . d = ln . d by A2, Def2; ::_thesis: verum end; A3: dom (exp_R ") = right_open_halfline 0 by Th16, FUNCT_1:33; then dom (exp_R ") = dom ln by Def2; hence A4: ln = exp_R " by A3, A1, PARTFUN1:5; ::_thesis: ( ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) ) A5: for x being Real st x > 0 holds ln is_differentiable_in x proof let x be Real; ::_thesis: ( x > 0 implies ln is_differentiable_in x ) assume x > 0 ; ::_thesis: ln is_differentiable_in x then x in { g where g is Real : 0 < g } ; then x in right_open_halfline 0 by XXREAL_1:230; hence ln is_differentiable_in x by A3, A4, Th17, FDIFF_1:9; ::_thesis: verum end; A6: for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) proof let x be Element of right_open_halfline 0; ::_thesis: 0 < diff (ln,x) x in right_open_halfline 0 ; then x in { g where g is Real : 0 < g } by XXREAL_1:230; then A7: ex g being Real st ( x = g & 0 < g ) ; 1 / x = x " by XCMPLX_1:215; hence 0 < diff (ln,x) by A3, A4, A7, Th17; ::_thesis: verum end; thus ln is one-to-one by A4, FUNCT_1:40; ::_thesis: ( dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) ) dom ln = right_open_halfline 0 by Def2; hence ( dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) ) by A4, A5, A6, Th16, Th17, FUNCT_1:33; ::_thesis: verum end; theorem :: TAYLOR_1:19 for x0 being real number for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds ( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) ) proof let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds ( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 implies ( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) ) ) assume A1: f is_differentiable_in x0 ; ::_thesis: ( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) ) A2: ( x0 is Real & exp_R is_differentiable_in f . x0 ) by Th16, FDIFF_1:9, XREAL_0:def_1; hence exp_R * f is_differentiable_in x0 by A1, FDIFF_2:13; ::_thesis: diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) thus diff ((exp_R * f),x0) = (diff (exp_R,(f . x0))) * (diff (f,x0)) by A1, A2, FDIFF_2:13 .= (exp_R . (f . x0)) * (diff (f,x0)) by Th16 ; ::_thesis: verum end; theorem :: TAYLOR_1:20 for x0 being real number for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) ) proof let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 & f . x0 > 0 implies ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) ) ) assume that A1: f is_differentiable_in x0 and A2: f . x0 > 0 ; ::_thesis: ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) ) f . x0 in { g where g is Real : 0 < g } by A2; then A3: f . x0 in right_open_halfline 0 by XXREAL_1:230; then A4: ln is_differentiable_in f . x0 by Th18, FDIFF_1:9; A5: x0 is Real by XREAL_0:def_1; hence ln * f is_differentiable_in x0 by A1, A4, FDIFF_2:13; ::_thesis: diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) thus diff ((ln * f),x0) = (diff (ln,(f . x0))) * (diff (f,x0)) by A1, A4, A5, FDIFF_2:13 .= (1 / (f . x0)) * (diff (f,x0)) by A3, Th18 .= ((diff (f,x0)) / (f . x0)) * 1 by XCMPLX_1:75 .= (diff (f,x0)) / (f . x0) ; ::_thesis: verum end; definition let p be real number ; func #R p -> PartFunc of REAL,REAL means :Def4: :: TAYLOR_1:def 4 ( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = d #R p ) ); existence ex b1 being PartFunc of REAL,REAL st ( dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = d #R p ) ) proof defpred S1[ set ] means \$1 in right_open_halfline 0; reconsider p = p as Real by XREAL_0:def_1; deffunc H1( Real) -> Element of REAL = \$1 #R p; consider f being PartFunc of REAL,REAL such that A1: for d being Element of REAL holds ( d in dom f iff S1[d] ) and A2: for d being Element of REAL st d in dom f holds f /. d = H1(d) from PARTFUN2:sch_2(); take f ; ::_thesis: ( dom f = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f . d = d #R p ) ) for x being set st x in right_open_halfline 0 holds x in dom f by A1; then A3: right_open_halfline 0 c= dom f by TARSKI:def_3; for x being set st x in dom f holds x in right_open_halfline 0 by A1; then dom f c= right_open_halfline 0 by TARSKI:def_3; hence A4: dom f = right_open_halfline 0 by A3, XBOOLE_0:def_10; ::_thesis: for d being Element of right_open_halfline 0 holds f . d = d #R p let d be Element of right_open_halfline 0; ::_thesis: f . d = d #R p f /. d = d #R p by A2, A4; hence f . d = d #R p by A4, PARTFUN1:def_6; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = d #R p ) & dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = d #R p ) holds b1 = b2 proof let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f1 . d = d #R p ) & dom f2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f2 . d = d #R p ) implies f1 = f2 ) assume that A5: dom f1 = right_open_halfline 0 and A6: for d being Element of right_open_halfline 0 holds f1 . d = d #R p and A7: dom f2 = right_open_halfline 0 and A8: for d being Element of right_open_halfline 0 holds f2 . d = d #R p ; ::_thesis: f1 = f2 for d being Element of REAL st d in right_open_halfline 0 holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies f1 . d = f2 . d ) assume A9: d in right_open_halfline 0 ; ::_thesis: f1 . d = f2 . d thus f1 . d = d #R p by A6, A9 .= f2 . d by A8, A9 ; ::_thesis: verum end; hence f1 = f2 by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def4 defines #R TAYLOR_1:def_4_:_ for p being real number for b2 being PartFunc of REAL,REAL holds ( b2 = #R p iff ( dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = d #R p ) ) ); theorem Th21: :: TAYLOR_1:21 for x, p being real number st x > 0 holds ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) proof let x, p be real number ; ::_thesis: ( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) ) set f = #R p; A1: p is Real by XREAL_0:def_1; A2: for x being Real st 0 < x holds ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) ) proof let x be Real; ::_thesis: ( 0 < x implies ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) ) ) assume A3: x > 0 ; ::_thesis: ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) ) A4: ln is_differentiable_in x by A3, Th18; then A5: p (#) ln is_differentiable_in x by A1, FDIFF_1:15; x in { g where g is Real : 0 < g } by A3; then A6: x in right_open_halfline 0 by XXREAL_1:230; then A7: x in dom (p (#) ln) by Th18, VALUED_1:def_5; A8: diff ((p (#) ln),x) = p * (diff (ln,x)) by A1, A4, FDIFF_1:15 .= p * (1 / x) by A6, Th18 ; A9: exp_R is_differentiable_in (p (#) ln) . x by SIN_COS:65; hence exp_R * (p (#) ln) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) diff (exp_R,((p (#) ln) . x)) = exp_R . ((p (#) ln) . x) by Th16 .= exp_R . (p * (ln . x)) by A7, VALUED_1:def_5 .= exp_R . (p * (log (number_e,x))) by A6, Def2 .= exp_R . (log (number_e,(x to_power p))) by A3, Lm4, POWER:55 .= x to_power p by A3, Th15, POWER:34 ; hence diff ((exp_R * (p (#) ln)),x) = (x to_power p) * (p * (1 / x)) by A5, A9, A8, FDIFF_2:13 .= p * ((x to_power p) * (1 / x)) .= p * ((x to_power p) * (1 / (x to_power 1))) by POWER:25 .= p * ((x to_power p) * (x to_power (- 1))) by A3, POWER:28 .= p * (x to_power (p + (- 1))) by A3, POWER:27 .= p * (x #R (p - 1)) by A3, POWER:def_2 ; ::_thesis: verum end; rng (p (#) ln) c= dom exp_R by Th16; then A10: dom (exp_R * (p (#) ln)) = dom (p (#) ln) by RELAT_1:27 .= right_open_halfline 0 by Th18, VALUED_1:def_5 ; A11: for d being Element of REAL st d in right_open_halfline 0 holds (exp_R * (p (#) ln)) . d = (#R p) . d proof let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies (exp_R * (p (#) ln)) . d = (#R p) . d ) assume A12: d in right_open_halfline 0 ; ::_thesis: (exp_R * (p (#) ln)) . d = (#R p) . d A13: d in dom (p (#) ln) by A12, Th18, VALUED_1:def_5; d in { g where g is Real : 0 < g } by A12, XXREAL_1:230; then A14: ex g being Real st ( g = d & g > 0 ) ; thus (exp_R * (p (#) ln)) . d = (exp_R * (p (#) ln)) /. d by A10, A12, PARTFUN1:def_6 .= exp_R /. ((p (#) ln) /. d) by A10, A12, PARTFUN2:3 .= exp_R . ((p (#) ln) . d) by A13, PARTFUN1:def_6 .= exp_R . (p * (ln . d)) by A13, VALUED_1:def_5 .= exp_R . (p * (log (number_e,d))) by A12, Def2 .= exp_R . (log (number_e,(d to_power p))) by A14, Lm4, POWER:55 .= d to_power p by A14, Th15, POWER:34 .= d #R p by A14, POWER:def_2 .= (#R p) . d by A12, Def4 ; ::_thesis: verum end; dom (#R p) = right_open_halfline 0 by Def4; then ( x is Real & exp_R * (p (#) ln) = #R p ) by A10, A11, PARTFUN1:5, XREAL_0:def_1; hence ( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) ) by A2; ::_thesis: verum end; theorem :: TAYLOR_1:22 for x0, p being real number for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds ( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) ) proof let x0, p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds ( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 & f . x0 > 0 implies ( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) ) ) assume that A1: f is_differentiable_in x0 and A2: f . x0 > 0 ; ::_thesis: ( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) ) A3: x0 is Real by XREAL_0:def_1; A4: #R p is_differentiable_in f . x0 by A2, Th21; hence (#R p) * f is_differentiable_in x0 by A1, A3, FDIFF_2:13; ::_thesis: diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) thus diff (((#R p) * f),x0) = (diff ((#R p),(f . x0))) * (diff (f,x0)) by A1, A4, A3, FDIFF_2:13 .= (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) by A2, Th21 ; ::_thesis: verum end; begin definition let f be PartFunc of REAL,REAL; let Z be Subset of REAL; func diff (f,Z) -> Functional_Sequence of REAL,REAL means :Def5: :: TAYLOR_1:def 5 ( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `| Z ) ); existence ex b1 being Functional_Sequence of REAL,REAL st ( b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `| Z ) ) proof reconsider fZ = f | Z as Element of PFuncs (REAL,REAL) by PARTFUN1:45; defpred S1[ set , set , set ] means ex h being PartFunc of REAL,REAL st ( \$2 = h & \$3 = h `| Z ); A1: for n being Element of NAT for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] let x be Element of PFuncs (REAL,REAL); ::_thesis: ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] reconsider x9 = x as PartFunc of REAL,REAL by PARTFUN1:46; reconsider y = x9 `| Z as Element of PFuncs (REAL,REAL) by PARTFUN1:45; ex h being PartFunc of REAL,REAL st ( x = h & y = h `| Z ) ; hence ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] ; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (REAL,REAL)) such that A2: ( g . 0 = fZ & ( for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch_2(A1); reconsider g = g as Functional_Sequence of REAL,REAL ; take g ; ::_thesis: ( g . 0 = f | Z & ( for i being Nat holds g . (i + 1) = (g . i) `| Z ) ) thus g . 0 = f | Z by A2; ::_thesis: for i being Nat holds g . (i + 1) = (g . i) `| Z let i be Nat; ::_thesis: g . (i + 1) = (g . i) `| Z i is Element of NAT by ORDINAL1:def_12; then S1[i,g . i,g . (i + 1)] by A2; hence g . (i + 1) = (g . i) `| Z ; ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of REAL,REAL st b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `| Z ) & b2 . 0 = f | Z & ( for i being Nat holds b2 . (i + 1) = (b2 . i) `| Z ) holds b1 = b2 proof let seq1, seq2 be Functional_Sequence of REAL,REAL; ::_thesis: ( seq1 . 0 = f | Z & ( for i being Nat holds seq1 . (i + 1) = (seq1 . i) `| Z ) & seq2 . 0 = f | Z & ( for i being Nat holds seq2 . (i + 1) = (seq2 . i) `| Z ) implies seq1 = seq2 ) assume that A3: seq1 . 0 = f | Z and A4: for n being Nat holds seq1 . (n + 1) = (seq1 . n) `| Z and A5: seq2 . 0 = f | Z and A6: for n being Nat holds seq2 . (n + 1) = (seq2 . n) `| Z ; ::_thesis: seq1 = seq2 defpred S1[ Element of NAT ] means seq1 . \$1 = seq2 . \$1; A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] thus seq1 . (k + 1) = (seq1 . k) `| Z by A4 .= seq2 . (k + 1) by A6, A8 ; ::_thesis: verum end; A9: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines diff TAYLOR_1:def_5_:_ for f being PartFunc of REAL,REAL for Z being Subset of REAL for b3 being Functional_Sequence of REAL,REAL holds ( b3 = diff (f,Z) iff ( b3 . 0 = f | Z & ( for i being Nat holds b3 . (i + 1) = (b3 . i) `| Z ) ) ); definition let f be PartFunc of REAL,REAL; let n be Nat; let Z be Subset of REAL; predf is_differentiable_on n,Z means :Def6: :: TAYLOR_1:def 6 for i being Element of NAT st i <= n - 1 holds (diff (f,Z)) . i is_differentiable_on Z; end; :: deftheorem Def6 defines is_differentiable_on TAYLOR_1:def_6_:_ for f being PartFunc of REAL,REAL for n being Nat for Z being Subset of REAL holds ( f is_differentiable_on n,Z iff for i being Element of NAT st i <= n - 1 holds (diff (f,Z)) . i is_differentiable_on Z ); theorem Th23: :: TAYLOR_1:23 for f being PartFunc of REAL,REAL for Z being Subset of REAL for n being Nat st f is_differentiable_on n,Z holds for m being Nat st m <= n holds f is_differentiable_on m,Z proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for n being Nat st f is_differentiable_on n,Z holds for m being Nat st m <= n holds f is_differentiable_on m,Z let Z be Subset of REAL; ::_thesis: for n being Nat st f is_differentiable_on n,Z holds for m being Nat st m <= n holds f is_differentiable_on m,Z let n be Nat; ::_thesis: ( f is_differentiable_on n,Z implies for m being Nat st m <= n holds f is_differentiable_on m,Z ) assume A1: f is_differentiable_on n,Z ; ::_thesis: for m being Nat st m <= n holds f is_differentiable_on m,Z let m be Nat; ::_thesis: ( m <= n implies f is_differentiable_on m,Z ) assume A2: m <= n ; ::_thesis: f is_differentiable_on m,Z now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_m_-_1_holds_ (diff_(f,Z))_._i_is_differentiable_on_Z A3: m - 1 <= n - 1 by A2, XREAL_1:13; let i be Element of NAT ; ::_thesis: ( i <= m - 1 implies (diff (f,Z)) . i is_differentiable_on Z ) assume i <= m - 1 ; ::_thesis: (diff (f,Z)) . i is_differentiable_on Z then i <= n - 1 by A3, XXREAL_0:2; hence (diff (f,Z)) . i is_differentiable_on Z by A1, Def6; ::_thesis: verum end; hence f is_differentiable_on m,Z by Def6; ::_thesis: verum end; definition let f be PartFunc of REAL,REAL; let Z be Subset of REAL; let a, b be real number ; func Taylor (f,Z,a,b) -> Real_Sequence means :Def7: :: TAYLOR_1:def 7 for n being Nat holds it . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !); existence ex b1 being Real_Sequence st for n being Nat holds b1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) proof deffunc H1( Element of NAT ) -> Element of REAL = ((((diff (f,Z)) . \$1) . a) * ((b - a) |^ \$1)) / (\$1 !); consider seq being Real_Sequence such that A1: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1(); take seq ; ::_thesis: for n being Nat holds seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) let n be Nat; ::_thesis: seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) n is Element of NAT by ORDINAL1:def_12; hence seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds b2 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) holds b1 = b2 proof deffunc H1( Nat) -> Element of REAL = ((((diff (f,Z)) . \$1) . a) * ((b - a) |^ \$1)) / (\$1 !); let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Nat holds s1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds s2 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) implies s1 = s2 ) assume that A2: for n being Nat holds s1 . n = H1(n) and A3: for n being Nat holds s2 . n = H1(n) ; ::_thesis: s1 = s2 now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ s1_._x_=_s2_._x let x be set ; ::_thesis: ( x in NAT implies s1 . x = s2 . x ) assume x in NAT ; ::_thesis: s1 . x = s2 . x then reconsider n = x as Element of NAT ; thus s1 . x = H1(n) by A2 .= s2 . x by A3 ; ::_thesis: verum end; hence s1 = s2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def7 defines Taylor TAYLOR_1:def_7_:_ for f being PartFunc of REAL,REAL for Z being Subset of REAL for a, b being real number for b5 being Real_Sequence holds ( b5 = Taylor (f,Z,a,b) iff for n being Nat holds b5 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ); Lm5: for b being Real ex g being PartFunc of REAL,REAL st ( dom g = [#] REAL & ( for x being Real holds ( g . x = b - x & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) proof defpred S1[ set ] means \$1 in REAL ; let b be Real; ::_thesis: ex g being PartFunc of REAL,REAL st ( dom g = [#] REAL & ( for x being Real holds ( g . x = b - x & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) deffunc H1( Real) -> Element of REAL = b - \$1; consider g being PartFunc of REAL,REAL such that A1: for d being Element of REAL holds ( d in dom g iff S1[d] ) and A2: for d being Element of REAL st d in dom g holds g /. d = H1(d) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds ( g . x = b - x & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) for x being set st x in REAL holds x in dom g by A1; then A3: REAL c= dom g by TARSKI:def_3; then A4: dom g = [#] REAL by XBOOLE_0:def_10; A5: for d being Element of REAL holds g . d = b - d proof let d be Element of REAL ; ::_thesis: g . d = b - d g /. d = b - d by A2, A4; hence g . d = b - d by A4, PARTFUN1:def_6; ::_thesis: verum end; A6: for d being Real st d in REAL holds g . d = ((- 1) * d) + b proof let d be Real; ::_thesis: ( d in REAL implies g . d = ((- 1) * d) + b ) assume d in REAL ; ::_thesis: g . d = ((- 1) * d) + b thus g . d = b - d by A5 .= ((- 1) * d) + b ; ::_thesis: verum end; then A7: g is_differentiable_on dom g by A4, FDIFF_1:23; for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) proof let d be Real; ::_thesis: ( g is_differentiable_in d & diff (g,d) = - 1 ) thus g is_differentiable_in d by A4, A7, FDIFF_1:9; ::_thesis: diff (g,d) = - 1 thus diff (g,d) = (g `| (dom g)) . d by A4, A7, FDIFF_1:def_7 .= - 1 by A4, A6, FDIFF_1:23 ; ::_thesis: verum end; hence ( dom g = [#] REAL & ( for x being Real holds ( g . x = b - x & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) by A3, A5, XBOOLE_0:def_10; ::_thesis: verum end; Lm6: for n being Element of NAT for l, b being Real ex g being PartFunc of REAL,REAL st ( dom g = [#] REAL & ( for x being Real holds ( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) ) proof defpred S1[ set ] means \$1 in REAL ; let n be Element of NAT ; ::_thesis: for l, b being Real ex g being PartFunc of REAL,REAL st ( dom g = [#] REAL & ( for x being Real holds ( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) ) let l, b be Real; ::_thesis: ex g being PartFunc of REAL,REAL st ( dom g = [#] REAL & ( for x being Real holds ( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) ) deffunc H1( Real) -> Element of REAL = (l * ((b - \$1) |^ (n + 1))) / ((n + 1) !); consider g being PartFunc of REAL,REAL such that A1: for d being Element of REAL holds ( d in dom g iff S1[d] ) and A2: for d being Element of REAL st d in dom g holds g /. d = H1(d) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds ( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) ) consider f being PartFunc of REAL,REAL such that A3: dom f = [#] REAL and A4: for x being Real holds f . x = b - x and A5: for x being Real holds ( f is_differentiable_in x & diff (f,x) = - 1 ) by Lm5; ( dom (#Z (n + 1)) = REAL & rng f c= REAL ) by FUNCT_2:def_1; then A6: dom ((#Z (n + 1)) * f) = dom f by RELAT_1:27; for x being set st x in REAL holds x in dom g by A1; then A7: REAL c= dom g by TARSKI:def_3; then A8: dom g = [#] REAL by XBOOLE_0:def_10; A9: for d being Element of REAL holds g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) proof let d be Element of REAL ; ::_thesis: g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) g /. d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A2, A8; hence g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A8, PARTFUN1:def_6; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f))_holds_ ((l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f))_._x_=_g_._x let x be Element of REAL ; ::_thesis: ( x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) implies ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x ) assume x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) ; ::_thesis: ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x hence ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = (l / ((n + 1) !)) * (((#Z (n + 1)) * f) . x) by VALUED_1:def_5 .= (l / ((n + 1) !)) * (((#Z (n + 1)) * f) /. x) by A3, A6, PARTFUN1:def_6 .= (l / ((n + 1) !)) * ((#Z (n + 1)) /. (f /. x)) by A3, A6, PARTFUN2:3 .= (l / ((n + 1) !)) * ((#Z (n + 1)) . (f . x)) by A3, PARTFUN1:def_6 .= (l / ((n + 1) !)) * ((f . x) #Z (n + 1)) by Def1 .= (l / ((n + 1) !)) * ((f . x) |^ (n + 1)) by PREPOWER:36 .= (l / ((n + 1) !)) * ((b - x) |^ (n + 1)) by A4 .= (l * ((b - x) |^ (n + 1))) / ((n + 1) !) by XCMPLX_1:74 .= g . x by A9 ; ::_thesis: verum end; A11: for x being Real holds ( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) ) proof let x be Real; ::_thesis: ( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) ) A12: ( f is_differentiable_in x & #Z (n + 1) is_differentiable_in f . x ) by A5, Th2; hence (#Z (n + 1)) * f is_differentiable_in x by FDIFF_2:13; ::_thesis: diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) diff ((#Z (n + 1)),(f . x)) = (n + 1) * ((f . x) #Z ((n + 1) - 1)) by Th2; hence diff (((#Z (n + 1)) * f),x) = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (diff (f,x)) by A12, FDIFF_2:13 .= ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (- 1) by A5 .= ((n + 1) * ((b - x) #Z ((n + 1) - 1))) * (- 1) by A4 .= - ((n + 1) * ((b - x) #Z n)) ; ::_thesis: verum end; A13: now__::_thesis:_for_x_being_Real_holds_ (_(l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f)_is_differentiable_in_x_&_diff_(((l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f)),x)_=_-_((l_*_((b_-_x)_|^_n))_/_(n_!))_) let x be Real; ::_thesis: ( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) ) A14: (n + 1) / ((n + 1) !) = (1 * (n + 1)) / ((n !) * (n + 1)) by NEWTON:15 .= 1 / (n !) by XCMPLX_1:91 ; A15: (#Z (n + 1)) * f is_differentiable_in x by A11; hence (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x by FDIFF_1:15; ::_thesis: diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) thus diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = (l / ((n + 1) !)) * (diff (((#Z (n + 1)) * f),x)) by A15, FDIFF_1:15 .= ((diff (((#Z (n + 1)) * f),x)) / ((n + 1) !)) * l by XCMPLX_1:75 .= l * ((- ((n + 1) * ((b - x) #Z n))) / ((n + 1) !)) by A11 .= l * ((- ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)) by PREPOWER:36 .= (l * (- ((n + 1) * ((b - x) |^ n)))) / ((n + 1) !) by XCMPLX_1:74 .= ((- l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) !) .= (- l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) !)) by XCMPLX_1:74 .= (- l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) !))) by XCMPLX_1:74 .= (- l) * (((b - x) |^ n) / (n !)) by A14, XCMPLX_1:99 .= - (l * (((b - x) |^ n) / (n !))) .= - ((l * ((b - x) |^ n)) / (n !)) by XCMPLX_1:74 ; ::_thesis: verum end; dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) = dom g by A8, A3, A6, VALUED_1:def_5; then (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) = g by A10, PARTFUN1:5; hence ( dom g = [#] REAL & ( for x being Real holds ( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) ) by A7, A9, A13, XBOOLE_0:def_10; ::_thesis: verum end; Lm7: for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL for b being Real ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL for b being Real ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for b being Real ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) let Z be Subset of REAL; ::_thesis: for b being Real ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) let b be Real; ::_thesis: ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) defpred S1[ set ] means \$1 in Z; deffunc H1( Real) -> Element of REAL = (f . b) - ((Partial_Sums (Taylor (f,Z,\$1,b))) . n); consider g being PartFunc of REAL,REAL such that A1: for d being Element of REAL holds ( d in dom g iff S1[d] ) and A2: for d being Element of REAL st d in dom g holds g /. d = H1(d) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) for x being set st x in dom g holds x in Z by A1; then A3: dom g c= Z by TARSKI:def_3; for x being set st x in Z holds x in dom g by A1; then A4: Z c= dom g by TARSKI:def_3; for d being Real st d in Z holds g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) proof let d be Real; ::_thesis: ( d in Z implies g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) ) assume A5: d in Z ; ::_thesis: g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) g /. d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) by A2, A4, A5; hence g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) by A4, A5, PARTFUN1:def_6; ::_thesis: verum end; hence ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th24: :: TAYLOR_1:24 for f being PartFunc of REAL,REAL for Z being Subset of REAL for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & ].a,b.[ c= Z holds ((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & ].a,b.[ c= Z holds ((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n let Z be Subset of REAL; ::_thesis: for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & ].a,b.[ c= Z holds ((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n defpred S1[ Element of NAT ] means ( f is_differentiable_on \$1,Z implies for a, b being Real st a < b & ].a,b.[ c= Z holds ((diff (f,Z)) . \$1) | ].a,b.[ = (diff (f,].a,b.[)) . \$1 ); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] assume A3: f is_differentiable_on k + 1,Z ; ::_thesis: for a, b being Real st a < b & ].a,b.[ c= Z holds ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1) let a, b be Real; ::_thesis: ( a < b & ].a,b.[ c= Z implies ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1) ) assume that A4: a < b and A5: ].a,b.[ c= Z ; ::_thesis: ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1) k <= (k + 1) - 1 ; then A6: (diff (f,Z)) . k is_differentiable_on Z by A3, Def6; then A7: (diff (f,Z)) . k is_differentiable_on ].a,b.[ by A5, FDIFF_1:26; then A8: dom (((diff (f,Z)) . k) `| ].a,b.[) = ].a,b.[ by FDIFF_1:def_7; A9: dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) = (dom (((diff (f,Z)) . k) `| Z)) /\ ].a,b.[ by RELAT_1:61 .= Z /\ ].a,b.[ by A6, FDIFF_1:def_7 .= ].a,b.[ by A5, XBOOLE_1:28 ; A10: now__::_thesis:_for_x_being_Real_st_x_in_dom_((((diff_(f,Z))_._k)_`|_Z)_|_].a,b.[)_holds_ ((((diff_(f,Z))_._k)_`|_Z)_|_].a,b.[)_._x_=_(((diff_(f,Z))_._k)_`|_].a,b.[)_._x let x be Real; ::_thesis: ( x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) implies ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x ) assume A11: x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) ; ::_thesis: ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x thus ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| Z) . x by A9, A11, FUNCT_1:49 .= diff (((diff (f,Z)) . k),x) by A5, A6, A9, A11, FDIFF_1:def_7 .= (((diff (f,Z)) . k) `| ].a,b.[) . x by A7, A9, A11, FDIFF_1:def_7 ; ::_thesis: verum end; thus ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (((diff (f,Z)) . k) `| Z) | ].a,b.[ by Def5 .= ((diff (f,Z)) . k) `| ].a,b.[ by A9, A8, A10, PARTFUN1:5 .= (((diff (f,Z)) . k) | ].a,b.[) `| ].a,b.[ by A7, FDIFF_2:16 .= ((diff (f,].a,b.[)) . k) `| ].a,b.[ by A2, A3, A4, A5, Th23, NAT_1:11 .= (diff (f,].a,b.[)) . (k + 1) by Def5 ; ::_thesis: verum end; A12: S1[ 0 ] proof assume f is_differentiable_on 0 ,Z ; ::_thesis: for a, b being Real st a < b & ].a,b.[ c= Z holds ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0 let a, b be Real; ::_thesis: ( a < b & ].a,b.[ c= Z implies ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0 ) assume that a < b and A13: ].a,b.[ c= Z ; ::_thesis: ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0 thus ((diff (f,Z)) . 0) | ].a,b.[ = (f | Z) | ].a,b.[ by Def5 .= f | ].a,b.[ by A13, FUNCT_1:51 .= (diff (f,].a,b.[)) . 0 by Def5 ; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A12, A1); ::_thesis: verum end; Lm8: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f holds for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f holds for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f implies for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) ) assume A1: Z c= dom f ; ::_thesis: for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) defpred S1[ Element of NAT ] means ( f is_differentiable_on \$1,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . \$1) | [.a,b.] is continuous & f is_differentiable_on \$1 + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . \$1) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (\$1 + 1)) . x) * ((b - x) |^ \$1)) / (\$1 !)) ) ) ); A2: S1[ 0 ] proof assume f is_differentiable_on 0 ,Z ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ implies for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) ) assume that A3: a < b and A4: [.a,b.] c= Z and A5: ((diff (f,Z)) . 0) | [.a,b.] is continuous and A6: f is_differentiable_on 0 + 1,].a,b.[ ; ::_thesis: for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) A7: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A8: ].a,b.[ c= Z by A4, XBOOLE_1:1; let g be PartFunc of REAL,REAL; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ) implies ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) ) assume that A9: dom g = Z and A10: for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ; ::_thesis: ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) A11: b in [.a,b.] by A3, XXREAL_1:1; hence g . b = (f . b) - ((Partial_Sums (Taylor (f,Z,b,b))) . 0) by A4, A10 .= (f . b) - ((Taylor (f,Z,b,b)) . 0) by SERIES_1:def_1 .= (f . b) - (((((diff (f,Z)) . 0) . b) * ((b - b) |^ 0)) / (0 !)) by Def7 .= (f . b) - ((((f | Z) . b) * ((b - b) |^ 0)) / (0 !)) by Def5 .= (f . b) - (((f . b) * ((b - b) |^ 0)) / (0 !)) by A4, A11, FUNCT_1:49 .= (f . b) - ((f . b) * 1) by NEWTON:4, NEWTON:12 .= 0 ; ::_thesis: ( g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) consider y being PartFunc of REAL,REAL such that A12: dom y = [#] REAL and A13: for x being Real holds y . x = (f . b) - x and A14: for x being Real holds ( y is_differentiable_in x & diff (y,x) = - 1 ) by Lm5; rng f c= REAL ; then A15: dom (y * f) = dom f by A12, RELAT_1:27; for x being Real st x in REAL holds y is_differentiable_in x by A14; then y is_differentiable_on REAL by A12, FDIFF_1:9; then y | REAL is continuous by FDIFF_1:25; then A16: y | (f .: [.a,b.]) is continuous by FCONT_1:16; rng f c= dom y by A12; then A17: dom (y * f) = dom f by RELAT_1:27; A18: [.a,b.] c= dom f by A1, A4, XBOOLE_1:1; then A19: ].a,b.[ c= dom f by A7, XBOOLE_1:1; 0 <= (0 + 1) - 1 ; then (diff (f,].a,b.[)) . 0 is_differentiable_on ].a,b.[ by A6, Def6; then f | ].a,b.[ is_differentiable_on ].a,b.[ by Def5; then for x being Real st x in ].a,b.[ holds f | ].a,b.[ is_differentiable_in x by FDIFF_1:9; then A20: f is_differentiable_on ].a,b.[ by A19, FDIFF_1:def_6; A21: for x being Real st x in ].a,b.[ holds ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) proof A22: (diff (f,].a,b.[)) . (0 + 1) = ((diff (f,].a,b.[)) . 0) `| ].a,b.[ by Def5 .= (f | ].a,b.[) `| ].a,b.[ by Def5 .= f `| ].a,b.[ by A20, FDIFF_2:16 ; let x be Real; ::_thesis: ( x in ].a,b.[ implies ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) assume A23: x in ].a,b.[ ; ::_thesis: ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) A24: f is_differentiable_in x by A20, A23, FDIFF_1:9; A25: y is_differentiable_in f . x by A14; hence y * f is_differentiable_in x by A24, FDIFF_2:13; ::_thesis: diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) A26: ((b - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12; thus diff ((y * f),x) = (diff (y,(f . x))) * (diff (f,x)) by A25, A24, FDIFF_2:13 .= (diff (y,(f . x))) * ((f `| ].a,b.[) . x) by A20, A23, FDIFF_1:def_7 .= (- 1) * (((diff (f,].a,b.[)) . (0 + 1)) . x) by A14, A22 .= - ((((diff (f,].a,b.[)) . (0 + 1)) . x) * (((b - x) |^ 0) / (0 !))) by A26 .= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) by XCMPLX_1:74 ; ::_thesis: verum end; then for x being Real st x in ].a,b.[ holds y * f is_differentiable_in x ; then A27: y * f is_differentiable_on ].a,b.[ by A19, A17, FDIFF_1:9; A28: dom ((y * f) | [.a,b.]) = (dom (y * f)) /\ [.a,b.] by RELAT_1:61 .= [.a,b.] by A1, A4, A15, XBOOLE_1:1, XBOOLE_1:28 .= Z /\ [.a,b.] by A4, XBOOLE_1:28 .= dom (g | [.a,b.]) by A9, RELAT_1:61 ; A29: now__::_thesis:_for_xx_being_set_st_xx_in_dom_(g_|_[.a,b.])_holds_ (g_|_[.a,b.])_._xx_=_((y_*_f)_|_[.a,b.])_._xx let xx be set ; ::_thesis: ( xx in dom (g | [.a,b.]) implies (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx ) assume A30: xx in dom (g | [.a,b.]) ; ::_thesis: (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx reconsider x = xx as Real by A30; dom (g | [.a,b.]) = (dom g) /\ [.a,b.] by RELAT_1:61; then dom (g | [.a,b.]) c= [.a,b.] by XBOOLE_1:17; then A31: x in [.a,b.] by A30; A32: ((b - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12; thus (g | [.a,b.]) . xx = g . x by A30, FUNCT_1:47 .= (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) by A4, A10, A31 .= (f . b) - ((Taylor (f,Z,x,b)) . 0) by SERIES_1:def_1 .= (f . b) - (((((diff (f,Z)) . 0) . x) * ((b - x) |^ 0)) / (0 !)) by Def7 .= (f . b) - ((((f | Z) . x) * ((b - x) |^ 0)) / (0 !)) by Def5 .= (f . b) - (((f . x) * ((b - x) |^ 0)) / (0 !)) by A4, A31, FUNCT_1:49 .= (f . b) - ((f . x) * (((b - x) |^ 0) / (0 !))) by XCMPLX_1:74 .= y . (f . x) by A13, A32 .= (y * f) . x by A18, A31, FUNCT_1:13 .= ((y * f) | [.a,b.]) . xx by A28, A30, FUNCT_1:47 ; ::_thesis: verum end; (f | Z) | [.a,b.] is continuous by A5, Def5; then ((f | Z) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:15; then (f | [.a,b.]) | [.a,b.] is continuous by A4, FUNCT_1:51; then f | [.a,b.] is continuous by FCONT_1:15; then (y * f) | [.a,b.] is continuous by A16, FCONT_1:25; hence g | [.a,b.] is continuous by A28, A29, FUNCT_1:2; ::_thesis: ( g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) A33: dom ((y * f) | ].a,b.[) = (dom (y * f)) /\ ].a,b.[ by RELAT_1:61 .= ].a,b.[ by A7, A18, A17, XBOOLE_1:1, XBOOLE_1:28 .= Z /\ ].a,b.[ by A4, A7, XBOOLE_1:1, XBOOLE_1:28 .= dom (g | ].a,b.[) by A9, RELAT_1:61 ; now__::_thesis:_for_xx_being_set_st_xx_in_dom_(g_|_].a,b.[)_holds_ (g_|_].a,b.[)_._xx_=_((y_*_f)_|_].a,b.[)_._xx let xx be set ; ::_thesis: ( xx in dom (g | ].a,b.[) implies (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx ) assume A34: xx in dom (g | ].a,b.[) ; ::_thesis: (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx reconsider x = xx as Real by A34; dom (g | ].a,b.[) = (dom g) /\ ].a,b.[ by RELAT_1:61; then dom (g | ].a,b.[) c= ].a,b.[ by XBOOLE_1:17; then A35: x in ].a,b.[ by A34; A36: ((b - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12; thus (g | ].a,b.[) . xx = g . x by A34, FUNCT_1:47 .= (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) by A10, A8, A35 .= (f . b) - ((Taylor (f,Z,x,b)) . 0) by SERIES_1:def_1 .= (f . b) - (((((diff (f,Z)) . 0) . x) * ((b - x) |^ 0)) / (0 !)) by Def7 .= (f . b) - ((((f | Z) . x) * ((b - x) |^ 0)) / (0 !)) by Def5 .= (f . b) - (((f . x) * ((b - x) |^ 0)) / (0 !)) by A8, A35, FUNCT_1:49 .= (f . b) - ((f . x) * (((b - x) |^ 0) / (0 !))) by XCMPLX_1:74 .= y . (f . x) by A13, A36 .= (y * f) . x by A19, A35, FUNCT_1:13 .= ((y * f) | ].a,b.[) . xx by A33, A34, FUNCT_1:47 ; ::_thesis: verum end; then A37: g | ].a,b.[ = (y * f) | ].a,b.[ by A33, FUNCT_1:2; then g | ].a,b.[ is_differentiable_on ].a,b.[ by A27, FDIFF_2:16; then for x being Real st x in ].a,b.[ holds g | ].a,b.[ is_differentiable_in x by FDIFF_1:9; hence A38: g is_differentiable_on ].a,b.[ by A9, A8, FDIFF_1:def_6; ::_thesis: for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) now__::_thesis:_for_x_being_Real_st_x_in_].a,b.[_holds_ (_g_is_differentiable_in_x_&_diff_(g,x)_=_-_(((((diff_(f,].a,b.[))_._(0_+_1))_._x)_*_((b_-_x)_|^_0))_/_(0_!))_) let x be Real; ::_thesis: ( x in ].a,b.[ implies ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) assume A39: x in ].a,b.[ ; ::_thesis: ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) thus g is_differentiable_in x by A38, A39, FDIFF_1:9; ::_thesis: diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) thus diff (g,x) = (g `| ].a,b.[) . x by A38, A39, FDIFF_1:def_7 .= ((g | ].a,b.[) `| ].a,b.[) . x by A38, FDIFF_2:16 .= ((y * f) `| ].a,b.[) . x by A37, A27, FDIFF_2:16 .= diff ((y * f),x) by A27, A39, FDIFF_1:def_7 .= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) by A21, A39 ; ::_thesis: verum end; hence for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ; ::_thesis: verum end; A40: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A41: S1[k] ; ::_thesis: S1[k + 1] assume A42: f is_differentiable_on k + 1,Z ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ implies for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) ) assume that A43: a < b and A44: [.a,b.] c= Z and A45: ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous and A46: f is_differentiable_on (k + 1) + 1,].a,b.[ ; ::_thesis: for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) k <= (k + 1) - 1 ; then (diff (f,Z)) . k is_differentiable_on Z by A42, Def6; then ((diff (f,Z)) . k) | Z is continuous by FDIFF_1:25; then A47: ((diff (f,Z)) . k) | [.a,b.] is continuous by A44, FCONT_1:16; A48: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A49: ].a,b.[ c= Z by A44, XBOOLE_1:1; consider gk being PartFunc of REAL,REAL such that A50: dom gk = Z and A51: for x being Real st x in Z holds gk . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . k) by Lm7; A52: f is_differentiable_on k + 1,].a,b.[ by A46, Th23, NAT_1:11; then A53: gk is_differentiable_on ].a,b.[ by A41, A42, A43, A44, A47, A50, A51, Th23, NAT_1:11; A54: gk | [.a,b.] is continuous by A41, A42, A43, A44, A47, A52, A50, A51, Th23, NAT_1:11; now__::_thesis:_for_gk1_being_PartFunc_of_REAL,REAL_st_dom_gk1_=_Z_&_(_for_x_being_Real_st_x_in_Z_holds_ gk1_._x_=_(f_._b)_-_((Partial_Sums_(Taylor_(f,Z,x,b)))_._(k_+_1))_)_holds_ (_gk1_._b_=_0_&_gk1_|_[.a,b.]_is_continuous_&_gk1_is_differentiable_on_].a,b.[_&_(_for_x_being_Real_st_x_in_].a,b.[_holds_ diff_(gk1,x)_=_-_(((((diff_(f,].a,b.[))_._((k_+_1)_+_1))_._x)_*_((b_-_x)_|^_(k_+_1)))_/_((k_+_1)_!))_)_) k <= (k + 1) - 1 ; then A55: (diff (f,Z)) . k is_differentiable_on Z by A42, Def6; k <= ((k + 1) + 1) - 1 by NAT_1:11; then A56: (diff (f,].a,b.[)) . k is_differentiable_on ].a,b.[ by A46, Def6; A57: (diff (f,Z)) . (k + 1) = ((diff (f,Z)) . k) `| Z by Def5; let gk1 be PartFunc of REAL,REAL; ::_thesis: ( dom gk1 = Z & ( for x being Real st x in Z holds gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) implies ( gk1 . b = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) ) assume that A58: dom gk1 = Z and A59: for x being Real st x in Z holds gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ; ::_thesis: ( gk1 . b = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) A60: b in [.a,b.] by A43, XXREAL_1:1; then gk1 . b = (f . b) - ((Partial_Sums (Taylor (f,Z,b,b))) . (k + 1)) by A44, A59 .= (f . b) - (((Partial_Sums (Taylor (f,Z,b,b))) . k) + ((Taylor (f,Z,b,b)) . (k + 1))) by SERIES_1:def_1 .= ((f . b) - ((Partial_Sums (Taylor (f,Z,b,b))) . k)) - ((Taylor (f,Z,b,b)) . (k + 1)) .= (gk . b) - ((Taylor (f,Z,b,b)) . (k + 1)) by A44, A51, A60 .= 0 - ((Taylor (f,Z,b,b)) . (k + 1)) by A41, A42, A43, A44, A47, A52, A50, A51, Th23, NAT_1:11 .= 0 - (((((diff (f,Z)) . (k + 1)) . b) * ((b - b) |^ (k + 1))) / ((k + 1) !)) by Def7 .= 0 - (((((diff (f,Z)) . (k + 1)) . b) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6 .= 0 ; hence gk1 . b = 0 ; ::_thesis: ( gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) consider h being PartFunc of REAL,REAL such that A61: dom h = [#] REAL and A62: for x being Real holds h . x = (1 * ((b - x) |^ (k + 1))) / ((k + 1) !) and A63: for x being Real holds ( h is_differentiable_in x & diff (h,x) = - ((1 * ((b - x) |^ k)) / (k !)) ) by Lm6; A64: dom (((diff (f,Z)) . (k + 1)) (#) h) = (dom ((diff (f,Z)) . (k + 1))) /\ (dom h) by VALUED_1:def_4 .= Z /\ REAL by A61, A57, A55, FDIFF_1:def_7 .= Z by XBOOLE_1:28 ; A65: dom (gk - (((diff (f,Z)) . (k + 1)) (#) h)) = (dom gk) /\ (dom (((diff (f,Z)) . (k + 1)) (#) h)) by VALUED_1:12 .= Z by A50, A64 ; thus gk1 | [.a,b.] is continuous ::_thesis: ( gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) proof set ghk = gk - (((diff (f,Z)) . (k + 1)) (#) h); for x being Real st x in REAL holds h is_differentiable_in x by A63; then h is_differentiable_on REAL by A61, FDIFF_1:9; then h | REAL is continuous by FDIFF_1:25; then A66: h | [.a,b.] is continuous by FCONT_1:16; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ gk1_._x_=_(gk_-_(((diff_(f,Z))_._(k_+_1))_(#)_h))_._x let x be Real; ::_thesis: ( x in Z implies gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x ) assume A67: x in Z ; ::_thesis: gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x thus gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) by A59, A67 .= (f . b) - (((Partial_Sums (Taylor (f,Z,x,b))) . k) + ((Taylor (f,Z,x,b)) . (k + 1))) by SERIES_1:def_1 .= ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . k)) - ((Taylor (f,Z,x,b)) . (k + 1)) .= (gk . x) - ((Taylor (f,Z,x,b)) . (k + 1)) by A51, A67 .= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) by Def7 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((b - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A62 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5 .= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A65, A67, VALUED_1:13 ; ::_thesis: verum end; then A68: gk1 = gk - (((diff (f,Z)) . (k + 1)) (#) h) by A58, A65, PARTFUN1:5; [.a,b.] c= dom ((diff (f,Z)) . (k + 1)) by A44, A57, A55, FDIFF_1:def_7; then (((diff (f,Z)) . (k + 1)) (#) h) | ([.a,b.] /\ [.a,b.]) is continuous by A45, A61, A66, FCONT_1:19; hence gk1 | [.a,b.] is continuous by A44, A50, A54, A64, A68, FCONT_1:19; ::_thesis: verum end; A69: (diff (f,].a,b.[)) . (k + 1) = ((diff (f,].a,b.[)) . k) `| ].a,b.[ by Def5; set gfh = gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h); A70: dom (((diff (f,].a,b.[)) . (k + 1)) (#) h) = (dom ((diff (f,].a,b.[)) . (k + 1))) /\ (dom h) by VALUED_1:def_4 .= ].a,b.[ /\ REAL by A61, A69, A56, FDIFF_1:def_7 .= ].a,b.[ by XBOOLE_1:28 ; then A71: dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = Z /\ ].a,b.[ by A50, VALUED_1:12 .= ].a,b.[ by A44, A48, XBOOLE_1:1, XBOOLE_1:28 ; A72: for x being Real st x in ].a,b.[ holds (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x proof let x be Real; ::_thesis: ( x in ].a,b.[ implies (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x ) assume A73: x in ].a,b.[ ; ::_thesis: (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x thus (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x = (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) (#) h) . x) by A71, A73, VALUED_1:13 .= (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (h . x)) by VALUED_1:5 .= (gk . x) - (((((diff (f,Z)) . (k + 1)) | ].a,b.[) . x) * (h . x)) by A42, A43, A44, A48, Th24, XBOOLE_1:1 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A73, FUNCT_1:49 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5 .= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A49, A65, A73, VALUED_1:13 ; ::_thesis: verum end; A74: now__::_thesis:_for_xx_being_set_st_xx_in_dom_(gk_-_(((diff_(f,].a,b.[))_._(k_+_1))_(#)_h))_holds_ gk1_._xx_=_(gk_-_(((diff_(f,].a,b.[))_._(k_+_1))_(#)_h))_._xx let xx be set ; ::_thesis: ( xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) implies gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx ) assume A75: xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) ; ::_thesis: gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx reconsider x = xx as Real by A75; thus gk1 . xx = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) by A49, A59, A71, A75 .= (f . b) - (((Partial_Sums (Taylor (f,Z,x,b))) . k) + ((Taylor (f,Z,x,b)) . (k + 1))) by SERIES_1:def_1 .= ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . k)) - ((Taylor (f,Z,x,b)) . (k + 1)) .= (gk . x) - ((Taylor (f,Z,x,b)) . (k + 1)) by A49, A51, A71, A75 .= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) by Def7 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((b - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A62 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5 .= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A49, A65, A71, A75, VALUED_1:13 .= (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx by A71, A72, A75 ; ::_thesis: verum end; k + 1 <= ((k + 1) + 1) - 1 ; then A76: (diff (f,].a,b.[)) . (k + 1) is_differentiable_on ].a,b.[ by A46, Def6; for x being Real st x in ].a,b.[ holds h is_differentiable_in x by A63; then A77: h is_differentiable_on ].a,b.[ by A61, FDIFF_1:9; then A78: ((diff (f,].a,b.[)) . (k + 1)) (#) h is_differentiable_on ].a,b.[ by A70, A76, FDIFF_1:21; then A79: gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h) is_differentiable_on ].a,b.[ by A53, A71, FDIFF_1:19; dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = (dom gk1) /\ ].a,b.[ by A44, A48, A58, A71, XBOOLE_1:1, XBOOLE_1:28; then A80: (gk1 | ].a,b.[) | ].a,b.[ = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ by A74, FUNCT_1:46; then (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ = gk1 | ].a,b.[ by FUNCT_1:51; then for x being Real st x in ].a,b.[ holds gk1 | ].a,b.[ is_differentiable_in x by A79, FDIFF_1:def_6; hence A81: gk1 is_differentiable_on ].a,b.[ by A49, A58, FDIFF_1:def_6; ::_thesis: for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) now__::_thesis:_for_x_being_Real_st_x_in_].a,b.[_holds_ diff_(gk1,x)_=_-_(((((diff_(f,].a,b.[))_._((k_+_1)_+_1))_._x)_*_((b_-_x)_|^_(k_+_1)))_/_((k_+_1)_!)) let x be Real; ::_thesis: ( x in ].a,b.[ implies diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) assume A82: x in ].a,b.[ ; ::_thesis: diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) thus diff (gk1,x) = (gk1 `| ].a,b.[) . x by A81, A82, FDIFF_1:def_7 .= ((gk1 | ].a,b.[) `| ].a,b.[) . x by A81, FDIFF_2:16 .= (((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[) `| ].a,b.[) . x by A80, FUNCT_1:51 .= ((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) `| ].a,b.[) . x by A79, FDIFF_2:16 .= (diff (gk,x)) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A53, A71, A78, A82, FDIFF_1:19 .= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A41, A42, A43, A44, A47, A52, A50, A51, A82, Th23, NAT_1:11 .= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (((((diff (f,].a,b.[)) . (k + 1)) (#) h) `| ].a,b.[) . x) by A78, A82, FDIFF_1:def_7 .= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x)))) by A70, A76, A77, A82, FDIFF_1:21 .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - ((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x))) .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (((1 * ((b - x) |^ (k + 1))) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x))) by A62 .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (- ((1 * ((b - x) |^ k)) / (k !)))) by A63 .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * ((1 * ((b - x) |^ k)) / (k !)))) - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) + (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) by XCMPLX_1:74 .= - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) .= - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * ((((diff (f,].a,b.[)) . (k + 1)) `| ].a,b.[) . x)) by A76, A82, FDIFF_1:def_7 .= - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (((diff (f,].a,b.[)) . ((k + 1) + 1)) . x)) by Def5 .= - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) by XCMPLX_1:74 ; ::_thesis: verum end; hence for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ; ::_thesis: verum end; hence for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A40); hence for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) holds ( g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) ; ::_thesis: verum end; Lm9: for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) ) assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) ) assume A2: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) consider g being PartFunc of REAL,REAL such that A3: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) by Lm7; take g ; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) thus ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) by A1, A2, A3, Lm8; ::_thesis: verum end; theorem Th25: :: TAYLOR_1:25 for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) ) assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) ) assume that A2: a < b and A3: [.a,b.] c= Z and A4: ( ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) let l be Real; ::_thesis: for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) consider p being PartFunc of REAL,REAL such that A5: dom p = [#] REAL and A6: for x being Real holds p . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) and A7: for x being Real holds ( p is_differentiable_in x & diff (p,x) = - ((l * ((b - x) |^ n)) / (n !)) ) by Lm6; consider h being PartFunc of REAL,REAL such that A8: dom h = Z and A9: for x being Real st x in Z holds h . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) and A10: h . b = 0 and A11: h | [.a,b.] is continuous and A12: h is_differentiable_on ].a,b.[ and A13: for x being Real st x in ].a,b.[ holds diff (h,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) by A1, A2, A3, A4, Lm9; A14: [.a,b.] c= (dom h) /\ (dom p) by A3, A8, A5, XBOOLE_1:19; let g be PartFunc of REAL,REAL; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 implies ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) ) assume that A15: dom g = [#] REAL and A16: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) and A17: ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 ; ::_thesis: ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) set hp = h - p; A18: dom (h - p) = (dom h) /\ (dom p) by VALUED_1:12 .= Z by A8, A5, XBOOLE_1:28 ; A19: for x being set st x in dom (h - p) holds (h - p) . x = g . x proof let x be set ; ::_thesis: ( x in dom (h - p) implies (h - p) . x = g . x ) assume A20: x in dom (h - p) ; ::_thesis: (h - p) . x = g . x reconsider xx = x as Real by A20; thus (h - p) . x = (h . xx) - (p . xx) by A20, VALUED_1:13 .= ((f . b) - ((Partial_Sums (Taylor (f,Z,xx,b))) . n)) - (p . xx) by A9, A18, A20 .= ((f . b) - ((Partial_Sums (Taylor (f,Z,xx,b))) . n)) - ((l * ((b - xx) |^ (n + 1))) / ((n + 1) !)) by A6 .= g . x by A16 ; ::_thesis: verum end; for x being Real st x in REAL holds p is_differentiable_in x by A7; then p is_differentiable_on REAL by A5, FDIFF_1:9; then p | REAL is continuous by FDIFF_1:25; then A21: p | [.a,b.] is continuous by FCONT_1:16; ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A22: ].a,b.[ c= Z by A3, XBOOLE_1:1; A23: dom (h - p) = (dom g) /\ Z by A15, A18, XBOOLE_1:28; then A24: (h - p) | ].a,b.[ = (g | Z) | ].a,b.[ by A19, FUNCT_1:46 .= g | ].a,b.[ by A22, FUNCT_1:51 ; A25: for x being Real st x in ].a,b.[ holds ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) proof let x be Real; ::_thesis: ( x in ].a,b.[ implies ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) assume A26: x in ].a,b.[ ; ::_thesis: ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) A27: h is_differentiable_in x by A12, A26, FDIFF_1:9; A28: p is_differentiable_in x by A7; hence h - p is_differentiable_in x by A27, FDIFF_1:14; ::_thesis: diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) thus diff ((h - p),x) = (diff (h,x)) - (diff (p,x)) by A27, A28, FDIFF_1:14 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) - (diff (p,x)) by A13, A26 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) - (- ((l * ((b - x) |^ n)) / (n !))) by A7 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ; ::_thesis: verum end; then for x being Real st x in ].a,b.[ holds h - p is_differentiable_in x ; then A29: h - p is_differentiable_on ].a,b.[ by A18, A22, FDIFF_1:9; then for x being Real st x in ].a,b.[ holds (h - p) | ].a,b.[ is_differentiable_in x by FDIFF_1:def_6; hence A30: g is_differentiable_on ].a,b.[ by A15, A24, FDIFF_1:def_6; ::_thesis: ( g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) thus g . a = 0 by A16, A17; ::_thesis: ( g . b = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) A31: b in [.a,b.] by A2, XXREAL_1:1; then g . b = (h - p) . b by A3, A18, A19 .= (h . b) - (p . b) by A3, A18, A31, VALUED_1:13 .= 0 - ((l * ((b - b) |^ (n + 1))) / ((n + 1) !)) by A10, A6 .= 0 - ((l * ((0 |^ n) * 0)) / ((n + 1) !)) by NEWTON:6 .= 0 ; hence g . b = 0 ; ::_thesis: ( g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) ) (h - p) | [.a,b.] = (g | Z) | [.a,b.] by A23, A19, FUNCT_1:46 .= g | [.a,b.] by A3, FUNCT_1:51 ; hence g | [.a,b.] is continuous by A11, A14, A21, FCONT_1:18; ::_thesis: for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) thus for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ::_thesis: verum proof let x be Real; ::_thesis: ( x in ].a,b.[ implies diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ) assume A32: x in ].a,b.[ ; ::_thesis: diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) thus diff (g,x) = (g `| ].a,b.[) . x by A30, A32, FDIFF_1:def_7 .= ((g | ].a,b.[) `| ].a,b.[) . x by A30, FDIFF_2:16 .= ((h - p) `| ].a,b.[) . x by A24, A29, FDIFF_2:16 .= diff ((h - p),x) by A29, A32, FDIFF_1:def_7 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) by A25, A32 ; ::_thesis: verum end; end; theorem Th26: :: TAYLOR_1:26 for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL for b, l being Real ex g being Function of REAL,REAL st for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL for b, l being Real ex g being Function of REAL,REAL st for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for b, l being Real ex g being Function of REAL,REAL st for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) let Z be Subset of REAL; ::_thesis: for b, l being Real ex g being Function of REAL,REAL st for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) let b, l be Real; ::_thesis: ex g being Function of REAL,REAL st for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) deffunc H1( Real) -> Element of REAL = ((f . b) - ((Partial_Sums (Taylor (f,Z,\$1,b))) . n)) - ((l * ((b - \$1) |^ (n + 1))) / ((n + 1) !)); consider g being Function of REAL,REAL such that A1: for d being Element of REAL holds g . d = H1(d) from FUNCT_2:sch_4(); take g ; ::_thesis: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) thus for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) by A1; ::_thesis: verum end; theorem Th27: :: TAYLOR_1:27 for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) ) assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) ) assume that A2: a < b and A3: ( [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) b - a <> 0 by A2; then A4: (b - a) |^ (n + 1) <> 0 by CARD_4:3; deffunc H1( Real) -> Element of REAL = (f . b) - ((Partial_Sums (Taylor (f,Z,\$1,b))) . n); reconsider l = H1(a) / (((b - a) |^ (n + 1)) / ((n + 1) !)) as Real ; consider g being Function of REAL,REAL such that A5: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) by Th26; A6: ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = H1(a) - ((H1(a) / (((b - a) |^ (n + 1)) / ((n + 1) !))) * (((b - a) |^ (n + 1)) / ((n + 1) !))) by XCMPLX_1:74 .= H1(a) - H1(a) by A4, XCMPLX_1:50, XCMPLX_1:87 .= 0 ; then A7: g . a = 0 by A5; A8: dom g = REAL by FUNCT_2:def_1; then A9: g | [.a,b.] is continuous by A1, A2, A3, A5, A6, Th25; ( g is_differentiable_on ].a,b.[ & g . b = 0 ) by A1, A2, A3, A5, A6, A8, Th25; then consider c being Real such that A10: c in ].a,b.[ and A11: diff (g,c) = 0 by A2, A8, A7, A9, ROLLE:1; c in { r where r is Real : ( a < r & r < b ) } by A10, RCOMP_1:def_2; then ex r being Real st ( c = r & a < r & r < b ) ; then b - c <> 0 ; then A12: (b - c) |^ n <> 0 by CARD_4:3; dom g = REAL by FUNCT_2:def_1; then (- (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / (n !))) + ((l * ((b - c) |^ n)) / (n !)) = 0 by A1, A2, A3, A5, A6, A10, A11, Th25; then ((((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / (n !)) * (n !)) - (((l * ((b - c) |^ n)) / (n !)) * (n !)) = 0 ; then ((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) - (((l * ((b - c) |^ n)) / (n !)) * (n !)) = 0 by XCMPLX_1:87; then (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) - (l * ((b - c) |^ n))) / ((b - c) |^ n) = 0 / ((b - c) |^ n) by XCMPLX_1:87; then (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / ((b - c) |^ n)) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by XCMPLX_1:120; then (((diff (f,].a,b.[)) . (n + 1)) . c) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by A12, XCMPLX_1:89; then ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 by A6, A12, XCMPLX_1:89; then f . b = (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) + ((Partial_Sums (Taylor (f,Z,a,b))) . n) ; hence ex c being Real st ( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) by A10; ::_thesis: verum end; Lm10: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f holds for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f holds for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f implies for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) ) assume A1: Z c= dom f ; ::_thesis: for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) defpred S1[ Element of NAT ] means ( f is_differentiable_on \$1,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . \$1) | [.a,b.] is continuous & f is_differentiable_on \$1 + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . \$1) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (\$1 + 1)) . x) * ((a - x) |^ \$1)) / (\$1 !)) ) ) ); A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] assume A4: f is_differentiable_on k + 1,Z ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ implies for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) ) assume that A5: a < b and A6: [.a,b.] c= Z and A7: ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous and A8: f is_differentiable_on (k + 1) + 1,].a,b.[ ; ::_thesis: for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) k <= (k + 1) - 1 ; then (diff (f,Z)) . k is_differentiable_on Z by A4, Def6; then ((diff (f,Z)) . k) | Z is continuous by FDIFF_1:25; then A9: ((diff (f,Z)) . k) | [.a,b.] is continuous by A6, FCONT_1:16; A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A11: ].a,b.[ c= Z by A6, XBOOLE_1:1; consider gk being PartFunc of REAL,REAL such that A12: dom gk = Z and A13: for x being Real st x in Z holds gk . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k) by Lm7; A14: f is_differentiable_on k + 1,].a,b.[ by A8, Th23, NAT_1:11; then A15: gk is_differentiable_on ].a,b.[ by A3, A4, A5, A6, A9, A12, A13, Th23, NAT_1:11; A16: gk | [.a,b.] is continuous by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1:11; now__::_thesis:_for_gk1_being_PartFunc_of_REAL,REAL_st_dom_gk1_=_Z_&_(_for_x_being_Real_st_x_in_Z_holds_ gk1_._x_=_(f_._a)_-_((Partial_Sums_(Taylor_(f,Z,x,a)))_._(k_+_1))_)_holds_ (_gk1_._a_=_0_&_gk1_|_[.a,b.]_is_continuous_&_gk1_is_differentiable_on_].a,b.[_&_(_for_x_being_Real_st_x_in_].a,b.[_holds_ diff_(gk1,x)_=_-_(((((diff_(f,].a,b.[))_._((k_+_1)_+_1))_._x)_*_((a_-_x)_|^_(k_+_1)))_/_((k_+_1)_!))_)_) k <= (k + 1) - 1 ; then A17: (diff (f,Z)) . k is_differentiable_on Z by A4, Def6; k <= ((k + 1) + 1) - 1 by NAT_1:11; then A18: (diff (f,].a,b.[)) . k is_differentiable_on ].a,b.[ by A8, Def6; A19: (diff (f,Z)) . (k + 1) = ((diff (f,Z)) . k) `| Z by Def5; let gk1 be PartFunc of REAL,REAL; ::_thesis: ( dom gk1 = Z & ( for x being Real st x in Z holds gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) implies ( gk1 . a = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) ) assume that A20: dom gk1 = Z and A21: for x being Real st x in Z holds gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ; ::_thesis: ( gk1 . a = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) A22: a in [.a,b.] by A5, XXREAL_1:1; then gk1 . a = (f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . (k + 1)) by A6, A21 .= (f . a) - (((Partial_Sums (Taylor (f,Z,a,a))) . k) + ((Taylor (f,Z,a,a)) . (k + 1))) by SERIES_1:def_1 .= ((f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . k)) - ((Taylor (f,Z,a,a)) . (k + 1)) .= (gk . a) - ((Taylor (f,Z,a,a)) . (k + 1)) by A6, A13, A22 .= 0 - ((Taylor (f,Z,a,a)) . (k + 1)) by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1:11 .= 0 - (((((diff (f,Z)) . (k + 1)) . a) * ((a - a) |^ (k + 1))) / ((k + 1) !)) by Def7 .= 0 - (((((diff (f,Z)) . (k + 1)) . a) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6 .= 0 ; hence gk1 . a = 0 ; ::_thesis: ( gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) consider h being PartFunc of REAL,REAL such that A23: dom h = [#] REAL and A24: for x being Real holds h . x = (1 * ((a - x) |^ (k + 1))) / ((k + 1) !) and A25: for x being Real holds ( h is_differentiable_in x & diff (h,x) = - ((1 * ((a - x) |^ k)) / (k !)) ) by Lm6; A26: dom (((diff (f,Z)) . (k + 1)) (#) h) = (dom ((diff (f,Z)) . (k + 1))) /\ (dom h) by VALUED_1:def_4 .= Z /\ REAL by A23, A19, A17, FDIFF_1:def_7 .= Z by XBOOLE_1:28 ; A27: dom (gk - (((diff (f,Z)) . (k + 1)) (#) h)) = (dom gk) /\ (dom (((diff (f,Z)) . (k + 1)) (#) h)) by VALUED_1:12 .= Z by A12, A26 ; thus gk1 | [.a,b.] is continuous ::_thesis: ( gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) proof set ghk = gk - (((diff (f,Z)) . (k + 1)) (#) h); for x being Real st x in REAL holds h is_differentiable_in x by A25; then h is_differentiable_on REAL by A23, FDIFF_1:9; then h | REAL is continuous by FDIFF_1:25; then A28: h | [.a,b.] is continuous by FCONT_1:16; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ gk1_._x_=_(gk_-_(((diff_(f,Z))_._(k_+_1))_(#)_h))_._x let x be Real; ::_thesis: ( x in Z implies gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x ) assume A29: x in Z ; ::_thesis: gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x thus gk1 . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) by A21, A29 .= (f . a) - (((Partial_Sums (Taylor (f,Z,x,a))) . k) + ((Taylor (f,Z,x,a)) . (k + 1))) by SERIES_1:def_1 .= ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k)) - ((Taylor (f,Z,x,a)) . (k + 1)) .= (gk . x) - ((Taylor (f,Z,x,a)) . (k + 1)) by A13, A29 .= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) by Def7 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A24 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5 .= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A27, A29, VALUED_1:13 ; ::_thesis: verum end; then A30: gk1 = gk - (((diff (f,Z)) . (k + 1)) (#) h) by A20, A27, PARTFUN1:5; [.a,b.] c= dom ((diff (f,Z)) . (k + 1)) by A6, A19, A17, FDIFF_1:def_7; then (((diff (f,Z)) . (k + 1)) (#) h) | ([.a,b.] /\ [.a,b.]) is continuous by A7, A23, A28, FCONT_1:19; hence gk1 | [.a,b.] is continuous by A6, A12, A16, A26, A30, FCONT_1:19; ::_thesis: verum end; A31: (diff (f,].a,b.[)) . (k + 1) = ((diff (f,].a,b.[)) . k) `| ].a,b.[ by Def5; set gfh = gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h); A32: dom (((diff (f,].a,b.[)) . (k + 1)) (#) h) = (dom ((diff (f,].a,b.[)) . (k + 1))) /\ (dom h) by VALUED_1:def_4 .= ].a,b.[ /\ REAL by A23, A31, A18, FDIFF_1:def_7 .= ].a,b.[ by XBOOLE_1:28 ; A33: dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = Z /\ (dom (((diff (f,].a,b.[)) . (k + 1)) (#) h)) by A12, VALUED_1:12 .= ].a,b.[ by A6, A10, A32, XBOOLE_1:1, XBOOLE_1:28 ; A34: for x being Real st x in ].a,b.[ holds (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x proof let x be Real; ::_thesis: ( x in ].a,b.[ implies (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x ) assume A35: x in ].a,b.[ ; ::_thesis: (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x thus (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x = (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) (#) h) . x) by A33, A35, VALUED_1:13 .= (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (h . x)) by VALUED_1:5 .= (gk . x) - (((((diff (f,Z)) . (k + 1)) | ].a,b.[) . x) * (h . x)) by A4, A5, A6, A10, Th24, XBOOLE_1:1 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A35, FUNCT_1:49 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5 .= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A11, A27, A35, VALUED_1:13 ; ::_thesis: verum end; A36: now__::_thesis:_for_xx_being_set_st_xx_in_dom_(gk_-_(((diff_(f,].a,b.[))_._(k_+_1))_(#)_h))_holds_ gk1_._xx_=_(gk_-_(((diff_(f,].a,b.[))_._(k_+_1))_(#)_h))_._xx let xx be set ; ::_thesis: ( xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) implies gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx ) assume A37: xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) ; ::_thesis: gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx reconsider x = xx as Real by A37; thus gk1 . xx = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) by A11, A21, A33, A37 .= (f . a) - (((Partial_Sums (Taylor (f,Z,x,a))) . k) + ((Taylor (f,Z,x,a)) . (k + 1))) by SERIES_1:def_1 .= ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k)) - ((Taylor (f,Z,x,a)) . (k + 1)) .= (gk . x) - ((Taylor (f,Z,x,a)) . (k + 1)) by A11, A13, A33, A37 .= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) by Def7 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A24 .= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5 .= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A11, A27, A33, A37, VALUED_1:13 .= (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx by A33, A34, A37 ; ::_thesis: verum end; k + 1 <= ((k + 1) + 1) - 1 ; then A38: (diff (f,].a,b.[)) . (k + 1) is_differentiable_on ].a,b.[ by A8, Def6; for x being Real st x in ].a,b.[ holds h is_differentiable_in x by A25; then A39: h is_differentiable_on ].a,b.[ by A23, FDIFF_1:9; then A40: ((diff (f,].a,b.[)) . (k + 1)) (#) h is_differentiable_on ].a,b.[ by A32, A38, FDIFF_1:21; then A41: gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h) is_differentiable_on ].a,b.[ by A15, A33, FDIFF_1:19; dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = (dom gk1) /\ ].a,b.[ by A6, A10, A20, A33, XBOOLE_1:1, XBOOLE_1:28; then A42: (gk1 | ].a,b.[) | ].a,b.[ = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ by A36, FUNCT_1:46; then (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ = gk1 | ].a,b.[ by FUNCT_1:51; then for x being Real st x in ].a,b.[ holds gk1 | ].a,b.[ is_differentiable_in x by A41, FDIFF_1:def_6; hence A43: gk1 is_differentiable_on ].a,b.[ by A11, A20, FDIFF_1:def_6; ::_thesis: for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) now__::_thesis:_for_x_being_Real_st_x_in_].a,b.[_holds_ diff_(gk1,x)_=_-_(((((diff_(f,].a,b.[))_._((k_+_1)_+_1))_._x)_*_((a_-_x)_|^_(k_+_1)))_/_((k_+_1)_!)) let x be Real; ::_thesis: ( x in ].a,b.[ implies diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) assume A44: x in ].a,b.[ ; ::_thesis: diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) thus diff (gk1,x) = (gk1 `| ].a,b.[) . x by A43, A44, FDIFF_1:def_7 .= ((gk1 | ].a,b.[) `| ].a,b.[) . x by A43, FDIFF_2:16 .= (((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[) `| ].a,b.[) . x by A42, FUNCT_1:51 .= ((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) `| ].a,b.[) . x by A41, FDIFF_2:16 .= (diff (gk,x)) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A15, A33, A40, A44, FDIFF_1:19 .= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A3, A4, A5, A6, A9, A14, A12, A13, A44, Th23, NAT_1:11 .= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((((diff (f,].a,b.[)) . (k + 1)) (#) h) `| ].a,b.[) . x) by A40, A44, FDIFF_1:def_7 .= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x)))) by A32, A38, A39, A44, FDIFF_1:21 .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - ((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x))) .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((1 * ((a - x) |^ (k + 1))) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x))) by A24 .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (- ((1 * ((a - x) |^ k)) / (k !)))) by A25 .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * ((1 * ((a - x) |^ k)) / (k !)))) - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) .= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) + (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) by XCMPLX_1:74 .= - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) .= - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * ((((diff (f,].a,b.[)) . (k + 1)) `| ].a,b.[) . x)) by A38, A44, FDIFF_1:def_7 .= - ((((a - x) |^ (k + 1)) / ((k + 1) !)) * (((diff (f,].a,b.[)) . ((k + 1) + 1)) . x)) by Def5 .= - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) by XCMPLX_1:74 ; ::_thesis: verum end; hence for x being Real st x in ].a,b.[ holds diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ; ::_thesis: verum end; hence for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) !)) ) ) ; ::_thesis: verum end; A45: S1[ 0 ] proof assume f is_differentiable_on 0 ,Z ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ implies for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) ) assume that A46: a < b and A47: [.a,b.] c= Z and A48: ((diff (f,Z)) . 0) | [.a,b.] is continuous and A49: f is_differentiable_on 0 + 1,].a,b.[ ; ::_thesis: for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) A50: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A51: ].a,b.[ c= Z by A47, XBOOLE_1:1; let g be PartFunc of REAL,REAL; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ) implies ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) ) assume that A52: dom g = Z and A53: for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) ; ::_thesis: ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) A54: a in [.a,b.] by A46, XXREAL_1:1; hence g . a = (f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . 0) by A47, A53 .= (f . a) - ((Taylor (f,Z,a,a)) . 0) by SERIES_1:def_1 .= (f . a) - (((((diff (f,Z)) . 0) . a) * ((a - a) |^ 0)) / (0 !)) by Def7 .= (f . a) - ((((f | Z) . a) * ((a - a) |^ 0)) / (0 !)) by Def5 .= (f . a) - (((f . a) * ((a - a) |^ 0)) / (0 !)) by A47, A54, FUNCT_1:49 .= (f . a) - ((f . a) * 1) by NEWTON:4, NEWTON:12 .= 0 ; ::_thesis: ( g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) consider y being PartFunc of REAL,REAL such that A55: dom y = [#] REAL and A56: for x being Real holds y . x = (f . a) - x and A57: for x being Real holds ( y is_differentiable_in x & diff (y,x) = - 1 ) by Lm5; rng f c= REAL ; then A58: dom (y * f) = dom f by A55, RELAT_1:27; for x being Real st x in REAL holds y is_differentiable_in x by A57; then y is_differentiable_on REAL by A55, FDIFF_1:9; then y | REAL is continuous by FDIFF_1:25; then A59: y | (f .: [.a,b.]) is continuous by FCONT_1:16; rng f c= dom y by A55; then A60: dom (y * f) = dom f by RELAT_1:27; A61: [.a,b.] c= dom f by A1, A47, XBOOLE_1:1; then A62: ].a,b.[ c= dom f by A50, XBOOLE_1:1; 0 <= (0 + 1) - 1 ; then (diff (f,].a,b.[)) . 0 is_differentiable_on ].a,b.[ by A49, Def6; then f | ].a,b.[ is_differentiable_on ].a,b.[ by Def5; then for x being Real st x in ].a,b.[ holds f | ].a,b.[ is_differentiable_in x by FDIFF_1:9; then A63: f is_differentiable_on ].a,b.[ by A62, FDIFF_1:def_6; A64: for x being Real st x in ].a,b.[ holds ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) proof A65: (diff (f,].a,b.[)) . (0 + 1) = ((diff (f,].a,b.[)) . 0) `| ].a,b.[ by Def5 .= (f | ].a,b.[) `| ].a,b.[ by Def5 .= f `| ].a,b.[ by A63, FDIFF_2:16 ; let x be Real; ::_thesis: ( x in ].a,b.[ implies ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) assume A66: x in ].a,b.[ ; ::_thesis: ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) A67: f is_differentiable_in x by A63, A66, FDIFF_1:9; A68: y is_differentiable_in f . x by A57; hence y * f is_differentiable_in x by A67, FDIFF_2:13; ::_thesis: diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) A69: ((a - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12; thus diff ((y * f),x) = (diff (y,(f . x))) * (diff (f,x)) by A68, A67, FDIFF_2:13 .= (diff (y,(f . x))) * ((f `| ].a,b.[) . x) by A63, A66, FDIFF_1:def_7 .= (- 1) * (((diff (f,].a,b.[)) . (0 + 1)) . x) by A57, A65 .= - ((((diff (f,].a,b.[)) . (0 + 1)) . x) * (((a - x) |^ 0) / (0 !))) by A69 .= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) by XCMPLX_1:74 ; ::_thesis: verum end; then for x being Real st x in ].a,b.[ holds y * f is_differentiable_in x ; then A70: y * f is_differentiable_on ].a,b.[ by A62, A60, FDIFF_1:9; A71: dom ((y * f) | [.a,b.]) = (dom (y * f)) /\ [.a,b.] by RELAT_1:61 .= [.a,b.] by A1, A47, A58, XBOOLE_1:1, XBOOLE_1:28 .= Z /\ [.a,b.] by A47, XBOOLE_1:28 .= dom (g | [.a,b.]) by A52, RELAT_1:61 ; A72: now__::_thesis:_for_xx_being_set_st_xx_in_dom_(g_|_[.a,b.])_holds_ (g_|_[.a,b.])_._xx_=_((y_*_f)_|_[.a,b.])_._xx let xx be set ; ::_thesis: ( xx in dom (g | [.a,b.]) implies (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx ) assume A73: xx in dom (g | [.a,b.]) ; ::_thesis: (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx reconsider x = xx as Real by A73; dom (g | [.a,b.]) = (dom g) /\ [.a,b.] by RELAT_1:61; then dom (g | [.a,b.]) c= [.a,b.] by XBOOLE_1:17; then A74: x in [.a,b.] by A73; thus (g | [.a,b.]) . xx = g . x by A73, FUNCT_1:47 .= (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) by A47, A53, A74 .= (f . a) - ((Taylor (f,Z,x,a)) . 0) by SERIES_1:def_1 .= (f . a) - (((((diff (f,Z)) . 0) . x) * ((a - x) |^ 0)) / (0 !)) by Def7 .= (f . a) - ((((f | Z) . x) * ((a - x) |^ 0)) / (0 !)) by Def5 .= (f . a) - (((f . x) * ((a - x) |^ 0)) / (0 !)) by A47, A74, FUNCT_1:49 .= (f . a) - ((f . x) * 1) by NEWTON:4, NEWTON:12 .= y . (f . x) by A56 .= (y * f) . x by A61, A74, FUNCT_1:13 .= ((y * f) | [.a,b.]) . xx by A71, A73, FUNCT_1:47 ; ::_thesis: verum end; (f | Z) | [.a,b.] is continuous by A48, Def5; then ((f | Z) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:15; then (f | [.a,b.]) | [.a,b.] is continuous by A47, FUNCT_1:51; then f | [.a,b.] is continuous by FCONT_1:15; then (y * f) | [.a,b.] is continuous by A59, FCONT_1:25; hence g | [.a,b.] is continuous by A71, A72, FUNCT_1:2; ::_thesis: ( g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) A75: dom ((y * f) | ].a,b.[) = (dom (y * f)) /\ ].a,b.[ by RELAT_1:61 .= ].a,b.[ by A50, A61, A60, XBOOLE_1:1, XBOOLE_1:28 .= Z /\ ].a,b.[ by A47, A50, XBOOLE_1:1, XBOOLE_1:28 .= dom (g | ].a,b.[) by A52, RELAT_1:61 ; now__::_thesis:_for_xx_being_set_st_xx_in_dom_(g_|_].a,b.[)_holds_ (g_|_].a,b.[)_._xx_=_((y_*_f)_|_].a,b.[)_._xx let xx be set ; ::_thesis: ( xx in dom (g | ].a,b.[) implies (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx ) assume A76: xx in dom (g | ].a,b.[) ; ::_thesis: (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx reconsider x = xx as Real by A76; dom (g | ].a,b.[) = (dom g) /\ ].a,b.[ by RELAT_1:61; then dom (g | ].a,b.[) c= ].a,b.[ by XBOOLE_1:17; then A77: x in ].a,b.[ by A76; A78: ((a - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12; thus (g | ].a,b.[) . xx = g . x by A76, FUNCT_1:47 .= (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) by A53, A51, A77 .= (f . a) - ((Taylor (f,Z,x,a)) . 0) by SERIES_1:def_1 .= (f . a) - (((((diff (f,Z)) . 0) . x) * ((a - x) |^ 0)) / (0 !)) by Def7 .= (f . a) - ((((f | Z) . x) * ((a - x) |^ 0)) / (0 !)) by Def5 .= (f . a) - (((f . x) * ((a - x) |^ 0)) / (0 !)) by A51, A77, FUNCT_1:49 .= (f . a) - ((f . x) * (((a - x) |^ 0) / (0 !))) by XCMPLX_1:74 .= y . (f . x) by A56, A78 .= (y * f) . x by A62, A77, FUNCT_1:13 .= ((y * f) | ].a,b.[) . xx by A75, A76, FUNCT_1:47 ; ::_thesis: verum end; then A79: g | ].a,b.[ = (y * f) | ].a,b.[ by A75, FUNCT_1:2; then g | ].a,b.[ is_differentiable_on ].a,b.[ by A70, FDIFF_2:16; then for x being Real st x in ].a,b.[ holds g | ].a,b.[ is_differentiable_in x by FDIFF_1:9; hence A80: g is_differentiable_on ].a,b.[ by A52, A51, FDIFF_1:def_6; ::_thesis: for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) now__::_thesis:_for_x_being_Real_st_x_in_].a,b.[_holds_ (_g_is_differentiable_in_x_&_diff_(g,x)_=_-_(((((diff_(f,].a,b.[))_._(0_+_1))_._x)_*_((a_-_x)_|^_0))_/_(0_!))_) let x be Real; ::_thesis: ( x in ].a,b.[ implies ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) ) assume A81: x in ].a,b.[ ; ::_thesis: ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ) thus g is_differentiable_in x by A80, A81, FDIFF_1:9; ::_thesis: diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) thus diff (g,x) = (g `| ].a,b.[) . x by A80, A81, FDIFF_1:def_7 .= ((g | ].a,b.[) `| ].a,b.[) . x by A80, FDIFF_2:16 .= ((y * f) `| ].a,b.[) . x by A79, A70, FDIFF_2:16 .= diff ((y * f),x) by A70, A81, FDIFF_1:def_7 .= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) by A64, A81 ; ::_thesis: verum end; hence for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A45, A2); hence for n being Element of NAT st f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for g being PartFunc of REAL,REAL st dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) holds ( g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) ; ::_thesis: verum end; Lm11: for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) ) assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) ) assume A2: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex g being PartFunc of REAL,REAL st ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) consider g being PartFunc of REAL,REAL such that A3: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) ) by Lm7; take g ; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) thus ( dom g = Z & ( for x being Real st x in Z holds g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & g . a = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) ) ) by A1, A2, A3, Lm10; ::_thesis: verum end; theorem Th28: :: TAYLOR_1:28 for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) ) assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) ) assume that A2: a < b and A3: [.a,b.] c= Z and A4: ( ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: for l being Real for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) let l be Real; ::_thesis: for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) consider p being PartFunc of REAL,REAL such that A5: dom p = [#] REAL and A6: for x being Real holds p . x = (l * ((a - x) |^ (n + 1))) / ((n + 1) !) and A7: for x being Real holds ( p is_differentiable_in x & diff (p,x) = - ((l * ((a - x) |^ n)) / (n !)) ) by Lm6; consider h being PartFunc of REAL,REAL such that A8: dom h = Z and A9: for x being Real st x in Z holds h . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) and A10: h . a = 0 and A11: h | [.a,b.] is continuous and A12: h is_differentiable_on ].a,b.[ and A13: for x being Real st x in ].a,b.[ holds diff (h,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !)) by A1, A2, A3, A4, Lm11; A14: [.a,b.] c= (dom h) /\ (dom p) by A3, A8, A5, XBOOLE_1:19; let g be PartFunc of REAL,REAL; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 implies ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) ) assume that A15: dom g = [#] REAL and A16: for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) and A17: ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 ; ::_thesis: ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) set hp = h - p; A18: dom (h - p) = (dom h) /\ (dom p) by VALUED_1:12 .= Z by A8, A5, XBOOLE_1:28 ; A19: for x being set st x in dom (h - p) holds (h - p) . x = g . x proof let x be set ; ::_thesis: ( x in dom (h - p) implies (h - p) . x = g . x ) assume A20: x in dom (h - p) ; ::_thesis: (h - p) . x = g . x reconsider xx = x as Real by A20; thus (h - p) . x = (h . xx) - (p . xx) by A20, VALUED_1:13 .= ((f . a) - ((Partial_Sums (Taylor (f,Z,xx,a))) . n)) - (p . xx) by A9, A18, A20 .= ((f . a) - ((Partial_Sums (Taylor (f,Z,xx,a))) . n)) - ((l * ((a - xx) |^ (n + 1))) / ((n + 1) !)) by A6 .= g . x by A16 ; ::_thesis: verum end; for x being Real st x in REAL holds p is_differentiable_in x by A7; then p is_differentiable_on REAL by A5, FDIFF_1:9; then p | REAL is continuous by FDIFF_1:25; then A21: p | [.a,b.] is continuous by FCONT_1:16; ].a,b.[ c= [.a,b.] by XXREAL_1:25; then A22: ].a,b.[ c= Z by A3, XBOOLE_1:1; A23: dom (h - p) = (dom g) /\ Z by A15, A18, XBOOLE_1:28; then A24: (h - p) | ].a,b.[ = (g | Z) | ].a,b.[ by A19, FUNCT_1:46 .= g | ].a,b.[ by A22, FUNCT_1:51 ; A25: for x being Real st x in ].a,b.[ holds ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) proof let x be Real; ::_thesis: ( x in ].a,b.[ implies ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) assume A26: x in ].a,b.[ ; ::_thesis: ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) A27: h is_differentiable_in x by A12, A26, FDIFF_1:9; A28: p is_differentiable_in x by A7; hence h - p is_differentiable_in x by A27, FDIFF_1:14; ::_thesis: diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) thus diff ((h - p),x) = (diff (h,x)) - (diff (p,x)) by A27, A28, FDIFF_1:14 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) - (diff (p,x)) by A13, A26 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) - (- ((l * ((a - x) |^ n)) / (n !))) by A7 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ; ::_thesis: verum end; then for x being Real st x in ].a,b.[ holds h - p is_differentiable_in x ; then A29: h - p is_differentiable_on ].a,b.[ by A18, A22, FDIFF_1:9; then for x being Real st x in ].a,b.[ holds (h - p) | ].a,b.[ is_differentiable_in x by FDIFF_1:def_6; hence A30: g is_differentiable_on ].a,b.[ by A15, A24, FDIFF_1:def_6; ::_thesis: ( g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) thus g . b = 0 by A16, A17; ::_thesis: ( g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) A31: a in [.a,b.] by A2, XXREAL_1:1; then g . a = (h - p) . a by A3, A18, A19 .= (h . a) - (p . a) by A3, A18, A31, VALUED_1:13 .= 0 - ((l * ((a - a) |^ (n + 1))) / ((n + 1) !)) by A10, A6 .= 0 - ((l * ((0 |^ n) * 0)) / ((n + 1) !)) by NEWTON:6 .= 0 ; hence g . a = 0 ; ::_thesis: ( g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) (h - p) | [.a,b.] = (g | Z) | [.a,b.] by A23, A19, FUNCT_1:46 .= g | [.a,b.] by A3, FUNCT_1:51 ; hence g | [.a,b.] is continuous by A11, A14, A21, FCONT_1:18; ::_thesis: for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) thus for x being Real st x in ].a,b.[ holds diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ::_thesis: verum proof let x be Real; ::_thesis: ( x in ].a,b.[ implies diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) assume A32: x in ].a,b.[ ; ::_thesis: diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) thus diff (g,x) = (g `| ].a,b.[) . x by A30, A32, FDIFF_1:def_7 .= ((g | ].a,b.[) `| ].a,b.[) . x by A30, FDIFF_2:16 .= ((h - p) `| ].a,b.[) . x by A24, A29, FDIFF_2:16 .= diff ((h - p),x) by A29, A32, FDIFF_1:def_7 .= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) by A25, A32 ; ::_thesis: verum end; end; theorem Th29: :: TAYLOR_1:29 for n being Element of NAT for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) ) assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) ) assume that A2: a < b and A3: ( [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) a - b <> 0 by A2; then A4: (a - b) |^ (n + 1) <> 0 by CARD_4:3; deffunc H1( Real) -> Element of REAL = (f . a) - ((Partial_Sums (Taylor (f,Z,\$1,a))) . n); reconsider l = H1(b) / (((a - b) |^ (n + 1)) / ((n + 1) !)) as Real ; consider g being Function of REAL,REAL such that A5: for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) by Th26; A6: ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = H1(b) - ((H1(b) / (((a - b) |^ (n + 1)) / ((n + 1) !))) * (((a - b) |^ (n + 1)) / ((n + 1) !))) by XCMPLX_1:74 .= H1(b) - H1(b) by A4, XCMPLX_1:50, XCMPLX_1:87 .= 0 ; then A7: g . b = 0 by A5; A8: dom g = REAL by FUNCT_2:def_1; then A9: g | [.a,b.] is continuous by A1, A2, A3, A5, A6, Th28; ( g is_differentiable_on ].a,b.[ & g . a = 0 ) by A1, A2, A3, A5, A6, A8, Th28; then consider c being Real such that A10: c in ].a,b.[ and A11: diff (g,c) = 0 by A2, A8, A7, A9, ROLLE:1; c in { r where r is Real : ( a < r & r < b ) } by A10, RCOMP_1:def_2; then ex r being Real st ( c = r & a < r & r < b ) ; then a - c <> 0 ; then A12: (a - c) |^ n <> 0 by CARD_4:3; dom g = REAL by FUNCT_2:def_1; then (- (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / (n !))) + ((l * ((a - c) |^ n)) / (n !)) = 0 by A1, A2, A3, A5, A6, A10, A11, Th28; then ((((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / (n !)) * (n !)) - (((l * ((a - c) |^ n)) / (n !)) * (n !)) = 0 ; then ((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (((l * ((a - c) |^ n)) / (n !)) * (n !)) = 0 by XCMPLX_1:87; then (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (l * ((a - c) |^ n))) / ((a - c) |^ n) = 0 / ((a - c) |^ n) by XCMPLX_1:87; then (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / ((a - c) |^ n)) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0 by XCMPLX_1:120; then (((diff (f,].a,b.[)) . (n + 1)) . c) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0 by A12, XCMPLX_1:89; then ((diff (f,].a,b.[)) . (n + 1)) . c = l by A12, XCMPLX_1:89; then f . a = (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) + ((Partial_Sums (Taylor (f,Z,b,a))) . n) by A6; hence ex c being Real st ( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) by A10; ::_thesis: verum end; theorem Th30: :: TAYLOR_1:30 for f being PartFunc of REAL,REAL for Z being Subset of REAL for Z1 being open Subset of REAL st Z1 c= Z holds for n being Element of NAT st f is_differentiable_on n,Z holds ((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for Z1 being open Subset of REAL st Z1 c= Z holds for n being Element of NAT st f is_differentiable_on n,Z holds ((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n let Z be Subset of REAL; ::_thesis: for Z1 being open Subset of REAL st Z1 c= Z holds for n being Element of NAT st f is_differentiable_on n,Z holds ((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n let Z1 be open Subset of REAL; ::_thesis: ( Z1 c= Z implies for n being Element of NAT st f is_differentiable_on n,Z holds ((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n ) assume A1: Z1 c= Z ; ::_thesis: for n being Element of NAT st f is_differentiable_on n,Z holds ((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n defpred S1[ Element of NAT ] means ( f is_differentiable_on \$1,Z implies ((diff (f,Z)) . \$1) | Z1 = (diff (f,Z1)) . \$1 ); A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] assume A4: f is_differentiable_on k + 1,Z ; ::_thesis: ((diff (f,Z)) . (k + 1)) | Z1 = (diff (f,Z1)) . (k + 1) k <= (k + 1) - 1 ; then A5: (diff (f,Z)) . k is_differentiable_on Z by A4, Def6; then A6: (diff (f,Z)) . k is_differentiable_on Z1 by A1, FDIFF_1:26; then A7: dom (((diff (f,Z)) . k) `| Z1) = Z1 by FDIFF_1:def_7; A8: dom ((((diff (f,Z)) . k) `| Z) | Z1) = (dom (((diff (f,Z)) . k) `| Z)) /\ Z1 by RELAT_1:61 .= Z /\ Z1 by A5, FDIFF_1:def_7 .= Z1 by A1, XBOOLE_1:28 ; A9: now__::_thesis:_for_x_being_Real_st_x_in_dom_((((diff_(f,Z))_._k)_`|_Z)_|_Z1)_holds_ ((((diff_(f,Z))_._k)_`|_Z)_|_Z1)_._x_=_(((diff_(f,Z))_._k)_`|_Z1)_._x let x be Real; ::_thesis: ( x in dom ((((diff (f,Z)) . k) `| Z) | Z1) implies ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . x ) assume A10: x in dom ((((diff (f,Z)) . k) `| Z) | Z1) ; ::_thesis: ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . x thus ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z) . x by A8, A10, FUNCT_1:49 .= diff (((diff (f,Z)) . k),x) by A1, A5, A8, A10, FDIFF_1:def_7 .= (((diff (f,Z)) . k) `| Z1) . x by A6, A8, A10, FDIFF_1:def_7 ; ::_thesis: verum end; thus ((diff (f,Z)) . (k + 1)) | Z1 = (((diff (f,Z)) . k) `| Z) | Z1 by Def5 .= ((diff (f,Z)) . k) `| Z1 by A8, A7, A9, PARTFUN1:5 .= ((diff (f,Z1)) . k) `| Z1 by A3, A4, A6, Th23, FDIFF_2:16, NAT_1:11 .= (diff (f,Z1)) . (k + 1) by Def5 ; ::_thesis: verum end; A11: S1[ 0 ] proof assume f is_differentiable_on 0 ,Z ; ::_thesis: ((diff (f,Z)) . 0) | Z1 = (diff (f,Z1)) . 0 thus ((diff (f,Z)) . 0) | Z1 = (f | Z) | Z1 by Def5 .= f | Z1 by A1, FUNCT_1:51 .= (diff (f,Z1)) . 0 by Def5 ; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A2); ::_thesis: verum end; theorem Th31: :: TAYLOR_1:31 for f being PartFunc of REAL,REAL for Z being Subset of REAL for Z1 being open Subset of REAL st Z1 c= Z holds for n being Nat st f is_differentiable_on n + 1,Z holds f is_differentiable_on n + 1,Z1 proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for Z1 being open Subset of REAL st Z1 c= Z holds for n being Nat st f is_differentiable_on n + 1,Z holds f is_differentiable_on n + 1,Z1 let Z be Subset of REAL; ::_thesis: for Z1 being open Subset of REAL st Z1 c= Z holds for n being Nat st f is_differentiable_on n + 1,Z holds f is_differentiable_on n + 1,Z1 let Z1 be open Subset of REAL; ::_thesis: ( Z1 c= Z implies for n being Nat st f is_differentiable_on n + 1,Z holds f is_differentiable_on n + 1,Z1 ) assume A1: Z1 c= Z ; ::_thesis: for n being Nat st f is_differentiable_on n + 1,Z holds f is_differentiable_on n + 1,Z1 let n be Nat; ::_thesis: ( f is_differentiable_on n + 1,Z implies f is_differentiable_on n + 1,Z1 ) assume A2: f is_differentiable_on n + 1,Z ; ::_thesis: f is_differentiable_on n + 1,Z1 now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_(n_+_1)_-_1_holds_ (diff_(f,Z1))_._k_is_differentiable_on_Z1 let k be Element of NAT ; ::_thesis: ( k <= (n + 1) - 1 implies (diff (f,Z1)) . k is_differentiable_on Z1 ) assume A3: k <= (n + 1) - 1 ; ::_thesis: (diff (f,Z1)) . k is_differentiable_on Z1 (diff (f,Z)) . k is_differentiable_on Z by A2, A3, Def6; then (diff (f,Z)) . k is_differentiable_on Z1 by A1, FDIFF_1:26; then A4: ((diff (f,Z)) . k) | Z1 is_differentiable_on Z1 by FDIFF_2:16; n <= n + 1 by NAT_1:11; then k <= n + 1 by A3, XXREAL_0:2; hence (diff (f,Z1)) . k is_differentiable_on Z1 by A1, A2, A4, Th23, Th30; ::_thesis: verum end; hence f is_differentiable_on n + 1,Z1 by Def6; ::_thesis: verum end; theorem Th32: :: TAYLOR_1:32 for f being PartFunc of REAL,REAL for Z being Subset of REAL for x being Real st x in Z holds for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL for x being Real st x in Z holds for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n let Z be Subset of REAL; ::_thesis: for x being Real st x in Z holds for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n let x be Real; ::_thesis: ( x in Z implies for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n ) assume A1: x in Z ; ::_thesis: for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n defpred S1[ Element of NAT ] means f . x = (Partial_Sums (Taylor (f,Z,x,x))) . \$1; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] thus (Partial_Sums (Taylor (f,Z,x,x))) . (k + 1) = ((Partial_Sums (Taylor (f,Z,x,x))) . k) + ((Taylor (f,Z,x,x)) . (k + 1)) by SERIES_1:def_1 .= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((x - x) |^ (k + 1))) / ((k + 1) !)) by A3, Def7 .= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6 .= f . x ; ::_thesis: verum end; (Partial_Sums (Taylor (f,Z,x,x))) . 0 = (Taylor (f,Z,x,x)) . 0 by SERIES_1:def_1 .= ((((diff (f,Z)) . 0) . x) * ((x - x) |^ 0)) / (0 !) by Def7 .= (((f | Z) . x) * ((x - x) |^ 0)) / (0 !) by Def5 .= (((f | Z) . x) * 1) / 1 by NEWTON:4, NEWTON:12 .= f . x by A1, FUNCT_1:49 ; then A4: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); hence for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n ; ::_thesis: verum end; theorem :: TAYLOR_1:33 for n being Element of NAT for f being PartFunc of REAL,REAL for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) let f be PartFunc of REAL,REAL; ::_thesis: for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) let x0, r be Real; ::_thesis: ( ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ implies for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) assume that A1: ].(x0 - r),(x0 + r).[ c= dom f and A2: 0 < r and A3: f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ ; ::_thesis: for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) let x be Real; ::_thesis: ( x in ].(x0 - r),(x0 + r).[ implies ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) assume A4: x in ].(x0 - r),(x0 + r).[ ; ::_thesis: ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) now__::_thesis:_(_(_x_<_x0_&_ex_s_being_Element_of_REAL_st_ (_0_<_s_&_s_<_1_&_f_._x_=_((Partial_Sums_(Taylor_(f,].(x0_-_r),(x0_+_r).[,x0,x)))_._n)_+_(((((diff_(f,].(x0_-_r),(x0_+_r).[))_._(n_+_1))_._(x0_+_(s_*_(x_-_x0))))_*_((x_-_x0)_|^_(n_+_1)))_/_((n_+_1)_!))_)_)_or_(_x_=_x0_&_ex_s_being_Element_of_REAL_st_ (_0_<_s_&_s_<_1_&_((Partial_Sums_(Taylor_(f,].(x0_-_r),(x0_+_r).[,x0,x)))_._n)_+_(((((diff_(f,].(x0_-_r),(x0_+_r).[))_._(n_+_1))_._(x0_+_(s_*_(x_-_x0))))_*_((x_-_x0)_|^_(n_+_1)))_/_((n_+_1)_!))_=_f_._x_)_)_or_(_x_>_x0_&_ex_s_being_Element_of_REAL_st_ (_0_<_s_&_s_<_1_&_f_._x_=_((Partial_Sums_(Taylor_(f,].(x0_-_r),(x0_+_r).[,x0,x)))_._n)_+_(((((diff_(f,].(x0_-_r),(x0_+_r).[))_._(n_+_1))_._(x0_+_(s_*_(x_-_x0))))_*_((x_-_x0)_|^_(n_+_1)))_/_((n_+_1)_!))_)_)_) percases ( x < x0 or x = x0 or x > x0 ) by XXREAL_0:1; caseA5: x < x0 ; ::_thesis: ex s being Element of REAL st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) abs (x0 - x0) = 0 by ABSVALUE:2; then x0 in ].(x0 - r),(x0 + r).[ by A2, RCOMP_1:1; then A6: [.x,x0.] c= ].(x0 - r),(x0 + r).[ by A4, XXREAL_2:def_12; n <= (n + 1) - 1 ; then (diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A3, Def6; then ((diff (f,].(x0 - r),(x0 + r).[)) . n) | ].(x0 - r),(x0 + r).[ is continuous by FDIFF_1:25; then A7: ((diff (f,].(x0 - r),(x0 + r).[)) . n) | [.x,x0.] is continuous by A6, FCONT_1:16; A8: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A3, Th23, NAT_1:11; set t = x0 - x; A9: x0 - x > 0 by A5, XREAL_1:50; A10: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25; then f is_differentiable_on n + 1,].x,x0.[ by A3, A6, Th31, XBOOLE_1:1; then consider c being Real such that A11: c in ].x,x0.[ and A12: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].x,x0.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A1, A5, A6, A8, A7, Th29; take s = (x0 - c) / (x0 - x); ::_thesis: ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) A13: x0 + (s * (x - x0)) = x0 - (((x0 - c) / (x0 - x)) * (x0 - x)) .= x0 - (x0 - c) by A9, XCMPLX_1:87 .= c ; c in { p where p is Real : ( x0 - (x0 - x) < p & p < x0 ) } by A11, RCOMP_1:def_2; then A14: ex g being Real st ( g = c & x0 - (x0 - x) < g & g < x0 ) ; then 0 < x0 - c by XREAL_1:50; then 0 / (x0 - x) < (x0 - c) / (x0 - x) by A9, XREAL_1:74; hence 0 < s ; ::_thesis: ( s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) (x0 - (x0 - x)) + (x0 - x) < c + (x0 - x) by A14, XREAL_1:8; then x0 - c < x0 - x by XREAL_1:19; then (x0 - c) / (x0 - x) < (x0 - x) / (x0 - x) by A9, XREAL_1:74; hence s < 1 by A9, XCMPLX_1:60; ::_thesis: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ((diff (f,].x,x0.[)) . (n + 1)) . c = (((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) | ].x,x0.[) . c by A3, A6, A10, Th30, XBOOLE_1:1 .= ((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . c by A11, FUNCT_1:49 ; hence f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A12, A13; ::_thesis: verum end; caseA15: x = x0 ; ::_thesis: ex s being Element of REAL st ( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x ) set s = 1 / 2; take s = 1 / 2; ::_thesis: ( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x ) thus ( 0 < s & s < 1 ) ; ::_thesis: ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x set c = x0 + (s * (x - x0)); thus ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = (f . x) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x) |^ (n + 1))) / ((n + 1) !)) by A4, A15, Th32 .= (f . x) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((0 |^ n) * 0)) / ((n + 1) !)) by NEWTON:6 .= f . x ; ::_thesis: verum end; caseA16: x > x0 ; ::_thesis: ex s being Element of REAL st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) set t = x - x0; A17: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A3, Th23, NAT_1:11; abs (x0 - x0) = 0 by ABSVALUE:2; then x0 in ].(x0 - r),(x0 + r).[ by A2, RCOMP_1:1; then A18: [.x0,x.] c= ].(x0 - r),(x0 + r).[ by A4, XXREAL_2:def_12; n <= (n + 1) - 1 ; then (diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A3, Def6; then ((diff (f,].(x0 - r),(x0 + r).[)) . n) | ].(x0 - r),(x0 + r).[ is continuous by FDIFF_1:25; then A19: ((diff (f,].(x0 - r),(x0 + r).[)) . n) | [.x0,x.] is continuous by A18, FCONT_1:16; A20: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25; then f is_differentiable_on n + 1,].x0,x.[ by A3, A18, Th31, XBOOLE_1:1; then consider c being Real such that A21: c in ].x0,x.[ and A22: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].x0,x.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A1, A16, A18, A17, A19, Th27; take s = (c - x0) / (x - x0); ::_thesis: ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) A23: x - x0 > 0 by A16, XREAL_1:50; then A24: x0 + (s * (x - x0)) = x0 + (c - x0) by XCMPLX_1:87 .= c ; c in { p where p is Real : ( x0 < p & p < x0 + (x - x0) ) } by A21, RCOMP_1:def_2; then A25: ex g being Real st ( g = c & x0 < g & g < x0 + (x - x0) ) ; then 0 < c - x0 by XREAL_1:50; then 0 / (x - x0) < (c - x0) / (x - x0) by A23, XREAL_1:74; hence 0 < s ; ::_thesis: ( s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) c - x0 < x - x0 by A25, XREAL_1:19; then (c - x0) / (x - x0) < (x - x0) / (x - x0) by A23, XREAL_1:74; hence s < 1 by A23, XCMPLX_1:60; ::_thesis: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ((diff (f,].x0,x.[)) . (n + 1)) . c = (((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) | ].x0,x.[) . c by A3, A18, A20, Th30, XBOOLE_1:1 .= ((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . c by A21, FUNCT_1:49 ; hence f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A22, A24; ::_thesis: verum end; end; end; hence ex s being Real st ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ; ::_thesis: verum end;