:: COMPLEX1  semantic presentation begin  






theorem :: COMPLEX1:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Re"::: "z" ->    ($#m1_hidden :::"set"::: )   means :: COMPLEX1:def 1 (Bool it  ($#r1_hidden :::"="::: )  "z") if (Bool "z"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  otherwise (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Num 2) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool "z"  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )); func  :::"Im"::: "z" ->    ($#m1_hidden :::"set"::: )   means :: COMPLEX1:def 2 (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) if (Bool "z"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  otherwise (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Num 2) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool "z"  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" )); end; 










:: deftheorem    defines :::"Re"::: COMPLEX1:def 1 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_complex1 :::"Re"::: )  (Set (Var "z")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Var "z")))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_complex1 :::"Re"::: )  (Set (Var "z")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Num 2) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" ))  ")" )  ")"   ")" ))); 
 
:: deftheorem    defines :::"Im"::: COMPLEX1:def 2 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_complex1 :::"Im"::: )  (Set (Var "z")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_complex1 :::"Im"::: )  (Set (Var "z")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Num 2) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1)))  ")" ))  ")" )  ")"   ")" ))); 
 registrationlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_complex1 :::"Re"::: )  "z") ->   ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set   ($#k2_complex1 :::"Im"::: )  "z") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"Re"::: redefine func  :::"Re"::: "z" ->   ($#m1_subset_1 :::"Real":::); :: original: :::"Im"::: redefine func  :::"Im"::: "z" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: COMPLEX1:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Num 2) "," (Set  ($#k1_numbers :::"REAL"::: ) ) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st" (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"   ($#k5_funct_4 :::"-->"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; 
 





theorem :: COMPLEX1:3 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z2"))))) "holds"  (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "z2")))) ; 
 definitionlet "z1", "z2" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; redefine pred "z1" :::"="::: "z2" means :: COMPLEX1:def 3 (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  "z1")  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  "z2")) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  "z1")  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  "z2"))  ")" ); end; 





:: deftheorem    defines :::"="::: COMPLEX1:def 3 :  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "z2"))) "iff" (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z2"))))  ")" )  ")" )); 
 notationsynonym  :::"0c":::  for  :::"0"::: ; end; definition:: original: :::"0c"::: redefine func  :::"0c":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); end; definitionfunc  :::"1r":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 4 (Num 1); :: original: :::"<i>"::: redefine func  :::"<i>":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); end; 




:: deftheorem    defines :::"1r"::: COMPLEX1:def 4 :  (Bool (Set   ($#k6_complex1 :::"1r"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)); 
 
theorem :: COMPLEX1:4 (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) ; 
 
theorem :: COMPLEX1:5 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (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"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:6 (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  ($#k6_complex1 :::"1r"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  ($#k6_complex1 :::"1r"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) ; 
 
theorem :: COMPLEX1:7 (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ) ; 
 definitionlet "z1", "z2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"+"::: redefine func "z1" :::"+"::: "z2" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 5 (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z1" ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z1" ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 






:: deftheorem    defines :::"+"::: COMPLEX1:def 5 :  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "z1"))  ($#k8_complex1 :::"+"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: COMPLEX1:8 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" )))  ")" )) ; 
 definitionlet "z1", "z2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"*"::: redefine func "z1" :::"*"::: "z2" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 6 (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z1" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z1" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z1" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z1" ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 






:: deftheorem    defines :::"*"::: COMPLEX1:def 6 :  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "z1"))  ($#k9_complex1 :::"*"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: COMPLEX1:9 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" ) ")" )))  ")" )) ; 
 
theorem :: COMPLEX1:10 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: COMPLEX1:11 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: COMPLEX1:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) ; 
 
theorem :: COMPLEX1:13 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "z")))) ; 
 
