:: SIN_COS9 semantic presentation begin theorem :: SIN_COS9:1 (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) ; theorem :: SIN_COS9:2 (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) ; theorem :: SIN_COS9:3 (Bool "(" (Bool (Set ($#k29_sin_cos :::"tan"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k29_sin_cos :::"tan"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) ")" ) ; theorem :: SIN_COS9:4 (Bool "(" (Bool (Set ($#k30_sin_cos :::"cot"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k30_sin_cos :::"cot"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ) ; theorem :: SIN_COS9:5 (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS9:6 (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS9:7 (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS9:8 (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS9:9 (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; theorem :: SIN_COS9:10 (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; registration cluster (Set bbbadK5_RELAT_1((Set ($#k29_sin_cos :::"tan"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k30_sin_cos :::"cot"::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; definitionfunc :::"arctan"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SIN_COS9:def 1 (Set (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ); func :::"arccot"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SIN_COS9:def 2 (Set (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ); end; :: deftheorem defines :::"arctan"::: SIN_COS9:def 1 : (Bool (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )); :: deftheorem defines :::"arccot"::: SIN_COS9:def 2 : (Bool (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )); definitionlet "r" be ($#m1_subset_1 :::"Real":::); func :::"arctan"::: "r" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS9:def 3 (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) "r"); func :::"arccot"::: "r" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS9:def 4 (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) "r"); end; :: deftheorem defines :::"arctan"::: SIN_COS9:def 3 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k3_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))))); :: deftheorem defines :::"arccot"::: SIN_COS9:def 4 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))))); definitionlet "r" be ($#m1_subset_1 :::"Real":::); :: original: :::"arctan"::: redefine func :::"arctan"::: "r" -> ($#m1_subset_1 :::"Real":::); :: original: :::"arccot"::: redefine func :::"arccot"::: "r" -> ($#m1_subset_1 :::"Real":::); end; theorem :: SIN_COS9:11 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: SIN_COS9:12 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) ; registration cluster (Set ($#k1_sin_cos9 :::"arctan"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set ($#k2_sin_cos9 :::"arccot"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: SIN_COS9:13 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x"))))) ; theorem :: SIN_COS9:14 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x"))))) ; theorem :: SIN_COS9:15 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x"))))) ; theorem :: SIN_COS9:16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x"))))) ; theorem :: SIN_COS9:17 (Bool "(" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) ; theorem :: SIN_COS9:18 (Bool "(" (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) ; theorem :: SIN_COS9:19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:20 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:21 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SIN_COS9:22 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SIN_COS9:23 (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ))) ; theorem :: SIN_COS9:24 (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ))) ; registration cluster (Set bbbadK5_RELAT_1((Set ($#k29_sin_cos :::"tan"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k30_sin_cos :::"cot"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: SIN_COS9:25 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )) ; theorem :: SIN_COS9:26 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )) ; theorem :: SIN_COS9:27 (Bool (Set (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:28 (Bool (Set (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:29 (Bool (Set (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:30 (Bool (Set (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:31 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SIN_COS9:32 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SIN_COS9:33 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SIN_COS9:34 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SIN_COS9:35 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) ; theorem :: SIN_COS9:36 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) & (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) ; theorem :: SIN_COS9:37 (Bool "(" (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) & (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ")" ) ; theorem :: SIN_COS9:38 (Bool "(" (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) ; theorem :: SIN_COS9:39 (Bool "(" (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) & (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" ) ; theorem :: SIN_COS9:40 (Bool "(" (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) & (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" ) ; theorem :: SIN_COS9:41 (Bool "(" (Bool (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: SIN_COS9:42 (Bool "(" (Bool (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: SIN_COS9:43 (Bool "(" (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: SIN_COS9:44 (Bool "(" (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" ) ; theorem :: SIN_COS9:45 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS9:46 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS9:47 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS9:48 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS9:49 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:50 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SIN_COS9:51 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SIN_COS9:52 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SIN_COS9:53 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS9:54 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS9:55 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SIN_COS9:56 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SIN_COS9:57 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS9:58 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS9:59 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS9:60 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS9:61 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS9:62 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS9:63 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r")))) & (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" )) ; theorem :: SIN_COS9:64 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r")))) & (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) ; theorem :: SIN_COS9:65 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r")))) & (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" )) ; theorem :: SIN_COS9:66 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r")))) & (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) ; theorem :: SIN_COS9:67 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k5_sin_cos9 :::"arctan"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" )))) ; theorem :: SIN_COS9:68 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k6_sin_cos9 :::"arccot"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ")" )))) ; theorem :: SIN_COS9:69 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" ($#k5_sin_cos9 :::"arctan"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r"))))) ; theorem :: SIN_COS9:70 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" ($#k6_sin_cos9 :::"arccot"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r"))))) ; theorem :: SIN_COS9:71 (Bool (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SIN_COS9:72 (Bool (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SIN_COS9:73 (Bool (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: SIN_COS9:74 (Bool (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) ; theorem :: SIN_COS9:75 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: SIN_COS9:76 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS9:77 (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS9:78 (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS9:79 (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) "is" ($#v3_rcomp_1 :::"open"::: ) ) ; theorem :: SIN_COS9:80 (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) "is" ($#v3_rcomp_1 :::"open"::: ) ) ; begin theorem :: SIN_COS9:81 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:82 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:83 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:84 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:85 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ))) ; theorem :: SIN_COS9:86 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_fdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ))) ; theorem :: SIN_COS9:87 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:88 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:89 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:90 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:91 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_prepower :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:92 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_prepower :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:93 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:94 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:95 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:96 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:97 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:98 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:99 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:100 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:101 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) ")" ) ")" ))) ; theorem :: SIN_COS9:102 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Num 2))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ))) ; theorem :: SIN_COS9:103 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Num 2))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ))) ; theorem :: SIN_COS9:104 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Num 2))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ))) ; theorem :: SIN_COS9:105 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:106 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:107 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:108 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:109 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:110 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Num 2) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:111 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:112 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:113 (Bool "for" (Set (Var "h")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:114 (Bool "for" (Set (Var "h")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set ($#k1_taylor_1 :::"#Z"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:115 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:116 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:117 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:118 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:119 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:120 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:121 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:122 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k32_valued_1 :::"-"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k32_valued_1 :::"-"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:123 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:124 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:125 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:126 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: SIN_COS9:127 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:128 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:129 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos9 :::"arctan"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: SIN_COS9:130 (Bool "for" (Set (Var "Z")) "being" ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) )) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "Z")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ")" ) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "Z")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k2_sin_cos9 :::"arccot"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ))) ")" ) ")" )) ;