Theory "complex"

Parents transc

Signature

Constant	Type
IM	:complex -> real
RE	:complex -> real
arg	:complex -> real
complex_add	:complex -> complex -> complex
complex_div	:complex -> complex -> complex
complex_exp	:complex -> complex
complex_inv	:complex -> complex
complex_mul	:complex -> complex -> complex
complex_neg	:complex -> complex
complex_of_num	:num -> complex
complex_of_real	:real -> complex
complex_pow	:complex -> num -> complex
complex_scalar_lmul	:real -> complex -> complex
complex_scalar_rmul	:complex -> real -> complex
complex_sub	:complex -> complex -> complex
conj	:complex -> complex
i	:complex
modu	:complex -> real

Definitions

RE

⊢ ∀z. RE z = FST z

IM

⊢ ∀z. IM z = SND z

complex_of_real

⊢ ∀x. complex_of_real x = (x,0)

complex_of_num

⊢ ∀n. &n = complex_of_real (&n)

i

⊢ i = (0,1)

complex_add

⊢ ∀z w. z + w = (RE z + RE w,IM z + IM w)

complex_neg

⊢ ∀z. -z = (-RE z,-IM z)

complex_mul

⊢ ∀z w. z * w = (RE z * RE w − IM z * IM w,RE z * IM w + IM z * RE w)

complex_inv

⊢ ∀z.
      inv z =
      (RE z / (RE z pow 2 + IM z pow 2),-IM z / (RE z pow 2 + IM z pow 2))

complex_sub

⊢ ∀z w. z − w = z + -w

complex_div

⊢ ∀z w. z / w = z * inv w

complex_scalar_lmul

⊢ ∀k z. k * z = (k * RE z,k * IM z)

complex_scalar_rmul

⊢ ∀z k. z * k = (RE z * k,IM z * k)

conj

⊢ ∀z. conj z = (RE z,-IM z)

modu

⊢ ∀z. modu z = sqrt (RE z pow 2 + IM z pow 2)

arg

⊢ ∀z.
      arg z = if 0 ≤ IM z then acs (RE z / modu z)
      else -acs (RE z / modu z) + 2 * pi

complex_pow_def

⊢ (∀z. z pow 0 = 1) ∧ ∀z n. z pow SUC n = z * z pow n

complex_exp

⊢ ∀z. exp z = exp (RE z) * (cos (IM z),sin (IM z))

Theorems

COMPLEX_LEMMA1

⊢ ∀a b c d.
      (a * c − b * d) pow 2 + (a * d + b * c) pow 2 =
      (a pow 2 + b pow 2) * (c pow 2 + d pow 2)

COMPLEX_LEMMA2

⊢ ∀x y. abs x ≤ sqrt (x pow 2 + y pow 2)

COMPLEX

⊢ ∀z. (RE z,IM z) = z

COMPLEX_RE_IM_EQ

⊢ ∀z w. z = w ⇔ RE z = RE w ∧ IM z = IM w

RE_COMPLEX_OF_REAL

⊢ ∀x. RE (complex_of_real x) = x

IM_COMPLEX_OF_REAL

⊢ ∀x. IM (complex_of_real x) = 0

COMPLEX_0

⊢ 0 = complex_of_real 0

COMPLEX_1

⊢ 1 = complex_of_real 1

COMPLEX_10

⊢ 1 ≠ 0

COMPLEX_0_THM

⊢ ∀z. z = 0 ⇔ RE z pow 2 + IM z pow 2 = 0

COMPLEX_ADD_COMM

⊢ ∀z w. z + w = w + z

COMPLEX_ADD_ASSOC

⊢ ∀z w v. z + (w + v) = z + w + v

COMPLEX_ADD_RID

⊢ ∀z. z + 0 = z

COMPLEX_ADD_LID

⊢ ∀z. 0 + z = z

COMPLEX_ADD_RINV

⊢ ∀z. z + -z = 0

