:: by Czes{\l}aw Byli\'nski

::

:: Received May 11, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

registration

let n be Nat;

ex b_{1} being FinSequence st

( b_{1} is n -element & b_{1} is natural-valued )

end;
cluster Relation-like NAT -defined Function-like natural-valued V60() n -element FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof end;

registration

ex b_{1} being FinSequence st b_{1} is real-valued
end;

cluster Relation-like NAT -defined Function-like real-valued V60() FinSequence-like FinSubsequence-like for set ;

existence ex b

proof end;

definition

let F be real-valued Relation;

:: original: rng

redefine func rng F -> Subset of REAL;

coherence

rng F is Subset of REAL by VALUED_0:def 3;

end;
:: original: rng

redefine func rng F -> Subset of REAL;

coherence

rng F is Subset of REAL by VALUED_0:def 3;

registration

let D be non empty set ;

let F be Function of REAL,D;

let F1 be real-valued FinSequence;

coherence

F * F1 is FinSequence-like

end;
let F be Function of REAL,D;

let F1 be real-valued FinSequence;

coherence

F * F1 is FinSequence-like

proof end;

registration
end;

registration
end;

definition

compatibility

for b_{1} being Element of bool [:[:REAL,REAL:],REAL:] holds

( b_{1} = diffreal iff b_{1} = addreal * ((id REAL),compreal) )

;

end;
for b

