:: Arithmetic Operations on Short Finite Sequences
:: by Rafa{\l} Ziobro
::
:: Copyright (c) 2018-2019 Association of Mizar Users

:: empty Relations are full of adjectives
registration
coherence
for b1 being Relation st b1 is empty holds
b1 is positive-yielding
proof end;
coherence
for b1 being Relation st b1 is empty holds
b1 is negative-yielding
proof end;
end;

registration
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is NAT -valued
proof end;
end;

registration
let f be complex-valued Function;
let k be object ;
reduce (0 (#) f) . k to 0 ;
reducibility
(0 (#) f) . k = 0
proof end;
end;

registration
let f be complex-valued Function;
reduce 1 (#) f to f;
reducibility
1 (#) f = f
by RFUNCT_1:21;
reduce (- 1) (#) (- f) to f;
reducibility
(- 1) (#) (- f) = f
proof end;
coherence
proof end;
coherence
f - f is empty-yielding
proof end;
end;

registration
let D be set ;
existence
ex b1 being D -valued FinSequence st b1 is empty-yielding
proof end;
end;

registration
coherence
for b1 being FinSequence st b1 is empty-yielding holds
b1 is NAT -valued
proof end;
existence
not for b1 being empty-yielding FinSequence holds b1 is empty
proof end;
end;

registration
let n be Nat;
existence
ex b1 being empty-yielding NAT -valued FinSequence st b1 is n -element
proof end;
cluster min (n,0) -> zero ;
coherence
min (n,0) is zero
by XXREAL_0:def 9;
reduce max (n,0) to n;
reducibility
max (n,0) = n
by XXREAL_0:def 10;
end;

registration
let a be non zero Nat;
reduce min (a,1) to 1;
reducibility
min (a,1) = 1
by ;
reduce max (a,1) to a;
reducibility
max (a,1) = a
by ;
end;

registration
let a be non trivial Nat;
reduce min (a,2) to 2;
reducibility
min (a,2) = 2
proof end;
reduce max (a,2) to a;
reducibility
max (a,2) = a
proof end;
end;

registration
let a be positive Real;
let b be positive Nat;
cluster b |-> a -> positive ;
coherence
b |-> a is positive
proof end;
end;

registration
coherence
for b1 being Relation st b1 is empty-yielding holds
b1 is Function-like
proof end;
coherence
for b1 being Function st b1 is empty-yielding holds
b1 is natural-valued
proof end;
coherence
for b1 being real-valued Function st b1 is empty-yielding holds
b1 is nonpositive-yielding
proof end;
coherence
for b1 being real-valued Function st b1 is empty-yielding holds
b1 is nonnegative-yielding
proof end;
coherence
for b1 being non empty real-valued Function st b1 is empty-yielding holds
not b1 is positive-yielding
proof end;
coherence
for b1 being non empty real-valued Function st b1 is empty-yielding holds
not b1 is negative-yielding
proof end;
coherence
for b1 being non empty real-valued Function st b1 is positive-yielding holds
not b1 is nonpositive-yielding
proof end;
coherence
for b1 being non empty real-valued Function st b1 is negative-yielding holds
not b1 is nonnegative-yielding
proof end;
end;

registration
let f be empty-yielding Function;
let c be Complex;
coherence
proof end;
end;

registration
let f be empty-yielding Function;
let g be complex-valued Function;
coherence
proof end;
end;

:: length of FinSequences
registration
let f be complex-valued FinSequence;
let x be Complex;
cluster x + f -> len f -element ;
coherence
f + x is len f -element
proof end;
cluster f - x -> len f -element ;
coherence
f - x is len f -element
proof end;
end;

registration
let f be complex-valued FinSequence;
coherence
abs f is len f -element
proof end;
cluster - f -> len f -element ;
coherence
- f is len f -element
proof end;
cluster f " -> len f -element ;
coherence
f " is len f -element
proof end;
end;

registration
let n, m be Nat;
let f be n -element complex-valued FinSequence;
let g be m -element complex-valued FinSequence;
cluster f + g -> min (n,m) -element ;
coherence
f + g is min (n,m) -element
proof end;
cluster f (#) g -> min (n,m) -element ;
coherence
f (#) g is min (n,m) -element
proof end;
cluster f - g -> min (n,m) -element ;
coherence
f - g is min (n,m) -element
proof end;
cluster f /" g -> min (n,m) -element ;
coherence
f /" g is min (n,m) -element
proof end;
end;

registration
let n, m be Nat;
let f be n -element complex-valued FinSequence;
let g be empty-yielding n + m -element complex-valued FinSequence;
reduce f + g to f;
reducibility
f + g = f
proof end;
end;

registration
let n be Nat;
let f be n -element complex-valued FinSequence;
let g be empty-yielding n -element complex-valued FinSequence;
reduce f + g to f;
reducibility
f + g = f
proof end;
end;

registration
let X be non empty set ;
existence
ex b1 being empty-yielding X -defined Function st b1 is total
proof end;
end;

registration
let X be non empty set ;
let f be X -defined total complex-valued Function;
let g be empty-yielding X -defined total Function;
reduce f + g to f;
reducibility
f + g = f
proof end;
end;

registration
let f be Relation;
existence
ex b1 being Relation st b1 is dom f -defined
by RELAT_1:def 18;
cluster f null f -> dom f -defined ;
coherence
f null f is dom f -defined
by RELAT_1:def 18;
existence
ex b1 being dom f -defined Relation st b1 is total
proof end;
end;

registration
let f be complex-valued Function;
existence
ex b1 being empty-yielding dom f -defined Function st b1 is total
proof end;
cluster - f -> dom f -defined ;
coherence
- f is dom f -defined
proof end;
cluster - f -> total ;
coherence
- f is total
proof end;
cluster f " -> dom f -defined ;
coherence
f " is dom f -defined
proof end;
cluster f " -> total ;
coherence
f " is total
proof end;
coherence
abs f is dom f -defined
proof end;
cluster |.f.| -> total ;
coherence
abs f is total
proof end;
end;

registration
let f be complex-valued Function;
let c be Complex;
cluster c + f -> dom f -defined ;
coherence
c + f is dom f -defined
proof end;
cluster c + f -> total ;
coherence
c + f is total
proof end;
cluster f - c -> dom f -defined ;
coherence
f - c is dom f -defined
proof end;
cluster f - c -> total ;
coherence
f - c is total
proof end;
cluster c * f -> dom f -defined ;
coherence
c (#) f is dom f -defined
proof end;
cluster c * f -> total ;
coherence
c (#) f is total
proof end;
end;

registration
let f be FinSequence;
coherence
for b1 being FinSequence st b1 is len f -element holds
b1 is dom f -defined
proof end;
end;

registration
let n be Nat;
coherence
for b1 being FinSequence st b1 is n -element holds
b1 is Seg n -defined
proof end;
coherence
for b1 being FinSequence st b1 is total & b1 is Seg n -defined holds
b1 is n -element
proof end;
end;

theorem EMP: :: FINSEQ_9:1
for f being complex-valued FinSequence holds 0 (#) f = (len f) |-> 0
proof end;

registration
let f be complex-valued FinSequence;
reduce f + ((len f) |-> 0) to f;
reducibility
f + ((len f) |-> 0) = f
proof end;
end;

registration
let n be Nat;
let D be non empty set ;
let X be non empty Subset of D;
existence
ex b1 being X -valued FinSequence st b1 is n -element
proof end;
existence
ex b1 being FinSequence of X st b1 is n -element
proof end;
end;

registration
let f be real-valued Function;
cluster f + (abs f) -> nonnegative-yielding ;
coherence
f + (abs f) is nonnegative-yielding
proof end;
cluster (abs f) - f -> nonnegative-yielding ;
coherence
(abs f) - f is nonnegative-yielding
proof end;
end;

registration
let f be real-valued nonnegative-yielding Function;
let x be object ;
cluster f . x -> non negative ;
coherence
not f . x is negative
proof end;
end;

registration
let f be real-valued nonpositive-yielding Function;
let x be object ;
cluster f . x -> non positive ;
coherence
not f . x is positive
proof end;
end;

registration
let f be real-valued nonnegative-yielding Function;
let r be non negative Real;
coherence
proof end;
cluster (- r) * f -> nonpositive-yielding ;
coherence
(- r) (#) f is nonpositive-yielding
proof end;
end;

registration
let f be real-valued nonnegative-yielding Function;
coherence
proof end;
end;

registration
let f be real-valued nonpositive-yielding Function;
let r be non negative Real;
coherence
proof end;
cluster (- r) * f -> nonnegative-yielding ;
coherence
(- r) (#) f is nonnegative-yielding
proof end;
end;

registration
let f be real-valued nonpositive-yielding Function;
coherence
proof end;
end;

registration
coherence
for b1 being INT -valued Function st b1 is nonnegative-yielding holds
b1 is natural-valued
proof end;
end;

registration
let f be INT -valued Function;
cluster (1 / 2) * (f + (abs f)) -> natural-valued ;
coherence
(1 / 2) (#) (f + (abs f)) is natural-valued
proof end;
cluster (1 / 2) * ((abs f) - f) -> natural-valued ;
coherence
(1 / 2) (#) ((abs f) - f) is natural-valued
proof end;
end;

:: Values are members of the range
theorem NV: :: FINSEQ_9:2
for f being Relation holds
( rng f is natural-membered iff f is natural-valued )
proof end;

theorem :: FINSEQ_9:3
for f being Relation holds
( f is NAT -valued iff rng f is natural-membered )
proof end;

theorem :: FINSEQ_9:4
for f being Relation holds
( rng f is integer-membered iff f is INT -valued )
proof end;

theorem :: FINSEQ_9:5
for f being Relation holds
( rng f is rational-membered iff f is RAT -valued )
proof end;

theorem RV: :: FINSEQ_9:6
for f being Relation holds
( rng f is real-membered iff f is real-valued )
proof end;

theorem :: FINSEQ_9:7
for f being Relation holds
( f is REAL -valued iff rng f is real-membered )
proof end;

theorem CV: :: FINSEQ_9:8
for f being Relation holds
( rng f is complex-membered iff f is complex-valued )
proof end;

theorem :: FINSEQ_9:9
for f being Relation holds
( f is COMPLEX -valued iff rng f is complex-membered )
proof end;

:: similarly: Relations are defined over members of their domain
theorem :: FINSEQ_9:10
for f being Relation holds
( dom f is natural-membered iff f is NAT -defined )
proof end;

registration
let f be INT -defined Relation;
coherence ;
end;

theorem :: FINSEQ_9:11
for f being Relation holds
( dom f is integer-membered iff f is INT -defined )
proof end;

registration
let f be RAT -defined Relation;
coherence ;
end;

theorem :: FINSEQ_9:12
for f being Relation holds
( dom f is rational-membered iff f is RAT -defined )
proof end;

registration
let f be REAL -defined Relation;
coherence ;
end;

theorem :: FINSEQ_9:13
for f being Relation holds
( dom f is real-membered iff f is REAL -defined )
proof end;

registration
let f be COMPLEX -defined Relation;
coherence ;
end;

theorem :: FINSEQ_9:14
for f being Relation holds
( dom f is complex-membered iff f is COMPLEX -defined )
proof end;

theorem N2103: :: FINSEQ_9:15
for D being set
for f being Function holds
( f is D -valued iff f is Function of (dom f),D )
proof end;

theorem T2103: :: FINSEQ_9:16
for C being set
for f being b1 -defined total Function holds f is Function of C,(rng f)
proof end;

theorem :: FINSEQ_9:17
for C, D being set
for f being b1 -defined total Function holds
( f is Function of C,D iff f is D -valued )
proof end;

theorem :: FINSEQ_9:18
for f being real-valued Function holds f is Function of (dom f),REAL
proof end;

theorem :: FINSEQ_9:19
for f being complex-valued FinSequence holds
( f - f = 0 (#) f & f - f = (len f) |-> 0 )
proof end;

theorem Lmkdf: :: FINSEQ_9:20
for a being Complex
for f being FinSequence
for k being Nat st k in dom f holds
((len f) |-> a) . k = a
proof end;

registration
let a be Real;
let k be non zero Nat;
let l be Nat;
let f be k + l -element FinSequence;
reduce ((len f) |-> a) . k to a;
reducibility
((len f) |-> a) . k = a
proof end;
end;

definition
let f be complex-valued Function;
func delneg f -> complex-valued Function equals :: FINSEQ_9:def 1
(1 / 2) (#) (f + (abs f));
correctness
coherence
(1 / 2) (#) (f + (abs f)) is complex-valued Function
;
;
func delpos f -> complex-valued Function equals :: FINSEQ_9:def 2
(1 / 2) (#) ((abs f) - f);
correctness
coherence
(1 / 2) (#) ((abs f) - f) is complex-valued Function
;
;
correctness
coherence ;
;
end;

:: deftheorem defines delneg FINSEQ_9:def 1 :
for f being complex-valued Function holds delneg f = (1 / 2) (#) (f + (abs f));

:: deftheorem defines delpos FINSEQ_9:def 2 :
for f being complex-valued Function holds delpos f = (1 / 2) (#) ((abs f) - f);

:: deftheorem defines delall FINSEQ_9:def 3 :
for f being complex-valued Function holds delall f = 0 (#) f;

theorem DMN: :: FINSEQ_9:21
for f being complex-valued Function holds
( dom f = dom () & dom f = dom () & dom f = dom () )
proof end;

theorem VAL: :: FINSEQ_9:22
for f being complex-valued Function
for x being object holds f . x = (() . x) - (() . x)
proof end;

theorem DNP: :: FINSEQ_9:23
for f being complex-valued Function holds f = () - ()
proof end;

theorem VOR: :: FINSEQ_9:24
for f being real-valued Function
for x being object holds
( f . x = () . x or f . x = - (() . x) )
proof end;

theorem ZOR: :: FINSEQ_9:25
for f being real-valued Function
for x being object holds
( () . x = 0 or () . x = 0 )
proof end;

registration
let f be real-valued Function;
cluster () (#) () -> empty-yielding ;
coherence
() (#) () is empty-yielding
proof end;
end;

theorem :: FINSEQ_9:26
for f being real-valued Function holds delall f = () (#) ()
proof end;

registration
let f be complex-valued Function;
let f1 be empty-yielding dom f -defined total Function;
reduce f + f1 to f;
reducibility
f + f1 = f
proof end;
reduce f - f1 to f;
reducibility
f - f1 = f
proof end;
end;

registration
let f be complex-valued Function;
let f1 be dom f -defined total complex-valued Function;
let f2 be empty-yielding dom f -defined total Function;
reduce f1 + f2 to f1;
reducibility
f1 + f2 = f1
proof end;
reduce f1 - f2 to f1;
reducibility
f1 - f2 = f1
proof end;
end;

registration
let f be complex-valued Function;
cluster f - f -> dom f -defined ;
coherence
f - f is dom f -defined
proof end;
cluster f - f -> total ;
coherence
f - f is total
proof end;
end;

theorem :: FINSEQ_9:27
for f being complex-valued Function holds abs f = () + ()
proof end;

registration
let f be empty FinSequence;
coherence by RVSUM_1:94;
cluster Product f -> non zero ;
coherence
not Product f is zero
by RVSUM_1:94;
end;

registration
let f be real-valued positive-yielding FinSequence;
coherence
proof end;
end;

registration
let f be complex-valued FinSequence;
coherence
proof end;
coherence
proof end;
end;

theorem DNF: :: FINSEQ_9:28
for f being complex-valued Function holds delneg f = delpos (- f)
proof end;

registration
let f be real-valued nonnegative-yielding Function;
reduce abs f to f;
reducibility
abs f = f
proof end;
reduce delneg f to f;
reducibility
delneg f = f
proof end;
identify delpos f with delall f;
correctness
compatibility ;
proof end;
identify delall f with delpos f;
correctness
compatibility ;
;
end;

registration
let f be real-valued nonpositive-yielding Function;
reduce - () to f;
reducibility
- () = f
proof end;
coherence
proof end;
identify delneg f with delall f;
correctness
compatibility ;
proof end;
identify delall f with delneg f;
correctness
compatibility ;
;
end;

theorem :: FINSEQ_9:29
for f being FinSequence of INT ex f1, f2 being FinSequence of NAT st f = f1 - f2
proof end;

registration
let a be Integer;
let n be Nat;
cluster n |-> a -> INT -valued ;
coherence
n |-> a is INT -valued
proof end;
end;

registration
let f be empty-yielding non empty FinSequence;
coherence
Product f is zero
proof end;
end;

theorem :: FINSEQ_9:30
for f1, f2 being FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f1 holds
( f1 . k >= f2 . k & f2 . k > 0 ) ) holds
Product f1 >= Product f2
proof end;

theorem :: FINSEQ_9:31
for a being Real
for f being FinSequence of REAL st ( for k being Element of NAT st k in dom f holds
( 0 < f . k & f . k <= a ) ) holds
Product f <= Product ((len f) |-> a)
proof end;

theorem :: FINSEQ_9:32
for a being non negative Real
for f being FinSequence of REAL st ( for k being Nat st k in dom f holds
f . k >= a ) holds
Product f >= a |^ (len f)
proof end;

theorem N454: :: FINSEQ_9:33
for f1, f2 being nonnegative-yielding FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
f1 . k >= f2 . k ) holds
Product f1 >= Product f2
proof end;

theorem :: FINSEQ_9:34
for f1, f2 being FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k >= 0 ) ) holds
Product f1 >= Product f2
proof end;

theorem :: FINSEQ_9:35
for a being positive Real
for f being nonnegative-yielding FinSequence of REAL st ( for k being Element of NAT st k in dom f holds
f . k <= a ) holds
Product f <= a |^ (len f)
proof end;

:: Basic operations on short finsequences
registration
let a be Complex;
reduce (- <*(- a)*>) . 1 to a;
reducibility
(- <*(- a)*>) . 1 = a
proof end;
reduce (<*(a ")*> ") . 1 to a;
reducibility
(<*(a ")*> ") . 1 = a
proof end;
end;

theorem APB: :: FINSEQ_9:36
for a, b being Complex holds <*a*> + <*b*> = <*(a + b)*>
proof end;

theorem :: FINSEQ_9:37
for a, b being Complex holds <*a*> - <*b*> = <*(a - b)*>
proof end;

theorem AMB: :: FINSEQ_9:38
for a, b being Complex holds <*a*> (#) <*b*> = <*(a * b)*>
proof end;

theorem :: FINSEQ_9:39
for a, b being Complex holds <*a*> /" <*b*> = <*(a * (b "))*>
proof end;

registration
let n be Nat;
let f be n -element FinSequence;
let a be Complex;
reduce (f ^ <*a*>) . (n + 1) to a;
reducibility
(f ^ <*a*>) . (n + 1) = a
proof end;
reduce (f ^ <*a*>) | n to f;
reducibility
(f ^ <*a*>) | n = f
proof end;
end;

registration
let a, b, c, d be Complex;
cluster <*a,b,c,d*> -> complex-valued ;
coherence
<*a,b,c,d*> is complex-valued
proof end;
end;

registration
let a, b be Complex;
reduce (- <*(- a),b*>) . 1 to a;
reducibility
(- <*(- a),b*>) . 1 = a
proof end;
reduce (- <*a,(- b)*>) . 2 to b;
reducibility
(- <*a,(- b)*>) . 2 = b
proof end;
reduce (<*(a "),b*> ") . 1 to a;
reducibility
(<*(a "),b*> ") . 1 = a
proof end;
reduce (<*a,(b ")*> ") . 2 to b;
reducibility
(<*a,(b ")*> ") . 2 = b
proof end;
end;

registration
let a, b, c be Complex;
reduce <*a,b,c*> . 1 to a;
reducibility
<*a,b,c*> . 1 = a
by FINSEQ_1:45;
reduce <*a,b,c*> . 2 to b;
reducibility
<*a,b,c*> . 2 = b
by FINSEQ_1:45;
reduce (- <*(- a),b,c*>) . 1 to a;
reducibility
(- <*(- a),b,c*>) . 1 = a
proof end;
reduce (- <*a,(- b),c*>) . 2 to b;
reducibility
(- <*a,(- b),c*>) . 2 = b
proof end;
reduce (- <*a,b,(- c)*>) . 3 to c;
reducibility
(- <*a,b,(- c)*>) . 3 = c
proof end;
reduce (<*(a "),b,c*> ") . 1 to a;
reducibility
(<*(a "),b,c*> ") . 1 = a
proof end;
reduce (<*a,(b "),c*> ") . 2 to b;
reducibility
(<*a,(b "),c*> ") . 2 = b
proof end;
reduce (<*a,b,(c ")*> ") . 3 to c;
reducibility
(<*a,b,(c ")*> ") . 3 = c
proof end;
end;

theorem FPA: :: FINSEQ_9:40
for a, b being Complex
for n being Nat
for f, g being b3 -element complex-valued FinSequence holds (f ^ <*a*>) + (g ^ <*b*>) = (f + g) ^ <*(a + b)*>
proof end;

theorem AP2: :: FINSEQ_9:41
for a, b, x, y being Complex holds <*a,b*> + <*x,y*> = <*(a + x),(b + y)*>
proof end;

theorem AP3: :: FINSEQ_9:42
for a, b, c, x, y, z being Complex holds <*a,b,c*> + <*x,y,z*> = <*(a + x),(b + y),(c + z)*>
proof end;

theorem :: FINSEQ_9:43
for a, b, c, d, x, y, z, v being Complex holds <*a,b,c,d*> + <*x,y,z,v*> = <*(a + x),(b + y),(c + z),(d + v)*>
proof end;

theorem FMA: :: FINSEQ_9:44
for a, b being Complex
for n being Nat
for f, g being b3 -element complex-valued FinSequence holds (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*>
proof end;

theorem AM2: :: FINSEQ_9:45
for a, b, x, y being Complex holds <*a,b*> (#) <*x,y*> = <*(a * x),(b * y)*>
proof end;

theorem AM3: :: FINSEQ_9:46
for a, b, c, x, y, z being Complex holds <*a,b,c*> (#) <*x,y,z*> = <*(a * x),(b * y),(c * z)*>
proof end;

theorem :: FINSEQ_9:47
for a, b, c, d, x, y, z, v being Complex holds <*a,b,c,d*> (#) <*x,y,z,v*> = <*(a * x),(b * y),(c * z),(d * v)*>
proof end;

theorem :: FINSEQ_9:48
for a being Complex
for n being non zero Nat
for f being b2 -element complex-valued FinSequence holds <*a*> + f = <*(a + (f . 1))*>
proof end;

theorem :: FINSEQ_9:49
for a, b being Complex
for n being non trivial Nat
for f being b3 -element complex-valued FinSequence holds <*a,b*> + f = <*(a + (f . 1)),(b + (f . 2))*>
proof end;

theorem :: FINSEQ_9:50
for a being Complex
for n being non zero Nat
for f being b2 -element complex-valued FinSequence holds <*a*> (#) f = <*(a * (f . 1))*>
proof end;

theorem :: FINSEQ_9:51
for a, b being Complex
for n being non trivial Nat
for f being b3 -element complex-valued FinSequence holds <*a,b*> (#) f = <*(a * (f . 1)),(b * (f . 2))*>
proof end;