COMPLEX_ADD_LINV

⊢ ∀z. -z + z = 0

COMPLEX_MUL_COMM

⊢ ∀z w. z * w = w * z

COMPLEX_MUL_ASSOC

⊢ ∀z w v. z * (w * v) = z * w * v

COMPLEX_MUL_RID

⊢ ∀z. z * 1 = z

COMPLEX_MUL_LID

⊢ ∀z. 1 * z = z

COMPLEX_MUL_RINV

⊢ ∀z. z ≠ 0 ⇒ z * inv z = 1

COMPLEX_MUL_LINV

⊢ ∀z. z ≠ 0 ⇒ inv z * z = 1

COMPLEX_ADD_LDISTRIB

⊢ ∀z w v. z * (w + v) = z * w + z * v

COMPLEX_ADD_RDISTRIB

⊢ ∀z w v. (z + w) * v = z * v + w * v

COMPLEX_EQ_LADD

⊢ ∀z w v. z + w = z + v ⇔ w = v

COMPLEX_EQ_RADD

⊢ ∀z w v. z + v = w + v ⇔ z = w

COMPLEX_ADD_RID_UNIQ

⊢ ∀z w. z + w = z ⇔ w = 0

COMPLEX_ADD_LID_UNIQ

⊢ ∀z w. z + w = w ⇔ z = 0

COMPLEX_NEGNEG

⊢ ∀z. - -z = z

COMPLEX_NEG_EQ

⊢ ∀z w. -z = w ⇔ z = -w

COMPLEX_EQ_NEG

⊢ ∀z w. -z = -w ⇔ z = w

COMPLEX_RNEG_UNIQ

⊢ ∀z w. z + w = 0 ⇔ w = -z

COMPLEX_LNEG_UNIQ

⊢ ∀z w. z + w = 0 ⇔ z = -w

COMPLEX_NEG_ADD

⊢ ∀z w. -(z + w) = -z + -w

COMPLEX_MUL_RZERO

⊢ ∀z. z * 0 = 0

COMPLEX_MUL_LZERO

⊢ ∀z. 0 * z = 0

COMPLEX_NEG_LMUL

⊢ ∀z w. -(z * w) = -z * w

COMPLEX_NEG_RMUL

⊢ ∀z w. -(z * w) = z * -w

COMPLEX_NEG_MUL2

⊢ ∀z w. -z * -w = z * w

COMPLEX_ENTIRE

⊢ ∀z w. z * w = 0 ⇔ z = 0 ∨ w = 0

COMPLEX_NEG_0

⊢ -0 = 0

COMPLEX_NEG_EQ0

⊢ ∀z. -z = 0 ⇔ z = 0

COMPLEX_SUB_REFL

⊢ ∀z. z − z = 0

COMPLEX_SUB_RZERO

⊢ ∀z. z − 0 = z

COMPLEX_SUB_LZERO

⊢ ∀z. 0 − z = -z

COMPLEX_SUB_LNEG

⊢ ∀z w. -z − w = -(z + w)

COMPLEX_SUB_NEG2

⊢ ∀z w. -z − -w = w − z

COMPLEX_NEG_SUB

⊢ ∀z w. -(z − w) = w − z

COMPLEX_SUB_RNEG

⊢ ∀z w. z − -w = z + w

COMPLEX_SUB_ADD

⊢ ∀z w. z − w + w = z

COMPLEX_SUB_ADD2

⊢ ∀z w. w + (z − w) = z

COMPLEX_ADD_SUB

⊢ ∀z w. z + w − z = w

COMPLEX_SUB_SUB

⊢ ∀z w. z − w − z = -w

COMPLEX_SUB_SUB2

⊢ ∀z w. z − (z − w) = w

COMPLEX_ADD_SUB2

⊢ ∀z w. z − (z + w) = -w

COMPLEX_ADD2_SUB2

⊢ ∀z w u v. z + w − (u + v) = z − u + (w − v)