( b

proof end;

correctness ;

definition

ex b_{1} being UnOp of REAL st

for r being real number holds b_{1} . r = r ^2

for b_{1}, b_{2} being UnOp of REAL st ( for r being real number holds b_{1} . r = r ^2 ) & ( for r being real number holds b_{2} . r = r ^2 ) holds

b_{1} = b_{2}
end;

func sqrreal -> UnOp of REAL means :Def2: :: RVSUM_1:def 2

for r being real number holds it . r = r ^2 ;

existence for r being real number holds it . r = r ^2 ;

ex b

for r being real number holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :

for b_{1} being UnOp of REAL holds

( b_{1} = sqrreal iff for r being real number holds b_{1} . r = r ^2 );

for b

( b

definition
end;

:: deftheorem defines multreal RVSUM_1:def 3 :

for x being real number holds x multreal = multreal [;] (x,(id REAL));

for x being real number holds x multreal = multreal [;] (x,(id REAL));

Lm1: for r, r1 being real number holds (multreal [;] (r,(id REAL))) . r1 = r * r1

proof end;

Lm2: for F being real-valued FinSequence holds F is FinSequence of REAL

proof end;

definition

let F1, F2 be real-valued FinSequence;

F1 + F2 is FinSequence of REAL by Lm2;

compatibility

for b_{1} being FinSequence of REAL holds

( b_{1} = F1 + F2 iff b_{1} = addreal .: (F1,F2) )

for b_{1} being FinSequence of REAL

for F1, F2 being real-valued FinSequence st b_{1} = addreal .: (F1,F2) holds

b_{1} = addreal .: (F2,F1)

end;
:: original: +

redefine func F1 + F2 -> FinSequence of REAL equals :: RVSUM_1:def 4

addreal .: (F1,F2);

coherence redefine func F1 + F2 -> FinSequence of REAL equals :: RVSUM_1:def 4

addreal .: (F1,F2);

F1 + F2 is FinSequence of REAL by Lm2;

compatibility

for b

( b

proof end;

commutativity for b

for F1, F2 being real-valued FinSequence st b

b

proof end;

:: deftheorem defines + RVSUM_1:def 4 :

for F1, F2 being real-valued FinSequence holds F1 + F2 = addreal .: (F1,F2);

for F1, F2 being real-valued FinSequence holds F1 + F2 = addreal .: (F1,F2);

definition

let i be Nat;

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

:: original: +

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

coherence

R1 + R2 is Element of i -tuples_on REAL by FINSEQ_2:120;

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

:: original: +

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

coherence

R1 + R2 is Element of i -tuples_on REAL by FINSEQ_2:120;

theorem :: RVSUM_1:11

for s being set

for i being Nat

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

for i being Nat

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

proof end;

theorem :: RVSUM_1:15

theorem :: RVSUM_1:16

for i being Nat

for R being Element of i -tuples_on REAL holds R + (i |-> 0) = R by BINOP_2:2, FINSEQOP:56;

for R being Element of i -tuples_on REAL holds R + (i |-> 0) = R by BINOP_2:2, FINSEQOP:56;

theorem :: RVSUM_1:17

definition

let F be real-valued FinSequence;

coherence

- F is FinSequence of REAL by Lm2;

compatibility

for b_{1} being FinSequence of REAL holds

( b_{1} = - F iff b_{1} = compreal * F )

end;
coherence

- F is FinSequence of REAL by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines - RVSUM_1:def 5 :

for F being real-valued FinSequence holds - F = compreal * F;

for F being real-valued FinSequence holds - F = compreal * F;

definition

let i be Nat;

let R be Element of i -tuples_on REAL;

:: original: -

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

coherence

- R is Element of i -tuples_on REAL by FINSEQ_2:113;

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

:: original: -

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

coherence

- R is Element of i -tuples_on REAL by FINSEQ_2:113;

theorem :: RVSUM_1:18

theorem :: RVSUM_1:22

theorem :: RVSUM_1:23

definition

let F1, F2 be real-valued FinSequence;

F1 - F2 is FinSequence of REAL by Lm2;

compatibility

for b_{1} being FinSequence of REAL holds

( b_{1} = F1 - F2 iff b_{1} = diffreal .: (F1,F2) )

end;
:: original: -

redefine func F1 - F2 -> FinSequence of REAL equals :: RVSUM_1:def 6

diffreal .: (F1,F2);

coherence redefine func F1 - F2 -> FinSequence of REAL equals :: RVSUM_1:def 6

diffreal .: (F1,F2);

F1 - F2 is FinSequence of REAL by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines - RVSUM_1:def 6 :

for F1, F2 being real-valued FinSequence holds F1 - F2 = diffreal .: (F1,F2);

for F1, F2 being real-valued FinSequence holds F1 - F2 = diffreal .: (F1,F2);

definition

let i be Nat;

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

:: original: -

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

coherence

R1 - R2 is Element of i -tuples_on REAL by FINSEQ_2:120;

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

:: original: -

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

coherence

R1 - R2 is Element of i -tuples_on REAL by FINSEQ_2:120;

theorem :: RVSUM_1:27

for s being set

for i being Nat

for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)

for i being Nat

for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)

proof end;

theorem :: RVSUM_1:33

theorem :: RVSUM_1:37

theorem :: RVSUM_1:39

theorem :: RVSUM_1:40

theorem :: RVSUM_1:41

theorem :: RVSUM_1:44

for s being set

for r being real number

for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;

for r being real number

for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;

definition

let F be real-valued FinSequence;

let r be real number ;

coherence

r * F is FinSequence of REAL by Lm2;

compatibility

for b_{1} being FinSequence of REAL holds

( b_{1} = r * F iff b_{1} = (r multreal) * F )

end;
let r be real number ;

coherence

r * F is FinSequence of REAL by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines * RVSUM_1:def 7 :

for F being real-valued FinSequence

for r being real number holds r * F = (r multreal) * F;

for F being real-valued FinSequence

for r being real number holds r * F = (r multreal) * F;

definition

let i be Nat;

let R be Element of i -tuples_on REAL;

let r be real number ;

:: original: *

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

coherence

r * R is Element of i -tuples_on REAL by FINSEQ_2:113;

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

let r be real number ;

:: original: *

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

coherence

r * R is Element of i -tuples_on REAL by FINSEQ_2:113;

theorem :: RVSUM_1:45

for s being set

for r being real number

for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;

for r being real number

for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;

theorem :: RVSUM_1:49

for r1, r2 being real number

for F being real-valued FinSequence holds (r1 * r2) * F = r1 * (r2 * F) by RFUNCT_1:17;

for F being real-valued FinSequence holds (r1 * r2) * F = r1 * (r2 * F) by RFUNCT_1:17;

theorem :: RVSUM_1:50

for r1, r2 being real number

for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F)

