tt('const/complex/IM', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > 'type/realax/real')).
tt('const/complex/RE', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > 'type/realax/real')).
tt('const/complex/arg', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > 'type/realax/real')).
tt('const/complex/complex_add', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/complex_div', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/complex_exp', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real'))).
tt('const/complex/complex_inv', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real'))).
tt('const/complex/complex_mul', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/complex_neg', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real'))).
tt('const/complex/complex_of_num', ty, ('type/num/num' > ('type/pair/prod' 'type/realax/real' 'type/realax/real'))).
tt('const/complex/complex_of_real', ty, ('type/realax/real' > ('type/pair/prod' 'type/realax/real' 'type/realax/real'))).
tt('const/complex/complex_pow', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/num/num' > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/complex_scalar_lmul', ty, ('type/realax/real' > (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/complex_scalar_rmul', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/realax/real' > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/complex_sub', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real')))).
tt('const/complex/conj', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > ('type/pair/prod' 'type/realax/real' 'type/realax/real'))).
tt('const/complex/i', ty, ('type/pair/prod' 'type/realax/real' 'type/realax/real')).
tt('const/complex/modu', ty, (('type/pair/prod' 'type/realax/real' 'type/realax/real') > 'type/realax/real')).
tt('thm/complex/COMPLEX_LEMMA1_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real', d : 'type/realax/real']: (('const/realax/real_add' ('const/real/pow' ('const/real/real_sub' ('const/realax/real_mul' a c) ('const/realax/real_mul' b d)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/realax/real_add' ('const/realax/real_mul' a d) ('const/realax/real_mul' b c)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/realax/real_mul' ('const/realax/real_add' ('const/real/pow' a ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' b ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/realax/real_add' ('const/real/pow' c ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' d ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/COMPLEX_LEMMA2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/abs' x) ('const/transc/sqrt' ('const/realax/real_add' ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' y ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/RE_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/RE' z) = (('const/pair/FST' 'type/realax/real' 'type/realax/real') z)))).
tt('thm/complex/IM_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/IM' z) = (('const/pair/SND' 'type/realax/real' 'type/realax/real') z)))).
tt('thm/complex/COMPLEX_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/complex/RE' z) ('const/complex/IM' z)) = z))).
tt('thm/complex/COMPLEX_RE_IM_EQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((z = w) = ((('const/complex/RE' z) = ('const/complex/RE' w)) & (('const/complex/IM' z) = ('const/complex/IM' w)))))).
tt('thm/complex/complex_of_real_', def, (![x : 'type/realax/real']: (('const/complex/complex_of_real' x) = (('const/pair/,' 'type/realax/real' 'type/realax/real') x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/complex/RE_COMPLEX_OF_REAL_', ax, (![x : 'type/realax/real']: (('const/complex/RE' ('const/complex/complex_of_real' x)) = x))).
tt('thm/complex/IM_COMPLEX_OF_REAL_', ax, (![x : 'type/realax/real']: (('const/complex/IM' ('const/complex/complex_of_real' x)) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/complex/complex_of_num_', def, (![n : 'type/num/num']: (('const/complex/complex_of_num' n) = ('const/complex/complex_of_real' ('const/real/real_of_num' n))))).
tt('thm/complex/COMPLEX_0_', ax, (('const/complex/complex_of_num' 'const/num/0') = ('const/complex/complex_of_real' ('const/real/real_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_1_', ax, (('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ('const/complex/complex_of_real' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/COMPLEX_10_', ax, (~ (('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_0_THM_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((z = ('const/complex/complex_of_num' 'const/num/0')) = (('const/realax/real_add' ('const/real/pow' ('const/complex/RE' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/complex/IM' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/complex/i_', def, ('const/complex/i' = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/complex_add_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' z w) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/realax/real_add' ('const/complex/RE' z) ('const/complex/RE' w)) ('const/realax/real_add' ('const/complex/IM' z) ('const/complex/IM' w)))))).
tt('thm/complex/complex_neg_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' z) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/realax/real_neg' ('const/complex/RE' z)) ('const/realax/real_neg' ('const/complex/IM' z)))))).
tt('thm/complex/complex_mul_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z w) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/real/real_sub' ('const/realax/real_mul' ('const/complex/RE' z) ('const/complex/RE' w)) ('const/realax/real_mul' ('const/complex/IM' z) ('const/complex/IM' w))) ('const/realax/real_add' ('const/realax/real_mul' ('const/complex/RE' z) ('const/complex/IM' w)) ('const/realax/real_mul' ('const/complex/IM' z) ('const/complex/RE' w))))))).
tt('thm/complex/complex_inv_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_inv' z) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/real/#slash#' ('const/complex/RE' z) ('const/realax/real_add' ('const/real/pow' ('const/complex/RE' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/complex/IM' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/real/#slash#' ('const/realax/real_neg' ('const/complex/IM' z)) ('const/realax/real_add' ('const/real/pow' ('const/complex/RE' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/complex/IM' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/complex/complex_sub_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' z w) = ('const/complex/complex_add' z ('const/complex/complex_neg' w))))).
tt('thm/complex/complex_div_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_div' z w) = ('const/complex/complex_mul' z ('const/complex/complex_inv' w))))).
tt('thm/complex/COMPLEX_ADD_COMM_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' z w) = ('const/complex/complex_add' w z)))).
tt('thm/complex/COMPLEX_ADD_ASSOC_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' z ('const/complex/complex_add' w v)) = ('const/complex/complex_add' ('const/complex/complex_add' z w) v)))).
tt('thm/complex/COMPLEX_ADD_RID_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' z ('const/complex/complex_of_num' 'const/num/0')) = z))).
tt('thm/complex/COMPLEX_ADD_LID_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' ('const/complex/complex_of_num' 'const/num/0') z) = z))).
tt('thm/complex/COMPLEX_ADD_RINV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' z ('const/complex/complex_neg' z)) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_ADD_LINV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' ('const/complex/complex_neg' z) z) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_MUL_COMM_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z w) = ('const/complex/complex_mul' w z)))).
tt('thm/complex/COMPLEX_MUL_ASSOC_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_mul' w v)) = ('const/complex/complex_mul' ('const/complex/complex_mul' z w) v)))).
tt('thm/complex/COMPLEX_MUL_RID_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = z))).
tt('thm/complex/COMPLEX_MUL_LID_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z) = z))).
tt('thm/complex/COMPLEX_MUL_RINV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_mul' z ('const/complex/complex_inv' z)) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/complex/COMPLEX_MUL_LINV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_mul' ('const/complex/complex_inv' z) z) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/complex/COMPLEX_ADD_LDISTRIB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_add' w v)) = ('const/complex/complex_add' ('const/complex/complex_mul' z w) ('const/complex/complex_mul' z v))))).
tt('thm/complex/COMPLEX_ADD_RDISTRIB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_add' z w) v) = ('const/complex/complex_add' ('const/complex/complex_mul' z v) ('const/complex/complex_mul' w v))))).
tt('thm/complex/COMPLEX_EQ_LADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_add' z w) = ('const/complex/complex_add' z v)) = (w = v)))).
tt('thm/complex/COMPLEX_EQ_RADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_add' z v) = ('const/complex/complex_add' w v)) = (z = w)))).
tt('thm/complex/COMPLEX_ADD_RID_UNIQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_add' z w) = z) = (w = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_ADD_LID_UNIQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_add' z w) = w) = (z = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_NEGNEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_neg' z)) = z))).
tt('thm/complex/COMPLEX_NEG_EQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_neg' z) = w) = (z = ('const/complex/complex_neg' w))))).
tt('thm/complex/COMPLEX_EQ_NEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_neg' z) = ('const/complex/complex_neg' w)) = (z = w)))).
tt('thm/complex/COMPLEX_RNEG_UNIQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_add' z w) = ('const/complex/complex_of_num' 'const/num/0')) = (w = ('const/complex/complex_neg' z))))).
tt('thm/complex/COMPLEX_LNEG_UNIQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_add' z w) = ('const/complex/complex_of_num' 'const/num/0')) = (z = ('const/complex/complex_neg' w))))).
tt('thm/complex/COMPLEX_NEG_ADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_add' z w)) = ('const/complex/complex_add' ('const/complex/complex_neg' z) ('const/complex/complex_neg' w))))).
tt('thm/complex/COMPLEX_MUL_RZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_of_num' 'const/num/0')) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_MUL_LZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_of_num' 'const/num/0') z) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_NEG_LMUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_mul' z w)) = ('const/complex/complex_mul' ('const/complex/complex_neg' z) w)))).
tt('thm/complex/COMPLEX_NEG_RMUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_mul' z w)) = ('const/complex/complex_mul' z ('const/complex/complex_neg' w))))).
tt('thm/complex/COMPLEX_NEG_MUL2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_neg' z) ('const/complex/complex_neg' w)) = ('const/complex/complex_mul' z w)))).
tt('thm/complex/COMPLEX_ENTIRE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_mul' z w) = ('const/complex/complex_of_num' 'const/num/0')) = ((z = ('const/complex/complex_of_num' 'const/num/0')) | (w = ('const/complex/complex_of_num' 'const/num/0')))))).
tt('thm/complex/COMPLEX_NEG_0_', ax, (('const/complex/complex_neg' ('const/complex/complex_of_num' 'const/num/0')) = ('const/complex/complex_of_num' 'const/num/0'))).
tt('thm/complex/COMPLEX_NEG_EQ0_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_neg' z) = ('const/complex/complex_of_num' 'const/num/0')) = (z = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_SUB_REFL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' z z) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_SUB_RZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' z ('const/complex/complex_of_num' 'const/num/0')) = z))).
tt('thm/complex/COMPLEX_SUB_LZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_of_num' 'const/num/0') z) = ('const/complex/complex_neg' z)))).
tt('thm/complex/COMPLEX_SUB_LNEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_neg' z) w) = ('const/complex/complex_neg' ('const/complex/complex_add' z w))))).
tt('thm/complex/COMPLEX_SUB_NEG2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_neg' z) ('const/complex/complex_neg' w)) = ('const/complex/complex_sub' w z)))).
tt('thm/complex/COMPLEX_NEG_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_sub' z w)) = ('const/complex/complex_sub' w z)))).
tt('thm/complex/COMPLEX_SUB_RNEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' z ('const/complex/complex_neg' w)) = ('const/complex/complex_add' z w)))).
tt('thm/complex/COMPLEX_SUB_ADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' ('const/complex/complex_sub' z w) w) = z))).
tt('thm/complex/COMPLEX_SUB_ADD2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' w ('const/complex/complex_sub' z w)) = z))).
tt('thm/complex/COMPLEX_ADD_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_add' z w) z) = w))).
tt('thm/complex/COMPLEX_SUB_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_sub' z w) z) = ('const/complex/complex_neg' w)))).
tt('thm/complex/COMPLEX_SUB_SUB2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' z ('const/complex/complex_sub' z w)) = w))).
tt('thm/complex/COMPLEX_ADD_SUB2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' z ('const/complex/complex_add' z w)) = ('const/complex/complex_neg' w)))).
tt('thm/complex/COMPLEX_ADD2_SUB2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), u : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_add' z w) ('const/complex/complex_add' u v)) = ('const/complex/complex_add' ('const/complex/complex_sub' z u) ('const/complex/complex_sub' w v))))).
tt('thm/complex/COMPLEX_SUB_TRIANGLE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' ('const/complex/complex_sub' z w) ('const/complex/complex_sub' w v)) = ('const/complex/complex_sub' z v)))).
tt('thm/complex/COMPLEX_SUB_0_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_sub' z w) = ('const/complex/complex_of_num' 'const/num/0')) = (z = w)))).
tt('thm/complex/COMPLEX_EQ_SUB_LADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((z = ('const/complex/complex_sub' w v)) = (('const/complex/complex_add' z v) = w)))).
tt('thm/complex/COMPLEX_EQ_SUB_RADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_sub' z w) = v) = (z = ('const/complex/complex_add' v w))))).
tt('thm/complex/COMPLEX_MUL_RNEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_neg' w)) = ('const/complex/complex_neg' ('const/complex/complex_mul' z w))))).
tt('thm/complex/COMPLEX_MUL_LNEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_neg' z) w) = ('const/complex/complex_neg' ('const/complex/complex_mul' z w))))).
tt('thm/complex/COMPLEX_SUB_LDISTRIB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_sub' w v)) = ('const/complex/complex_sub' ('const/complex/complex_mul' z w) ('const/complex/complex_mul' z v))))).
tt('thm/complex/COMPLEX_SUB_RDISTRIB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_sub' z w) v) = ('const/complex/complex_sub' ('const/complex/complex_mul' z v) ('const/complex/complex_mul' w v))))).
tt('thm/complex/COMPLEX_DIFFSQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_add' z w) ('const/complex/complex_sub' z w)) = ('const/complex/complex_sub' ('const/complex/complex_mul' z z) ('const/complex/complex_mul' w w))))).
tt('thm/complex/COMPLEX_EQ_LMUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_mul' z w) = ('const/complex/complex_mul' z v)) = ((z = ('const/complex/complex_of_num' 'const/num/0')) | (w = v))))).
tt('thm/complex/COMPLEX_EQ_RMUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_mul' z v) = ('const/complex/complex_mul' w v)) = ((v = ('const/complex/complex_of_num' 'const/num/0')) | (z = w))))).
tt('thm/complex/COMPLEX_EQ_LMUL2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => ((w = v) = (('const/complex/complex_mul' z w) = ('const/complex/complex_mul' z v)))))).
tt('thm/complex/COMPLEX_EQ_RMUL_IMP_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) & (('const/complex/complex_mul' w z) = ('const/complex/complex_mul' v z))) => (w = v)))).
tt('thm/complex/COMPLEX_EQ_LMUL_IMP_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) & (('const/complex/complex_mul' z w) = ('const/complex/complex_mul' z v))) => (w = v)))).
tt('thm/complex/COMPLEX_NEG_INV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_inv' ('const/complex/complex_neg' z)) = ('const/complex/complex_neg' ('const/complex/complex_inv' z)))))).
tt('thm/complex/COMPLEX_INV_MUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) & (~ (w = ('const/complex/complex_of_num' 'const/num/0')))) => (('const/complex/complex_inv' ('const/complex/complex_mul' z w)) = ('const/complex/complex_mul' ('const/complex/complex_inv' z) ('const/complex/complex_inv' w)))))).
tt('thm/complex/COMPLEX_INVINV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_inv' ('const/complex/complex_inv' z)) = z)))).
tt('thm/complex/COMPLEX_LINV_UNIQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_mul' z w) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (z = ('const/complex/complex_inv' w))))).
tt('thm/complex/COMPLEX_RINV_UNIQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_mul' z w) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (w = ('const/complex/complex_inv' z))))).
tt('thm/complex/COMPLEX_INV_0_', ax, (('const/complex/complex_inv' ('const/complex/complex_of_num' 'const/num/0')) = ('const/complex/complex_of_num' 'const/num/0'))).
tt('thm/complex/COMPLEX_INV1_', ax, (('const/complex/complex_inv' ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/complex/COMPLEX_INV_INV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_inv' ('const/complex/complex_inv' z)) = z))).
tt('thm/complex/COMPLEX_INV_NEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_inv' ('const/complex/complex_neg' z)) = ('const/complex/complex_neg' ('const/complex/complex_inv' z))))).
tt('thm/complex/COMPLEX_INV_EQ_0_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_inv' z) = ('const/complex/complex_of_num' 'const/num/0')) = (z = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_INV_NZ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (~ (('const/complex/complex_inv' z) = ('const/complex/complex_of_num' 'const/num/0')))))).
tt('thm/complex/COMPLEX_INV_INJ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_inv' z) = ('const/complex/complex_inv' w)) = (z = w)))).
tt('thm/complex/COMPLEX_NEG_LDIV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_div' z w)) = ('const/complex/complex_div' ('const/complex/complex_neg' z) w)))).
tt('thm/complex/COMPLEX_NEG_RDIV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_div' z w)) = ('const/complex/complex_div' z ('const/complex/complex_neg' w))))).
tt('thm/complex/COMPLEX_NEG_DIV2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_div' ('const/complex/complex_neg' z) ('const/complex/complex_neg' w)) = ('const/complex/complex_div' z w)))).
tt('thm/complex/COMPLEX_INV_1OVER_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_inv' z) = ('const/complex/complex_div' ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z)))).
tt('thm/complex/COMPLEX_DIV1_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_div' z ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = z))).
tt('thm/complex/COMPLEX_DIV_ADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' ('const/complex/complex_div' z v) ('const/complex/complex_div' w v)) = ('const/complex/complex_div' ('const/complex/complex_add' z w) v)))).
tt('thm/complex/COMPLEX_DIV_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_sub' ('const/complex/complex_div' z v) ('const/complex/complex_div' w v)) = ('const/complex/complex_div' ('const/complex/complex_sub' z w) v)))).
tt('thm/complex/COMPLEX_DIV_RMUL_CANCEL_', ax, (![v : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (v = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_div' ('const/complex/complex_mul' z v) ('const/complex/complex_mul' w v)) = ('const/complex/complex_div' z w))))).
tt('thm/complex/COMPLEX_DIV_LMUL_CANCEL_', ax, (![v : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (v = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_div' ('const/complex/complex_mul' v z) ('const/complex/complex_mul' v w)) = ('const/complex/complex_div' z w))))).
tt('thm/complex/COMPLEX_DIV_DENOM_CANCEL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_div' ('const/complex/complex_div' w z) ('const/complex/complex_div' v z)) = ('const/complex/complex_div' w v))))).
tt('thm/complex/COMPLEX_DIV_INNER_CANCEL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_mul' ('const/complex/complex_div' w z) ('const/complex/complex_div' z v)) = ('const/complex/complex_div' w v))))).
tt('thm/complex/COMPLEX_DIV_OUTER_CANCEL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_mul' ('const/complex/complex_div' z w) ('const/complex/complex_div' v z)) = ('const/complex/complex_div' v w))))).
tt('thm/complex/COMPLEX_DIV_MUL2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) & (~ (w = ('const/complex/complex_of_num' 'const/num/0')))) => (![v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_div' v w) = ('const/complex/complex_div' ('const/complex/complex_mul' z v) ('const/complex/complex_mul' z w))))))).
tt('thm/complex/COMPLEX_ADD_RAT_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), u : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (w = ('const/complex/complex_of_num' 'const/num/0'))) & (~ (v = ('const/complex/complex_of_num' 'const/num/0')))) => (('const/complex/complex_add' ('const/complex/complex_div' z w) ('const/complex/complex_div' u v)) = ('const/complex/complex_div' ('const/complex/complex_add' ('const/complex/complex_mul' z v) ('const/complex/complex_mul' w u)) ('const/complex/complex_mul' w v)))))).
tt('thm/complex/COMPLEX_SUB_RAT_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), u : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (w = ('const/complex/complex_of_num' 'const/num/0'))) & (~ (v = ('const/complex/complex_of_num' 'const/num/0')))) => (('const/complex/complex_sub' ('const/complex/complex_div' z w) ('const/complex/complex_div' u v)) = ('const/complex/complex_div' ('const/complex/complex_sub' ('const/complex/complex_mul' z v) ('const/complex/complex_mul' w u)) ('const/complex/complex_mul' w v)))))).
tt('thm/complex/COMPLEX_DIV_LZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_div' ('const/complex/complex_of_num' 'const/num/0') z) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_DIV_REFL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/complex_div' z z) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/complex/COMPLEX_SUB_INV2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) & (~ (w = ('const/complex/complex_of_num' 'const/num/0')))) => (('const/complex/complex_sub' ('const/complex/complex_inv' z) ('const/complex/complex_inv' w)) = ('const/complex/complex_div' ('const/complex/complex_sub' w z) ('const/complex/complex_mul' z w)))))).
tt('thm/complex/COMPLEX_EQ_RDIV_EQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (v = ('const/complex/complex_of_num' 'const/num/0'))) => ((z = ('const/complex/complex_div' w v)) = (('const/complex/complex_mul' z v) = w))))).
tt('thm/complex/COMPLEX_EQ_LDIV_EQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), v : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (v = ('const/complex/complex_of_num' 'const/num/0'))) => ((('const/complex/complex_div' z v) = w) = (z = ('const/complex/complex_mul' w v)))))).
tt('thm/complex/COMPLEX_OF_REAL_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/complex/complex_of_real' x) = ('const/complex/complex_of_real' y)) = (x = y)))).
tt('thm/complex/COMPLEX_OF_REAL_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/complex/complex_add' ('const/complex/complex_of_real' x) ('const/complex/complex_of_real' y)) = ('const/complex/complex_of_real' ('const/realax/real_add' x y))))).
tt('thm/complex/COMPLEX_OF_REAL_NEG_', ax, (![x : 'type/realax/real']: (('const/complex/complex_neg' ('const/complex/complex_of_real' x)) = ('const/complex/complex_of_real' ('const/realax/real_neg' x))))).
tt('thm/complex/COMPLEX_OF_REAL_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/complex/complex_mul' ('const/complex/complex_of_real' x) ('const/complex/complex_of_real' y)) = ('const/complex/complex_of_real' ('const/realax/real_mul' x y))))).
tt('thm/complex/COMPLEX_OF_REAL_INV_', ax, (![x : 'type/realax/real']: (('const/complex/complex_inv' ('const/complex/complex_of_real' x)) = ('const/complex/complex_of_real' ('const/realax/inv' x))))).
tt('thm/complex/COMPLEX_OF_REAL_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/complex/complex_sub' ('const/complex/complex_of_real' x) ('const/complex/complex_of_real' y)) = ('const/complex/complex_of_real' ('const/real/real_sub' x y))))).
tt('thm/complex/COMPLEX_OF_REAL_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/complex/complex_div' ('const/complex/complex_of_real' x) ('const/complex/complex_of_real' y)) = ('const/complex/complex_of_real' ('const/real/#slash#' x y))))).
tt('thm/complex/COMPLEX_OF_NUM_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/complex/complex_of_num' m) = ('const/complex/complex_of_num' n)) = (m = n)))).
tt('thm/complex/COMPLEX_OF_NUM_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/complex/complex_add' ('const/complex/complex_of_num' m) ('const/complex/complex_of_num' n)) = ('const/complex/complex_of_num' ('const/arithmetic/+' m n))))).
tt('thm/complex/COMPLEX_OF_NUM_MUL_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/complex/complex_mul' ('const/complex/complex_of_num' m) ('const/complex/complex_of_num' n)) = ('const/complex/complex_of_num' ('const/arithmetic/*' m n))))).
tt('thm/complex/complex_scalar_lmul_', def, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' k z) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/realax/real_mul' k ('const/complex/RE' z)) ('const/realax/real_mul' k ('const/complex/IM' z)))))).
tt('thm/complex/complex_scalar_rmul_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), k : 'type/realax/real']: (('const/complex/complex_scalar_rmul' z k) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/realax/real_mul' ('const/complex/RE' z) k) ('const/realax/real_mul' ('const/complex/IM' z) k))))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' k ('const/complex/complex_scalar_lmul' l z)) = ('const/complex/complex_scalar_lmul' ('const/realax/real_mul' k l) z)))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_NEG_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_scalar_lmul' k z)) = ('const/complex/complex_scalar_lmul' ('const/realax/real_neg' k) z)))).
tt('thm/complex/COMPLEX_NEG_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' k ('const/complex/complex_neg' z)) = ('const/complex/complex_scalar_lmul' ('const/realax/real_neg' k) z)))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_ADD_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/realax/real_add' k l) z) = ('const/complex/complex_add' ('const/complex/complex_scalar_lmul' k z) ('const/complex/complex_scalar_lmul' l z))))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_SUB_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/real/real_sub' k l) z) = ('const/complex/complex_sub' ('const/complex/complex_scalar_lmul' k z) ('const/complex/complex_scalar_lmul' l z))))).
tt('thm/complex/COMPLEX_ADD_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' k ('const/complex/complex_add' z w)) = ('const/complex/complex_add' ('const/complex/complex_scalar_lmul' k z) ('const/complex/complex_scalar_lmul' k w))))).
tt('thm/complex/COMPLEX_SUB_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' k ('const/complex/complex_sub' z w)) = ('const/complex/complex_sub' ('const/complex/complex_scalar_lmul' k z) ('const/complex/complex_scalar_lmul' k w))))).
tt('thm/complex/COMPLEX_MUL_SCALAR_LMUL2_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_scalar_lmul' k z) ('const/complex/complex_scalar_lmul' l w)) = ('const/complex/complex_scalar_lmul' ('const/realax/real_mul' k l) ('const/complex/complex_mul' z w))))).
tt('thm/complex/COMPLEX_LMUL_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_scalar_lmul' k z) w) = ('const/complex/complex_scalar_lmul' k ('const/complex/complex_mul' z w))))).
tt('thm/complex/COMPLEX_RMUL_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/complex_scalar_lmul' k w)) = ('const/complex/complex_scalar_lmul' k ('const/complex/complex_mul' z w))))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_ZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/real/real_of_num' 'const/num/0') z) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_ZERO_SCALAR_LMUL_', ax, (![k : 'type/realax/real']: (('const/complex/complex_scalar_lmul' k ('const/complex/complex_of_num' 'const/num/0')) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_ONE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z) = z))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_NEG1_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z) = ('const/complex/complex_neg' z)))).
tt('thm/complex/COMPLEX_DOUBLE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_add' z z) = ('const/complex/complex_scalar_lmul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) z)))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_ENTIRE_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_scalar_lmul' k z) = ('const/complex/complex_of_num' 'const/num/0')) = ((k = ('const/real/real_of_num' 'const/num/0')) | (z = ('const/complex/complex_of_num' 'const/num/0')))))).
tt('thm/complex/COMPLEX_EQ_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_scalar_lmul' k z) = ('const/complex/complex_scalar_lmul' k w)) = ((k = ('const/real/real_of_num' 'const/num/0')) | (z = w))))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_EQ_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_scalar_lmul' k z) = ('const/complex/complex_scalar_lmul' l z)) = ((k = l) | (z = ('const/complex/complex_of_num' 'const/num/0')))))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_EQ1_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_scalar_lmul' k z) = z) = ((k = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) | (z = ('const/complex/complex_of_num' 'const/num/0')))))).
tt('thm/complex/COMPLEX_INV_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (k = ('const/real/real_of_num' 'const/num/0'))) & (~ (z = ('const/complex/complex_of_num' 'const/num/0')))) => (('const/complex/complex_inv' ('const/complex/complex_scalar_lmul' k z)) = ('const/complex/complex_scalar_lmul' ('const/realax/inv' k) ('const/complex/complex_inv' z)))))).
tt('thm/complex/COMPLEX_SCALAR_LMUL_DIV2_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (((~ (l = ('const/real/real_of_num' 'const/num/0'))) & (~ (w = ('const/complex/complex_of_num' 'const/num/0')))) => (('const/complex/complex_div' ('const/complex/complex_scalar_lmul' k z) ('const/complex/complex_scalar_lmul' l w)) = ('const/complex/complex_scalar_lmul' ('const/real/#slash#' k l) ('const/complex/complex_div' z w)))))).
tt('thm/complex/COMPLEX_SCALAR_MUL_COMM_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' k z) = ('const/complex/complex_scalar_rmul' z k)))).
tt('thm/complex/COMPLEX_SCALAR_RMUL_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' ('const/complex/complex_scalar_rmul' z k) l) = ('const/complex/complex_scalar_rmul' z ('const/realax/real_mul' k l))))).
tt('thm/complex/COMPLEX_SCALAR_RMUL_NEG_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_neg' ('const/complex/complex_scalar_rmul' z k)) = ('const/complex/complex_scalar_rmul' z ('const/realax/real_neg' k))))).
tt('thm/complex/COMPLEX_NEG_SCALAR_RMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' ('const/complex/complex_neg' z) k) = ('const/complex/complex_scalar_rmul' z ('const/realax/real_neg' k))))).
tt('thm/complex/COMPLEX_SCALAR_RMUL_ADD_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' z ('const/realax/real_add' k l)) = ('const/complex/complex_add' ('const/complex/complex_scalar_rmul' z k) ('const/complex/complex_scalar_rmul' z l))))).
tt('thm/complex/COMPLEX_RSCALAR_RMUL_SUB_', ax, (![k : 'type/realax/real', l : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' z ('const/real/real_sub' k l)) = ('const/complex/complex_sub' ('const/complex/complex_scalar_rmul' z k) ('const/complex/complex_scalar_rmul' z l))))).
tt('thm/complex/COMPLEX_ADD_RSCALAR_RMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' ('const/complex/complex_add' z w) k) = ('const/complex/complex_add' ('const/complex/complex_scalar_rmul' z k) ('const/complex/complex_scalar_rmul' w k))))).
tt('thm/complex/COMPLEX_SUB_SCALAR_RMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' ('const/complex/complex_sub' z w) k) = ('const/complex/complex_sub' ('const/complex/complex_scalar_rmul' z k) ('const/complex/complex_scalar_rmul' w k))))).
tt('thm/complex/COMPLEX_SCALAR_RMUL_ZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' z ('const/real/real_of_num' 'const/num/0')) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_ZERO_SCALAR_RMUL_', ax, (![k : 'type/realax/real']: (('const/complex/complex_scalar_rmul' ('const/complex/complex_of_num' 'const/num/0') k) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_SCALAR_RMUL_ONE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = z))).
tt('thm/complex/COMPLEX_SCALAR_RMUL_NEG1_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_rmul' z ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ('const/complex/complex_neg' z)))).
tt('thm/complex/conj_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' z) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/complex/RE' z) ('const/realax/real_neg' ('const/complex/IM' z)))))).
tt('thm/complex/CONJ_REAL_REFL_', ax, (![x : 'type/realax/real']: (('const/complex/conj' ('const/complex/complex_of_real' x)) = ('const/complex/complex_of_real' x)))).
tt('thm/complex/CONJ_NUM_REFL_', ax, (![n : 'type/num/num']: (('const/complex/conj' ('const/complex/complex_of_num' n)) = ('const/complex/complex_of_num' n)))).
tt('thm/complex/CONJ_ADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_add' z w)) = ('const/complex/complex_add' ('const/complex/conj' z) ('const/complex/conj' w))))).
tt('thm/complex/CONJ_NEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_neg' z)) = ('const/complex/complex_neg' ('const/complex/conj' z))))).
tt('thm/complex/CONJ_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_sub' z w)) = ('const/complex/complex_sub' ('const/complex/conj' z) ('const/complex/conj' w))))).
tt('thm/complex/CONJ_MUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_mul' z w)) = ('const/complex/complex_mul' ('const/complex/conj' z) ('const/complex/conj' w))))).
tt('thm/complex/CONJ_INV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_inv' z)) = ('const/complex/complex_inv' ('const/complex/conj' z))))).
tt('thm/complex/CONJ_DIV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_div' z w)) = ('const/complex/complex_div' ('const/complex/conj' z) ('const/complex/conj' w))))).
tt('thm/complex/CONJ_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/complex_scalar_lmul' k z)) = ('const/complex/complex_scalar_lmul' k ('const/complex/conj' z))))).
tt('thm/complex/CONJ_CONJ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/conj' ('const/complex/conj' z)) = z))).
tt('thm/complex/CONJ_EQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/conj' z) = w) = (z = ('const/complex/conj' w))))).
tt('thm/complex/CONJ_EQ2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/conj' z) = ('const/complex/conj' w)) = (z = w)))).
tt('thm/complex/COMPLEX_MUL_RCONJ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/conj' z) z) = ('const/complex/complex_of_real' ('const/realax/real_add' ('const/real/pow' ('const/complex/RE' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/complex/IM' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/CONJ_ZERO_', ax, (('const/complex/conj' ('const/complex/complex_of_num' 'const/num/0')) = ('const/complex/complex_of_num' 'const/num/0'))).
tt('thm/complex/modu_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/modu' z) = ('const/transc/sqrt' ('const/realax/real_add' ('const/real/pow' ('const/complex/RE' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/complex/IM' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/arg_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/arg' z) = (('const/bool/COND' 'type/realax/real') ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/complex/IM' z)) ('const/transc/acs' ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z))) ('const/realax/real_add' ('const/realax/real_neg' ('const/transc/acs' ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z)))) ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) 'const/transc/pi')))))).
tt('thm/complex/MODU_POW2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/real/pow' ('const/complex/modu' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/realax/real_add' ('const/real/pow' ('const/complex/RE' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/complex/IM' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/complex/RE_IM_LE_MODU_0', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ('const/real/real_lte' ('const/real/abs' ('const/complex/RE' z)) ('const/complex/modu' z)))).
tt('thm/complex/RE_IM_LE_MODU_e1', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ('const/real/real_lte' ('const/real/abs' ('const/complex/IM' z)) ('const/complex/modu' z)))).
tt('thm/complex/MODU_POS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/complex/modu' z)))).
tt('thm/complex/COMPLEX_MUL_RCONJ1_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' z ('const/complex/conj' z)) = ('const/complex/complex_of_real' ('const/real/pow' ('const/complex/modu' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/complex/COMPLEX_MUL_LCONJ1_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/conj' z) z) = ('const/complex/complex_of_real' ('const/real/pow' ('const/complex/modu' z) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/complex/MODU_NEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/modu' ('const/complex/complex_neg' z)) = ('const/complex/modu' z)))).
tt('thm/complex/MODU_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/modu' ('const/complex/complex_sub' z w)) = ('const/complex/modu' ('const/complex/complex_sub' w z))))).
tt('thm/complex/MODU_CONJ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/modu' ('const/complex/conj' z)) = ('const/complex/modu' z)))).
tt('thm/complex/MODU_MUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/modu' ('const/complex/complex_mul' z w)) = ('const/realax/real_mul' ('const/complex/modu' z) ('const/complex/modu' w))))).
tt('thm/complex/MODU_0_', ax, (('const/complex/modu' ('const/complex/complex_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/complex/MODU_1_', ax, (('const/complex/modu' ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/complex/MODU_COMPLEX_INV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/modu' ('const/complex/complex_inv' z)) = ('const/realax/inv' ('const/complex/modu' z)))))).
tt('thm/complex/MODU_DIV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (w = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/complex/modu' ('const/complex/complex_div' z w)) = ('const/real/#slash#' ('const/complex/modu' z) ('const/complex/modu' w)))))).
tt('thm/complex/MODU_SCALAR_LMUL_', ax, (![k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/modu' ('const/complex/complex_scalar_lmul' k z)) = ('const/realax/real_mul' ('const/real/abs' k) ('const/complex/modu' z))))).
tt('thm/complex/MODU_REAL_', ax, (![x : 'type/realax/real']: (('const/complex/modu' ('const/complex/complex_of_real' x)) = ('const/real/abs' x)))).
tt('thm/complex/MODU_NUM_', ax, (![n : 'type/num/num']: (('const/complex/modu' ('const/complex/complex_of_num' n)) = ('const/real/real_of_num' n)))).
tt('thm/complex/MODU_ZERO_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((z = ('const/complex/complex_of_num' 'const/num/0')) = (('const/complex/modu' z) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/complex/MODU_NZ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/complex/modu' z))))).
tt('thm/complex/MODU_CASES_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((z = ('const/complex/complex_of_num' 'const/num/0')) | ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/complex/modu' z))))).
tt('thm/complex/RE_DIV_MODU_BOUNDS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z))) & ('const/real/real_lte' ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z)) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/IM_DIV_MODU_BOUNDS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z))) & ('const/real/real_lte' ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z)) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/RE_DIV_MODU_ACS_BOUNDS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/transc/acs' ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z)))) & ('const/real/real_lte' ('const/transc/acs' ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z))) 'const/transc/pi'))))).
tt('thm/complex/IM_DIV_MODU_ASN_BOUNDS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/real/real_lte' ('const/realax/real_neg' ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/transc/asn' ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z)))) & ('const/real/real_lte' ('const/transc/asn' ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z))) ('const/real/#slash#' 'const/transc/pi' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/complex/RE_DIV_MODU_ACS_COS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/transc/cos' ('const/transc/acs' ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z)))) = ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z)))))).
tt('thm/complex/IM_DIV_MODU_ASN_SIN_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/transc/sin' ('const/transc/asn' ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z)))) = ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z)))))).
tt('thm/complex/ARG_COS_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/transc/cos' ('const/complex/arg' z)) = ('const/real/#slash#' ('const/complex/RE' z) ('const/complex/modu' z)))))).
tt('thm/complex/ARG_SIN_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (('const/transc/sin' ('const/complex/arg' z)) = ('const/real/#slash#' ('const/complex/IM' z) ('const/complex/modu' z)))))).
tt('thm/complex/RE_MODU_ARG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/RE' z) = ('const/realax/real_mul' ('const/complex/modu' z) ('const/transc/cos' ('const/complex/arg' z)))))).
tt('thm/complex/IM_MODU_ARG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/IM' z) = ('const/realax/real_mul' ('const/complex/modu' z) ('const/transc/sin' ('const/complex/arg' z)))))).
tt('thm/complex/COMPLEX_TRIANGLE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/complex/modu' z) (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/complex/arg' z)) ('const/transc/sin' ('const/complex/arg' z)))) = z))).
tt('thm/complex/COMPLEX_MODU_ARG_EQ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((z = w) = ((('const/complex/modu' z) = ('const/complex/modu' w)) & (('const/complex/arg' z) = ('const/complex/arg' w)))))).
tt('thm/complex/MODU_UNIT_', ax, ![A : $t]: (![x : 'type/realax/real', y : A]: (('const/complex/modu' (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' x) ('const/transc/sin' x))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/COMPLEX_MUL_ARG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/complex/complex_mul' (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' x) ('const/transc/sin' x)) (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' y) ('const/transc/sin' y))) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/realax/real_add' x y)) ('const/transc/sin' ('const/realax/real_add' x y)))))).
tt('thm/complex/COMPLEX_INV_ARG_', ax, (![x : 'type/realax/real']: (('const/complex/complex_inv' (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' x) ('const/transc/sin' x))) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/realax/real_neg' x)) ('const/transc/sin' ('const/realax/real_neg' x)))))).
tt('thm/complex/COMPLEX_DIV_ARG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/complex/complex_div' (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' x) ('const/transc/sin' x)) (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' y) ('const/transc/sin' y))) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/real/real_sub' x y)) ('const/transc/sin' ('const/real/real_sub' x y)))))).
tt('thm/complex/complex_pow_def_0', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_pow' z 'const/num/0') = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/complex_pow_def_e1', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_pow' z ('const/num/SUC' n)) = ('const/complex/complex_mul' z ('const/complex/complex_pow' z n))))).
tt('thm/complex/complex_pow_def_compute_0', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_pow' z 'const/num/0') = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/complex_pow_def_compute_1', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_pow' z ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = ('const/complex/complex_mul' z ('const/complex/complex_pow' z ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/complex/complex_pow_def_compute_e2', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_pow' z ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = ('const/complex/complex_mul' z ('const/complex/complex_pow' z ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/complex/COMPLEX_POW_0_', ax, (![n : 'type/num/num']: (('const/complex/complex_pow' ('const/complex/complex_of_num' 'const/num/0') ('const/num/SUC' n)) = ('const/complex/complex_of_num' 'const/num/0')))).
tt('thm/complex/COMPLEX_POW_NZ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (~ (('const/complex/complex_pow' z n) = ('const/complex/complex_of_num' 'const/num/0')))))).
tt('thm/complex/COMPLEX_POWINV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((~ (z = ('const/complex/complex_of_num' 'const/num/0'))) => (![n : 'type/num/num']: (('const/complex/complex_inv' ('const/complex/complex_pow' z n)) = ('const/complex/complex_pow' ('const/complex/complex_inv' z) n)))))).
tt('thm/complex/MODU_COMPLEX_POW_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/modu' ('const/complex/complex_pow' z n)) = ('const/real/pow' ('const/complex/modu' z) n)))).
tt('thm/complex/COMPLEX_POW_ADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (('const/complex/complex_pow' z ('const/arithmetic/+' m n)) = ('const/complex/complex_mul' ('const/complex/complex_pow' z m) ('const/complex/complex_pow' z n))))).
tt('thm/complex/COMPLEX_POW_1_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_pow' z ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = z))).
tt('thm/complex/COMPLEX_POW_2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_pow' z ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/complex/complex_mul' z z)))).
tt('thm/complex/COMPLEX_POW_ONE_', ax, (![n : 'type/num/num']: (('const/complex/complex_pow' ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) n) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/COMPLEX_POW_MUL_', ax, (![n : 'type/num/num', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_pow' ('const/complex/complex_mul' z w) n) = ('const/complex/complex_mul' ('const/complex/complex_pow' z n) ('const/complex/complex_pow' w n))))).
tt('thm/complex/COMPLEX_POW_INV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_pow' ('const/complex/complex_inv' z) n) = ('const/complex/complex_inv' ('const/complex/complex_pow' z n))))).
tt('thm/complex/COMPLEX_POW_DIV_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_pow' ('const/complex/complex_div' z w) n) = ('const/complex/complex_div' ('const/complex/complex_pow' z n) ('const/complex/complex_pow' w n))))).
tt('thm/complex/COMPLEX_POW_L_', ax, (![n : 'type/num/num', k : 'type/realax/real', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_pow' ('const/complex/complex_scalar_lmul' k z) n) = ('const/complex/complex_scalar_lmul' ('const/real/pow' k n) ('const/complex/complex_pow' z n))))).
tt('thm/complex/COMPLEX_POW_ZERO_', ax, (![n : 'type/num/num', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_pow' z n) = ('const/complex/complex_of_num' 'const/num/0')) => (z = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_POW_ZERO_EQ_', ax, (![n : 'type/num/num', z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: ((('const/complex/complex_pow' z ('const/num/SUC' n)) = ('const/complex/complex_of_num' 'const/num/0')) = (z = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_POW_POW_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (('const/complex/complex_pow' ('const/complex/complex_pow' z m) n) = ('const/complex/complex_pow' z ('const/arithmetic/*' m n))))).
tt('thm/complex/DE_MOIVRE_LEMMA_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/complex/complex_pow' (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' x) ('const/transc/sin' x)) n) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/realax/real_mul' ('const/real/real_of_num' n) x)) ('const/transc/sin' ('const/realax/real_mul' ('const/real/real_of_num' n) x)))))).
tt('thm/complex/DE_MOIVRE_THM_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_pow' ('const/complex/complex_scalar_lmul' ('const/complex/modu' z) (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/complex/arg' z)) ('const/transc/sin' ('const/complex/arg' z)))) n) = ('const/complex/complex_scalar_lmul' ('const/real/pow' ('const/complex/modu' z) n) (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/complex/arg' z))) ('const/transc/sin' ('const/realax/real_mul' ('const/real/real_of_num' n) ('const/complex/arg' z)))))))).
tt('thm/complex/complex_exp_', def, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_exp' z) = ('const/complex/complex_scalar_lmul' ('const/transc/exp' ('const/complex/RE' z)) (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' ('const/complex/IM' z)) ('const/transc/sin' ('const/complex/IM' z))))))).
tt('thm/complex/EXP_IMAGINARY_', ax, (![x : 'type/realax/real']: (('const/complex/complex_exp' ('const/complex/complex_scalar_rmul' 'const/complex/i' x)) = (('const/pair/,' 'type/realax/real' 'type/realax/real') ('const/transc/cos' x) ('const/transc/sin' x))))).
tt('thm/complex/EULER_FORMULE_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_scalar_lmul' ('const/complex/modu' z) ('const/complex/complex_exp' ('const/complex/complex_scalar_rmul' 'const/complex/i' ('const/complex/arg' z)))) = z))).
tt('thm/complex/COMPLEX_EXP_ADD_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_exp' ('const/complex/complex_add' z w)) = ('const/complex/complex_mul' ('const/complex/complex_exp' z) ('const/complex/complex_exp' w))))).
tt('thm/complex/COMPLEX_EXP_NEG_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_exp' ('const/complex/complex_neg' z)) = ('const/complex/complex_inv' ('const/complex/complex_exp' z))))).
tt('thm/complex/COMPLEX_EXP_SUB_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_exp' ('const/complex/complex_sub' z w)) = ('const/complex/complex_div' ('const/complex/complex_exp' z) ('const/complex/complex_exp' w))))).
tt('thm/complex/COMPLEX_EXP_N_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_exp' ('const/complex/complex_scalar_lmul' ('const/real/real_of_num' n) z)) = ('const/complex/complex_pow' ('const/complex/complex_exp' z) n)))).
tt('thm/complex/COMPLEX_EXP_N2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), n : 'type/num/num']: (('const/complex/complex_exp' ('const/complex/complex_mul' ('const/complex/complex_of_num' n) z)) = ('const/complex/complex_pow' ('const/complex/complex_exp' z) n)))).
tt('thm/complex/COMPLEX_EXP_0_', ax, (('const/complex/complex_exp' ('const/complex/complex_of_num' 'const/num/0')) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/complex/COMPLEX_EXP_NZ_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (~ (('const/complex/complex_exp' z) = ('const/complex/complex_of_num' 'const/num/0'))))).
tt('thm/complex/COMPLEX_EXP_ADD_MUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real'), w : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_exp' ('const/complex/complex_add' z w)) ('const/complex/complex_exp' ('const/complex/complex_neg' z))) = ('const/complex/complex_exp' w)))).
tt('thm/complex/COMPLEX_EXP_NEG_MUL_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_exp' z) ('const/complex/complex_exp' ('const/complex/complex_neg' z))) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/complex/COMPLEX_EXP_NEG_MUL2_', ax, (![z : ('type/pair/prod' 'type/realax/real' 'type/realax/real')]: (('const/complex/complex_mul' ('const/complex/complex_exp' ('const/complex/complex_neg' z)) ('const/complex/complex_exp' z)) = ('const/complex/complex_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