COMPLEX_SUB_TRIANGLE

⊢ ∀z w v. z − w + (w − v) = z − v

COMPLEX_SUB_0

⊢ ∀z w. z − w = 0 ⇔ z = w

COMPLEX_EQ_SUB_LADD

⊢ ∀z w v. z = w − v ⇔ z + v = w

COMPLEX_EQ_SUB_RADD

⊢ ∀z w v. z − w = v ⇔ z = v + w

COMPLEX_MUL_RNEG

⊢ ∀z w. z * -w = -(z * w)

COMPLEX_MUL_LNEG

⊢ ∀z w. -z * w = -(z * w)

COMPLEX_SUB_LDISTRIB

⊢ ∀z w v. z * (w − v) = z * w − z * v

COMPLEX_SUB_RDISTRIB

⊢ ∀z w v. (z − w) * v = z * v − w * v

COMPLEX_DIFFSQ

⊢ ∀z w. (z + w) * (z − w) = z * z − w * w

COMPLEX_EQ_LMUL

⊢ ∀z w v. z * w = z * v ⇔ z = 0 ∨ w = v

COMPLEX_EQ_RMUL

⊢ ∀z w v. z * v = w * v ⇔ v = 0 ∨ z = w

COMPLEX_EQ_LMUL2

⊢ ∀z w v. z ≠ 0 ⇒ (w = v ⇔ z * w = z * v)

COMPLEX_EQ_RMUL_IMP

⊢ ∀z w v. z ≠ 0 ∧ w * z = v * z ⇒ w = v

COMPLEX_EQ_LMUL_IMP

⊢ ∀z w v. z ≠ 0 ∧ z * w = z * v ⇒ w = v

COMPLEX_NEG_INV

⊢ ∀z. z ≠ 0 ⇒ inv (-z) = -inv z

COMPLEX_INV_MUL

⊢ ∀z w. z ≠ 0 ∧ w ≠ 0 ⇒ inv (z * w) = inv z * inv w

COMPLEX_INVINV

⊢ ∀z. z ≠ 0 ⇒ inv (inv z) = z

COMPLEX_LINV_UNIQ

⊢ ∀z w. z * w = 1 ⇒ z = inv w

COMPLEX_RINV_UNIQ

⊢ ∀z w. z * w = 1 ⇒ w = inv z

COMPLEX_INV_0

⊢ inv 0 = 0

COMPLEX_INV1

⊢ inv 1 = 1

COMPLEX_INV_INV

⊢ ∀z. inv (inv z) = z

COMPLEX_INV_NEG

⊢ ∀z. inv (-z) = -inv z

COMPLEX_INV_EQ_0

⊢ ∀z. inv z = 0 ⇔ z = 0

COMPLEX_INV_NZ

⊢ ∀z. z ≠ 0 ⇒ inv z ≠ 0

COMPLEX_INV_INJ

⊢ ∀z w. inv z = inv w ⇔ z = w

COMPLEX_NEG_LDIV

⊢ ∀z w. -(z / w) = -z / w

COMPLEX_NEG_RDIV

⊢ ∀z w. -(z / w) = z / -w

COMPLEX_NEG_DIV2

⊢ ∀z w. -z / -w = z / w

COMPLEX_INV_1OVER

⊢ ∀z. inv z = 1 / z

COMPLEX_DIV1

⊢ ∀z. z / 1 = z

COMPLEX_DIV_ADD

⊢ ∀z w v. z / v + w / v = (z + w) / v

COMPLEX_DIV_SUB

⊢ ∀z w v. z / v − w / v = (z − w) / v

COMPLEX_DIV_RMUL_CANCEL

⊢ ∀v z w. v ≠ 0 ⇒ z * v / (w * v) = z / w

COMPLEX_DIV_LMUL_CANCEL

⊢ ∀v z w. v ≠ 0 ⇒ v * z / (v * w) = z / w

COMPLEX_DIV_DENOM_CANCEL