for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F)

proof end;

theorem :: RVSUM_1:51

for r being real number

for F1, F2 being real-valued FinSequence holds r * (F1 + F2) = (r * F1) + (r * F2) by RFUNCT_1:16;

for F1, F2 being real-valued FinSequence holds r * (F1 + F2) = (r * F1) + (r * F2) by RFUNCT_1:16;

definition

let F be real-valued FinSequence;

compatibility

for b_{1} being FinSequence of REAL holds

( b_{1} = sqr F iff b_{1} = sqrreal * F )

sqr F is FinSequence of REAL by Lm2;

end;
compatibility

for b

( b

proof end;

coherence sqr F is FinSequence of REAL by Lm2;

:: deftheorem defines sqr RVSUM_1:def 8 :

for F being real-valued FinSequence holds sqr F = sqrreal * F;

for F being real-valued FinSequence holds sqr F = sqrreal * F;

definition

let i be Nat;

let R be Element of i -tuples_on REAL;

:: original: sqr

redefine func sqr R -> Element of i -tuples_on REAL;

coherence

sqr R is Element of i -tuples_on REAL by FINSEQ_2:113;

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

:: original: sqr

redefine func sqr R -> Element of i -tuples_on REAL;

coherence

sqr R is Element of i -tuples_on REAL by FINSEQ_2:113;

definition

let F1, F2 be real-valued FinSequence;

mlt (F1,F2) is FinSequence of REAL by Lm2;

compatibility

for b_{1} being FinSequence of REAL holds

( b_{1} = mlt (F1,F2) iff b_{1} = multreal .: (F1,F2) )

for b_{1} being FinSequence of REAL

for F1, F2 being real-valued FinSequence st b_{1} = multreal .: (F1,F2) holds

b_{1} = multreal .: (F2,F1)

end;
:: original: mlt

redefine func mlt (F1,F2) -> FinSequence of REAL equals :: RVSUM_1:def 9

multreal .: (F1,F2);

coherence redefine func mlt (F1,F2) -> FinSequence of REAL equals :: RVSUM_1:def 9

multreal .: (F1,F2);

mlt (F1,F2) is FinSequence of REAL by Lm2;

compatibility

for b

( b

proof end;

commutativity for b

for F1, F2 being real-valued FinSequence st b

b

proof end;

:: deftheorem defines mlt RVSUM_1:def 9 :

for F1, F2 being real-valued FinSequence holds mlt (F1,F2) = multreal .: (F1,F2);

for F1, F2 being real-valued FinSequence holds mlt (F1,F2) = multreal .: (F1,F2);

theorem :: RVSUM_1:59

for s being set

for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;

for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;

definition

let i be Nat;

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

:: original: mlt

redefine func mlt (R1,R2) -> Element of i -tuples_on REAL;

coherence

mlt (R1,R2) is Element of i -tuples_on REAL by FINSEQ_2:120;

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

:: original: mlt

redefine func mlt (R1,R2) -> Element of i -tuples_on REAL;

coherence

mlt (R1,R2) is Element of i -tuples_on REAL by FINSEQ_2:120;

theorem :: RVSUM_1:60

for s being set

for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;

for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;

theorem Th63: :: RVSUM_1:63

for i being Nat

for r being real number

for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R

for r being real number

for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R

proof end;

theorem :: RVSUM_1:65

for r being real number

for F1, F2 being real-valued FinSequence holds r * (mlt (F1,F2)) = mlt ((r * F1),F2) by RFUNCT_1:12;

for F1, F2 being real-valued FinSequence holds r * (mlt (F1,F2)) = mlt ((r * F1),F2) by RFUNCT_1:12;

theorem :: RVSUM_1:66

theorem Th68: :: RVSUM_1:68

for F1, F2 being real-valued FinSequence holds sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)

proof end;

theorem Th69: :: RVSUM_1:69

for F1, F2 being real-valued FinSequence holds sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2)

proof end;

registration

coherence

