:: TAYLOR_2 semantic presentation begin theorem :: TAYLOR_2:1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")))))) ; 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" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Maclaurin"::: "(" "f" "," "Z" "," "a" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) equals :: TAYLOR_2:def 1 (Set ($#k6_taylor_1 :::"Taylor"::: ) "(" "f" "," "Z" "," (Set ($#k6_numbers :::"0"::: ) ) "," "a" ")" ); end; :: deftheorem defines :::"Maclaurin"::: TAYLOR_2:def 1 : (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")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_taylor_1 :::"Taylor"::: ) "(" (Set (Var "f")) "," (Set (Var "Z")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ")" ))))); theorem :: TAYLOR_2:2 (Bool "for" (Set (Var "n")) "being" ($#m1_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 "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (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 "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (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 "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (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 "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (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_2:3 (Bool "for" (Set (Var "n")) "being" ($#m1_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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (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 ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (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")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (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 :::"!"::: ) ")" ) ")" ))) ")" )))))) ; theorem :: TAYLOR_2:4 (Bool "for" (Set (Var "n")) "being" ($#m1_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 "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (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 "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (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 ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (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_2:5 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) ")" )) ; theorem :: TAYLOR_2:6 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")))))) ; theorem :: TAYLOR_2:7 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: TAYLOR_2:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ))))) ; theorem :: TAYLOR_2:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (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 :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (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_2:10 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z"))))) ; theorem :: TAYLOR_2:11 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "M")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "M"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "L"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "M")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))) ")" ) ")" ))) ; theorem :: TAYLOR_2:12 (Bool "for" (Set (Var "M")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "M")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "L")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" (Set (Var "M")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k2_newton :::"|^"::: ) (Set (Var "m")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k3_newton :::"!"::: ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))))) ; theorem :: TAYLOR_2:13 (Bool "for" (Set (Var "r")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "m")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "m")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))))) ; theorem :: TAYLOR_2:14 (Bool "for" (Set (Var "r")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))))))) ; theorem :: TAYLOR_2:15 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "x")) ($#k4_sin_cos :::"rExpSeq"::: ) ) "is" ($#v2_series_1 :::"absolutely_summable"::: ) )) ; theorem :: TAYLOR_2:16 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "(" (Bool (Set ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "x")) ($#k4_sin_cos :::"rExpSeq"::: ) )) & (Bool (Set ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ) "is" ($#v2_series_1 :::"absolutely_summable"::: ) ) & (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ))) ")" )) ; theorem :: TAYLOR_2:17 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) ")" )) ; theorem :: TAYLOR_2:18 (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 "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ))))) ; theorem :: TAYLOR_2:19 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" ))) & (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" ))) & (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" ))) & (Bool (Set (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "Z")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" ))) ")" ))) ; theorem :: TAYLOR_2:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ))) & (Bool (Set (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k3_newton :::"!"::: ) ")" ))) & (Bool (Set (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: TAYLOR_2:21 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k16_sin_cos :::"sin"::: ) ) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z"))) & (Bool (Set ($#k19_sin_cos :::"cos"::: ) ) ($#r1_taylor_1 :::"is_differentiable_on"::: ) (Set (Var "n")) "," (Set (Var "Z"))) ")" ))) ; theorem :: TAYLOR_2:22 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "r2")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ))) ")" )) ")" ) ")" ))) ; theorem :: TAYLOR_2:23 (Bool "for" (Set (Var "r")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "m")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "m")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k5_taylor_1 :::"diff"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "m")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "m")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k3_newton :::"!"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ))))) ; theorem :: TAYLOR_2:24 (Bool "for" (Set (Var "r")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) ")" ))))) ; theorem :: TAYLOR_2:25 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "x")) ($#k22_sin_cos :::"P_sin"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))) & (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "x")) ($#k23_sin_cos :::"P_cos"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))) ")" ))) ; theorem :: TAYLOR_2:26 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "x")) ($#k22_sin_cos :::"P_sin"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "x")) ($#k23_sin_cos :::"P_cos"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))) ")" ))) ; theorem :: TAYLOR_2:27 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "x")) ($#k23_sin_cos :::"P_cos"::: ) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")))))) ; theorem :: TAYLOR_2:28 (Bool "for" (Set (Var "r")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ))) & (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" ($#k1_taylor_2 :::"Maclaurin"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ) "," (Set (Var "x")) ")" ")" ))) ")" )) ;