⊢ ∀z w v. z ≠ 0 ⇒ w / z / (v / z) = w / v

COMPLEX_DIV_INNER_CANCEL

⊢ ∀z w v. z ≠ 0 ⇒ w / z * (z / v) = w / v

COMPLEX_DIV_OUTER_CANCEL

⊢ ∀z w v. z ≠ 0 ⇒ z / w * (v / z) = v / w

COMPLEX_DIV_MUL2

⊢ ∀z w. z ≠ 0 ∧ w ≠ 0 ⇒ ∀v. v / w = z * v / (z * w)

COMPLEX_ADD_RAT

⊢ ∀z w u v. w ≠ 0 ∧ v ≠ 0 ⇒ z / w + u / v = (z * v + w * u) / (w * v)

COMPLEX_SUB_RAT

⊢ ∀z w u v. w ≠ 0 ∧ v ≠ 0 ⇒ z / w − u / v = (z * v − w * u) / (w * v)

COMPLEX_DIV_LZERO

⊢ ∀z. 0 / z = 0

COMPLEX_DIV_REFL

⊢ ∀z. z ≠ 0 ⇒ z / z = 1

COMPLEX_SUB_INV2

⊢ ∀z w. z ≠ 0 ∧ w ≠ 0 ⇒ inv z − inv w = (w − z) / (z * w)

COMPLEX_EQ_RDIV_EQ

⊢ ∀z w v. v ≠ 0 ⇒ (z = w / v ⇔ z * v = w)

COMPLEX_EQ_LDIV_EQ

⊢ ∀z w v. v ≠ 0 ⇒ (z / v = w ⇔ z = w * v)

COMPLEX_OF_REAL_EQ

⊢ ∀x y. complex_of_real x = complex_of_real y ⇔ x = y

COMPLEX_OF_REAL_ADD

⊢ ∀x y. complex_of_real x + complex_of_real y = complex_of_real (x + y)

COMPLEX_OF_REAL_NEG

⊢ ∀x. -complex_of_real x = complex_of_real (-x)

COMPLEX_OF_REAL_MUL

⊢ ∀x y. complex_of_real x * complex_of_real y = complex_of_real (x * y)

COMPLEX_OF_REAL_INV

⊢ ∀x. inv (complex_of_real x) = complex_of_real x⁻¹

COMPLEX_OF_REAL_SUB

⊢ ∀x y. complex_of_real x − complex_of_real y = complex_of_real (x − y)

COMPLEX_OF_REAL_DIV

⊢ ∀x y. complex_of_real x / complex_of_real y = complex_of_real (x / y)

COMPLEX_OF_NUM_EQ

⊢ ∀m n. &m = &n ⇔ m = n

COMPLEX_OF_NUM_ADD

⊢ ∀m n. &m + &n = &(m + n)

COMPLEX_OF_NUM_MUL

⊢ ∀m n. &m * &n = &(m * n)

COMPLEX_SCALAR_LMUL

⊢ ∀k l z. k * (l * z) = k * l * z

COMPLEX_SCALAR_LMUL_NEG

⊢ ∀k z. -(k * z) = -k * z

COMPLEX_NEG_SCALAR_LMUL

⊢ ∀k z. k * -z = -k * z

COMPLEX_SCALAR_LMUL_ADD

⊢ ∀k l z. (k + l) * z = k * z + l * z

COMPLEX_SCALAR_LMUL_SUB

⊢ ∀k l z. (k − l) * z = k * z − l * z

COMPLEX_ADD_SCALAR_LMUL

⊢ ∀k z w. k * (z + w) = k * z + k * w

COMPLEX_SUB_SCALAR_LMUL

⊢ ∀k z w. k * (z − w) = k * z − k * w

COMPLEX_MUL_SCALAR_LMUL2

⊢ ∀k l z w. k * z * (l * w) = k * l * (z * w)

COMPLEX_LMUL_SCALAR_LMUL

