:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received April 25, 2005

:: Copyright (c) 2005-2019 Association of Mizar Users

definition

let z be FinSequence of COMPLEX ;

z *' is FinSequence of COMPLEX

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = z *' iff ( len b_{1} = len z & ( for i being Nat st 1 <= i & i <= len z holds

b_{1} . i = (z . i) *' ) ) )

end;
:: original: *'

redefine func z *' -> FinSequence of COMPLEX means :Def1: :: COMPLSP2:def 1

( len it = len z & ( for i being Nat st 1 <= i & i <= len z holds

it . i = (z . i) *' ) );

coherence redefine func z *' -> FinSequence of COMPLEX means :Def1: :: COMPLSP2:def 1

( len it = len z & ( for i being Nat st 1 <= i & i <= len z holds

it . i = (z . i) *' ) );

z *' is FinSequence of COMPLEX

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem Def1 defines *' COMPLSP2:def 1 :

for z, b_{2} being FinSequence of COMPLEX holds

( b_{2} = z *' iff ( len b_{2} = len z & ( for i being Nat st 1 <= i & i <= len z holds

b_{2} . i = (z . i) *' ) ) );

for z, b

( b

b

Lm1: for x being FinSequence of COMPLEX

for c being Element of COMPLEX holds c * x = (multcomplex [;] (c,(id COMPLEX))) * x

proof end;

theorem :: COMPLSP2:1

theorem :: COMPLSP2:2

definition

let i be Element of NAT ;

let R1, R2 be Element of i -tuples_on COMPLEX;

:: original: -

redefine func R1 - R2 -> Element of i -tuples_on COMPLEX;

coherence

R1 - R2 is Element of i -tuples_on COMPLEX

end;
let R1, R2 be Element of i -tuples_on COMPLEX;

:: original: -

redefine func R1 - R2 -> Element of i -tuples_on COMPLEX;

coherence

R1 - R2 is Element of i -tuples_on COMPLEX

proof end;

definition

let i be Element of NAT ;

let R1, R2 be Element of i -tuples_on COMPLEX;

:: original: +

redefine func R1 + R2 -> Element of i -tuples_on COMPLEX;

coherence

R1 + R2 is Element of i -tuples_on COMPLEX

end;
let R1, R2 be Element of i -tuples_on COMPLEX;

:: original: +

redefine func R1 + R2 -> Element of i -tuples_on COMPLEX;

coherence

R1 + R2 is Element of i -tuples_on COMPLEX

proof end;

definition

let i be Element of NAT ;

let R be Element of i -tuples_on COMPLEX;

let r be Complex;

:: original: (#)

redefine func r * R -> Element of i -tuples_on COMPLEX;

coherence

r (#) R is Element of i -tuples_on COMPLEX

end;
let R be Element of i -tuples_on COMPLEX;

let r be Complex;

:: original: (#)

redefine func r * R -> Element of i -tuples_on COMPLEX;

coherence

r (#) R is Element of i -tuples_on COMPLEX

proof end;

Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX

proof end;

::$CT 4

definition

let i be Element of NAT ;

let R be Element of i -tuples_on COMPLEX;

:: original: -

redefine func - R -> Element of i -tuples_on COMPLEX;

coherence

- R is Element of i -tuples_on COMPLEX

end;
let R be Element of i -tuples_on COMPLEX;

:: original: -

redefine func - R -> Element of i -tuples_on COMPLEX;

coherence

- R is Element of i -tuples_on COMPLEX

proof end;

theorem :: COMPLSP2:14

theorem Th12: :: COMPLSP2:16

for x being FinSequence of COMPLEX

for i being Nat

for a being Complex holds (a * x) . i = a * (x . i)

for i being Nat

for a being Complex holds (a * x) . i = a * (x . i)

proof end;

theorem Th14: :: COMPLSP2:18

for i, j being Element of NAT

for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 + R2) . j = (R1 . j) + (R2 . j)

for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 + R2) . j = (R1 . j) + (R2 . j)

proof end;

theorem Th16: :: COMPLSP2:20

for i, j being Element of NAT

for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 - R2) . j = (R1 . j) - (R2 . j)

for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 - R2) . j = (R1 . j) - (R2 . j)

proof end;

theorem Th21: :: COMPLSP2:25

for i being Element of NAT

for x, y being complex-valued FinSequence st len x = len y holds

(x - y) . i = (x . i) - (y . i)

for x, y being complex-valued FinSequence st len x = len y holds

(x - y) . i = (x . i) - (y . i)

proof end;

theorem Th22: :: COMPLSP2:26

for i being Element of NAT

for x, y being complex-valued FinSequence st len x = len y holds

(x + y) . i = (x . i) + (y . i)

for x, y being complex-valued FinSequence st len x = len y holds

(x + y) . i = (x . i) + (y . i)

proof end;

definition

let z be FinSequence of COMPLEX ;

coherence

(1 / 2) * (z + (z *')) is FinSequence of REAL

end;
coherence

(1 / 2) * (z + (z *')) is FinSequence of REAL

proof end;

:: deftheorem defines Re COMPLSP2:def 2 :

for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *'));

for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *'));

definition

let z be FinSequence of COMPLEX ;

coherence

(- ((1 / 2) * <i>)) * (z - (z *')) is FinSequence of REAL

end;
coherence

(- ((1 / 2) * <i>)) * (z - (z *')) is FinSequence of REAL

proof end;

:: deftheorem defines Im COMPLSP2:def 3 :

for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * <i>)) * (z - (z *'));

for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * <i>)) * (z - (z *'));

definition

let x, y be FinSequence of COMPLEX ;

((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX by XCMPLX_0:def 2;

end;
func |(x,y)| -> Element of COMPLEX equals :: COMPLSP2:def 4

((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

coherence ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX by XCMPLX_0:def 2;

:: deftheorem defines |( COMPLSP2:def 4 :

for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

theorem Th24: :: COMPLSP2:28

for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds

x + (y + z) = (x + y) + z

x + (y + z) = (x + y) + z

proof end;

::$CT

theorem Th25: :: COMPLSP2:30

for c being Complex

for x, y being FinSequence of COMPLEX st len x = len y holds

c * (x + y) = (c * x) + (c * y)

for x, y being FinSequence of COMPLEX st len x = len y holds

c * (x + y) = (c * x) + (c * y)

proof end;

::$CT

theorem Th26: :: COMPLSP2:32

for x, y being complex-valued FinSequence st len x = len y & x + y = 0c (len x) holds

( x = - y & y = - x )

( x = - y & y = - x )

proof end;

theorem Th30: :: COMPLSP2:36

for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds

(x - y) - z = x - (y + z)

(x - y) - z = x - (y + z)

proof end;

theorem Th31: :: COMPLSP2:37

for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds

x + (y - z) = (x + y) - z

x + (y - z) = (x + y) - z

proof end;

::$CT

theorem Th33: :: COMPLSP2:40

for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds

x - (y - z) = (x - y) + z

x - (y - z) = (x - y) + z

proof end;

theorem Th36: :: COMPLSP2:43

for c being Complex

for x, y being FinSequence of COMPLEX st len x = len y holds

c * (x - y) = (c * x) - (c * y)

for x, y being FinSequence of COMPLEX st len x = len y holds

c * (x - y) = (c * x) - (c * y)

proof end;

theorem :: COMPLSP2:44

for x1, y1 being Element of COMPLEX

for x2, y2 being Real st x1 = x2 & y1 = y2 holds

addcomplex . (x1,y1) = addreal . (x2,y2)

for x2, y2 being Real st x1 = x2 & y1 = y2 holds

addcomplex . (x1,y1) = addreal . (x2,y2)

proof end;

theorem Th38: :: COMPLSP2:45

for C being Function of [:COMPLEX,COMPLEX:],COMPLEX

for G being Function of [:REAL,REAL:],REAL

for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

for G being Function of [:REAL,REAL:],REAL

for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

proof end;

theorem :: COMPLSP2:46

for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds

addcomplex .: (x1,y1) = addreal .: (x2,y2)

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds

addcomplex .: (x1,y1) = addreal .: (x2,y2)

proof end;

::$CT

theorem Th41: :: COMPLSP2:49

for x, y being FinSequence of COMPLEX st len x = len y holds

( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )

( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )

proof end;

theorem :: COMPLSP2:50

for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds

diffcomplex .: (x1,y1) = diffreal .: (x2,y2)

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds

diffcomplex .: (x1,y1) = diffreal .: (x2,y2)

proof end;

::$CT

theorem Th43: :: COMPLSP2:52

for x, y being FinSequence of COMPLEX st len x = len y holds

( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) )

( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) )

proof end;

Lm3: for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x)

proof end;

theorem Th46: :: COMPLSP2:55

for h being Function of COMPLEX,COMPLEX

for g being Function of REAL,REAL

for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

for g being Function of REAL,REAL

for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds

h . (y1 . i) = g . (y2 . i) ) holds

h * y1 = g * y2

proof end;

theorem :: COMPLSP2:56

for y1 being FinSequence of COMPLEX

for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds

compcomplex * y1 = compreal * y2

for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds

compcomplex * y1 = compreal * y2

proof end;

::$CT

theorem :: COMPLSP2:61

for a1 being Element of COMPLEX

for y1 being FinSequence of COMPLEX

for a2 being Element of REAL

for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds

(a1 multcomplex) * y1 = (a2 multreal) * y2

for y1 being FinSequence of COMPLEX

for a2 being Element of REAL

for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds

(a1 multcomplex) * y1 = (a2 multreal) * y2

proof end;

::$CT

theorem Th54: :: COMPLSP2:65

for a being Element of COMPLEX

for x being FinSequence of COMPLEX holds

( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )

for x being FinSequence of COMPLEX holds

( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )

proof end;

theorem Th55: :: COMPLSP2:66

for x1, x2, y being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y holds

|((x1 + x2),y)| = |(x1,y)| + |(x2,y)|

|((x1 + x2),y)| = |(x1,y)| + |(x2,y)|

proof end;

theorem Th59: :: COMPLSP2:70

for x1, x2, x3 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len x3 holds

|((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|

|((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|

proof end;

theorem Th60: :: COMPLSP2:71

for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds

|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|

|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|

proof end;

theorem Th61: :: COMPLSP2:72

for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds

|(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|

|(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|

proof end;

theorem Th62: :: COMPLSP2:73

for x1, x2, y1, y2 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds

|((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

|((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th63: :: COMPLSP2:74

for x1, x2, y1, y2 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds

|((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

|((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

proof end;

theorem :: COMPLSP2:76

for x, y being FinSequence of COMPLEX st len x = len y holds

|((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|

|((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|

proof end;

theorem :: COMPLSP2:77

for x, y being FinSequence of COMPLEX st len x = len y holds

|((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|

|((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|

proof end;

theorem Th67: :: COMPLSP2:78

for a being Element of COMPLEX

for x, y being FinSequence of COMPLEX st len x = len y holds

|((a * x),y)| = a * |(x,y)|

for x, y being FinSequence of COMPLEX st len x = len y holds

|((a * x),y)| = a * |(x,y)|

proof end;

theorem Th68: :: COMPLSP2:79

for a being Element of COMPLEX

for x, y being FinSequence of COMPLEX st len x = len y holds

|(x,(a * y))| = (a *') * |(x,y)|

for x, y being FinSequence of COMPLEX st len x = len y holds

|(x,(a * y))| = (a *') * |(x,y)|

proof end;

theorem :: COMPLSP2:80

for a, b being Element of COMPLEX

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds

|(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds

|(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)

proof end;

theorem :: COMPLSP2:81

for a, b being Element of COMPLEX

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds

|(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|)

for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds

|(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|)

proof end;