theorem :: COMPLEX1:14 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:15 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:16 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ")" )))  ")" )) ; 
 definitionlet "z" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"-"::: redefine func  :::"-"::: "z" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 7 (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 





:: deftheorem    defines :::"-"::: COMPLEX1:def 7 :  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set   ($#k10_complex1 :::"-"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: COMPLEX1:17 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )))  ")" )) ; 
 
theorem :: COMPLEX1:18 (Bool (Set (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k9_complex1 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  ($#k6_complex1 :::"1r"::: ) ))) ; 
 definitionlet "z1", "z2" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"-"::: redefine func "z1" :::"-"::: "z2" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 8 (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z1" ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z1" ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 






:: deftheorem    defines :::"-"::: COMPLEX1:def 8 :  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "z1"))  ($#k11_complex1 :::"-"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: COMPLEX1:19 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" )))  ")" )) ; 
 definitionlet "z" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); :: original: :::"""::: redefine func "z" :::""":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 9 (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 





:: deftheorem    defines :::"""::: COMPLEX1:def 9 :  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "z"))  ($#k12_complex1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k10_real_1 :::"/"::: )  (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"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (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"::: )  ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: COMPLEX1:20 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k10_real_1 :::"/"::: )  (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"::: )  ")" ) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (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 :: COMPLEX1:21 (Bool (Set (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k12_complex1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ))) ; 
 
theorem :: COMPLEX1:22 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k2_real_1 :::"""::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:23 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k2_real_1 :::"""::: )  ")" )))  ")" )) ; 
 definitionlet "z1", "z2" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"/"::: redefine func "z1" :::"/"::: "z2" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMPLEX1:def 10 (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z1" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z1" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z1" ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z1" ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z2" ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z2" ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); end; 






:: deftheorem    defines :::"/"::: COMPLEX1:def 10 :  (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 
theorem :: COMPLEX1:24 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))  ")" )) ; 
 
theorem :: COMPLEX1:25 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:26 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z1")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z2")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func "z" :::"*'":::  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   equals :: COMPLEX1:def 11 (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "b2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "b2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))) "holds"  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "b1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "b1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))))
 ; end; 





:: deftheorem    defines :::"*'"::: COMPLEX1:def 11 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "z"))  ($#k14_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))); 
 definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"*'"::: redefine func "z" :::"*'":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); end; 
theorem :: COMPLEX1:27 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )))  ")" )) ; 
 
theorem :: COMPLEX1:28 (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: COMPLEX1:29 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: COMPLEX1:30 (Bool (Set (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_complex1 :::"1r"::: )  )) ; 
 
theorem :: COMPLEX1:31 (Bool (Set (Set  ($#k7_complex1 :::"<i>"::: ) )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ))) ; 
 
theorem :: COMPLEX1:32 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "z2"))  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMPLEX1:33 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMPLEX1:34 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "z2"))  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMPLEX1:35 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set (Var "z2"))  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMPLEX1:36 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k12_complex1 :::"""::: )  ))) ; 
 
theorem :: COMPLEX1:37 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" )  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z1"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "z2"))  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMPLEX1:38 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "z")))) ; 
 
theorem :: COMPLEX1:39 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: COMPLEX1:40 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ))  ($#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"::: )  ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:41 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: COMPLEX1:42 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )))  ")" )) ; 
 definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func :::"|.":::"z":::".|"::: ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: COMPLEX1:def 12 (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  "z" ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  "z" ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )); projectivity  
(Bool  "for" (Set (Var "b1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "b2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "b2")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "b1")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "b1")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )))))
 ; end; 





:: deftheorem    defines :::"|."::: COMPLEX1:def 12 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k16_complex1 :::"|."::: ) (Set (Var "z")) ($#k16_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k7_square_1 :::"sqrt"::: )  (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"::: )  ")" ) ")" )))); 
 definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"|."::: redefine func :::"|.":::"z":::".|"::: ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: COMPLEX1:43 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 registration
cluster (Set  ($#k16_complex1 :::"|."::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k16_complex1 :::".|"::: ) ) ->   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xreal_0 :::"real"::: )   ; 
end; 
theorem :: COMPLEX1:44 (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 registrationlet "z" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set  ($#k16_complex1 :::"|."::: ) "z" ($#k16_complex1 :::".|"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xreal_0 :::"real"::: )   ; 
end; 
theorem :: COMPLEX1:45 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set  ($#k16_complex1 :::"|."::: ) "z" ($#k16_complex1 :::".|"::: ) ) ->   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; 
theorem :: COMPLEX1:46 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:47 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))  ")" )) ; 
 
theorem :: COMPLEX1:48 (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  ($#k6_complex1 :::"1r"::: ) ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: COMPLEX1:49 (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  ($#k7_complex1 :::"<i>"::: ) ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: COMPLEX1:50 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1: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_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:52 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:53 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:54 (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  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:55 (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  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:56 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: COMPLEX1:57 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: COMPLEX1:58 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:59 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:60 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z1")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:61 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "z2")))  ")" )) ; 
 
theorem :: COMPLEX1:62 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "z2"))) "iff" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))  ")" )) ; 
 
theorem :: COMPLEX1:63 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: COMPLEX1:64 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:65 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: COMPLEX1:66 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z"))  ($#k5_xcmplx_0 :::"""::: )  ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#k2_real_1 :::"""::: )  ))) ; 
 
theorem :: COMPLEX1:67 (Bool  "for" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:68 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#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 :: COMPLEX1:69 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k15_complex1 :::"*'"::: )  ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:70 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: COMPLEX1:71 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) "or" (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))  ")" )) ; 
 
theorem :: COMPLEX1:72 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: COMPLEX1:73 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k5_real_1 :::"-"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: COMPLEX1:74 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k3_real_1 :::"+"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" ) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: COMPLEX1:75 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: COMPLEX1:76 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ))  ")" )) ; 
 notationlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; synonym  :::"abs"::: "z" for :::"|.":::"z":::".|":::; end; definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"|."::: redefine func  :::"abs"::: "z" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: COMPLEX1:77 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "d"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))  ")" )) ; 
 
theorem :: COMPLEX1:78 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "a")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: COMPLEX1:79 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )))) ; 
 
theorem :: COMPLEX1:80 (Bool  "for" (Set (Var "z1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "z1")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) )))) ;