:: by Library Committee

::

:: Received April 10, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

:: '+' operation only

:: using operation '*'

:: operations '+' and '*' only

theorem :: XCMPLX_1:9

theorem :: XCMPLX_1:10

:: using operation '-'

:: 2 times '-'

Lm1: for a, b being Complex holds (a ") * (b ") = (a * b) "

proof end;

Lm2: for a, b, c being Complex holds a / (b / c) = (a * c) / b

proof end;

Lm3: for a, b being Complex st b <> 0 holds

(a / b) * b = a

proof end;

Lm4: for a being Complex holds 1 / a = a "

proof end;

Lm5: for a being Complex st a <> 0 holds

a / a = 1

proof end;

:: using operations '-' and '+'

:: 2 times '-'

:: 3 times '-'

theorem :: XCMPLX_1:42

:: using operations '-' and '*', '+'

theorem :: XCMPLX_1:43

theorem :: XCMPLX_1:44

theorem :: XCMPLX_1:45

theorem :: XCMPLX_1:46

theorem :: XCMPLX_1:47

:: using operation '/'

:: 0

:: 2 times '/'

Lm6: for a, b, c, d being Complex holds (a / b) * (c / d) = (a * c) / (b * d)

proof end;

Lm7: for a, b being Complex holds (a / b) " = b / a

proof end;

Lm8: for a, b, c being Complex holds a * (b / c) = (a * b) / c

proof end;

Lm9: for a, b being Complex st b <> 0 holds

a = (a * b) / b

proof end;

Lm10: for a, b, c being Complex st c <> 0 holds

a / b = (a * c) / (b * c)

proof end;

:: 1

Lm11: for a, b being Complex holds (a * (b ")) " = (a ") * b

proof end;

Lm12: for a, b being Complex st a " = b " holds

a = b

proof end;

:: 0 and 1

:: using operations '/' and '+'

:: 2

:: 3

:: 4

:: using operations '/' and '*'

:: 3 times '/'

theorem :: XCMPLX_1:76

Lm13: for a, b, c, d being Complex holds (a / b) / (c / d) = (a * d) / (b * c)

proof end;

Lm14: for a, b being Complex holds a * (1 / b) = a / b

proof end;

Lm15: for a, b, c being Complex holds (1 / c) * (a / b) = a / (b * c)

proof end;

:: 4 times '/'

theorem :: XCMPLX_1:84

:: 0

:: 2 times '/'

:: 3 times '/'

:: 1

Lm16: for a being Complex holds 1 / (a ") = a

proof end;

:: 3 times '/'

:: 4 times '/'

:: 1 and 0

:: using operations '*', '+' and '/'

theorem Th116: :: XCMPLX_1:116

for a, b, c, d being Complex st b <> 0 & d <> 0 holds

(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)

(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)

proof end;

:: 2

:: 3

Lm17: for a, b being Complex holds - (a / b) = (- a) / b

proof end;

theorem :: XCMPLX_1:123

for a, b, d, e being Complex st b <> 0 & d <> 0 & b <> d & a / b = e / d holds

a / b = (a - e) / (b - d)

a / b = (a - e) / (b - d)

proof end;

:: using operations '-', '/' and '+'

:: using operations '-', '/' and '*'

theorem :: XCMPLX_1:130

for a, b, c, d being Complex st b <> 0 & d <> 0 holds

(a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)

(a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)

proof end;

:: using operation '-', '/', '*' and '+'

theorem :: XCMPLX_1:132

:: using unary operation '-'

:: using unary and binary operation '-'

:: binary '-' 4 times

:: 0

:: using unary and binary operations '-' and '+'

:: '+' 3 times

:: binary '-' 3 times

:: using unary and binary operations '-' and '+'

:: using unary and binary operations '-' and '+' (both '-' 2 times)

:: using unary operations '-' and '*'

:: Thx

:: using unary operations '-' and '/'

Lm18: for a being Complex st a <> 0 & a = a " & not a = 1 holds

a = - 1

proof end;

theorem :: XCMPLX_1:200

for a, b, d, e being Complex st b <> 0 & d <> 0 & b <> - d & a / b = e / d holds

a / b = (a + e) / (b + d)

a / b = (a + e) / (b + d)

proof end;

:: using operation '"'

:: using '"' and '*'

:: using '"', '*', and '+'

Lm19: for a being Complex holds (- a) " = - (a ")

proof end;

:: using '"', '*', and '-'

:: using '"' and '/'

:: using '"', '*', and '/'

:: both unary operations

:: from JORDAN4

:: from REAL_2, 2005.02.05, A.T.

:: from IRRAT_1, 2005.02.05, A.T.

:: from BORSUK_6, 2005.02.05, A.T.

:: Missing, 2005.07.04, A.T.