for b_{1} being FinSequence of COMPLEX holds b_{1} is complex-valued
;

ex b_{1} being FinSequence st

( b_{1} is real-valued & b_{1} is complex-valued )

end;
for b

cluster Relation-like NAT -defined Function-like complex-valued real-valued V60() FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof end;

definition

let F be complex-valued FinSequence;

ex b_{1} being complex number ex f being FinSequence of COMPLEX st

( f = F & b_{1} = addcomplex $$ f )

for b_{1}, b_{2} being complex number st ex f being FinSequence of COMPLEX st

( f = F & b_{1} = addcomplex $$ f ) & ex f being FinSequence of COMPLEX st

( f = F & b_{2} = addcomplex $$ f ) holds

b_{1} = b_{2}
;

end;
func Sum F -> complex number means :Def10: :: RVSUM_1:def 10

ex f being FinSequence of COMPLEX st

( f = F & it = addcomplex $$ f );

existence ex f being FinSequence of COMPLEX st

( f = F & it = addcomplex $$ f );

ex b

( f = F & b

proof end;

uniqueness for b

( f = F & b

( f = F & b

b

:: deftheorem Def10 defines Sum RVSUM_1:def 10 :

for F being complex-valued FinSequence

for b_{2} being complex number holds

( b_{2} = Sum F iff ex f being FinSequence of COMPLEX st

( f = F & b_{2} = addcomplex $$ f ) );

for F being complex-valued FinSequence

for b

( b

( f = F & b

definition

let F be FinSequence of COMPLEX ;

coherence

Sum F is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = Sum F iff b_{1} = addcomplex $$ F )
by Def10;

end;
coherence

Sum F is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

:: deftheorem defines Sum RVSUM_1:def 11 :

for F being FinSequence of COMPLEX holds Sum F = addcomplex $$ F;

for F being FinSequence of COMPLEX holds Sum F = addcomplex $$ F;

definition

let F be FinSequence of REAL ;

coherence

Sum F is Element of REAL by XREAL_0:def 1;

compatibility

for b_{1} being Element of REAL holds

( b_{1} = Sum F iff b_{1} = addreal $$ F )
by Th71;

end;
coherence

Sum F is Element of REAL by XREAL_0:def 1;

compatibility

for b

( b

:: deftheorem defines Sum RVSUM_1:def 12 :

for F being FinSequence of REAL holds Sum F = addreal $$ F;

for F being FinSequence of REAL holds Sum F = addreal $$ F;

theorem Th82: :: RVSUM_1:82

for i being Nat

for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds

R1 . j <= R2 . j ) holds

Sum R1 <= Sum R2

for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds

R1 . j <= R2 . j ) holds

Sum R1 <= Sum R2

proof end;

theorem Th83: :: RVSUM_1:83

for i being Nat

for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds

R1 . j <= R2 . j ) & ex j being Nat st

( j in Seg i & R1 . j < R2 . j ) holds

Sum R1 < Sum R2

for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds

R1 . j <= R2 . j ) & ex j being Nat st

( j in Seg i & R1 . j < R2 . j ) holds

Sum R1 < Sum R2

proof end;

theorem Th84: :: RVSUM_1:84

for F being real-valued FinSequence st ( for i being Nat st i in dom F holds

0 <= F . i ) holds

0 <= Sum F

0 <= F . i ) holds

0 <= Sum F

proof end;

theorem Th85: :: RVSUM_1:85

for F being real-valued FinSequence st ( for i being Nat st i in dom F holds

0 <= F . i ) & ex i being Nat st

( i in dom F & 0 < F . i ) holds

0 < Sum F

0 <= F . i ) & ex i being Nat st

( i in dom F & 0 < F . i ) holds

0 < Sum F

proof end;

theorem Th89: :: RVSUM_1:89

for i being Nat

for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

proof end;

theorem Th90: :: RVSUM_1:90

for i being Nat

for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

proof end;

theorem :: RVSUM_1:92

for i being Nat

for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))

for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))

proof end;

:: The Product of Finite Sequences of Real Numbers

definition