⊢ ∀k z w. k * z * w = k * (z * w)

COMPLEX_RMUL_SCALAR_LMUL

⊢ ∀k z w. z * (k * w) = k * (z * w)

COMPLEX_SCALAR_LMUL_ZERO

⊢ ∀z. 0 * z = 0

COMPLEX_ZERO_SCALAR_LMUL

⊢ ∀k. k * 0 = 0

COMPLEX_SCALAR_LMUL_ONE

⊢ ∀z. 1 * z = z

COMPLEX_SCALAR_LMUL_NEG1

⊢ ∀z. -1 * z = -z

COMPLEX_DOUBLE

⊢ ∀z. z + z = 2 * z

COMPLEX_SCALAR_LMUL_ENTIRE

⊢ ∀k z. k * z = 0 ⇔ k = 0 ∨ z = 0

COMPLEX_EQ_SCALAR_LMUL

⊢ ∀k z w. k * z = k * w ⇔ k = 0 ∨ z = w

COMPLEX_SCALAR_LMUL_EQ

⊢ ∀k l z. k * z = l * z ⇔ k = l ∨ z = 0

COMPLEX_SCALAR_LMUL_EQ1

⊢ ∀k z. k * z = z ⇔ k = 1 ∨ z = 0

COMPLEX_INV_SCALAR_LMUL

⊢ ∀k z. k ≠ 0 ∧ z ≠ 0 ⇒ inv (k * z) = k⁻¹ * inv z

COMPLEX_SCALAR_LMUL_DIV2

⊢ ∀k l z w. l ≠ 0 ∧ w ≠ 0 ⇒ k * z / (l * w) = k / l * (z / w)

COMPLEX_SCALAR_MUL_COMM

⊢ ∀k z. k * z = z * k

COMPLEX_SCALAR_RMUL

⊢ ∀k l z. z * k * l = z * (k * l)

COMPLEX_SCALAR_RMUL_NEG

⊢ ∀k z. -(z * k) = z * -k

COMPLEX_NEG_SCALAR_RMUL

⊢ ∀k z. -z * k = z * -k

COMPLEX_SCALAR_RMUL_ADD

⊢ ∀k l z. z * (k + l) = z * k + z * l

COMPLEX_RSCALAR_RMUL_SUB

⊢ ∀k l z. z * (k − l) = z * k − z * l

COMPLEX_ADD_RSCALAR_RMUL

⊢ ∀k z w. (z + w) * k = z * k + w * k

COMPLEX_SUB_SCALAR_RMUL

⊢ ∀k z w. (z − w) * k = z * k − w * k

COMPLEX_SCALAR_RMUL_ZERO

⊢ ∀z. z * 0 = 0

COMPLEX_ZERO_SCALAR_RMUL

⊢ ∀k. 0 * k = 0

COMPLEX_SCALAR_RMUL_ONE

⊢ ∀z. z * 1 = z

COMPLEX_SCALAR_RMUL_NEG1

⊢ ∀z. z * -1 = -z

CONJ_REAL_REFL

⊢ ∀x. conj (complex_of_real x) = complex_of_real x

CONJ_NUM_REFL

⊢ ∀n. conj (&n) = &n

CONJ_ADD

⊢ ∀z w. conj (z + w) = conj z + conj w

CONJ_NEG

⊢ ∀z. conj (-z) = -conj z

CONJ_SUB

⊢ ∀z w. conj (z − w) = conj z − conj w

CONJ_MUL

⊢ ∀z w. conj (z * w) = conj z * conj w

CONJ_INV

⊢ ∀z. conj (inv z) = inv (conj z)

CONJ_DIV

⊢ ∀z w. conj (z / w) = conj z / conj w

CONJ_SCALAR_LMUL

⊢ ∀k z. conj (k * z) = k * conj z

CONJ_CONJ

⊢ ∀z. conj (conj z) = z

CONJ_EQ

