include('Axioms/HolSmt+2.ax').
fof(mem_c_2Ecomplex_2EIM,axiom,( mem(c_2Ecomplex_2EIM,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Erealax_2Ereal)) )).
fof(mem_c_2Ecomplex_2ERE,axiom,( mem(c_2Ecomplex_2ERE,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Erealax_2Ereal)) )).
fof(mem_c_2Ecomplex_2Earg,axiom,( mem(c_2Ecomplex_2Earg,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Erealax_2Ereal)) )).
fof(mem_c_2Ecomplex_2Ecomplex__add,axiom,( mem(c_2Ecomplex_2Ecomplex__add,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Ecomplex__div,axiom,( mem(c_2Ecomplex_2Ecomplex__div,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Ecomplex__exp,axiom,( mem(c_2Ecomplex_2Ecomplex__exp,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Ecomplex_2Ecomplex__inv,axiom,( mem(c_2Ecomplex_2Ecomplex__inv,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Ecomplex_2Ecomplex__mul,axiom,( mem(c_2Ecomplex_2Ecomplex__mul,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Ecomplex__neg,axiom,( mem(c_2Ecomplex_2Ecomplex__neg,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Ecomplex_2Ecomplex__of__num,axiom,( mem(c_2Ecomplex_2Ecomplex__of__num,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Ecomplex_2Ecomplex__of__real,axiom,( mem(c_2Ecomplex_2Ecomplex__of__real,arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Ecomplex_2Ecomplex__pow,axiom,( mem(c_2Ecomplex_2Ecomplex__pow,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Ecomplex__scalar__lmul,axiom,( mem(c_2Ecomplex_2Ecomplex__scalar__lmul,arr(ty_2Erealax_2Ereal,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Ecomplex__scalar__rmul,axiom,( mem(c_2Ecomplex_2Ecomplex__scalar__rmul,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Ecomplex__sub,axiom,( mem(c_2Ecomplex_2Ecomplex__sub,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))) )).
fof(mem_c_2Ecomplex_2Econj,axiom,( mem(c_2Ecomplex_2Econj,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))) )).
fof(mem_c_2Ecomplex_2Ei,axiom,( mem(c_2Ecomplex_2Ei,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) )).
fof(mem_c_2Ecomplex_2Emodu,axiom,( mem(c_2Ecomplex_2Emodu,arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ty_2Erealax_2Ereal)) )).
fof(conj_thm_2Ecomplex_2ECOMPLEX__LEMMA1,lemma,(! [V0a] : ( mem(V0a,ty_2Erealax_2Ereal) => ! [V1b] : ( mem(V1b,ty_2Erealax_2Ereal) => ! [V2c] : ( mem(V2c,ty_2Erealax_2Ereal) => ! [V3d] : ( mem(V3d,ty_2Erealax_2Ereal) => ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,V0a),V2c)),ap(ap(c_2Erealax_2Ereal__mul,V1b),V3d))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,V0a),V3d)),ap(ap(c_2Erealax_2Ereal__mul,V1b),V2c))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(ap(c_2Erealax_2Ereal__mul,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,V0a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,V1b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,V2c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,V3d),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__LEMMA2,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,V0x)),ap(c_2Etransc_2Esqrt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,V0x),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,V1y),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))))) ) ))).
fof(ax_thm_2Ecomplex_2ERE,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2ERE,V0z) = ap(c_2Epair_2EFST(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0z) ) )).
fof(ax_thm_2Ecomplex_2EIM,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2EIM,V0z) = ap(c_2Epair_2ESND(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0z) ) )).
fof(conj_thm_2Ecomplex_2ECOMPLEX,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2EIM,V0z)) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__RE__IM__EQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( V0z = V1w ) <=> ( ( ap(c_2Ecomplex_2ERE,V0z) = ap(c_2Ecomplex_2ERE,V1w) ) & ( ap(c_2Ecomplex_2EIM,V0z) = ap(c_2Ecomplex_2EIM,V1w) ) ) ) ) ))).
fof(ax_thm_2Ecomplex_2Ecomplex__of__real,axiom, ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Ecomplex__of__real,V0x) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),V0x),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) ) )).
fof(conj_thm_2Ecomplex_2ERE__COMPLEX__OF__REAL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2ERE,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)) = V0x ) ))).
fof(conj_thm_2Ecomplex_2EIM__COMPLEX__OF__REAL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2EIM,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ))).
fof(ax_thm_2Ecomplex_2Ecomplex__of__num,axiom, ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ecomplex_2Ecomplex__of__num,V0n) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(c_2Ereal_2Ereal__of__num,V0n)) ) )).
fof(conj_thm_2Ecomplex_2ECOMPLEX__0,lemma,(( ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__1,lemma,(( ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__10,lemma,(( ~~ ( ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__0__THM,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ))).
fof(ax_thm_2Ecomplex_2Ei,axiom, ( c_2Ecomplex_2Ei = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) )).
fof(ax_thm_2Ecomplex_2Ecomplex__add,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(ap(c_2Erealax_2Ereal__add,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2ERE,V1w))),ap(ap(c_2Erealax_2Ereal__add,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2EIM,V1w))) ) ) )).
fof(ax_thm_2Ecomplex_2Ecomplex__neg,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,V0z) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Erealax_2Ereal__neg,ap(c_2Ecomplex_2ERE,V0z))),ap(c_2Erealax_2Ereal__neg,ap(c_2Ecomplex_2EIM,V0z))) ) )).
fof(ax_thm_2Ecomplex_2Ecomplex__mul,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2Ereal__sub,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2ERE,V1w))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2EIM,V1w)))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2EIM,V1w))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2ERE,V1w)))) ) ) )).
fof(ax_thm_2Ecomplex_2Ecomplex__inv,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__inv,V0z) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(ap(c_2Ereal_2E_2F,ap(c_2Erealax_2Ereal__neg,ap(c_2Ecomplex_2EIM,V0z))),ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) )).
fof(ax_thm_2Ecomplex_2Ecomplex__sub,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) ) ) )).
fof(ax_thm_2Ecomplex_2Ecomplex__div,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Ecomplex__inv,V1w)) ) ) )).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__COMM,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__add,V1w),V0z) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__ASSOC,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),ap(ap(c_2Ecomplex_2Ecomplex__add,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)),V2v) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RID,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LID,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)),V0z) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RINV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),ap(c_2Ecomplex_2Ecomplex__neg,V0z)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LINV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__COMM,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V0z) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__ASSOC,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)),V2v) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RID,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LID,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0z) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RINV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Ecomplex__inv,V0z)) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LINV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__inv,V0z)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LDISTRIB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(ap(c_2Ecomplex_2Ecomplex__add,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RDISTRIB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)),V2v) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2v)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V2v) ) <=> ( V1w = V2v ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V2v) = ap(ap(c_2Ecomplex_2Ecomplex__add,V1w),V2v) ) <=> ( V0z = V1w ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RID__UNIQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = V0z ) <=> ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LID__UNIQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = V1w ) <=> ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEGNEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(c_2Ecomplex_2Ecomplex__neg,V0z)) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__EQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Ecomplex__neg,V0z) = V1w ) <=> ( V0z = ap(c_2Ecomplex_2Ecomplex__neg,V1w) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__NEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Ecomplex__neg,V0z) = ap(c_2Ecomplex_2Ecomplex__neg,V1w) ) <=> ( V0z = V1w ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__RNEG__UNIQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( V1w = ap(c_2Ecomplex_2Ecomplex__neg,V0z) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__LNEG__UNIQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( V0z = ap(c_2Ecomplex_2Ecomplex__neg,V1w) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__ADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__LMUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__RMUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__MUL2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ENTIRE,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) | ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__0,lemma,(( ap(c_2Ecomplex_2Ecomplex__neg,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__EQ0,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Ecomplex__neg,V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__REFL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__LZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)),V0z) = ap(c_2Ecomplex_2Ecomplex__neg,V0z) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__LNEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),V1w) = ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__NEG2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V0z) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__SUB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V0z) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RNEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__ADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)),V1w) = V0z ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__ADD2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V1w),ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)) = V0z ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__SUB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)),V0z) = V1w ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SUB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)),V0z) = ap(c_2Ecomplex_2Ecomplex__neg,V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SUB2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)) = V1w ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__SUB2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)) = ap(c_2Ecomplex_2Ecomplex__neg,V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD2__SUB2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2u] : ( mem(V2u,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3v] : ( mem(V3v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__add,V2u),V3v)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V2u)),ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V3v)) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__TRIANGLE,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V2v) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__0,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( V0z = V1w ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__SUB__LADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( V0z = ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V2v) ) <=> ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V2v) = V1w ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__SUB__RADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w) = V2v ) <=> ( V0z = ap(ap(c_2Ecomplex_2Ecomplex__add,V2v),V1w) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RNEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) = ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LNEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),V1w) = ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__LDISTRIB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RDISTRIB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)),V2v) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2v)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIFFSQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V0z)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LMUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v) ) <=> ( ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) | ( V1w = V2v ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RMUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2v) ) <=> ( ( V2v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) | ( V0z = V1w ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LMUL2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ( V1w = V2v ) <=> ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v) ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RMUL__IMP,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V0z) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V2v),V0z) ) ) => ( V1w = V2v ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LMUL__IMP,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v) ) ) => ( V1w = V2v ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__INV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__neg,V0z)) = ap(c_2Ecomplex_2Ecomplex__neg,ap(c_2Ecomplex_2Ecomplex__inv,V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__MUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__inv,V0z)),ap(c_2Ecomplex_2Ecomplex__inv,V1w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INVINV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__inv,V0z)) = V0z ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__LINV__UNIQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) => ( V0z = ap(c_2Ecomplex_2Ecomplex__inv,V1w) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__RINV__UNIQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) => ( V1w = ap(c_2Ecomplex_2Ecomplex__inv,V0z) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__0,lemma,(( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV1,lemma,(( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__INV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__inv,V0z)) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__NEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__neg,V0z)) = ap(c_2Ecomplex_2Ecomplex__neg,ap(c_2Ecomplex_2Ecomplex__inv,V0z)) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__EQ__0,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Ecomplex__inv,V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__NZ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ~~ ( ap(c_2Ecomplex_2Ecomplex__inv,V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__INJ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Ecomplex__inv,V0z) = ap(c_2Ecomplex_2Ecomplex__inv,V1w) ) <=> ( V0z = V1w ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__LDIV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__RDIV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__DIV2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(c_2Ecomplex_2Ecomplex__neg,V0z)),ap(c_2Ecomplex_2Ecomplex__neg,V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__1OVER,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__inv,V0z) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0z) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV1,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__ADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V2v)),ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)),V2v) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__SUB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V2v)),ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)),V2v) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__RMUL__CANCEL,lemma,(! [V0v] : ( mem(V0v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),V0v)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V2w),V0v)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V1z),V2w) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__LMUL__CANCEL,lemma,(! [V0v] : ( mem(V0v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0v),V1z)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V0v),V2w)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V1z),V2w) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__DENOM__CANCEL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V0z)),ap(ap(c_2Ecomplex_2Ecomplex__div,V2v),V0z)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V2v) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__INNER__CANCEL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V0z)),ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V2v)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V2v) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__OUTER__CANCEL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__div,V2v),V0z)) = ap(ap(c_2Ecomplex_2Ecomplex__div,V2v),V1w) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__MUL2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,V2v),V1w) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RAT,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2u] : ( mem(V2u,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3v] : ( mem(V3v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V3v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__div,V2u),V3v)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V3v)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2u))),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V3v)) ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RAT,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2u] : ( mem(V2u,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3v] : ( mem(V3v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V3v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)),ap(ap(c_2Ecomplex_2Ecomplex__div,V2u),V3v)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V3v)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2u))),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V3v)) ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__LZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__REFL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__INV2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(c_2Ecomplex_2Ecomplex__inv,V0z)),ap(c_2Ecomplex_2Ecomplex__inv,V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V0z)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RDIV__EQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V2v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ( V0z = ap(ap(c_2Ecomplex_2Ecomplex__div,V1w),V2v) ) <=> ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V2v) = V1w ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LDIV__EQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2v] : ( mem(V2v,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V2v = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V2v) = V1w ) <=> ( V0z = ap(ap(c_2Ecomplex_2Ecomplex__mul,V1w),V2v) ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__EQ,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ( ap(c_2Ecomplex_2Ecomplex__of__real,V0x) = ap(c_2Ecomplex_2Ecomplex__of__real,V1y) ) <=> ( V0x = V1y ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__ADD,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)),ap(c_2Ecomplex_2Ecomplex__of__real,V1y)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__NEG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(c_2Erealax_2Ereal__neg,V0x)) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__MUL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)),ap(c_2Ecomplex_2Ecomplex__of__real,V1y)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Erealax_2Ereal__mul,V0x),V1y)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__INV,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(c_2Erealax_2Einv,V0x)) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__SUB,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)),ap(c_2Ecomplex_2Ecomplex__of__real,V1y)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Ereal_2Ereal__sub,V0x),V1y)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__DIV,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)),ap(c_2Ecomplex_2Ecomplex__of__real,V1y)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Ereal_2E_2F,V0x),V1y)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__NUM__EQ,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(c_2Ecomplex_2Ecomplex__of__num,V0m) = ap(c_2Ecomplex_2Ecomplex__of__num,V1n) ) <=> ( V0m = V1n ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__NUM__ADD,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,ap(c_2Ecomplex_2Ecomplex__of__num,V0m)),ap(c_2Ecomplex_2Ecomplex__of__num,V1n)) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(ap(c_2Earithmetic_2E_2B,V0m),V1n)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__OF__NUM__MUL,lemma,(! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Ecomplex__of__num,V0m)),ap(c_2Ecomplex_2Ecomplex__of__num,V1n)) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(ap(c_2Earithmetic_2E_2A,V0m),V1n)) ) ) ))).
fof(ax_thm_2Ecomplex_2Ecomplex__scalar__lmul,axiom, ! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(ap(c_2Erealax_2Ereal__mul,V0k),ap(c_2Ecomplex_2ERE,V1z))),ap(ap(c_2Erealax_2Ereal__mul,V0k),ap(c_2Ecomplex_2EIM,V1z))) ) ) )).
fof(ax_thm_2Ecomplex_2Ecomplex__scalar__rmul,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1k] : ( mem(V1k,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V0z),V1k) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2ERE,V0z)),V1k)),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2EIM,V0z)),V1k)) ) ) )).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1l),V2z)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Erealax_2Ereal__mul,V0k),V1l)),V2z) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__NEG,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Erealax_2Ereal__neg,V0k)),V1z) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(c_2Ecomplex_2Ecomplex__neg,V1z)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Erealax_2Ereal__neg,V0k)),V1z) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ADD,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Erealax_2Ereal__add,V0k),V1l)),V2z) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2z)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1l),V2z)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__SUB,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Ereal_2Ereal__sub,V0k),V1l)),V2z) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2z)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1l),V2z)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(ap(c_2Ecomplex_2Ecomplex__add,V1z),V2w)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(ap(c_2Ecomplex_2Ecomplex__sub,V1z),V2w)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__SCALAR__LMUL2,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3w] : ( mem(V3w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2z)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1l),V3w)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Erealax_2Ereal__mul,V0k),V1l)),ap(ap(c_2Ecomplex_2Ecomplex__mul,V2z),V3w)) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__LMUL__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)),V2w) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),V2w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__RMUL__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2w)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),V2w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ZERO__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ONE,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0z) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__NEG1,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),V0z) = ap(c_2Ecomplex_2Ecomplex__neg,V0z) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DOUBLE,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V0z) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),V0z) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ENTIRE,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( ( V0k = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) | ( V1z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__EQ__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2w) ) <=> ( ( V0k = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) | ( V1z = V2w ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__EQ,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2z) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1l),V2z) ) <=> ( ( V0k = V1l ) | ( V2z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__EQ1,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z) = V1z ) <=> ( ( V0k = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) | ( V1z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V0k = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V1z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Erealax_2Einv,V0k)),ap(c_2Ecomplex_2Ecomplex__inv,V1z)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__DIV2,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V3w] : ( mem(V3w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ( ~~ ( V1l = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) & ( ~~ ( V3w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V2z)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1l),V3w)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Ereal_2E_2F,V0k),V1l)),ap(ap(c_2Ecomplex_2Ecomplex__div,V2z),V3w)) ) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__MUL__COMM,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V1z),V0k) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),V0k)),V1l) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),ap(ap(c_2Erealax_2Ereal__mul,V0k),V1l)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__NEG,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__neg,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V1z),V0k)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V1z),ap(c_2Erealax_2Ereal__neg,V0k)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__NEG__SCALAR__RMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,ap(c_2Ecomplex_2Ecomplex__neg,V1z)),V0k) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V1z),ap(c_2Erealax_2Ereal__neg,V0k)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__ADD,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),ap(ap(c_2Erealax_2Ereal__add,V0k),V1l)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),V0k)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),V1l)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__RSCALAR__RMUL__SUB,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1l] : ( mem(V1l,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),ap(ap(c_2Ereal_2Ereal__sub,V0k),V1l)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),V0k)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2z),V1l)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RSCALAR__RMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,ap(ap(c_2Ecomplex_2Ecomplex__add,V1z),V2w)),V0k) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V1z),V0k)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2w),V0k)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SCALAR__RMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,ap(ap(c_2Ecomplex_2Ecomplex__sub,V1z),V2w)),V0k) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V1z),V0k)),ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V2w),V0k)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__ZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V0z),ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__ZERO__SCALAR__RMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)),V0k) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__ONE,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V0z),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__NEG1,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,V0z),ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) = ap(c_2Ecomplex_2Ecomplex__neg,V0z) ) ))).
fof(ax_thm_2Ecomplex_2Econj,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,V0z) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Erealax_2Ereal__neg,ap(c_2Ecomplex_2EIM,V0z))) ) )).
fof(conj_thm_2Ecomplex_2ECONJ__REAL__REFL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Econj,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)) = ap(c_2Ecomplex_2Ecomplex__of__real,V0x) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__NUM__REFL,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ecomplex_2Econj,ap(c_2Ecomplex_2Ecomplex__of__num,V0n)) = ap(c_2Ecomplex_2Ecomplex__of__num,V0n) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__ADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(ap(c_2Ecomplex_2Ecomplex__add,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__add,ap(c_2Ecomplex_2Econj,V0z)),ap(c_2Ecomplex_2Econj,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__NEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(c_2Ecomplex_2Ecomplex__neg,V0z)) = ap(c_2Ecomplex_2Ecomplex__neg,ap(c_2Ecomplex_2Econj,V0z)) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__SUB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__sub,ap(c_2Ecomplex_2Econj,V0z)),ap(c_2Ecomplex_2Econj,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__MUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Econj,V0z)),ap(c_2Ecomplex_2Econj,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__INV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(c_2Ecomplex_2Ecomplex__inv,V0z)) = ap(c_2Ecomplex_2Ecomplex__inv,ap(c_2Ecomplex_2Econj,V0z)) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__DIV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(c_2Ecomplex_2Econj,V0z)),ap(c_2Ecomplex_2Econj,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),ap(c_2Ecomplex_2Econj,V1z)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__CONJ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Econj,ap(c_2Ecomplex_2Econj,V0z)) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__EQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Econj,V0z) = V1w ) <=> ( V0z = ap(c_2Ecomplex_2Econj,V1w) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__EQ2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(c_2Ecomplex_2Econj,V0z) = ap(c_2Ecomplex_2Econj,V1w) ) <=> ( V0z = V1w ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RCONJ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Econj,V0z)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LCONJ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Econj,V0z)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) ))).
fof(conj_thm_2Ecomplex_2ECONJ__ZERO,lemma,(( ap(c_2Ecomplex_2Econj,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ))).
fof(ax_thm_2Ecomplex_2Emodu,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Emodu,V0z) = ap(c_2Etransc_2Esqrt,ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))) ) )).
fof(ax_thm_2Ecomplex_2Earg,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Earg,V0z) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ecomplex_2EIM,V0z))),ap(c_2Etransc_2Eacs,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))),ap(ap(c_2Erealax_2Ereal__add,ap(c_2Erealax_2Ereal__neg,ap(c_2Etransc_2Eacs,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z))))),ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),c_2Etransc_2Epi))) ) )).
fof(conj_thm_2Ecomplex_2EMODU__POW2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = ap(ap(c_2Erealax_2Ereal__add,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))),ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ))).
fof(conj_thm_2Ecomplex_2ERE__IM__LE__MODU,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Ecomplex_2ERE,V0z))),ap(c_2Ecomplex_2Emodu,V0z))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Ecomplex_2EIM,V0z))),ap(c_2Ecomplex_2Emodu,V0z))) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__POS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ecomplex_2Emodu,V0z))) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RCONJ1,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),ap(c_2Ecomplex_2Econj,V0z)) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LCONJ1,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(c_2Ecomplex_2Econj,V0z)),V0z) = ap(c_2Ecomplex_2Ecomplex__of__real,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__NEG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Ecomplex__neg,V0z)) = ap(c_2Ecomplex_2Emodu,V0z) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__SUB,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Emodu,ap(ap(c_2Ecomplex_2Ecomplex__sub,V0z),V1w)) = ap(c_2Ecomplex_2Emodu,ap(ap(c_2Ecomplex_2Ecomplex__sub,V1w),V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__CONJ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Econj,V0z)) = ap(c_2Ecomplex_2Emodu,V0z) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__MUL,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Emodu,ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V1w)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Ecomplex_2Emodu,V1w)) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__0,lemma,(( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ))).
fof(conj_thm_2Ecomplex_2EMODU__1,lemma,(( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ))).
fof(conj_thm_2Ecomplex_2EMODU__COMPLEX__INV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Ecomplex__inv,V0z)) = ap(c_2Erealax_2Einv,ap(c_2Ecomplex_2Emodu,V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__DIV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V1w = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Ecomplex_2Emodu,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)) = ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Ecomplex_2Emodu,V1w)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__SCALAR__LMUL,lemma,(! [V0k] : ( mem(V0k,ty_2Erealax_2Ereal) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Emodu,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V0k),V1z)) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Eabs,V0k)),ap(c_2Ecomplex_2Emodu,V1z)) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__REAL,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Ecomplex__of__real,V0x)) = ap(c_2Ereal_2Eabs,V0x) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__NUM,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ecomplex_2Emodu,ap(c_2Ecomplex_2Ecomplex__of__num,V0n)) = ap(c_2Ereal_2Ereal__of__num,V0n) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__ZERO,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( ap(c_2Ecomplex_2Emodu,V0z) = ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__NZ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) <=> p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ecomplex_2Emodu,V0z))) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__CASES,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) | p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Ecomplex_2Emodu,V0z))) ) ))).
fof(conj_thm_2Ecomplex_2ERE__DIV__MODU__BOUNDS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Ecomplex_2EIM__DIV__MODU__BOUNDS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))),ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ))).
fof(conj_thm_2Ecomplex_2ERE__DIV__MODU__ACS__BOUNDS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,c_2Enum_2E0)),ap(c_2Etransc_2Eacs,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z))))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Eacs,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))),c_2Etransc_2Epi)) ) ) ))).
fof(conj_thm_2Ecomplex_2EIM__DIV__MODU__ASN__BOUNDS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))),ap(c_2Etransc_2Easn,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z))))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Etransc_2Easn,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))),ap(ap(c_2Ereal_2E_2F,c_2Etransc_2Epi),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))))) ) ) ))).
fof(conj_thm_2Ecomplex_2ERE__DIV__MODU__ACS__COS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Etransc_2Ecos,ap(c_2Etransc_2Eacs,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))) = ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2EIM__DIV__MODU__ASN__SIN,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Etransc_2Esin,ap(c_2Etransc_2Easn,ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z)))) = ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2EARG__COS,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Etransc_2Ecos,ap(c_2Ecomplex_2Earg,V0z)) = ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2ERE,V0z)),ap(c_2Ecomplex_2Emodu,V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2EARG__SIN,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ap(c_2Etransc_2Esin,ap(c_2Ecomplex_2Earg,V0z)) = ap(ap(c_2Ereal_2E_2F,ap(c_2Ecomplex_2EIM,V0z)),ap(c_2Ecomplex_2Emodu,V0z)) ) ) ))).
fof(conj_thm_2Ecomplex_2ERE__MODU__ARG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2ERE,V0z) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Etransc_2Ecos,ap(c_2Ecomplex_2Earg,V0z))) ) ))).
fof(conj_thm_2Ecomplex_2EIM__MODU__ARG,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2EIM,V0z) = ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ecomplex_2Emodu,V0z)),ap(c_2Etransc_2Esin,ap(c_2Ecomplex_2Earg,V0z))) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__TRIANGLE,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Ecomplex_2Emodu,V0z)),ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(c_2Ecomplex_2Earg,V0z))),ap(c_2Etransc_2Esin,ap(c_2Ecomplex_2Earg,V0z)))) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MODU__ARG__EQ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( V0z = V1w ) <=> ( ( ap(c_2Ecomplex_2Emodu,V0z) = ap(c_2Ecomplex_2Emodu,V1w) ) & ( ap(c_2Ecomplex_2Earg,V0z) = ap(c_2Ecomplex_2Earg,V1w) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__UNIT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,A_27a) => ( ap(c_2Ecomplex_2Emodu,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V0x))) = ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) )))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__MUL__ARG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V0x))),ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V1y)),ap(c_2Etransc_2Esin,V1y))) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y))),ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__add,V0x),V1y))) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__INV__ARG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V0x))) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(c_2Erealax_2Ereal__neg,V0x))),ap(c_2Etransc_2Esin,ap(c_2Erealax_2Ereal__neg,V0x))) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__DIV__ARG,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1y] : ( mem(V1y,ty_2Erealax_2Ereal) => ( ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V0x))),ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V1y)),ap(c_2Etransc_2Esin,V1y))) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(ap(c_2Ereal_2Ereal__sub,V0x),V1y))),ap(c_2Etransc_2Esin,ap(ap(c_2Ereal_2Ereal__sub,V0x),V1y))) ) ) ))).
fof(ax_thm_2Ecomplex_2Ecomplex__pow__def,axiom, ( ( ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),c_2Enum_2E0) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),ap(c_2Enum_2ESUC,V2n)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),V2n)) ) ) ) )).
fof(conj_thm_2Ecomplex_2Ecomplex__pow__def__compute,lemma,(( ( ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),c_2Enum_2E0) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) ) & ( ( ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V2n))) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V2n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))))) ) ) ) ) & ! [V3z] : ( mem(V3z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V4n] : ( mem(V4n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V3z),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V4n))) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V3z),ap(ap(c_2Ecomplex_2Ecomplex__pow,V3z),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V4n)))) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__0,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0)),ap(c_2Enum_2ESUC,V0n)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__NZ,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ( ~~ ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V1n) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POWINV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ~~ ( V0z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Ecomplex_2Ecomplex__inv,ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V1n)) = ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(c_2Ecomplex_2Ecomplex__inv,V0z)),V1n) ) ) ) ))).
fof(conj_thm_2Ecomplex_2EMODU__COMPLEX__POW,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(c_2Ecomplex_2Emodu,ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V1n)) = ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2Emodu,V0z)),V1n) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__ADD,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),ap(ap(c_2Earithmetic_2E_2B,V1m),V2n)) = ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V1m)),ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V2n)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__1,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) = V0z ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__2,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = ap(ap(c_2Ecomplex_2Ecomplex__mul,V0z),V0z) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__ONE,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V0n) = ap(c_2Ecomplex_2Ecomplex__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__MUL,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2w] : ( mem(V2w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(ap(c_2Ecomplex_2Ecomplex__mul,V1z),V2w)),V0n) = ap(ap(c_2Ecomplex_2Ecomplex__mul,ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),V0n)),ap(ap(c_2Ecomplex_2Ecomplex__pow,V2w),V0n)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__INV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(c_2Ecomplex_2Ecomplex__inv,V0z)),V1n) = ap(c_2Ecomplex_2Ecomplex__inv,ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V1n)) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__DIV,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1w] : ( mem(V1w,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(ap(c_2Ecomplex_2Ecomplex__div,V0z),V1w)),V2n) = ap(ap(c_2Ecomplex_2Ecomplex__div,ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V2n)),ap(ap(c_2Ecomplex_2Ecomplex__pow,V1w),V2n)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__L,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1k] : ( mem(V1k,ty_2Erealax_2Ereal) => ! [V2z] : ( mem(V2z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,V1k),V2z)),V0n) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Ereal_2Epow,V1k),V0n)),ap(ap(c_2Ecomplex_2Ecomplex__pow,V2z),V0n)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__ZERO,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),V0n) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) => ( V1z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__ZERO__EQ,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1z] : ( mem(V1z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ( ap(ap(c_2Ecomplex_2Ecomplex__pow,V1z),ap(c_2Enum_2ESUC,V0n)) = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) <=> ( V1z = ap(c_2Ecomplex_2Ecomplex__of__num,c_2Enum_2E0) ) ) ) ))).
fof(conj_thm_2Ecomplex_2ECOMPLEX__POW__POW,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),V1m)),V2n) = ap(ap(c_2Ecomplex_2Ecomplex__pow,V0z),ap(ap(c_2Earithmetic_2E_2A,V1m),V2n)) ) ) ) ))).
fof(conj_thm_2Ecomplex_2EDE__MOIVRE__LEMMA,lemma,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V0x))),V1n) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),V0x))),ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),V0x))) ) ) ))).
fof(conj_thm_2Ecomplex_2EDE__MOIVRE__THM,lemma,(! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Ecomplex_2Ecomplex__pow,ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Ecomplex_2Emodu,V0z)),ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(c_2Ecomplex_2Earg,V0z))),ap(c_2Etransc_2Esin,ap(c_2Ecomplex_2Earg,V0z))))),V1n) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(ap(c_2Ereal_2Epow,ap(c_2Ecomplex_2Emodu,V0z)),V1n)),ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),ap(c_2Ecomplex_2Earg,V0z)))),ap(c_2Etransc_2Esin,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,V1n)),ap(c_2Ecomplex_2Earg,V0z))))) ) ) ))).
fof(ax_thm_2Ecomplex_2Ecomplex__exp,axiom, ! [V0z] : ( mem(V0z,ty_2Epair_2Eprod(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)) => ( ap(c_2Ecomplex_2Ecomplex__exp,V0z) = ap(ap(c_2Ecomplex_2Ecomplex__scalar__lmul,ap(c_2Etransc_2Eexp,ap(c_2Ecomplex_2ERE,V0z))),ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,ap(c_2Ecomplex_2EIM,V0z))),ap(c_2Etransc_2Esin,ap(c_2Ecomplex_2EIM,V0z)))) ) )).
fof(conj_thm_2Ecomplex_2EEXP__IMAGINARY,conjecture,(! [V0x] : ( mem(V0x,ty_2Erealax_2Ereal) => ( ap(c_2Ecomplex_2Ecomplex__exp,ap(ap(c_2Ecomplex_2Ecomplex__scalar__rmul,c_2Ecomplex_2Ei),V0x)) = ap(ap(c_2Epair_2E_2C(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),ap(c_2Etransc_2Ecos,V0x)),ap(c_2Etransc_2Esin,V0x)) ) ))).