let F be complex-valued FinSequence;

ex b_{1} being complex number ex f being FinSequence of COMPLEX st

( f = F & b_{1} = multcomplex $$ f )

for b_{1}, b_{2} being complex number st ex f being FinSequence of COMPLEX st

( f = F & b_{1} = multcomplex $$ f ) & ex f being FinSequence of COMPLEX st

( f = F & b_{2} = multcomplex $$ f ) holds

b_{1} = b_{2}
;

end;
func Product F -> complex number means :Def13: :: RVSUM_1:def 13

ex f being FinSequence of COMPLEX st

( f = F & it = multcomplex $$ f );

existence ex f being FinSequence of COMPLEX st

( f = F & it = multcomplex $$ f );

ex b

( f = F & b

proof end;

uniqueness for b

( f = F & b

( f = F & b

b

:: deftheorem Def13 defines Product RVSUM_1:def 13 :

for F being complex-valued FinSequence

for b_{2} being complex number holds

( b_{2} = Product F iff ex f being FinSequence of COMPLEX st

( f = F & b_{2} = multcomplex $$ f ) );

for F being complex-valued FinSequence

for b

( b

( f = F & b

definition

let F be FinSequence of COMPLEX ;

Product F is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = Product F iff b_{1} = multcomplex $$ F )
by Def13;

end;
:: original: Product

redefine func Product F -> Element of COMPLEX equals :: RVSUM_1:def 14

multcomplex $$ F;

coherence redefine func Product F -> Element of COMPLEX equals :: RVSUM_1:def 14

multcomplex $$ F;

Product F is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

:: deftheorem defines Product RVSUM_1:def 14 :

for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F;

for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F;

definition

let F be FinSequence of REAL ;

Product F is Element of REAL by XREAL_0:def 1;

compatibility

for b_{1} being Element of REAL holds

( b_{1} = Product F iff b_{1} = multreal $$ F )
by Th93;

end;
:: original: Product

redefine func Product F -> Element of REAL equals :: RVSUM_1:def 15

multreal $$ F;

coherence redefine func Product F -> Element of REAL equals :: RVSUM_1:def 15

multreal $$ F;

Product F is Element of REAL by XREAL_0:def 1;

compatibility

for b

( b

:: deftheorem defines Product RVSUM_1:def 15 :

for F being FinSequence of REAL holds Product F = multreal $$ F;

for F being FinSequence of REAL holds Product F = multreal $$ F;

Lm3: for F being empty FinSequence holds Product F = 1

proof end;

registration
end;

registration
end;

theorem Th96: :: RVSUM_1:96

for F being complex-valued FinSequence

for r being complex number holds Product (F ^ <*r*>) = (Product F) * r

for r being complex number holds Product (F ^ <*r*>) = (Product F) * r

proof end;

theorem :: RVSUM_1:98

for r being real number

for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)

for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)

proof end;

Lm4: for p being complex-valued FinSequence st len p <> 0 holds

ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*>

proof end;

theorem :: RVSUM_1:103

for F being complex-valued FinSequence holds

( ex k being Nat st

( k in dom F & F . k = 0 ) iff Product F = 0 )

( ex k being Nat st

( k in dom F & F . k = 0 ) iff Product F = 0 )

proof end;

theorem :: RVSUM_1:104

for i, j being Nat

for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))

for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))

proof end;

theorem :: RVSUM_1:105

for i, j being Nat

for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))

for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))

proof end;

theorem :: RVSUM_1:106

for i being Nat

for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))

for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))

proof end;

theorem Th107: :: RVSUM_1:107

for i being Nat

for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)

for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)

proof end;

theorem :: RVSUM_1:108

for i being Nat

for r being real number

for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)

for r being real number

for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)

proof end;

theorem :: RVSUM_1:109

begin

theorem :: RVSUM_1:111

for i, j being Nat

for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))

for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))

proof end;

theorem :: RVSUM_1:112

theorem :: RVSUM_1:113

for i being Nat

for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))

for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))

proof end;

begin

theorem Th118: :: RVSUM_1:118

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

mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))

mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))