⊢ ∀z w. conj z = w ⇔ z = conj w

CONJ_EQ2

⊢ ∀z w. conj z = conj w ⇔ z = w

COMPLEX_MUL_RCONJ

⊢ ∀z. conj z * z = complex_of_real (RE z pow 2 + IM z pow 2)

CONJ_ZERO

⊢ conj 0 = 0

MODU_POW2

⊢ ∀z. modu z pow 2 = RE z pow 2 + IM z pow 2

RE_IM_LE_MODU

⊢ ∀z. abs (RE z) ≤ modu z ∧ abs (IM z) ≤ modu z

MODU_POS

⊢ ∀z. 0 ≤ modu z

COMPLEX_MUL_RCONJ1

⊢ ∀z. z * conj z = complex_of_real (modu z pow 2)

COMPLEX_MUL_LCONJ1

⊢ ∀z. conj z * z = complex_of_real (modu z pow 2)

MODU_NEG

⊢ ∀z. modu (-z) = modu z

MODU_SUB

⊢ ∀z w. modu (z − w) = modu (w − z)

MODU_CONJ

⊢ ∀z. modu (conj z) = modu z

MODU_MUL

⊢ ∀z w. modu (z * w) = modu z * modu w

MODU_0

⊢ modu 0 = 0

MODU_1

⊢ modu 1 = 1

MODU_COMPLEX_INV

⊢ ∀z. z ≠ 0 ⇒ modu (inv z) = (modu z)⁻¹

MODU_DIV

⊢ ∀z w. w ≠ 0 ⇒ modu (z / w) = modu z / modu w

MODU_SCALAR_LMUL

⊢ ∀k z. modu (k * z) = abs k * modu z

MODU_REAL

⊢ ∀x. modu (complex_of_real x) = abs x

MODU_NUM

⊢ ∀n. modu (&n) = &n

MODU_ZERO

⊢ ∀z. z = 0 ⇔ modu z = 0

MODU_NZ

⊢ ∀z. z ≠ 0 ⇔ 0 < modu z

MODU_CASES

⊢ ∀z. z = 0 ∨ 0 < modu z

RE_DIV_MODU_BOUNDS

⊢ ∀z. z ≠ 0 ⇒ -1 ≤ RE z / modu z ∧ RE z / modu z ≤ 1

IM_DIV_MODU_BOUNDS

⊢ ∀z. z ≠ 0 ⇒ -1 ≤ IM z / modu z ∧ IM z / modu z ≤ 1

RE_DIV_MODU_ACS_BOUNDS

⊢ ∀z. z ≠ 0 ⇒ 0 ≤ acs (RE z / modu z) ∧ acs (RE z / modu z) ≤ pi

IM_DIV_MODU_ASN_BOUNDS

⊢ ∀z. z ≠ 0 ⇒ -(pi / 2) ≤ asn (IM z / modu z) ∧ asn (IM z / modu z) ≤ pi / 2

RE_DIV_MODU_ACS_COS

⊢ ∀z. z ≠ 0 ⇒ cos (acs (RE z / modu z)) = RE z / modu z

IM_DIV_MODU_ASN_SIN

⊢ ∀z. z ≠ 0 ⇒ sin (asn (IM z / modu z)) = IM z / modu z

ARG_COS

⊢ ∀z. z ≠ 0 ⇒ cos (arg z) = RE z / modu z

ARG_SIN

⊢ ∀z. z ≠ 0 ⇒ sin (arg z) = IM z / modu z

RE_MODU_ARG

⊢ ∀z. RE z = modu z * cos (arg z)

IM_MODU_ARG

⊢ ∀z. IM z = modu z * sin (arg z)

COMPLEX_TRIANGLE

⊢ ∀z. modu z * (cos (arg z),sin (arg z)) = z

COMPLEX_MODU_ARG_EQ

⊢ ∀z w. z = w ⇔ modu z = modu w ∧ arg z = arg w

MODU_UNIT

⊢ ∀x y. modu (cos x,sin x) = 1

COMPLEX_MUL_ARG

⊢ ∀x y. (cos x,sin x) * (cos y,sin y) = (cos (x + y),sin (x + y))

COMPLEX_INV_ARG

⊢ ∀x. inv (cos x,sin x) = (cos (-x),sin (-x))

COMPLEX_DIV_ARG

⊢ ∀x y. (cos x,sin x) / (cos y,sin y) = (cos (x − y),sin (x − y))

complex_pow_def_compute

⊢ (∀z. z pow 0 = 1) ∧
  (∀z n. z pow NUMERAL (BIT1 n) = z * z pow (NUMERAL (BIT1 n) − 1)) ∧
  ∀z n. z pow NUMERAL (BIT2 n) = z * z pow NUMERAL (BIT1 n)

COMPLEX_POW_0

⊢ ∀n. 0 pow SUC n = 0

COMPLEX_POW_NZ

⊢ ∀z n. z ≠ 0 ⇒ z pow n ≠ 0

COMPLEX_POWINV

⊢ ∀z. z ≠ 0 ⇒ ∀n. inv (z pow n) = inv z pow n

MODU_COMPLEX_POW

⊢ ∀z n. modu (z pow n) = modu z pow n

COMPLEX_POW_ADD

⊢ ∀z m n. z pow (m + n) = z pow m * z pow n

COMPLEX_POW_1

⊢ ∀z. z pow 1 = z

COMPLEX_POW_2

⊢ ∀z. z pow 2 = z * z

COMPLEX_POW_ONE

⊢ ∀n. 1 pow n = 1

COMPLEX_POW_MUL

⊢ ∀n z w. (z * w) pow n = z pow n * w pow n

COMPLEX_POW_INV

⊢ ∀z n. inv z pow n = inv (z pow n)

COMPLEX_POW_DIV

⊢ ∀z w n. (z / w) pow n = z pow n / w pow n

COMPLEX_POW_L

⊢ ∀n k z. (k * z) pow n = k pow n * z pow n

COMPLEX_POW_ZERO

⊢ ∀n z. z pow n = 0 ⇒ z = 0

COMPLEX_POW_ZERO_EQ

⊢ ∀n z. z pow SUC n = 0 ⇔ z = 0

COMPLEX_POW_POW

⊢ ∀z m n. (z pow m) pow n = z pow (m * n)

DE_MOIVRE_LEMMA

⊢ ∀x n. (cos x,sin x) pow n = (cos (&n * x),sin (&n * x))

DE_MOIVRE_THM

⊢ ∀z n.
      (modu z * (cos (arg z),sin (arg z))) pow n =
      modu z pow n * (cos (&n * arg z),sin (&n * arg z))

EXP_IMAGINARY

⊢ ∀x. exp (i * x) = (cos x,sin x)

EULER_FORMULE

⊢ ∀z. modu z * exp (i * arg z) = z

COMPLEX_EXP_ADD

⊢ ∀z w. exp (z + w) = exp z * exp w

COMPLEX_EXP_NEG

⊢ ∀z. exp (-z) = inv (exp z)

COMPLEX_EXP_SUB

⊢ ∀z w. exp (z − w) = exp z / exp w

COMPLEX_EXP_N

⊢ ∀z n. exp (&n * z) = exp z pow n

COMPLEX_EXP_N2

⊢ ∀z n. exp (&n * z) = exp z pow n

COMPLEX_EXP_0

⊢ exp 0 = 1

COMPLEX_EXP_NZ

⊢ ∀z. exp z ≠ 0

COMPLEX_EXP_ADD_MUL

⊢ ∀z w. exp (z + w) * exp (-z) = exp w

COMPLEX_EXP_NEG_MUL

⊢ ∀z. exp z * exp (-z) = 1

COMPLEX_EXP_NEG_MUL2

⊢ ∀z. exp (-z) * exp z = 1