:: COMPLEX2 semantic presentation begin theorem :: COMPLEX2:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set (Var "a")) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ($#k1_int_1 :::"/]"::: ) ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" ))) ; theorem :: COMPLEX2:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: COMPLEX2:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")) ")" ) ")" ))) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")) ")" ) ")" ))) ")" )) ; theorem :: COMPLEX2:4 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k5_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k5_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" )) ; theorem :: COMPLEX2:5 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "a")) ($#k5_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "a")) ($#k5_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "a")) ")" ))) ")" )) ; theorem :: COMPLEX2:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) "iff" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")))) ")" )) ; theorem :: COMPLEX2:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) "iff" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")))) ")" )) ; theorem :: COMPLEX2:8 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a")) ")" ))))) ; theorem :: COMPLEX2:9 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "a")) ")" ))))) ; theorem :: COMPLEX2:10 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "b")))) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; begin theorem :: COMPLEX2:12 (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 :::""::: ) ) ")" )))) ; theorem :: COMPLEX2:13 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "implies" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" & "(" (Bool (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "implies" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k9_real_1 :::"-"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ")" )) ; theorem :: COMPLEX2:14 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:15 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )) ")" )) ; theorem :: COMPLEX2:16 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) "iff" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: COMPLEX2:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) "iff" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: COMPLEX2:18 (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 ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "iff" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: COMPLEX2:19 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) "iff" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: COMPLEX2:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: COMPLEX2:21 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "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_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: COMPLEX2:22 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) "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_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: COMPLEX2:23 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" ) ")" )) ; theorem :: COMPLEX2:24 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:25 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ))) ")" )) ; theorem :: COMPLEX2:26 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "a")) ")" ) ($#k13_complex1 :::"/"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "a")) ")" ) ($#k13_complex1 :::"/"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ))) ")" )) ; theorem :: COMPLEX2:27 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")))))) ; theorem :: COMPLEX2:28 (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ))))) ; begin definitionlet "x", "y" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::".|."::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: COMPLEX2:def 1 (Set "x" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "y" ($#k15_complex1 :::"*'"::: ) ")" )); end; :: deftheorem defines :::".|."::: COMPLEX2:def 1 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k15_complex1 :::"*'"::: ) ")" )))); theorem :: COMPLEX2:29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "y")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: COMPLEX2:30 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_complex2 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ")" ))) & (Bool (Set (Set (Var "z")) ($#k1_complex2 :::".|."::: ) (Set (Var "z"))) ($#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 :: COMPLEX2:31 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_complex2 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) )) & (Bool (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "z")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" ))) ")" )) ; theorem :: COMPLEX2:32 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPLEX2:33 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:34 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ($#k15_complex1 :::"*'"::: ) ))) ; theorem :: COMPLEX2:35 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k8_complex1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" )))) ; theorem :: COMPLEX2:36 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" (Set (Var "y")) ($#k8_complex1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" )))) ; theorem :: COMPLEX2:37 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:38 (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:39 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k9_complex1 :::"*"::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:40 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_complex1 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: COMPLEX2:41 (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "y")) "," (Set (Var "b")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_complex1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_complex1 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k15_complex1 :::"*'"::: ) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: COMPLEX2:42 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:43 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:44 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:45 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_complex2 :::".|."::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y"))))) ; theorem :: COMPLEX2:46 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_complex2 :::".|."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" )))) ; theorem :: COMPLEX2:47 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set "(" (Set (Var "y")) ($#k11_complex1 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "z")) ")" )))) ; theorem :: COMPLEX2:48 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k8_complex1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_complex2 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k8_complex1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "x")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_complex2 :::".|."::: ) (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "x")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )))) ; theorem :: COMPLEX2:50 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ))) "or" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "x")) ($#k1_complex2 :::".|."::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "x")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "y")) ($#k17_complex1 :::".|"::: ) ) ")" ))) ")" ) ")" )) ; begin definitionlet "a" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#m1_subset_1 :::"Real":::); func :::"Rotate"::: "(" "a" "," "r" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: COMPLEX2:def 2 (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) "a" ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" "r" ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) "a" ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) "a" ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" "r" ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) "a" ")" ) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )); end; :: deftheorem defines :::"Rotate"::: COMPLEX2:def 2 : (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))); theorem :: COMPLEX2:51 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: COMPLEX2:52 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: COMPLEX2:53 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPLEX2:54 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" ) ")" )))))) ; theorem :: COMPLEX2:55 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ))) ; theorem :: COMPLEX2:56 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "r")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "r")) ")" ) ")" ))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "r")) ")" ) ")" ))) ")" ))) ; theorem :: COMPLEX2:57 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" (Set (Var "a")) ($#k8_complex1 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "b")) "," (Set (Var "r")) ")" ")" ))))) ; theorem :: COMPLEX2:58 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "a")) ")" ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" ))))) ; theorem :: COMPLEX2:59 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" (Set (Var "a")) ($#k11_complex1 :::"-"::: ) (Set (Var "b")) ")" ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "b")) "," (Set (Var "r")) ")" ")" ))))) ; theorem :: COMPLEX2:60 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set (Var "a"))))) ; begin definitionlet "a", "b" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"angle"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Real":::) equals :: COMPLEX2:def 3 (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" "b" "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) "a" ")" ) ")" ) ")" ")" )) if (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) "a") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool "b" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) otherwise (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) "a" ")" )); end; :: deftheorem defines :::"angle"::: COMPLEX2:def 3 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "implies" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "b")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" ) ")" ) ")" ")" ))) ")" & (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")) ")" ))) ")" ) ")" )); theorem :: COMPLEX2:61 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "r")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "a")))))) ; theorem :: COMPLEX2:62 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "b")) "," (Set (Var "r")) ")" ")" ))))) ; theorem :: COMPLEX2:63 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_complex2 :::"angle"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" )))) ; theorem :: COMPLEX2:64 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "b"))))) "holds" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "b")) ")" )))) ; theorem :: COMPLEX2:65 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_complex2 :::"angle"::: ) "(" (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "b")) "," (Set (Var "r")) ")" ")" ) ")" )))) ; theorem :: COMPLEX2:66 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_complex2 :::"angle"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" )))) ; theorem :: COMPLEX2:67 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_complex2 :::"angle"::: ) "(" (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "b")) ")" ) ")" ))) ; theorem :: COMPLEX2:68 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k10_complex1 :::"-"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: COMPLEX2:69 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) ) ")" ))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) ) ")" ) ")" ))) ")" )) ; definitionlet "x", "y", "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"angle"::: "(" "x" "," "y" "," "z" ")" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: COMPLEX2:def 4 (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" "z" ($#k6_xcmplx_0 :::"-"::: ) "y" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "y" ")" ) ")" )) if (Bool (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" "z" ($#k6_xcmplx_0 :::"-"::: ) "y" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "y" ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" "z" ($#k6_xcmplx_0 :::"-"::: ) "y" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "y" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"angle"::: COMPLEX2:def 4 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "z")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "z")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "z")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "z")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" ))) ")" ")" )); theorem :: COMPLEX2:70 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" )) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) ; theorem :: COMPLEX2:71 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "z")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ) ")" ))) ; theorem :: COMPLEX2:72 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set "(" (Set (Var "a")) ($#k8_complex1 :::"+"::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "b")) ($#k8_complex1 :::"+"::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "c")) ($#k8_complex1 :::"+"::: ) (Set (Var "d")) ")" ) ")" ))) ; theorem :: COMPLEX2:73 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k3_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ))) ; theorem :: COMPLEX2:74 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" (Set (Var "z")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ))) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: COMPLEX2:75 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2))) "or" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) ")" )) ; theorem :: COMPLEX2:76 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" "(" (Bool "(" (Bool "(" (Bool (Bool "not" (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) )))) & (Bool (Bool "not" (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) ) ")" )))) ")" ) "or" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2))) "or" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) & (Bool "(" (Bool "(" (Bool (Bool "not" (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2)))) & (Bool (Bool "not" (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) ")" ) "or" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) ))) "or" (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "a")) ($#k1_complex2 :::".|."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) ) ")" ))) ")" ) ")" ) ; theorem :: COMPLEX2:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2))) "or" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) "holds" (Bool (Set (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k11_complex1 :::"-"::: ) (Set (Var "y")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k11_complex1 :::"-"::: ) (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#k5_square_1 :::"^2"::: ) ))) ; theorem :: COMPLEX2:78 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "a")) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "b")) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "c")) "," (Set (Var "r")) ")" ")" ) ")" )))) ; theorem :: COMPLEX2:79 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:80 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" )) ; theorem :: COMPLEX2:81 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:82 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ; theorem :: COMPLEX2:83 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Bool "not" (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool "not" (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: COMPLEX2:84 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )) ; theorem :: COMPLEX2:85 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 5) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: COMPLEX2:86 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: COMPLEX2:87 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "not" (Bool "(" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" ))) "holds" (Bool "(" (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) & (Bool (Set ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: COMPLEX2:88 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) "or" (Bool (Set (Set "(" (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_complex2 :::"angle"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 5) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) ")" ) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) ")" ) ")" )) ;