proof end;

begin

definition

let x1, x2 be real-valued FinSequence;

correctness

coherence

Sum (mlt (x1,x2)) is real number ;

;

commutativity

for b_{1} being real number

for x1, x2 being real-valued FinSequence st b_{1} = Sum (mlt (x1,x2)) holds

b_{1} = Sum (mlt (x2,x1))
;

end;
correctness

coherence

Sum (mlt (x1,x2)) is real number ;

;

commutativity

for b

for x1, x2 being real-valued FinSequence st b

b

:: deftheorem defines |( RVSUM_1:def 16 :

for x1, x2 being real-valued FinSequence holds |(x1,x2)| = Sum (mlt (x1,x2));

for x1, x2 being real-valued FinSequence holds |(x1,x2)| = Sum (mlt (x1,x2));

definition

let x1, x2 be real-valued FinSequence;

:: original: |(

redefine func |(x1,x2)| -> Element of REAL ;

correctness

coherence

|(x1,x2)| is Element of REAL ;

;

commutativity

for x1, x2 being real-valued FinSequence holds |(x1,x2)| = |(x2,x1)| ;

end;
:: original: |(

redefine func |(x1,x2)| -> Element of REAL ;

correctness

coherence

|(x1,x2)| is Element of REAL ;

;

commutativity

for x1, x2 being real-valued FinSequence holds |(x1,x2)| = |(x2,x1)| ;

theorem Th120: :: RVSUM_1:120

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

|((x + y),z)| = |(x,z)| + |(y,z)|

|((x + y),z)| = |(x,z)| + |(y,z)|

proof end;

theorem Th121: :: RVSUM_1:121

for x, y being real-valued FinSequence

for a being real number st len x = len y holds

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

for a being real number st len x = len y holds

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

proof end;

theorem Th124: :: RVSUM_1:124

for x1, x2, x3 being real-valued FinSequence 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 :: RVSUM_1:125

for x, y being real number

for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds

|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)

for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds

|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)

proof end;

theorem Th126: :: RVSUM_1:126

for x1, x2, y1, y2 being real-valued FinSequence 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 Th127: :: RVSUM_1:127

for x1, x2, y1, y2 being real-valued FinSequence 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 :: RVSUM_1:128

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

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

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

proof end;

theorem :: RVSUM_1:129

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

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

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

proof end;

theorem Th130: :: RVSUM_1:130

for n being Nat

for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|

for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|

proof end;

theorem Th131: :: RVSUM_1:131

for n being Nat

for p1, p2 being Element of n -tuples_on REAL

for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|

for p1, p2 being Element of n -tuples_on REAL

for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|

proof end;

theorem Th134: :: RVSUM_1:134

for n being Nat

for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|

for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|

proof end;

theorem :: RVSUM_1:135

for n being Nat

for x, y being real number

for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)

for x, y being real number

for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)

proof end;

theorem Th136: :: RVSUM_1:136

for n being Nat

for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|

for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|

proof end;

theorem Th137: :: RVSUM_1:137

for n being Nat

for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|

for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|

proof end;

theorem :: RVSUM_1:138

for n being Nat

for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|

for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem Th139: :: RVSUM_1:139

for n being Nat

for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|

for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|

proof end;

definition

let p, q be real-valued FinSequence;

symmetry

for p, q being real-valued FinSequence st |(p,q)| = 0 holds

|(q,p)| = 0 ;

end;
symmetry

for p, q being real-valued FinSequence st |(p,q)| = 0 holds

|(q,p)| = 0 ;

:: deftheorem Def17 defines are_orthogonal RVSUM_1:def 17 :

for p, q being real-valued FinSequence holds

( p,q are_orthogonal iff |(p,q)| = 0 );

for p, q being real-valued FinSequence holds

( p,q are_orthogonal iff |(p,q)| = 0 );

theorem :: RVSUM_1:141

for n being Nat

for a being real number

for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds

a * p,q are_orthogonal

for a being real number

for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds

a * p,q are_orthogonal

proof end;

:: 2009.08.15, from TURING_0, A.T.