:: TAYLOR_1 semantic presentation begin definitionlet "q" be ($#m1_hidden :::"Integer":::); func :::"#Z"::: "q" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: TAYLOR_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_prepower :::"#Z"::: ) "q"))); end; :: deftheorem defines :::"#Z"::: TAYLOR_1:def 1 : (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_prepower :::"#Z"::: ) (Set (Var "q"))))) ")" ))); theorem :: TAYLOR_1:1 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "x")) ($#k4_prepower :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_prepower :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k4_prepower :::"#Z"::: ) (Set (Var "m")) ")" ))))) ; theorem :: TAYLOR_1:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k4_prepower :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ")" ))) ")" ))) ; theorem :: TAYLOR_1:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ($#k5_prepower :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ))) ")" )))) ; theorem :: TAYLOR_1:4 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" )))) ; theorem :: TAYLOR_1:5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_prepower :::"#R"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" (Set (Var "x")) ($#k13_complex1 :::"/"::: ) (Set (Var "i")) ")" ))))) ; theorem :: TAYLOR_1:6 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_prepower :::"#R"::: ) (Set "(" (Set (Var "m")) ($#k13_complex1 :::"/"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k13_complex1 :::"/"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ))))) ; theorem :: TAYLOR_1:7 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"Rational":::) "holds" (Bool (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k6_prepower :::"#Q"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" (Set (Var "q")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ))))) ; theorem :: TAYLOR_1:8 (Bool "for" (Set (Var "x")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_prepower :::"#R"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )))) ; theorem :: TAYLOR_1:9 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Num 1) ")" ) ($#k9_prepower :::"#R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Num 1) ")" ) ($#k3_power :::"to_power"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")))) & (Bool (Set (Set ($#k8_power :::"number_e"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")))) & (Bool (Set (Set ($#k8_power :::"number_e"::: ) ) ($#k9_prepower :::"#R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")))) ")" )) ; theorem :: TAYLOR_1:10 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k9_prepower :::"#R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1) ")" ) ($#k3_power :::"to_power"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set ($#k8_power :::"number_e"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set ($#k8_power :::"number_e"::: ) ) ($#k9_prepower :::"#R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) ; theorem :: TAYLOR_1:11 (Bool (Set ($#k8_power :::"number_e"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Num 2)) ; theorem :: TAYLOR_1:12 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: TAYLOR_1:13 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: TAYLOR_1:14 (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: TAYLOR_1:15 (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: TAYLOR_1:16 (Bool "(" (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ) ; registration cluster (Set ($#k24_sin_cos :::"exp_R"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: TAYLOR_1:17 (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun2 :::"""::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun2 :::"""::: ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun2 :::"""::: ) ")" )))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun2 :::"""::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x")))) ")" ) ")" ) ; registration cluster (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"log_"::: "a" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: TAYLOR_1:def 2 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k5_power :::"log"::: ) "(" "a" "," (Set (Var "d")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"log_"::: TAYLOR_1:def 2 : (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_taylor_1 :::"log_"::: ) (Set (Var "a")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k5_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" )) ")" ) ")" ) ")" ))); definitionfunc :::"ln"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: TAYLOR_1:def 3 (Set ($#k2_taylor_1 :::"log_"::: ) (Set ($#k8_power :::"number_e"::: ) )); end; :: deftheorem defines :::"ln"::: TAYLOR_1:def 3 : (Bool (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_taylor_1 :::"log_"::: ) (Set ($#k8_power :::"number_e"::: ) ))); theorem :: TAYLOR_1:18 (Bool "(" (Bool (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun2 :::"""::: ) )) & (Bool (Set ($#k3_taylor_1 :::"ln"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) "," (Set (Var "x")) ")" )) ")" ) ")" ) ; theorem :: TAYLOR_1:19 (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ))) ")" ))) ; theorem :: TAYLOR_1:20 (Bool "for" (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ))) ")" ))) ; definitionlet "p" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"#R"::: "p" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: TAYLOR_1:def 4 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k9_prepower :::"#R"::: ) "p")) ")" ) ")" ); end; :: deftheorem defines :::"#R"::: TAYLOR_1:def 4 : (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_taylor_1 :::"#R"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k9_prepower :::"#R"::: ) (Set (Var "p")))) ")" ) ")" ) ")" ))); theorem :: TAYLOR_1:21 (Bool "for" (Set (Var "x")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_taylor_1 :::"#R"::: ) (Set (Var "p"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" ($#k4_taylor_1 :::"#R"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k9_prepower :::"#R"::: ) (Set "(" (Set (Var "p")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ")" ))) ")" )) ; theorem :: TAYLOR_1:22 (Bool "for" (Set (Var "x0")) "," (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_taylor_1 :::"#R"::: ) (Set (Var "p")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x0"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set "(" ($#k4_taylor_1 :::"#R"::: ) (Set (Var "p")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ($#k10_prepower :::"#R"::: ) (Set "(" (Set (Var "p")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) ")" ")" ))) ")" ))) ; begin definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"diff"::: "(" "f" "," "Z" ")" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: TAYLOR_1:def 5 (Bool "(" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set "f" ($#k2_partfun1 :::"|"::: ) "Z")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" it ($#k1_seqfunc :::"."::: ) (Set (Var "i")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) "Z")) ")" ) ")" ); end; :: deftheorem defines :::"diff"::: TAYLOR_1:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "i")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")))) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "n" be ($#m1_hidden :::"Nat":::); let "Z" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_differentiable_on"::: "n" "," "Z" means :: TAYLOR_1:def 6 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set "n" ($#k5_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" "f" "," "Z" ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "i"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) "Z")); end; :: deftheorem defines :::"is_differentiable_on"::: TAYLOR_1:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "i"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) ")" )))); theorem :: TAYLOR_1:23 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "m")) "," (Set (Var "Z"))))))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "Z" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Taylor"::: "(" "f" "," "Z" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: TAYLOR_1:def 7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" "f" "," "Z" ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) "a" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" "b" ($#k6_xcmplx_0 :::"-"::: ) "a" ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))); end; :: deftheorem defines :::"Taylor"::: TAYLOR_1:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))) ")" ))))); theorem :: TAYLOR_1:24 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")))))))) ; theorem :: TAYLOR_1:25 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" ) & (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" ) ")" ))))))) ; theorem :: TAYLOR_1:26 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "x")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))))))))) ; theorem :: TAYLOR_1:27 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" )))))) ; theorem :: TAYLOR_1:28 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "x")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" ) & (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "g")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" ) ")" ))))))) ; theorem :: TAYLOR_1:29 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" )))))) ; theorem :: TAYLOR_1:30 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z1")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z1")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z1"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "Z1")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")))))))) ; theorem :: TAYLOR_1:31 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z1")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z1")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "Z1"))))))) ; theorem :: TAYLOR_1:32 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "x")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: TAYLOR_1:33 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x0")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x0")) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" )))))) ;