:: CFDIFF_2 semantic presentation begin theorem :: CFDIFF_2:1 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )) ; theorem :: CFDIFF_2:2 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "xy0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "u")))) & (Bool (Set (Set (Var "u")) ($#k1_seq_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ))) ")" ) ")" ) & (Bool (Set (Var "z0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x0")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y0")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) & (Bool (Set (Var "xy0")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "f")) ($#r1_cfdiff_1 :::"is_differentiable_in"::: ) (Set (Var "z0")))) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 1)) & (Bool (Set (Var "u")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 2)) & (Bool (Set (Var "v")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 1)) & (Bool (Set (Var "v")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 2)) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 1) ")" )) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "v")) "," (Set (Var "xy0")) "," (Num 2) ")" )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 2) ")" ")" ))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "v")) "," (Set (Var "xy0")) "," (Num 1) ")" )) ")" )))))) ; theorem :: CFDIFF_2:3 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: CFDIFF_2:4 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ))) ; theorem :: CFDIFF_2:5 (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "xy0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool (Set (Var "xy0")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "u"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "xy0")))) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 1)) & (Bool (Set (Var "u")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 2)) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 1) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set "(" ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "u")) ")" ) "," (Set (Var "xy0")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k10_finseq_1 :::"*>"::: ) ))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 2) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_pdiff_1 :::"diff"::: ) "(" (Set "(" ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "u")) ")" ) "," (Set (Var "xy0")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k10_finseq_1 :::"*>"::: ) ))) ")" )))) ; theorem :: CFDIFF_2:6 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" ($#k1_euclid :::"REAL"::: ) (Num 2) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "z0")) "being" ($#m1_hidden :::"Complex":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "xy0")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "u")))) & (Bool (Set (Set (Var "u")) ($#k1_seq_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "v")) ($#k1_seq_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ))) ")" ) ")" ) & (Bool (Set (Var "z0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x0")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y0")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) & (Bool (Set (Var "xy0")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x0")) "," (Set (Var "y0")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "u"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "xy0"))) & (Bool (Set ($#k3_pdiff_1 :::"<>*"::: ) (Set (Var "v"))) ($#r1_pdiff_1 :::"is_differentiable_in"::: ) (Set (Var "xy0"))) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "v")) "," (Set (Var "xy0")) "," (Num 2) ")" )) & (Bool (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "v")) "," (Set (Var "xy0")) "," (Num 1) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_cfdiff_1 :::"is_differentiable_in"::: ) (Set (Var "z0"))) & (Bool (Set (Var "u")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 1)) & (Bool (Set (Var "u")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 2)) & (Bool (Set (Var "v")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 1)) & (Bool (Set (Var "v")) ($#r3_pdiff_1 :::"is_partial_differentiable_in"::: ) (Set (Var "xy0")) "," (Num 2)) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 1) ")" )) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "v")) "," (Set (Var "xy0")) "," (Num 2) ")" )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "u")) "," (Set (Var "xy0")) "," (Num 2) ")" ")" ))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" ($#k2_cfdiff_1 :::"diff"::: ) "(" (Set (Var "f")) "," (Set (Var "z0")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pdiff_1 :::"partdiff"::: ) "(" (Set (Var "v")) "," (Set (Var "xy0")) "," (Num 1) ")" )) ")" )))))) ;