:: COMPTRIG semantic presentation begin scheme :: COMPTRIG:sch 1 Regrwithout0{ P1[ ($#m1_hidden :::"Nat":::)] } : (Bool P1[(Num 1)]) provided (Bool "ex" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool P1[(Set (Var "k"))])) and (Bool "for" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool P1[(Set (Var "k"))])) "holds" (Bool "ex" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool P1[(Set (Var "n"))]) ")" ))) proof end; theorem :: COMPTRIG:1 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPTRIG:2 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPTRIG:3 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: COMPTRIG:4 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; registration cluster (Set ($#k31_sin_cos :::"PI"::: ) ) -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; begin theorem :: COMPTRIG:5 (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set ($#k32_sin_cos :::"PI"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k32_sin_cos :::"PI"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) ; theorem :: COMPTRIG:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k2_rcomp_1 :::".["::: ) )) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_rcomp_1 :::".["::: ) )) ")" )) ; theorem :: COMPTRIG:7 (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 ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:8 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:9 (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 ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:10 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:11 (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 ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:12 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "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 2) ")" ) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG: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 "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:14 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:15 (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 "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:16 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:17 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: COMPTRIG:18 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) ; theorem :: COMPTRIG:19 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#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 :: COMPTRIG:20 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: COMPTRIG:21 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: COMPTRIG:22 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: COMPTRIG:23 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_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) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: COMPTRIG:24 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: COMPTRIG:25 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: COMPTRIG:26 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: COMPTRIG:27 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#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 :: COMPTRIG:28 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k16_sin_cos :::"sin"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: COMPTRIG:29 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k19_sin_cos :::"cos"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: COMPTRIG:30 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_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) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: COMPTRIG:31 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#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 :: COMPTRIG:32 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (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 :: COMPTRIG:33 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Num 2) ($#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 :::".]"::: ) )) ; begin definitionlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Arg"::: "z" -> ($#m1_subset_1 :::"Real":::) means :: COMPTRIG:def 1 (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) "z" ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) it ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) "z" ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) it ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) it) & (Bool it ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) if (Bool "z" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"Arg"::: COMPTRIG:def 1 : (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "b2")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "b2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) & (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))); theorem :: COMPTRIG:34 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")))) & (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) ; theorem :: COMPTRIG:35 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:36 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: COMPTRIG:37 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: COMPTRIG:38 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) ; theorem :: COMPTRIG:39 (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: COMPTRIG:40 (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set ($#k7_complex1 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) ; theorem :: COMPTRIG:41 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: COMPTRIG:42 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: COMPTRIG:43 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: COMPTRIG:44 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: COMPTRIG:45 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:46 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:47 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:48 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:49 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:50 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:51 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:52 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:53 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: COMPTRIG:54 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "n")) ($#k4_real_1 :::"*"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "n")) ($#k4_real_1 :::"*"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: COMPTRIG:55 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: COMPTRIG:56 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")))))) ; definitionlet "x" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); mode :::"CRoot"::: "of" "n" "," "x" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) means :: COMPTRIG:def 2 (Bool (Set it ($#k1_newton :::"|^"::: ) "n") ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"CRoot"::: COMPTRIG:def 2 : (Bool "for" (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "x"))) "iff" (Bool (Set (Set (Var "b3")) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))); theorem :: COMPTRIG:57 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) "is" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "x")))))) ; theorem :: COMPTRIG:58 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_comptrig :::"CRoot"::: ) "of" (Num 1) "," (Set (Var "x")) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: COMPTRIG:59 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set ($#k6_numbers :::"0"::: ) ) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: COMPTRIG:60 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "x")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: COMPTRIG:61 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPTRIG:62 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ;