:: Arithmetic Operations on Short Finite Sequences :: by Rafa{\l} Ziobro :: :: Received September 29, 2018 :: Copyright (c) 2018-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, INT_1, FINSEQ_1, ARYTM_3, XXREAL_0, FINSEQ_2, CARD_1, ARYTM_1, COMPLEX1, RELAT_1, FUNCT_1, CARD_3, TARSKI, REAL_1, XCMPLX_0, ORDINAL1, ORDINAL4, NEWTON, PARTFUN3, SUBSET_1, VALUED_0, FINSEQ_9, XBOOLE_0, MEMBERED, PARTFUN1, VALUED_1, FOMODEL0, ZFMISC_1; notations TARSKI, XBOOLE_0, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0, RVSUM_3, CARD_1, RELAT_1, FUNCT_1, INT_1, NEWTON, PARTFUN3, ABSVALUE, RVSUM_1, FINSEQ_1, FINSEQ_2, SUBSET_1, VALUED_0, FUNCT_2, FINSEQ_4, MEMBERED, PARTFUN1, VALUED_1, FOMODEL0, RELSET_1; constructors NEWTON, WSIERP_1, RELSET_1, RVSUM_3, FINSEQ_4, NEWTON04; registrations FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, NEWTON, XBOOLE_0, VALUED_0, FINSET_1, CARD_1, RVSUM_1, RVSUM_3, FINSEQ_2, PARTFUN3, FOMODEL0, MEMBERED, NEWTON02, FUNCT_2, NEWTON04, RELAT_1, ABSVALUE, NAT_2, EUCLID_9, VALUED_1, COMPLEX1, FINSEQ_4, FUNCOP_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: empty Relations are full of adjectives registration cluster empty -> positive-yielding for Relation; cluster empty -> negative-yielding for Relation; end; registration cluster natural-valued -> NAT-valued for Relation; end; registration let f be complex-valued Function, k be object; reduce (0(#)f).k to 0; end; registration let f be complex-valued Function; reduce 1(#)f to f; reduce (-1)(#)(-f) to f; cluster 0(#)f -> empty-yielding; cluster f - f -> empty-yielding; end; registration let D be set; cluster empty-yielding for D-valued FinSequence; end; registration cluster empty-yielding -> NAT-valued for FinSequence; cluster non empty for empty-yielding FinSequence; end; registration let n be Nat; cluster n-element for empty-yielding NAT-valued FinSequence; cluster min (n,0) -> zero; reduce max (n,0) to n; end; registration let a be non zero Nat; reduce min(a,1) to 1; reduce max(a,1) to a; end; registration let a be non trivial Nat; reduce min(a,2) to 2; reduce max(a,2) to a; end; registration let a be positive Real; let b be positive Nat; cluster b|->a -> positive; end; registration cluster empty-yielding -> Function-like for Relation; cluster empty-yielding -> natural-valued for Function; cluster empty-yielding -> nonpositive-yielding for real-valued Function; cluster empty-yielding -> nonnegative-yielding for real-valued Function; cluster empty-yielding -> non positive-yielding for non empty real-valued Function; cluster empty-yielding -> non negative-yielding for non empty real-valued Function; cluster positive-yielding -> non nonpositive-yielding for non empty real-valued Function; cluster negative-yielding -> non nonnegative-yielding for non empty real-valued Function; end; registration let f be empty-yielding Function, c be Complex; cluster c(#)f -> empty-yielding; end; registration let f be empty-yielding Function, g be complex-valued Function; cluster f(#)g -> empty-yielding; end; :: length of FinSequences registration let f be complex-valued FinSequence, x be Complex; cluster f + x -> (len f)-element; cluster f - x -> (len f)-element; end; registration let f be complex-valued FinSequence; cluster abs f -> (len f)-element; cluster -f -> (len f)-element; cluster f" -> (len f)-element; end; registration let n,m be Nat; let f be n-element complex-valued FinSequence, g be m-element complex-valued FinSequence; cluster f+g -> min(n,m)-element; cluster f(#)g -> min(n,m)-element; cluster f-g -> min(n,m)-element; cluster f /" g -> min(n,m)-element; end; registration let n,m be Nat, f be n-element complex-valued FinSequence, g be (n+m)-element empty-yielding complex-valued FinSequence; reduce f + g to f; end; registration let n be Nat, f be n-element complex-valued FinSequence, g be n-element empty-yielding complex-valued FinSequence; reduce f+g to f; end; registration let X be non empty set; cluster total for X-defined empty-yielding Function; end; registration let X be non empty set; let f be total X-defined complex-valued Function; let g be total X-defined empty-yielding Function; reduce f + g to f; end; registration let f be Relation; cluster (dom f)-defined for Relation; cluster f null f -> (dom f)-defined; cluster total for (dom f)-defined Relation; end; registration let f be complex-valued Function; cluster total for (dom f)-defined empty-yielding Function; cluster -f -> (dom f)-defined; cluster -f -> total; cluster f" -> (dom f)-defined; cluster f" -> total; cluster abs f -> (dom f)-defined; cluster abs f -> total; end; registration let f be complex-valued Function, c be Complex; cluster c + f -> (dom f)-defined; cluster c + f -> total; cluster f - c -> (dom f)-defined; cluster f - c -> total; cluster c(#)f -> (dom f)-defined; cluster c(#)f -> total; end; registration let f be FinSequence; cluster (len f)-element -> (dom f)-defined for FinSequence; end; registration let n be Nat; cluster n-element -> (Seg n)-defined for FinSequence; cluster total (Seg n)-defined -> n-element for FinSequence; end; theorem :: FINSEQ_9:1 for f be complex-valued FinSequence holds 0(#)f = (len f)|-> 0; registration let f be complex-valued FinSequence; reduce f + ((len f)|->0) to f; end; registration let n be Nat; let D be non empty set; let X be non empty Subset of D; cluster n-element for X-valued FinSequence; cluster n-element for FinSequence of X; end; registration let f be real-valued Function; cluster f + (abs f) -> nonnegative-yielding; cluster (abs f) - f -> nonnegative-yielding; end; registration let f be nonnegative-yielding real-valued Function, x be object; cluster f.x -> non negative; end; registration let f be nonpositive-yielding real-valued Function, x be object; cluster f.x -> non positive; end; registration let f be nonnegative-yielding real-valued Function, r be non negative Real; cluster r(#)f -> nonnegative-yielding; cluster (-r)(#)f -> nonpositive-yielding; end; registration let f be nonnegative-yielding real-valued Function; cluster -f -> nonpositive-yielding; end; registration let f be nonpositive-yielding real-valued Function, r be non negative Real; cluster r(#)f -> nonpositive-yielding; cluster (-r)(#)f -> nonnegative-yielding; end; registration let f be nonpositive-yielding real-valued Function; cluster -f -> nonnegative-yielding; end; registration cluster nonnegative-yielding -> natural-valued for INT-valued Function; end; registration let f be INT-valued Function; cluster (1/2)(#)(f+(abs f)) -> natural-valued; cluster (1/2)(#)((abs f)- f) -> natural-valued; end; :: Values are members of the range theorem :: FINSEQ_9:2 for f be Relation holds rng f is natural-membered iff f is natural-valued; theorem :: FINSEQ_9:3 for f be Relation holds f is NAT-valued iff rng f is natural-membered; theorem :: FINSEQ_9:4 for f be Relation holds rng f is integer-membered iff f is INT-valued; theorem :: FINSEQ_9:5 for f be Relation holds rng f is rational-membered iff f is RAT-valued; theorem :: FINSEQ_9:6 for f be Relation holds rng f is real-membered iff f is real-valued; theorem :: FINSEQ_9:7 for f be Relation holds f is REAL-valued iff rng f is real-membered; theorem :: FINSEQ_9:8 for f be Relation holds rng f is complex-membered iff f is complex-valued; theorem :: FINSEQ_9:9 for f be Relation holds f is COMPLEX-valued iff rng f is complex-membered; :: similarly: Relations are defined over members of their domain theorem :: FINSEQ_9:10 for f be Relation holds dom f is natural-membered iff f is NAT-defined; registration let f be INT-defined Relation; cluster dom f -> integer-membered; end; theorem :: FINSEQ_9:11 for f be Relation holds dom f is integer-membered iff f is INT-defined; registration let f be RAT-defined Relation; cluster dom f -> rational-membered; end; theorem :: FINSEQ_9:12 for f be Relation holds dom f is rational-membered iff f is RAT-defined; registration let f be REAL-defined Relation; cluster dom f -> real-membered; end; theorem :: FINSEQ_9:13 for f be Relation holds dom f is real-membered iff f is REAL-defined; registration let f be COMPLEX-defined Relation; cluster dom f -> complex-membered; end; theorem :: FINSEQ_9:14 for f be Relation holds dom f is complex-membered iff f is COMPLEX-defined; theorem :: FINSEQ_9:15 for D be set, f be Function holds f is D-valued iff f is Function of dom f,D; theorem :: FINSEQ_9:16 for C be set, f be total C-defined Function holds f is Function of C, rng f; theorem :: FINSEQ_9:17 for C,D be set, f be total C-defined Function holds f is Function of C,D iff f is D-valued; theorem :: FINSEQ_9:18 for f be real-valued Function holds f is Function of dom f,REAL; theorem :: FINSEQ_9:19 for f be complex-valued FinSequence holds f-f = 0(#)f & f-f = ((len f)|-> 0); theorem :: FINSEQ_9:20 for a be Complex, f be FinSequence, k be Nat st k in dom f holds ((len f) |-> a).k = a; registration let a be Real, k be non zero Nat, l be Nat, f be (k+l)-element FinSequence; reduce ((len f) |-> a).k to a; end; definition let f be complex-valued Function; func delneg f -> complex-valued Function equals :: FINSEQ_9:def 1 (1/2)(#)(f + (abs f)); func delpos f -> complex-valued Function equals :: FINSEQ_9:def 2 (1/2)(#)((abs f) - f); func delall f -> complex-valued Function equals :: FINSEQ_9:def 3 0(#)f; end; theorem :: FINSEQ_9:21 for f be complex-valued Function holds dom f = dom (delpos f) & dom f = dom (delneg f) & dom f = dom (delall f); theorem :: FINSEQ_9:22 for f be complex-valued Function, x be object holds f.x = (delneg f).x - (delpos f).x; theorem :: FINSEQ_9:23 for f be complex-valued Function holds f = delneg f - delpos f; theorem :: FINSEQ_9:24 for f be real-valued Function, x be object holds f.x = (delneg f).x or f.x = -(delpos f).x; theorem :: FINSEQ_9:25 for f be real-valued Function, x be object holds (delneg f).x = 0 or (delpos f).x = 0; registration let f be real-valued Function; cluster (delneg f)(#)(delpos f) -> empty-yielding; end; theorem :: FINSEQ_9:26 for f be real-valued Function holds delall f = (delneg f)(#)(delpos f); registration let f be complex-valued Function; let f1 be total (dom f)-defined empty-yielding Function; reduce f + f1 to f; reduce (f - f1) to f; end; registration let f be complex-valued Function; let f1 be total (dom f)-defined complex-valued Function; let f2 be total (dom f)-defined empty-yielding Function; reduce f1 + f2 to f1; reduce f1 - f2 to f1; end; registration let f be complex-valued Function; cluster f - f -> (dom f)-defined; cluster f - f -> total; end; theorem :: FINSEQ_9:27 for f be complex-valued Function holds abs f = delneg f + delpos f; registration let f be empty FinSequence; cluster Product f -> natural; cluster Product f -> non zero; end; registration let f be positive-yielding real-valued FinSequence; cluster Product f -> positive; end; registration let f be complex-valued FinSequence; cluster delneg f -> (len f)-element; cluster delpos f -> (len f)-element; end; theorem :: FINSEQ_9:28 for f be complex-valued Function holds delneg f = delpos (-f); registration let f be nonnegative-yielding real-valued Function; reduce (abs f) to f; reduce delneg f to f; identify delpos f with delall f; identify delall f with delpos f; end; registration let f be nonpositive-yielding real-valued Function; reduce - delpos f to f; cluster delneg f -> empty-yielding; identify delneg f with delall f; identify delall f with delneg f; end; theorem :: FINSEQ_9:29 for f be FinSequence of INT holds ex f1,f2 be FinSequence of NAT st f = f1 - f2; registration let a be Integer, n be Nat; cluster n|->a -> INT-valued; end; registration let f be non empty empty-yielding FinSequence; cluster Product f -> zero; 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; theorem :: FINSEQ_9:31 for a be Real for f be FinSequence of REAL st (for k be Element of NAT st k in dom f holds 0 < f.k <= a) holds Product f <= Product ((len f) |-> a); theorem :: FINSEQ_9:32 for a be non negative Real, f be FinSequence of REAL st (for k be Nat st k in dom f holds f.k >= a) holds Product (f) >= a|^(len f); theorem :: FINSEQ_9:33 for f1,f2 be nonnegative-yielding FinSequence of REAL st len f1 = len f2 & (for k be Element of NAT st k in dom f2 holds f1.k>=f2.k) holds Product f1 >= Product f2; theorem :: FINSEQ_9:34 ::NAT454: for f1,f2 being FinSequence of REAL st len f1 = len f2 & (for k be Element of NAT st k in dom f2 holds f1.k>=f2.k & f2.k>=0) holds Product f1 >= Product f2; theorem :: FINSEQ_9:35 for a be positive Real, f be nonnegative-yielding FinSequence of REAL st (for k be Element of NAT st k in dom f holds f.k <= a) holds Product (f) <= a|^(len f); :: Basic operations on short finsequences registration let a be Complex; reduce (-<*(-a)*>).1 to a; reduce (<*(a")*>").1 to a; end; theorem :: FINSEQ_9:36 for a,b be Complex holds <*a*>+<*b*> = <*(a+b)*>; theorem :: FINSEQ_9:37 for a,b be Complex holds <*a*>-<*b*> = <*(a-b)*>; theorem :: FINSEQ_9:38 for a,b be Complex holds <*a*>(#)<*b*> = <*(a*b)*>; theorem :: FINSEQ_9:39 for a,b be Complex holds <*a*>/"<*b*> = <*(a*b")*>; registration let n be Nat, f be n-element FinSequence, a be Complex; reduce (f^<*a*>).(n+1) to a; reduce (f^<*a*>)|n to f; end; registration let a,b,c,d be Complex; cluster <*a,b,c,d*> -> complex-valued; end; registration let a,b be Complex; reduce (-<*(-a),b*>).1 to a; reduce (-<*a,(-b)*>).2 to b; reduce (<*(a"),b*>").1 to a; reduce (<*a,(b")*>").2 to b; end; registration let a,b,c be Complex; reduce <*a,b,c*>.1 to a; reduce <*a,b,c*>.2 to b; reduce (-<*(-a),b,c*>).1 to a; reduce (-<*a,(-b),c*>).2 to b; reduce (-<*a,b,(-c)*>).3 to c; reduce (<*(a"),b,c*>").1 to a; reduce (<*a,(b"),c*>").2 to b; reduce (<*a,b,(c")*>").3 to c; end; theorem :: FINSEQ_9:40 for a,b be Complex, n be Nat, f,g be n-element complex-valued FinSequence holds (f^<*a*>)+(g^<*b*>) = (f+g)^<*a+b*>; theorem :: FINSEQ_9:41 for a,b,x,y be Complex holds <*a,b*>+<*x,y*> = <*a+x,b+y*>; theorem :: FINSEQ_9:42 for a,b,c,x,y,z be Complex holds <*a,b,c*>+<*x,y,z*> = <*a+x,b+y,c+z*>; theorem :: FINSEQ_9:43 for a,b,c,d,x,y,z,v be Complex holds <*a,b,c,d*>+<*x,y,z,v*> = <*a+x,b+y,c+z,d+v*>; theorem :: FINSEQ_9:44 for a,b be Complex, n be Nat, f,g be n-element complex-valued FinSequence holds (f^<*a*>)(#)(g^<*b*>) = (f(#)g)^<*a*b*>; theorem :: FINSEQ_9:45 for a,b,x,y be Complex holds <*a,b*>(#)<*x,y*> = <*a*x,b*y*>; theorem :: FINSEQ_9:46 for a,b,c,x,y,z be Complex holds <*a,b,c*>(#)<*x,y,z*> = <*a*x,b*y,c*z*>; theorem :: FINSEQ_9:47 for a,b,c,d,x,y,z,v be Complex holds <*a,b,c,d*>(#)<*x,y,z,v*> = <*a*x,b*y,c*z,d*v*>; theorem :: FINSEQ_9:48 for a be Complex, n be non zero Nat, f be n-element complex-valued FinSequence holds <*a*>+f = <*(a+f.1)*>; theorem :: FINSEQ_9:49 for a,b be Complex, n be non trivial Nat, f be n-element complex-valued FinSequence holds <*a,b*>+f = <*a+f.1,b+f.2*>; theorem :: FINSEQ_9:50 for a be Complex, n be non zero Nat, f be n-element complex-valued FinSequence holds <*a*>(#)f = <*a*f.1*>; theorem :: FINSEQ_9:51 for a,b be Complex, n be non trivial Nat, f be n-element complex-valued FinSequence holds <*a,b*>(#)f = <*a*f.1,b*f.2*>;