:: SIN_COS semantic presentation begin definitionlet "m", "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"CHK"::: "(" "m" "," "k" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: SIN_COS:def 1 (Num 1) if (Bool "m" ($#r1_xxreal_0 :::"<="::: ) "k") otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"CHK"::: SIN_COS:def 1 : (Bool "for" (Set (Var "m")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "implies" (Bool (Set ($#k1_sin_cos :::"CHK"::: ) "(" (Set (Var "m")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))))) "implies" (Bool (Set ($#k1_sin_cos :::"CHK"::: ) "(" (Set (Var "m")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); registrationlet "m", "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_sin_cos :::"CHK"::: ) "(" "m" "," "k" ")" ) -> ($#v1_xreal_0 :::"real"::: ) ; end; scheme :: SIN_COS:sch 1 ExComplexCASE{ F1( ($#m1_hidden :::"Nat":::) "," ($#m1_hidden :::"Nat":::)) -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "k")) "," (Set (Var "n")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) proof end; scheme :: SIN_COS:sch 2 ExRealCASE{ F1( ($#m1_hidden :::"Nat":::) "," ($#m1_hidden :::"Nat":::)) -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) } : (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set (Var "k")) "," (Set (Var "n")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) proof end; definitionfunc :::"Prod_real_n"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: SIN_COS:def 2 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Prod_real_n"::: SIN_COS:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos :::"Prod_real_n"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" )); definitionlet "n" be ($#m1_hidden :::"Nat":::); redefine func "n" :::"!"::: equals :: SIN_COS:def 3 (Set (Set ($#k2_sin_cos :::"Prod_real_n"::: ) ) ($#k8_nat_1 :::"."::: ) "n"); end; :: deftheorem defines :::"!"::: SIN_COS:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k3_newton :::"!"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos :::"Prod_real_n"::: ) ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))); definitionlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "z" :::"ExpSeq"::: -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "z" ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))); end; :: deftheorem defines :::"ExpSeq"::: SIN_COS:def 4 : (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))) ")" ))); definitionlet "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"rExpSeq"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: SIN_COS:def 5 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "a" ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))); end; :: deftheorem defines :::"rExpSeq"::: SIN_COS:def 5 : (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_sin_cos :::"rExpSeq"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )))) ")" ))); theorem :: SIN_COS:1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k3_newton :::"!"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "n")) ($#k3_newton :::"!"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ($#k3_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) ; theorem :: SIN_COS:2 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set "(" (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k3_newton :::"!"::: ) ")" ) ($#k3_nat_1 :::"*"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_newton :::"!"::: ) )) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "implies" (Bool (Set (Set "(" (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) )) ")" ")" )) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Coef"::: "n" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 6 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k3_newton :::"!"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Coef"::: SIN_COS:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_sin_cos :::"Coef"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" ))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Coef_e"::: "n" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 7 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Coef_e"::: SIN_COS:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_sin_cos :::"Coef_e"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k3_newton :::"!"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ($#k3_newton :::"!"::: ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" ))); definitionlet "seq" be ($#m1_subset_1 :::"Complex_Sequence":::); func :::"Shift"::: "seq" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 8 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "seq" ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ); end; :: deftheorem defines :::"Shift"::: SIN_COS:def 8 : (Bool "for" (Set (Var "seq")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_sin_cos :::"Shift"::: ) (Set (Var "seq")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ) ")" )); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z", "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Expan"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 9 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_sin_cos :::"Coef"::: ) "n" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "z" ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "w" ($#k1_newton :::"|^"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Expan"::: SIN_COS:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_sin_cos :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_sin_cos :::"Coef"::: ) (Set (Var "n")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "w")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" )))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z", "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Expan_e"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 10 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos :::"Coef_e"::: ) "n" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "z" ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "w" ($#k1_newton :::"|^"::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Expan_e"::: SIN_COS:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_sin_cos :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos :::"Coef_e"::: ) (Set (Var "n")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "w")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" )))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "z", "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Alfa"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 11 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" "w" ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Alfa"::: SIN_COS:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_sin_cos :::"Alfa"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" )))); definitionlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Conj"::: "(" "n" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: SIN_COS:def 12 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "a" ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" "b" ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" "b" ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Conj"::: SIN_COS:def 12 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_sin_cos :::"Conj"::: ) "(" (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "b")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "b")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" )))); definitionlet "z", "w" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Conj"::: "(" "n" "," "z" "," "w" ")" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 13 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "z" ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" "w" ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) "n" ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" "w" ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" "n" ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Conj"::: SIN_COS:def 13 : (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_sin_cos :::"Conj"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "implies" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" )))); theorem :: SIN_COS:3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ))) ; theorem :: SIN_COS:4 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k7_sin_cos :::"Shift"::: ) (Set (Var "seq")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))))) ; theorem :: SIN_COS:5 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k7_sin_cos :::"Shift"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ))))) ; theorem :: SIN_COS:6 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k8_complex1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k8_sin_cos :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SIN_COS:7 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_sin_cos :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set ($#k6_complex1 :::"1r"::: ) ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ) ")" ) ($#k25_valued_1 :::"(#)"::: ) (Set "(" ($#k8_sin_cos :::"Expan"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ))))) ; theorem :: SIN_COS:8 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "z")) ($#k8_complex1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k9_sin_cos :::"Expan_e"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SIN_COS:9 (Bool "(" (Bool (Set (Set ($#k5_complex1 :::"0c"::: ) ) ($#k3_sin_cos :::"ExpSeq"::: ) ) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) ) & (Bool (Set ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set ($#k5_complex1 :::"0c"::: ) ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ")" ) ; registrationlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "z" ($#k3_sin_cos :::"ExpSeq"::: ) ) -> ($#v2_comseq_3 :::"absolutely_summable"::: ) ; end; theorem :: SIN_COS:10 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" ($#k8_sin_cos :::"Expan"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS:11 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "l")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k10_sin_cos :::"Alfa"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_sin_cos :::"Alfa"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "l")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos :::"Expan_e"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "l")) ")" ))))) ; theorem :: SIN_COS:12 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k10_sin_cos :::"Alfa"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k10_sin_cos :::"Alfa"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k9_sin_cos :::"Expan_e"::: ) "(" (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ))))) ; theorem :: SIN_COS:13 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_sin_cos :::"Expan_e"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: SIN_COS:14 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k8_complex1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k10_sin_cos :::"Alfa"::: ) "(" (Set (Var "n")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SIN_COS:15 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "w")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k8_complex1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k12_sin_cos :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: SIN_COS:16 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ))) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ))) ")" ))) ; theorem :: SIN_COS:17 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )))) ; theorem :: SIN_COS:18 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SIN_COS:19 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "implies" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ")" ))) ; theorem :: SIN_COS:20 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" ($#k12_sin_cos :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k55_valued_1 :::".|"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" ($#k12_sin_cos :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k55_valued_1 :::".|"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: SIN_COS:21 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" ($#k12_sin_cos :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ($#k55_valued_1 :::".|"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))))))) ; theorem :: SIN_COS:22 (Bool "for" (Set (Var "z")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" ($#k12_sin_cos :::"Conj"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k3_comseq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; begin definitionfunc :::"exp"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: SIN_COS:def 14 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" )))); end; :: deftheorem defines :::"exp"::: SIN_COS:def 14 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k13_sin_cos :::"exp"::: ) )) "iff" (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" )))) ")" )); definitionlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"exp"::: "z" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS:def 15 (Set (Set ($#k13_sin_cos :::"exp"::: ) ) ($#k1_funct_1 :::"."::: ) "z"); end; :: deftheorem defines :::"exp"::: SIN_COS:def 15 : (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k14_sin_cos :::"exp"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_sin_cos :::"exp"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))); definitionlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"exp"::: redefine func :::"exp"::: "z" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; theorem :: SIN_COS:23 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set (Var "z1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set (Var "z1")) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set (Var "z2")) ")" )))) ; begin definitionfunc :::"sin"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SIN_COS:def 16 (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )))); end; :: deftheorem defines :::"sin"::: SIN_COS:def 16 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k16_sin_cos :::"sin"::: ) )) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )))) ")" )); definitionlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"sin"::: "th" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS:def 17 (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) "th"); end; :: deftheorem defines :::"sin"::: SIN_COS:def 17 : (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))))); registrationlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k17_sin_cos :::"sin"::: ) "th") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "th" be ($#m1_subset_1 :::"Real":::); :: original: :::"sin"::: redefine func :::"sin"::: "th" -> ($#m1_subset_1 :::"Real":::); end; definitionfunc :::"cos"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SIN_COS:def 18 (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )))); end; :: deftheorem defines :::"cos"::: SIN_COS:def 18 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k19_sin_cos :::"cos"::: ) )) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )))) ")" )); definitionlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"cos"::: "th" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS:def 19 (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) "th"); end; :: deftheorem defines :::"cos"::: SIN_COS:def 19 : (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))))); registrationlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k20_sin_cos :::"cos"::: ) "th") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "th" be ($#m1_subset_1 :::"Real":::); :: original: :::"cos"::: redefine func :::"cos"::: "th" -> ($#m1_subset_1 :::"Real":::); end; theorem :: SIN_COS:24 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k16_sin_cos :::"sin"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k19_sin_cos :::"cos"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" ) ; theorem :: SIN_COS:25 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "th")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS:26 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k15_complex1 :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )))) ; theorem :: SIN_COS:27 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) ")" ) ")" )) ; theorem :: SIN_COS:28 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS:29 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS:30 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ))) ")" )) ; theorem :: SIN_COS:31 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")))) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ))) ")" )) ; definitionlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func "th" :::"P_sin"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: SIN_COS:def 20 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_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 "(" "th" ($#k1_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 :::"!"::: ) ")" )))); func "th" :::"P_cos"::: -> ($#m1_subset_1 :::"Real_Sequence":::) means :: SIN_COS:def 21 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_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 "(" "th" ($#k1_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 :::"!"::: ) ")" )))); end; :: deftheorem defines :::"P_sin"::: SIN_COS:def 20 : (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "th")) ($#k22_sin_cos :::"P_sin"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_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 "th")) ($#k1_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 :::"!"::: ) ")" )))) ")" ))); :: deftheorem defines :::"P_cos"::: SIN_COS:def 21 : (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "th")) ($#k23_sin_cos :::"P_cos"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_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 "th")) ($#k1_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 :::"!"::: ) ")" )))) ")" ))); theorem :: SIN_COS:32 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k1_newton :::"|^"::: ) (Num 2))) & (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "k")))) ")" ))) ; theorem :: SIN_COS:33 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "th")) ($#k2_newton :::"|^"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "th")) ($#k2_newton :::"|^"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ))) ")" ))) ; theorem :: SIN_COS:34 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "n")) ($#k3_newton :::"!"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k3_newton :::"!"::: ) ))) ; theorem :: SIN_COS:35 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "th")) ($#k22_sin_cos :::"P_sin"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k8_comseq_3 :::"Im"::: ) (Set "(" (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "th")) ($#k23_sin_cos :::"P_cos"::: ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" ($#k7_comseq_3 :::"Re"::: ) (Set "(" (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: SIN_COS:36 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "th")) ($#k22_sin_cos :::"P_sin"::: ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k22_sin_cos :::"P_sin"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ))) & (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "th")) ($#k23_sin_cos :::"P_cos"::: ) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k23_sin_cos :::"P_cos"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "th")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS:37 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k23_sin_cos :::"P_cos"::: ) ")" ))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k22_sin_cos :::"P_sin"::: ) ")" ))) ")" )) ; theorem :: SIN_COS:38 (Bool "for" (Set (Var "p")) "," (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set (Var "th"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "p"))) ")" )) "holds" (Bool (Set (Var "th")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "p"))))) ; theorem :: SIN_COS:39 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "n")) ($#k3_newton :::"!"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k3_newton :::"!"::: ) ))) ; theorem :: SIN_COS:40 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "th"))) & (Bool (Set (Var "th")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "th")) ($#k1_newton :::"|^"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "th")) ($#k1_newton :::"|^"::: ) (Set (Var "n")))))) ; theorem :: SIN_COS:41 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "th")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "th")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k3_newton :::"!"::: ) ")" ))))) ; theorem :: SIN_COS:42 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS:43 (Bool "(" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1))) ")" ) ; theorem :: SIN_COS:44 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "th")) ($#k4_sin_cos :::"rExpSeq"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "th")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" )))) ; theorem :: SIN_COS:45 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "th")) ($#k4_sin_cos :::"rExpSeq"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS:46 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "q")) ")" ) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "q")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" ) ")" )))) ; definitionfunc :::"exp_R"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SIN_COS:def 22 (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "d")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )))); end; :: deftheorem defines :::"exp_R"::: SIN_COS:def 22 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) "iff" (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "d")) ($#k4_sin_cos :::"rExpSeq"::: ) ")" )))) ")" )); definitionlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"exp_R"::: "th" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS:def 23 (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) "th"); end; :: deftheorem defines :::"exp_R"::: SIN_COS:def 23 : (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))))); registrationlet "th" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k25_sin_cos :::"exp_R"::: ) "th") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "th" be ($#m1_subset_1 :::"Real":::); :: original: :::"exp_R"::: redefine func :::"exp_R"::: "th" -> ($#m1_subset_1 :::"Real":::); end; theorem :: SIN_COS:47 (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: SIN_COS:48 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "th")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )))) ; theorem :: SIN_COS:49 (Bool "for" (Set (Var "th")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set ($#k26_sin_cos :::"exp_R"::: ) (Set (Var "th"))))) ; theorem :: SIN_COS:50 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "p")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "q")) ")" )))) ; theorem :: SIN_COS:51 (Bool (Set ($#k26_sin_cos :::"exp_R"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: SIN_COS:52 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "th")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) ; theorem :: SIN_COS:53 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "th")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS:54 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS:55 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; begin definitionlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "z" :::"P_dt"::: -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 24 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "z" ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k3_newton :::"!"::: ) ")" )))); func "z" :::"P_t"::: -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: SIN_COS:def 25 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "z" ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k3_newton :::"!"::: ) ")" )))); end; :: deftheorem defines :::"P_dt"::: SIN_COS:def 24 : (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k27_sin_cos :::"P_dt"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k3_newton :::"!"::: ) ")" )))) ")" ))); :: deftheorem defines :::"P_t"::: SIN_COS:def 25 : (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k28_sin_cos :::"P_t"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k3_newton :::"!"::: ) ")" )))) ")" ))); theorem :: SIN_COS:56 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k27_sin_cos :::"P_dt"::: ) ) "is" ($#v2_comseq_3 :::"absolutely_summable"::: ) )) ; theorem :: SIN_COS:57 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k27_sin_cos :::"P_dt"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set ($#k6_complex1 :::"1r"::: ) ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z"))))) ; theorem :: SIN_COS:58 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k27_sin_cos :::"P_dt"::: ) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) ")" ) ")" ))) ; theorem :: SIN_COS:59 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z1")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z1")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k27_sin_cos :::"P_dt"::: ) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "z1")) ($#k3_sin_cos :::"ExpSeq"::: ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS:60 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_real_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "q")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "q")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set "(" (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k27_sin_cos :::"P_dt"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS:61 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_real_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set "(" (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k27_sin_cos :::"P_dt"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS:62 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_real_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "q")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "q")) ($#k27_sin_cos :::"P_dt"::: ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS:63 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k19_sin_cos :::"cos"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "p"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ))) ")" )) ; theorem :: SIN_COS:64 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k16_sin_cos :::"sin"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "p"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) ")" )) ; theorem :: SIN_COS:65 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "p"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) ")" )) ; theorem :: SIN_COS:66 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "th")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) ")" )) ; theorem :: SIN_COS:67 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k19_sin_cos :::"cos"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "th")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ))) ")" )) ; theorem :: SIN_COS:68 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k16_sin_cos :::"sin"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "th")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) ")" )) ; theorem :: SIN_COS:69 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "th")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" )) ; definitionfunc :::"tan"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SIN_COS:def 26 (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_rfunct_1 :::"/"::: ) (Set ($#k19_sin_cos :::"cos"::: ) )); func :::"cot"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SIN_COS:def 27 (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_rfunct_1 :::"/"::: ) (Set ($#k16_sin_cos :::"sin"::: ) )); end; :: deftheorem defines :::"tan"::: SIN_COS:def 26 : (Bool (Set ($#k29_sin_cos :::"tan"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_rfunct_1 :::"/"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ))); :: deftheorem defines :::"cot"::: SIN_COS:def 27 : (Bool (Set ($#k30_sin_cos :::"cot"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_rfunct_1 :::"/"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ))); theorem :: SIN_COS:70 (Bool "(" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) ")" ) ; theorem :: SIN_COS:71 (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS:72 (Bool "for" (Set (Var "th1")) "," (Set (Var "th2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "th1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "th2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th1"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th2"))))) "holds" (Bool (Set (Var "th1")) ($#r1_hidden :::"="::: ) (Set (Var "th2")))) ; begin definitionfunc :::"PI"::: -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) means :: SIN_COS:def 28 (Bool "(" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" it ($#k6_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k2_rcomp_1 :::".["::: ) )) ")" ); end; :: deftheorem defines :::"PI"::: SIN_COS:def 28 : (Bool "for" (Set (Var "b1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k31_sin_cos :::"PI"::: ) )) "iff" (Bool "(" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "b1")) ($#k6_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k2_rcomp_1 :::".["::: ) )) ")" ) ")" )); definition:: original: :::"PI"::: redefine func :::"PI"::: -> ($#m1_subset_1 :::"Real":::); end; theorem :: SIN_COS:73 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ; begin theorem :: SIN_COS:74 (Bool "for" (Set (Var "th1")) "," (Set (Var "th2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "th1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "th2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th2")) ")" ) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "th1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "th2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th2")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS:75 (Bool "for" (Set (Var "th1")) "," (Set (Var "th2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set "(" (Set (Var "th1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "th2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th2")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th2")) ")" ) ")" ))) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set "(" (Set (Var "th1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "th2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th2")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th2")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS:76 (Bool "(" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: SIN_COS:77 (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: SIN_COS:78 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "th")) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "th")) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th")) ")" ))) ")" )) ; theorem :: SIN_COS:79 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "th")) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "th")) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "th")) ")" ))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "th")) ")" ))) ")" )) ; theorem :: SIN_COS:80 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "th")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS:81 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "th")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "th"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; begin theorem :: SIN_COS:82 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")) ")" ) ")" )))) ; theorem :: SIN_COS:83 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")) ")" ) ")" )))) ; registration cluster (Set ($#k16_sin_cos :::"sin"::: ) ) -> ($#v1_fcont_1 :::"continuous"::: ) ; cluster (Set ($#k19_sin_cos :::"cos"::: ) ) -> ($#v1_fcont_1 :::"continuous"::: ) ; cluster (Set ($#k24_sin_cos :::"exp_R"::: ) ) -> ($#v1_fcont_1 :::"continuous"::: ) ; end;