:: Ordered Rings - Part I
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received October 11, 1990
:: Copyright (c) 1990-2026 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 NAT_1, XBOOLE_0, ALGSTR_0, VECTSP_1, FINSEQ_1, ORDINAL4, RELAT_1,
ARYTM_3, PARTFUN1, XXREAL_0, CARD_1, FUNCT_1, SQUARE_1, O_RING_1;
notations ORDINAL1, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, PARTFUN1, NUMBERS,
STRUCT_0, ALGSTR_0, VECTSP_1, XXREAL_0;
constructors RLVECT_1, PARTFUN1, XXREAL_0, NAT_1, VECTSP_1, RELSET_1, GROUP_1;
registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, NAT_1;
requirements NUMERALS, SUBSET, ARITHM;
theorems NAT_1, FINSEQ_1, FINSEQ_3, XREAL_1, FINSEQ_4, XXREAL_0, PARTFUN1;
schemes NAT_1;
begin :: Field-like Algebras
reserve i,j,k,m,n for Nat;
reserve R for non empty doubleLoopStr;
reserve x,y for Scalar of R;
reserve f,g,h for FinSequence of R;
Lm1: h=f^g iff dom h = Seg(len f + len g) & (for k be Nat st k in dom f holds
h/.k=f/.k) & for k be Nat st k in dom g holds h/.(len f + k)=g/.k
proof
A1: len f >= 0 by NAT_1:2;
thus h=f^g implies dom h = Seg(len f + len g) & (for k be Nat st k in dom f
holds h/.k=f/.k) & for k be Nat st k in dom g holds h/.(len f + k)=g/.k
proof
assume
A2: h=f^g;
hence dom h = Seg(len f + len g) by FINSEQ_1:def 7;
then
A3: len h=len f+len g by FINSEQ_1:def 3;
thus for k be Nat st k in dom f holds h/.k=f/.k
proof
let k be Nat such that
A4: k in dom f;
len f<=len f+len g & k<=len f by A4,FINSEQ_3:25,NAT_1:11;
then
A5: k<=len h by A3,XXREAL_0:2;
1<=k by A4,FINSEQ_3:25;
then k in dom h by A5,FINSEQ_3:25;
then h/.k=h.k by PARTFUN1:def 6
.=f.k by A2,A4,FINSEQ_1:def 7
.=f/.k by A4,PARTFUN1:def 6;
hence thesis;
end;
thus for k be Nat st k in dom g holds h/.(len f + k)=g/.k
proof
let k be Nat;
assume
A6: k in dom g;
then k<=len g by FINSEQ_3:25;
then
A7: len f+k<=len f+len g by XREAL_1:7;
1<=k by A6,FINSEQ_3:25;
then 0+1<=len f+k by A1,XREAL_1:7;
then len f + k in dom h by A3,A7,FINSEQ_3:25;
then h/.(len f + k)=h.(len f+k) by PARTFUN1:def 6
.=g.k by A2,A6,FINSEQ_1:def 7
.=g/.k by A6,PARTFUN1:def 6;
hence thesis;
end;
end;
assume that
A8: dom h = Seg(len f + len g) and
A9: for k be Nat st k in dom f holds h/.k=f/.k and
A10: for k be Nat st k in dom g holds h/.(len f + k)=g/.k;
A11: len h=len f+len g by A8,FINSEQ_1:def 3;
A12: for k be Nat st k in dom g holds h.(len f + k)=g.k
proof
let k be Nat;
assume
A13: k in dom g;
then k<=len g by FINSEQ_3:25;
then
A14: len f+k<=len f+len g by XREAL_1:7;
1<=k by A13,FINSEQ_3:25;
then 0+1<=len f+k by A1,XREAL_1:7;
then len f + k in dom h by A11,A14,FINSEQ_3:25;
then h.(len f + k)=h/.(len f+k) by PARTFUN1:def 6
.=g/.k by A10,A13
.=g.k by A13,PARTFUN1:def 6;
hence thesis;
end;
for k be Nat st k in dom f holds h.k=f.k
proof
let k be Nat such that
A15: k in dom f;
len f<=len f+len g & k<=len f by A15,FINSEQ_3:25,NAT_1:11;
then
A16: k<=len h by A11,XXREAL_0:2;
1<=k by A15,FINSEQ_3:25;
then k in dom h by A16,FINSEQ_3:25;
then h.k=h/.k by PARTFUN1:def 6
.=f/.k by A9,A15
.=f.k by A15,PARTFUN1:def 6;
hence thesis;
end;
hence thesis by A8,A12,FINSEQ_1:def 7;
end;
Lm2: f=<*x*> iff len f=1 & f/.1=x
proof
thus f=<*x*> implies len f=1 & f/.1=x by FINSEQ_1:40,FINSEQ_4:16;
assume that
A1: len f=1 and
A2: f/.1=x;
1 in dom f by A1,FINSEQ_3:25;
then f.1=x by A2,PARTFUN1:def 6;
hence thesis by A1,FINSEQ_1:40;
end;
Lm3: (f^<*x*>)/.(len f + 1)=x
proof
A1: 1<=len f+1 by NAT_1:11;
len f+1=len f+len<*x*> by FINSEQ_1:39
.=len(f^<*x*>) by FINSEQ_1:22;
then len f+1 in dom(f^<*x*>) by A1,FINSEQ_3:25;
then (f^<*x*>)/.(len f+1)=(f^<*x*>).(len f+1) by PARTFUN1:def 6
.=x by FINSEQ_1:42;
hence thesis;
end;
Lm4: i<>0 & i<=len f implies (f^g)/.i=f/.i
proof
assume that
A1: i<>0 and
A2: i<=len f;
0<=i by NAT_1:2;
then 0<i by A1,XXREAL_0:1;
then 0+1<=i by NAT_1:13;
then i in dom f by A2,FINSEQ_3:25;
hence thesis by Lm1;
end;
Lm5: i<>0 & i<=len g implies (f^g)/.(len f+i)=g/.i
proof
assume that
A1: i<>0 and
A2: i<=len g;
0<=i by NAT_1:2;
then 0<i by A1,XXREAL_0:1;
then 0+1<=i by NAT_1:13;
then i in dom g by A2,FINSEQ_3:25;
hence thesis by Lm1;
end;
definition
let R be non empty doubleLoopStr, x be Scalar of R;
func x^2 -> Scalar of R equals
x*x;
coherence;
end;
definition
let R be non empty doubleLoopStr, x be Scalar of R;
attr x is being_a_square means
ex y being Scalar of R st x=y^2;
end;
definition
let R,f;
attr f is being_a_Sum_of_squares means
len f<>0 & f/.1 is
being_a_square & for n st n<>0 & n<len f ex y st y is being_a_square & f/.(n+1)
=f/.n+y;
end;
definition
let R be non empty doubleLoopStr, x be Scalar of R;
attr x is being_a_sum_of_squares means
ex f being FinSequence of R st f is being_a_Sum_of_squares & x=f/.len f;
end;
Lm6: x is being_a_square implies <*x*> is being_a_Sum_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_a_square & <*x*>/.(n+1)=
<*x*>/.n+y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_a_square;
then
A4: <*x*>/.1 is being_a_square by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm7: x is being_a_square implies x is being_a_sum_of_squares
proof
assume x is being_a_square;
then
A1: <*x*> is being_a_Sum_of_squares by Lm6;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
definition
let R,f;
attr f is being_a_Product_of_squares means
len f<>0 & f/.1 is
being_a_square & for n st n<>0 & n<len f ex y st y is being_a_square & f/.(n+1)
=f/.n*y;
end;
definition
let R,x;
attr x is being_a_product_of_squares means
ex f st f is being_a_Product_of_squares & x=f/.len f;
end;
Lm8: x is being_a_square implies <*x*> is being_a_Product_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_a_square & <*x*>/.(n+1)=
<*x*>/.n*y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_a_square;
then
A4: <*x*>/.1 is being_a_square by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm9: x is being_a_square implies x is being_a_product_of_squares
proof
assume x is being_a_square;
then
A1: <*x*> is being_a_Product_of_squares by Lm8;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
definition
let R,f;
attr f is being_a_Sum_of_products_of_squares means
len f<>0 & f/.1 is
being_a_product_of_squares & for n st n<>0 & n<len f ex y st y is
being_a_product_of_squares & f/.(n+1)=f/.n+y;
end;
definition
let R,x;
attr x is being_a_sum_of_products_of_squares means
ex f st f is being_a_Sum_of_products_of_squares & x=f/.len f;
end;
Lm10: x is being_a_square implies <*x*> is being_a_Sum_of_products_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_a_product_of_squares & <*
x*>/.(n+1)=<*x*>/.n+y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_a_square;
then x is being_a_product_of_squares by Lm9;
then
A4: <*x*>/.1 is being_a_product_of_squares by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm11: x is being_a_square implies x is being_a_sum_of_products_of_squares
proof
assume x is being_a_square;
then
A1: <*x*> is being_a_Sum_of_products_of_squares by Lm10;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
Lm12: x is being_a_product_of_squares implies <*x*> is
being_a_Sum_of_products_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_a_product_of_squares & <*
x*>/.(n+1)=<*x*>/.n+y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_a_product_of_squares;
then
A4: <*x*>/.1 is being_a_product_of_squares by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm13: x is being_a_product_of_squares implies x is
being_a_sum_of_products_of_squares
proof
assume x is being_a_product_of_squares;
then
A1: <*x*> is being_a_Sum_of_products_of_squares by Lm12;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
Lm14: f is being_a_Sum_of_squares implies f is
being_a_Sum_of_products_of_squares
proof
assume
A1: f is being_a_Sum_of_squares;
then f/.1 is being_a_square;
then
A2: f/.1 is being_a_product_of_squares by Lm9;
A3: for n st n<>0 & n<len f ex y st y is being_a_product_of_squares & f/.(n+
1)=f/.n+y
proof
let n;
assume n<>0 & n<len f;
then ex y st y is being_a_square & f/.(n+1)=f/.n+y by A1;
hence thesis by Lm9;
end;
len f<>0 by A1;
hence thesis by A2,A3;
end;
Lm15: x is being_a_sum_of_squares implies x is
being_a_sum_of_products_of_squares
by Lm14;
definition
let R,f;
attr f is being_an_Amalgam_of_squares means
len f<>0 & for n st n<>0
& n<=len f holds f/.n is being_a_product_of_squares or ex i,j st f/.n=f/.i*f/.j
& i<>0 & i<n & j<>0 & j<n;
end;
definition
let R,x;
attr x is being_an_amalgam_of_squares means
ex f st f is being_an_Amalgam_of_squares & x=f/.len f;
end;
Lm16: x is being_a_square implies <*x*> is being_an_Amalgam_of_squares
proof
assume x is being_a_square;
then x is being_a_product_of_squares by Lm9;
then
A1: <*x*>/.1 is being_a_product_of_squares by Lm2;
A2: for n st n<>0 & n<=len <*x*> holds <*x*>/.n is
being_a_product_of_squares or ex i,j st <*x*>/.n=<*x*>/.i*<*x*>/.j & i<>0 & i<n
& j<>0 & j<n
proof
let n;
assume that
A3: n<>0 and
A4: n<=len <*x*>;
n<=1 by A4,Lm2;
hence thesis by A1,A3,NAT_1:25;
end;
len<*x*>=1 by Lm2;
hence thesis by A2;
end;
Lm17: x is being_a_square implies x is being_an_amalgam_of_squares
proof
assume x is being_a_square;
then
A1: <*x*> is being_an_Amalgam_of_squares by Lm16;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
Lm18: x is being_a_product_of_squares implies <*x*> is
being_an_Amalgam_of_squares
proof
assume x is being_a_product_of_squares;
then
A1: <*x*>/.1 is being_a_product_of_squares by Lm2;
A2: for n st n<>0 & n<=len <*x*> holds <*x*>/.n is
being_a_product_of_squares or ex i,j st <*x*>/.n=<*x*>/.i*<*x*>/.j & i<>0 & i<n
& j<>0 & j<n
proof
let n;
assume that
A3: n<>0 and
A4: n<=len <*x*>;
n<=1 by A4,Lm2;
hence thesis by A1,A3,NAT_1:25;
end;
len<*x*>=1 by Lm2;
hence thesis by A2;
end;
Lm19: x is being_a_product_of_squares implies x is being_an_amalgam_of_squares
proof
assume x is being_a_product_of_squares;
then
A1: <*x*> is being_an_Amalgam_of_squares by Lm18;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
definition
let R,f;
attr f is being_a_Sum_of_amalgams_of_squares means
len f<>0 & f/.1
is being_an_amalgam_of_squares & for n st n<>0 & n<len f ex y st y is
being_an_amalgam_of_squares & f/.(n+1)=f/.n+y;
end;
definition
let R,x;
attr x is being_a_sum_of_amalgams_of_squares means
ex f st f is being_a_Sum_of_amalgams_of_squares & x=f/.len f;
end;
Lm20: x is being_a_square implies <*x*> is being_a_Sum_of_amalgams_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_an_amalgam_of_squares &
<*x*>/.(n+1)=<*x*>/.n+y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_a_square;
then x is being_an_amalgam_of_squares by Lm17;
then
A4: <*x*>/.1 is being_an_amalgam_of_squares by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm21: x is being_a_square implies x is being_a_sum_of_amalgams_of_squares
proof
assume x is being_a_square;
then
A1: <*x*> is being_a_Sum_of_amalgams_of_squares by Lm20;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
Lm22: f is being_a_Sum_of_squares implies f is
being_a_Sum_of_amalgams_of_squares
proof
assume
A1: f is being_a_Sum_of_squares;
then f/.1 is being_a_square;
then
A2: f/.1 is being_an_amalgam_of_squares by Lm17;
A3: for n st n<>0 & n<len f ex y st y is being_an_amalgam_of_squares & f/.(n
+1)=f/.n+y
proof
let n;
assume n<>0 & n<len f;
then ex y st y is being_a_square & f/.(n+1)=f/.n+y by A1;
hence thesis by Lm17;
end;
len f<>0 by A1;
hence thesis by A2,A3;
end;
Lm23: x is being_a_sum_of_squares implies x is
being_a_sum_of_amalgams_of_squares
by Lm22;
Lm24: x is being_a_product_of_squares implies <*x*> is
being_a_Sum_of_amalgams_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_an_amalgam_of_squares &
<*x*>/.(n+1)=<*x*>/.n+y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_a_product_of_squares;
then x is being_an_amalgam_of_squares by Lm19;
then
A4: <*x*>/.1 is being_an_amalgam_of_squares by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm25: x is being_a_product_of_squares implies x is
being_a_sum_of_amalgams_of_squares
proof
assume x is being_a_product_of_squares;
then
A1: <*x*> is being_a_Sum_of_amalgams_of_squares by Lm24;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
Lm26: f is being_a_Sum_of_products_of_squares implies f is
being_a_Sum_of_amalgams_of_squares
proof
assume
A1: f is being_a_Sum_of_products_of_squares;
then f/.1 is being_a_product_of_squares;
then
A2: f/.1 is being_an_amalgam_of_squares by Lm19;
A3: for n st n<>0 & n<len f ex y st y is being_an_amalgam_of_squares & f/.(n
+1)=f/.n+y
proof
let n;
assume n<>0 & n<len f;
then ex y st y is being_a_product_of_squares & f/.(n+1)=f/.n+y by A1;
hence thesis by Lm19;
end;
len f<>0 by A1;
hence thesis by A2,A3;
end;
Lm27: x is being_a_sum_of_products_of_squares implies x is
being_a_sum_of_amalgams_of_squares
by Lm26;
Lm28: x is being_an_amalgam_of_squares implies <*x*> is
being_a_Sum_of_amalgams_of_squares
proof
A1: for n st n<>0 & n<len <*x*> ex y st y is being_an_amalgam_of_squares &
<*x*>/.(n+1)=<*x*>/.n+y
proof
let n;
assume that
A2: n<>0 and
A3: n<len <*x*>;
n<1 by A3,Lm2;
hence thesis by A2,NAT_1:25;
end;
assume x is being_an_amalgam_of_squares;
then
A4: <*x*>/.1 is being_an_amalgam_of_squares by Lm2;
len<*x*>=1 by Lm2;
hence thesis by A4,A1;
end;
Lm29: x is being_an_amalgam_of_squares implies x is
being_a_sum_of_amalgams_of_squares
proof
assume x is being_an_amalgam_of_squares;
then
A1: <*x*> is being_a_Sum_of_amalgams_of_squares by Lm28;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
definition
let R,f;
attr f is being_a_generation_from_squares means
len f<>0 & for n st
n<>0 & n<=len f holds f/.n is being_an_amalgam_of_squares or ex i,j st (f/.n=f
/.i*f/.j or f/.n=f/.i+f/.j) & i<>0 & i<n & j<>0 & j<n;
end;
definition
let R,x;
attr x is generated_from_squares means
ex f st f is being_a_generation_from_squares & x=f/.len f;
end;
Lm30: x is being_a_square implies <*x*> is being_a_generation_from_squares
proof
assume x is being_a_square;
then x is being_an_amalgam_of_squares by Lm17;
then
A1: <*x*>/.1 is being_an_amalgam_of_squares by Lm2;
A2: for n st n<>0 & n<=len <*x*> holds <*x*>/.n is
being_an_amalgam_of_squares or ex i,j st (<*x*>/.n=<*x*>/.i*<*x*>/.j or <*x*>/.
n=<*x*>/.i+<*x*>/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n;
assume that
A3: n<>0 and
A4: n<=len <*x*>;
n<=1 by A4,Lm2;
hence thesis by A1,A3,NAT_1:25;
end;
len<*x*>=1 by Lm2;
hence thesis by A2;
end;
Lm31: x is being_a_square implies x is generated_from_squares
proof
assume x is being_a_square;
then
A1: <*x*> is being_a_generation_from_squares by Lm30;
len<*x*>=1 & <*x*>/.1=x by Lm2;
hence thesis by A1;
end;
Lm32: f is being_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f/.i+f/.j*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: i<>0 and
A3: i<=len f and
A4: j<>0 and
A5: j<=len f;
set g=f^<*f/.i+f/.j*>;
A6: len g=len f+len<*f/.i+f/.j*> by FINSEQ_1:22
.=len f+1 by Lm2;
A7: for n st n<>0 & n<=len g holds g/.n is being_an_amalgam_of_squares or
ex i,j st (g/.n=g/.i*g/.j or g/.n=g/.i+g/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A8: n<>0 and
A9: n<=len g;
A10: now
assume n<len g;
then
A11: n<=len f by A6,NAT_1:13;
then
A12: g/.n=f/.n by A8,Lm4;
A13: now
given k,m such that
A14: f/.n=f/.k*f/.m or f/.n=f/.k+f/.m and
A15: k<>0 & k<n & m<>0 & m<n;
f/.k=g/.k & f/.m=g/.m by A11,A15,Lm4,XXREAL_0:2;
hence thesis by A12,A14,A15;
end;
f/.n is being_an_amalgam_of_squares implies thesis by A8,A11,Lm4;
hence thesis by A1,A8,A11,A13;
end;
now
assume
A16: n=len g;
then
A17: i<n & j<n by A3,A5,A6,NAT_1:13;
g/.n=f/.i+f/.j by A6,A16,Lm3
.=g/.i+f/.j by A2,A3,Lm4
.=g/.i+g/.j by A4,A5,Lm4;
hence thesis by A2,A4,A17;
end;
hence thesis by A9,A10,XXREAL_0:1;
end;
len f<>0 by A1;
then len f+len<*f/.i+f/.j*><>0;
then len (f^<*f/.i+f/.j*>)<>0 by FINSEQ_1:22;
hence thesis by A7;
end;
Lm33: f is being_a_generation_from_squares & g is
being_a_generation_from_squares implies f^g is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: g is being_a_generation_from_squares;
A3: for n st n<>0 & n<=len (f^g) holds (f^g)/.n is
being_an_amalgam_of_squares or ex i,j st ((f^g)/.n=(f^g)/.i*(f^g)/.j or (f^g)/.
n=(f^g)/.i+(f^g)/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n;
assume that
A4: n<>0 and
A5: n<=len (f^g);
A6: n<=len f+len g by A5,FINSEQ_1:22;
A7: now
assume
A8: len f<n;
then consider m being Nat such that
A9: n=len f+m by NAT_1:10;
len f+m<=len f+len g by A5,A9,FINSEQ_1:22;
then
A10: m<=len g by XREAL_1:6;
A11: m<>0 by A8,A9;
A12: m<=len g by A6,A9,XREAL_1:6;
A13: now
given k,l be Nat such that
A14: g/.m=g/.k*g/.l or g/.m=g/.k+g/.l and
A15: k<>0 and
A16: k<m and
A17: l<>0 and
A18: l<m;
A19: len f+k<>0 & len f+l<>0 by A15,A17;
A20: (f^g)/.n=(f^g)/.(len f+k)*(f^g)/.(len f+l) or (f^g)/.n=(f^g)/.(
len f+k)+(f^g)/.(len f+l)
proof
A21: now
assume g/.m=g/.k+g/.l;
then (f^g)/.n=g/.k+g/.l by A9,A11,A10,Lm5
.=(f^g)/.(len f+k)+g/.l by A12,A15,A16,Lm5,XXREAL_0:2
.=(f^g)/.(len f+k)+(f^g)/.(len f+l) by A12,A17,A18,Lm5,XXREAL_0:2
;
hence thesis;
end;
now
assume g/.m=g/.k*g/.l;
then (f^g)/.n=g/.k*g/.l by A9,A11,A10,Lm5
.=(f^g)/.(len f+k)*g/.l by A12,A15,A16,Lm5,XXREAL_0:2
.=(f^g)/.(len f+k)*(f^g)/.(len f+l) by A12,A17,A18,Lm5,XXREAL_0:2
;
hence thesis;
end;
hence thesis by A14,A21;
end;
len f+k<n & len f+l<n by A9,A16,A18,XREAL_1:6;
hence thesis by A20,A19;
end;
g/.m is being_an_amalgam_of_squares implies thesis by A9,A11,A10,Lm5;
hence thesis by A2,A11,A10,A13;
end;
now
assume
A22: n<=len f;
then
A23: (f^g)/.n=f/.n by A4,Lm4;
A24: now
given k,l be Nat such that
A25: f/.n=f/.k*f/.l or f/.n=f/.k+f/.l and
A26: k<>0 & k<n & l<>0 & l<n;
(f^g)/.k=f/.k & (f^g)/.l=f/.l by A22,A26,Lm4,XXREAL_0:2;
hence thesis by A23,A25,A26;
end;
f/.n is being_an_amalgam_of_squares implies thesis by A4,A22,Lm4;
hence thesis by A1,A4,A22,A24;
end;
hence thesis by A7;
end;
len f<>0 by A1;
then len f+len g<>0;
then len(f^g)<>0 by FINSEQ_1:22;
hence thesis by A3;
end;
Lm34: f is being_a_generation_from_squares & x is being_a_square implies f^<*x
*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: x is being_a_square;
<*x*> is being_a_generation_from_squares by A2,Lm30;
hence thesis by A1,Lm33;
end;
Lm35: f is being_a_generation_from_squares & x is being_a_square implies (f^<*
x*>)^<*f/.len f+x*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: x is being_a_square;
A3: f^<*x*> is being_a_generation_from_squares by A1,A2,Lm34;
len<*x*>=1 by Lm2;
then
A4: len f+1=len(f^<*x*>) by FINSEQ_1:22;
A5: len f<=len f+1 & len f+1<>0 by NAT_1:11;
A6: (f^<*x*>)/.(len f+1)=x by Lm3;
A7: len f<>0 by A1;
then (f^<*x*>)/.len f=f/.len f by Lm4;
hence thesis by A3,A7,A5,A4,A6,Lm32;
end;
Lm36: x is generated_from_squares & y is being_a_square implies x+y is
generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_square;
consider f such that
A3: f is being_a_generation_from_squares & x=f/.len f by A1;
take g=(f^<*y*>)^<*f/.len f+y*>;
len g=len(f^<*y*>)+len<*f/.len f+y*> by FINSEQ_1:22
.=len(f^<*y*>)+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm35;
end;
Lm37: f is being_a_Sum_of_squares & 0<>i & i<=len f implies f/.i is
generated_from_squares
proof
assume that
A1: f is being_a_Sum_of_squares and
A2: 0<>i & i<=len f;
defpred P[Nat] means 0<>$1 & $1<=len f implies f/.$1 is
generated_from_squares;
A3: for i st P[i] holds P[i+1]
proof
let i such that
A4: 0<>i & i<=len f implies f/.i is generated_from_squares;
assume that
0<>(i+1) and
A5: (i+1)<=len f;
A6: i<len f by A5,NAT_1:13;
A7: now
assume
A8: i<>0;
then ex y st y is being_a_square & f/.(i+1)=f/.i+y by A1,A6;
hence thesis by A4,A5,A8,Lm36,NAT_1:13;
end;
i = 0 implies thesis by A1,Lm31;
hence thesis by A7;
end;
A9: P[0];
for i holds P[i] from NAT_1:sch 2(A9,A3);
hence thesis by A2;
end;
Lm38: x is being_a_sum_of_squares implies x is generated_from_squares
proof
assume x is being_a_sum_of_squares;
then consider f such that
A1: f is being_a_Sum_of_squares and
A2: x=f/.len f;
thus thesis by A1,A2,Lm37;
end;
Lm39: f is being_an_Amalgam_of_squares implies f is
being_a_generation_from_squares
proof
assume
A1: f is being_an_Amalgam_of_squares;
hence len f<>0;
let n such that
A2: n<>0 & n<=len f;
A3: ( ex i,j st f/.n=f/.i*f/.j & i<>0 & i<n & j<>0 & j<n) implies thesis;
f/.n is being_a_product_of_squares implies thesis by Lm19;
hence thesis by A1,A2,A3;
end;
Lm40: x is being_an_amalgam_of_squares implies x is generated_from_squares
by Lm39;
Lm41: x is being_an_amalgam_of_squares implies <*x*> is
being_a_generation_from_squares
proof
set g=<*x*>;
assume
A1: x is being_an_amalgam_of_squares;
A2: for n st n<>0 & n<=len g holds g/.n is being_an_amalgam_of_squares or ex
i,j st (g/.n=g/.i*g/.j or g/.n=g/.i+g/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A3: n<>0 and
A4: n<=len g;
n<=1 by A4,Lm2;
then n<1+1 by NAT_1:13;
then n=1 by A3,NAT_1:23;
hence thesis by A1,Lm2;
end;
len g=1 by Lm2;
hence thesis by A2;
end;
Lm42: f is being_a_generation_from_squares & x is being_an_amalgam_of_squares
implies (f^<*x*>)^<*f/.len f+x*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: x is being_an_amalgam_of_squares;
<*x*> is being_a_generation_from_squares by A2,Lm41;
then
A3: f^<*x*> is being_a_generation_from_squares by A1,Lm33;
len<*x*>=1 by Lm2;
then
A4: len f+1=len(f^<*x*>) by FINSEQ_1:22;
A5: len f<=len f+1 & len f+1<>0 by NAT_1:11;
A6: (f^<*x*>)/.(len f+1)=x by Lm3;
A7: len f<>0 by A1;
then (f^<*x*>)/.len f=f/.len f by Lm4;
hence thesis by A3,A7,A5,A4,A6,Lm32;
end;
Lm43: x is generated_from_squares & y is being_an_amalgam_of_squares implies x
+y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_an_amalgam_of_squares;
consider f such that
A3: f is being_a_generation_from_squares & x=f/.len f by A1;
take g=(f^<*y*>)^<*f/.len f+y*>;
len g=len(f^<*y*>)+len<*f/.len f+y*> by FINSEQ_1:22
.=len(f^<*y*>)+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm42;
end;
Lm44: f is being_a_Sum_of_amalgams_of_squares implies for i holds i<>0 & i<=
len f implies f/.i is generated_from_squares
proof
defpred P[Nat] means $1<>0 & $1<=len f implies f/.$1 is
generated_from_squares;
assume
A1: f is being_a_Sum_of_amalgams_of_squares;
A2: for i st P[i] holds P[i+1]
proof
let i such that
A3: i<>0 & i<=len f implies f/.i is generated_from_squares;
assume that
(i+1)<>0 and
A4: (i+1)<=len f;
A5: now
assume
A6: i<>0;
i<len f by A4,NAT_1:13;
then ex y st y is being_an_amalgam_of_squares & f/.(i+1)=f/.i+y by A1,A6;
hence thesis by A3,A4,A6,Lm43,NAT_1:13;
end;
i = 0 implies thesis by A1,Lm40;
hence thesis by A5;
end;
A7: P[0];
thus for i holds P[i] from NAT_1:sch 2(A7,A2);
end;
theorem Th1:
x is being_a_sum_of_amalgams_of_squares implies x is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares;
then consider f such that
A1: f is being_a_Sum_of_amalgams_of_squares and
A2: x=f/.len f;
thus thesis by A1,A2,Lm44;
end;
Lm45: f is being_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f/.i*f/.j*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: i<>0 and
A3: i<=len f and
A4: j<>0 and
A5: j<=len f;
set g=f^<*f/.i*f/.j*>;
A6: len g=len f+len<*f/.i*f/.j*> by FINSEQ_1:22
.=len f+1 by Lm2;
A7: for n st n<>0 & n<=len g holds g/.n is being_an_amalgam_of_squares or
ex i,j st (g/.n=g/.i*g/.j or g/.n=g/.i+g/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A8: n<>0 and
A9: n<=len g;
A10: now
assume n<len g;
then
A11: n<=len f by A6,NAT_1:13;
then
A12: g/.n=f/.n by A8,Lm4;
A13: now
given k,m such that
A14: f/.n=f/.k*f/.m or f/.n=f/.k+f/.m and
A15: k<>0 & k<n & m<>0 & m<n;
f/.k=g/.k & f/.m=g/.m by A11,A15,Lm4,XXREAL_0:2;
hence thesis by A12,A14,A15;
end;
f/.n is being_an_amalgam_of_squares implies thesis by A8,A11,Lm4;
hence thesis by A1,A8,A11,A13;
end;
now
assume
A16: n=len g;
then
A17: i<n & j<n by A3,A5,A6,NAT_1:13;
g/.n=f/.i*f/.j by A6,A16,Lm3
.=g/.i*f/.j by A2,A3,Lm4
.=g/.i*g/.j by A4,A5,Lm4;
hence thesis by A2,A4,A17;
end;
hence thesis by A9,A10,XXREAL_0:1;
end;
len f<>0 by A1;
then len f+len<*f/.i*f/.j*><>0;
then len (f^<*f/.i*f/.j*>)<>0 by FINSEQ_1:22;
hence thesis by A7;
end;
Lm46: f is being_a_generation_from_squares & x is being_a_square implies (f^<*
x*>)^<*f/.len f*x*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: x is being_a_square;
A3: f^<*x*> is being_a_generation_from_squares by A1,A2,Lm34;
len<*x*>=1 by Lm2;
then
A4: len f+1=len(f^<*x*>) by FINSEQ_1:22;
A5: len f<=len f+1 & len f+1<>0 by NAT_1:11;
A6: (f^<*x*>)/.(len f+1)=x by Lm3;
A7: len f<>0 by A1;
then (f^<*x*>)/.len f=f/.len f by Lm4;
hence thesis by A3,A7,A5,A4,A6,Lm45;
end;
Lm47: x is generated_from_squares & y is being_a_square implies x*y is
generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_square;
consider f such that
A3: f is being_a_generation_from_squares & x=f/.len f by A1;
take g=(f^<*y*>)^<*f/.len f*y*>;
len g=len(f^<*y*>)+len<*f/.len f*y*> by FINSEQ_1:22
.=len(f^<*y*>)+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm46;
end;
Lm48: f is being_a_Product_of_squares & 0<>i & i<=len f implies f/.i is
generated_from_squares
proof
assume that
A1: f is being_a_Product_of_squares and
A2: 0<>i & i<=len f;
defpred P[Nat] means 0<>$1 & $1<=len f implies f/.$1 is
generated_from_squares;
A3: for i st P[i] holds P[i+1]
proof
let i such that
A4: 0<>i & i<=len f implies f/.i is generated_from_squares;
assume that
0<>(i+1) and
A5: (i+1)<=len f;
A6: i<len f by A5,NAT_1:13;
A7: now
assume
A8: i<>0;
then ex y st y is being_a_square & f/.(i+1)=f/.i*y by A1,A6;
hence thesis by A4,A5,A8,Lm47,NAT_1:13;
end;
i = 0 implies thesis by A1,Lm31;
hence thesis by A7;
end;
A9: P[0];
for i holds P[i] from NAT_1:sch 2(A9,A3);
hence thesis by A2;
end;
Lm49: x is being_a_product_of_squares implies x is generated_from_squares
proof
assume x is being_a_product_of_squares;
then consider f such that
A1: f is being_a_Product_of_squares and
A2: x=f/.len f;
thus thesis by A1,A2,Lm48;
end;
Lm50: x is being_a_product_of_squares implies <*x*> is
being_a_generation_from_squares
proof
set g=<*x*>;
A1: len g=1 by Lm2;
assume
A2: x is being_a_product_of_squares;
for n st n<>0 & n<=len g holds g/.n is being_an_amalgam_of_squares or ex
i,j st (g/.n=g/.i*g/.j or g/.n=g/.i+g/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A3: n<>0 and
A4: n<=len g;
n<1+1 by A1,A4,NAT_1:13;
then n=1 by A3,NAT_1:23;
then g/.n=x by Lm2;
hence thesis by A2,Lm19;
end;
hence thesis by A1;
end;
Lm51: f is being_a_generation_from_squares & x is being_a_product_of_squares
implies (f^<*x*>)^<*f/.len f+x*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: x is being_a_product_of_squares;
<*x*> is being_a_generation_from_squares by A2,Lm50;
then
A3: f^<*x*> is being_a_generation_from_squares by A1,Lm33;
len<*x*>=1 by Lm2;
then
A4: len f+1=len(f^<*x*>) by FINSEQ_1:22;
A5: len f<=len f+1 & len f+1<>0 by NAT_1:11;
A6: (f^<*x*>)/.(len f+1)=x by Lm3;
A7: len f<>0 by A1;
then (f^<*x*>)/.len f=f/.len f by Lm4;
hence thesis by A3,A7,A5,A4,A6,Lm32;
end;
Lm52: x is generated_from_squares & y is being_a_product_of_squares implies x+
y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_product_of_squares;
consider f such that
A3: f is being_a_generation_from_squares & x=f/.len f by A1;
take g=(f^<*y*>)^<*f/.len f+y*>;
len g=len(f^<*y*>)+len<*f/.len f+y*> by FINSEQ_1:22
.=len(f^<*y*>)+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm51;
end;
Lm53: f is being_a_Sum_of_products_of_squares & 0<>i & i<=len f implies f/.i
is generated_from_squares
proof
assume that
A1: f is being_a_Sum_of_products_of_squares and
A2: 0<>i & i<=len f;
defpred P[Nat] means 0<>$1 & $1<=len f implies f/.$1 is
generated_from_squares;
A3: for i st P[i] holds P[i+1]
proof
let i such that
A4: 0<>i & i<=len f implies f/.i is generated_from_squares;
assume that
0<>(i+1) and
A5: (i+1)<=len f;
A6: i<len f by A5,NAT_1:13;
A7: now
assume
A8: i<>0;
then
ex y st y is being_a_product_of_squares & f/.(i+1)=f/.i+y by A1,A6;
hence thesis by A4,A5,A8,Lm52,NAT_1:13;
end;
i = 0 implies thesis by A1,Lm49;
hence thesis by A7;
end;
A9: P[0];
for i holds P[i] from NAT_1:sch 2(A9,A3);
hence thesis by A2;
end;
Lm54: x is being_a_sum_of_products_of_squares implies x is
generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares;
then consider f such that
A1: f is being_a_Sum_of_products_of_squares and
A2: x=f/.len f;
thus thesis by A1,A2,Lm53;
end;
theorem
x is being_a_square implies x is being_a_sum_of_squares & x is
being_a_product_of_squares & x is being_a_sum_of_products_of_squares & x is
being_an_amalgam_of_squares & x is being_a_sum_of_amalgams_of_squares & x is
generated_from_squares by Lm7,Lm9,Lm11,Lm17,Lm21,Lm31;
theorem
x is being_a_sum_of_squares implies x is
being_a_sum_of_products_of_squares & x is being_a_sum_of_amalgams_of_squares &
x is generated_from_squares by Lm15,Lm23,Lm38;
theorem
x is being_a_product_of_squares implies x is
being_a_sum_of_products_of_squares & x is being_an_amalgam_of_squares & x is
being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm13,Lm19
,Lm25,Lm49;
theorem
x is being_a_sum_of_products_of_squares implies x is
being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm27,Lm54;
theorem
x is being_an_amalgam_of_squares implies x is
being_a_sum_of_amalgams_of_squares & x is generated_from_squares by Lm29,Lm40;
begin :: O_RING_2
Lm55: f is being_a_Sum_of_squares & x is being_a_square implies f^<*f/.len f+x
*> is being_a_Sum_of_squares
proof
assume that
A1: f is being_a_Sum_of_squares and
A2: x is being_a_square;
set g=f^<*f/.len f+x*>;
A3: len g=len f+len <*f/.len f+x*> by FINSEQ_1:22
.=len f+1 by Lm2;
A4: for n st n<>0 & n<len g holds f/.n=g/.n
proof
let n;
assume n<>0 & n<len g;
then 1<=n & n<=len f by A3,NAT_1:13,25;
then n in dom f by FINSEQ_3:25;
hence thesis by Lm1;
end;
A5: for n st n<>0 & n<len g ex y st y is being_a_square & g/.(n+1)=g/.n+y
proof
let n;
assume that
A6: n<>0 and
A7: n<len g;
A8: now
A9: f/.n=g/.n by A4,A6,A7;
assume
A10: n<len f;
then n+1<>0 & n+1<len g by A3,XREAL_1:6;
then f/.(n+1)=g/.(n+1) by A4;
hence thesis by A1,A6,A10,A9;
end;
A11: now
assume
A12: n=len f;
1<=n by A6,NAT_1:25;
then
A13: n in dom f by A12,FINSEQ_3:25;
g/.(n+1)=f/.n+x by A12,Lm3;
then g/.(n+1)=g/.n+x by A13,Lm1;
hence thesis by A2;
end;
n<=len f by A3,A7,NAT_1:13;
hence thesis by A8,A11,XXREAL_0:1;
end;
len f<>0 by A1;
then 1<=len f by NAT_1:25;
then 1<len g by A3,NAT_1:13;
then g/.1=f/.1 by A4;
then
A14: g/.1 is being_a_square by A1;
len g<>0 by A3;
hence thesis by A14,A5;
end;
Lm56: x is being_a_sum_of_squares & y is being_a_square implies x+y is
being_a_sum_of_squares
proof
assume that
A1: x is being_a_sum_of_squares and
A2: y is being_a_square;
consider f such that
A3: f is being_a_Sum_of_squares & x=f/.len f by A1;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm55;
end;
Lm57: f is being_a_Sum_of_products_of_squares & x is
being_a_product_of_squares implies f^<*f/.len f+x*> is
being_a_Sum_of_products_of_squares
proof
assume that
A1: f is being_a_Sum_of_products_of_squares and
A2: x is being_a_product_of_squares;
set g=f^<*f/.len f+x*>;
A3: len g=len f+len <*f/.len f+x*> by FINSEQ_1:22
.=len f+1 by Lm2;
A4: for n st n<>0 & n<len g holds f/.n=g/.n
proof
let n;
assume n<>0 & n<len g;
then 1<=n & n<=len f by A3,NAT_1:13,25;
then n in dom f by FINSEQ_3:25;
hence thesis by Lm1;
end;
A5: for n st n<>0 & n<len g ex y st y is being_a_product_of_squares & g/.(n
+1)=g/.n+y
proof
let n;
assume that
A6: n<>0 and
A7: n<len g;
A8: now
A9: f/.n=g/.n by A4,A6,A7;
assume
A10: n<len f;
then n+1<>0 & n+1<len g by A3,XREAL_1:6;
then f/.(n+1)=g/.(n+1) by A4;
hence thesis by A1,A6,A10,A9;
end;
A11: now
assume
A12: n=len f;
1<=n by A6,NAT_1:25;
then
A13: n in dom f by A12,FINSEQ_3:25;
g/.(n+1)=f/.n+x by A12,Lm3;
then g/.(n+1)=g/.n+x by A13,Lm1;
hence thesis by A2;
end;
n<=len f by A3,A7,NAT_1:13;
hence thesis by A8,A11,XXREAL_0:1;
end;
len f<>0 by A1;
then 1<=len f by NAT_1:25;
then 1<len g by A3,NAT_1:13;
then g/.1=f/.1 by A4;
then
A14: g/.1 is being_a_product_of_squares by A1;
len g<>0 by A3;
hence thesis by A14,A5;
end;
Lm58: x is being_a_sum_of_products_of_squares & y is
being_a_product_of_squares implies x+y is being_a_sum_of_products_of_squares
proof
assume that
A1: x is being_a_sum_of_products_of_squares and
A2: y is being_a_product_of_squares;
consider f such that
A3: f is being_a_Sum_of_products_of_squares & x=f/.len f by A1;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm57;
end;
Lm59: f is being_a_Sum_of_amalgams_of_squares & x is
being_an_amalgam_of_squares implies f^<*f/.len f+x*> is
being_a_Sum_of_amalgams_of_squares
proof
assume that
A1: f is being_a_Sum_of_amalgams_of_squares and
A2: x is being_an_amalgam_of_squares;
set g=f^<*f/.len f+x*>;
A3: len g=len f+len <*f/.len f+x*> by FINSEQ_1:22
.=len f+1 by Lm2;
A4: for n st n<>0 & n<len g holds f/.n=g/.n
proof
let n;
assume n<>0 & n<len g;
then 1<=n & n<=len f by A3,NAT_1:13,25;
then n in dom f by FINSEQ_3:25;
hence thesis by Lm1;
end;
A5: for n st n<>0 & n<len g ex y st y is being_an_amalgam_of_squares & g/.(
n+1)=g/.n+y
proof
let n;
assume that
A6: n<>0 and
A7: n<len g;
A8: now
A9: f/.n=g/.n by A4,A6,A7;
assume
A10: n<len f;
then n+1<>0 & n+1<len g by A3,XREAL_1:6;
then f/.(n+1)=g/.(n+1) by A4;
hence thesis by A1,A6,A10,A9;
end;
A11: now
assume
A12: n=len f;
1<=n by A6,NAT_1:25;
then
A13: n in dom f by A12,FINSEQ_3:25;
g/.(n+1)=f/.n+x by A12,Lm3;
then g/.(n+1)=g/.n+x by A13,Lm1;
hence thesis by A2;
end;
n<=len f by A3,A7,NAT_1:13;
hence thesis by A8,A11,XXREAL_0:1;
end;
len f<>0 by A1;
then 1<=len f by NAT_1:25;
then 1<len g by A3,NAT_1:13;
then g/.1=f/.1 by A4;
then
A14: g/.1 is being_an_amalgam_of_squares by A1;
len g<>0 by A3;
hence thesis by A14,A5;
end;
Lm60: x is being_a_sum_of_amalgams_of_squares & y is
being_an_amalgam_of_squares implies x+y is being_a_sum_of_amalgams_of_squares
proof
assume that
A1: x is being_a_sum_of_amalgams_of_squares and
A2: y is being_an_amalgam_of_squares;
consider f such that
A3: f is being_a_Sum_of_amalgams_of_squares & x=f/.len f by A1;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm59;
end;
Lm61: f is being_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f/.i+f/.j*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: i<>0 and
A3: i<=len f and
A4: j<>0 and
A5: j<=len f;
set g=f^<*f/.i+f/.j*>;
A6: len g=len f+len<*f/.i+f/.j*> by FINSEQ_1:22
.=len f+1 by Lm2;
A7: for n st n<>0 & n<=len g holds g/.n is being_an_amalgam_of_squares or
ex i,j st (g/.n=g/.i*g/.j or g/.n=g/.i+g/.j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A8: n<>0 and
A9: n<=len g;
A10: now
assume n<len g;
then
A11: n<=len f by A6,NAT_1:13;
then
A12: g/.n=f/.n by A8,Lm4;
A13: now
given k,m such that
A14: f/.n=f/.k*f/.m or f/.n=f/.k+f/.m and
A15: k<>0 & k<n & m<>0 & m<n;
f/.k=g/.k & f/.m=g/.m by A11,A15,Lm4,XXREAL_0:2;
hence thesis by A12,A14,A15;
end;
f/.n is being_an_amalgam_of_squares implies thesis by A8,A11,Lm4;
hence thesis by A1,A8,A11,A13;
end;
now
assume
A16: n=len g;
then
A17: i<n & j<n by A3,A5,A6,NAT_1:13;
g/.n=f/.i+f/.j by A6,A16,Lm3
.=g/.i+f/.j by A2,A3,Lm4
.=g/.i+g/.j by A4,A5,Lm4;
hence thesis by A2,A4,A17;
end;
hence thesis by A9,A10,XXREAL_0:1;
end;
len f<>0 by A1;
then len f+len<*f/.i+f/.j*><>0;
then len (f^<*f/.i+f/.j*>)<>0 by FINSEQ_1:22;
hence thesis by A7;
end;
Lm62: x is being_a_square & y is being_a_square implies x+y is
being_a_sum_of_squares
proof
assume
A1: x is being_a_square & y is being_a_square;
take g=<*x*>^<*x+y*>;
len<*x*>=1 by Lm2;
then
A2: <*x*>/.len<*x*>=x by Lm2;
len g=len <*x*>+len <*x+y*> by FINSEQ_1:22
.=len <*x*>+1 by Lm2;
hence thesis by A1,A2,Lm3,Lm6,Lm55;
end;
Lm63: f is being_a_generation_from_squares & g is
being_a_generation_from_squares implies (f^g)^<*f/.len f+g/.len g*> is
being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: g is being_a_generation_from_squares;
A3: len g<>0 by A2;
len f<>0 by A1;
then 1<=len f by NAT_1:25;
then len f in dom f by FINSEQ_3:25;
then
A4: len f+len g<=len(f^g) & (f^g)/.len f=f/.len f by Lm1,FINSEQ_1:22;
len f<=len f+len g by NAT_1:11;
then
A5: len f<=len(f^g) by FINSEQ_1:22;
1<=len g by A3,NAT_1:25;
then len g in dom g by FINSEQ_3:25;
then
A6: (f^g)/.(len f+len g)=g/.len g by Lm1;
(f^g) is being_a_generation_from_squares & len f<>0 by A1,A2,Lm33;
hence thesis by A5,A4,A6,Lm61;
end;
Lm64: x is generated_from_squares & y is generated_from_squares implies x+y is
generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is generated_from_squares;
consider f such that
A3: f is being_a_generation_from_squares and
A4: x=f/.len f by A1;
consider g such that
A5: g is being_a_generation_from_squares and
A6: y=g/.len g by A2;
set h=(f^g)^<*f/.len f+g/.len g*>;
len h=len(f^g)+len<*f/.len f+g/.len g*> by FINSEQ_1:22
.=len(f^g)+1 by Lm2;
then
A7: h/.len h=x+g/.len g by A4,Lm3;
h is being_a_generation_from_squares by A3,A5,Lm63;
hence thesis by A6,A7;
end;
theorem
x is being_a_square & y is being_a_square or x is
being_a_sum_of_squares & y is being_a_square implies x+y is
being_a_sum_of_squares by Lm56,Lm62;
Lm65: x is being_a_sum_of_products_of_squares & y is being_a_square implies x+
y is being_a_sum_of_products_of_squares
proof
assume that
A1: x is being_a_sum_of_products_of_squares and
A2: y is being_a_square;
consider f such that
A3: f is being_a_Sum_of_products_of_squares & x=f/.len f by A1;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm9,Lm57;
end;
theorem
x is being_a_sum_of_products_of_squares & y is being_a_square or x is
being_a_sum_of_products_of_squares & y is being_a_product_of_squares implies x+
y is being_a_sum_of_products_of_squares by Lm58,Lm65;
Lm66: x is being_an_amalgam_of_squares & y is being_a_product_of_squares
implies x+y is being_a_sum_of_amalgams_of_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is being_a_product_of_squares;
x is being_a_sum_of_amalgams_of_squares by A1,Lm29;
then consider f such that
A3: f is being_a_Sum_of_amalgams_of_squares & x=f/.len f;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm19,Lm59;
end;
Lm67: x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares
implies x+y is being_a_sum_of_amalgams_of_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is being_an_amalgam_of_squares;
x is being_a_sum_of_amalgams_of_squares by A1,Lm29;
then consider f such that
A3: f is being_a_Sum_of_amalgams_of_squares & x=f/.len f;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm59;
end;
Lm68: x is being_a_sum_of_amalgams_of_squares & y is
being_a_product_of_squares implies x+y is being_a_sum_of_amalgams_of_squares
proof
assume that
A1: x is being_a_sum_of_amalgams_of_squares and
A2: y is being_a_product_of_squares;
consider f such that
A3: f is being_a_Sum_of_amalgams_of_squares & x=f/.len f by A1;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm19,Lm59;
end;
Lm69: x is being_a_sum_of_amalgams_of_squares & y is being_a_square implies x+
y is being_a_sum_of_amalgams_of_squares
proof
assume that
A1: x is being_a_sum_of_amalgams_of_squares and
A2: y is being_a_square;
consider f such that
A3: f is being_a_Sum_of_amalgams_of_squares & x=f/.len f by A1;
take g=f^<*x+y*>;
len g=len f+len <*x+y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm17,Lm59;
end;
theorem
x is being_an_amalgam_of_squares & (y is being_a_product_of_squares or
y is being_an_amalgam_of_squares) or x is being_a_sum_of_amalgams_of_squares &
(y is being_a_square or y is being_a_product_of_squares or y is
being_an_amalgam_of_squares) implies x+y is being_a_sum_of_amalgams_of_squares
by Lm60,Lm66,Lm67,Lm68,Lm69;
Lm70: x is being_a_square & y is being_a_sum_of_squares implies x+y is
generated_from_squares
proof
assume x is being_a_square & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm38;
hence thesis by Lm64;
end;
Lm71: x is being_a_square & y is being_a_product_of_squares implies x+y is
generated_from_squares
proof
assume x is being_a_square & y is being_a_product_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm49;
hence thesis by Lm64;
end;
Lm72: x is being_a_square & y is generated_from_squares implies x+y is
generated_from_squares
proof
assume that
A1: x is being_a_square and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm31;
hence thesis by A2,Lm64;
end;
Lm73: x is being_a_square & y is being_a_sum_of_products_of_squares implies x+
y is generated_from_squares
proof
assume x is being_a_square & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm54;
hence thesis by Lm64;
end;
Lm74: x is being_a_square & y is being_an_amalgam_of_squares implies x+y is
generated_from_squares by Lm40,Lm72;
Lm75: x is being_a_square & y is being_a_sum_of_amalgams_of_squares implies x+
y is generated_from_squares by Lm72,Th1;
theorem
x is being_a_square & (y is being_a_sum_of_squares or y is
being_a_product_of_squares or y is being_a_sum_of_products_of_squares or y is
being_an_amalgam_of_squares or y is being_a_sum_of_amalgams_of_squares or y is
generated_from_squares) implies x+y is generated_from_squares by Lm70,Lm71,Lm72
,Lm73,Lm74,Lm75;
theorem
x is being_a_sum_of_squares & y is being_a_sum_of_squares implies x+y
is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_squares & y is being_a_product_of_squares implies
x+y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_product_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm49;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares
implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm54;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_squares & y is being_an_amalgam_of_squares implies
x+y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_an_amalgam_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm40;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares
implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Th1;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_squares & y is generated_from_squares implies x+y
is generated_from_squares
proof
assume that
A1: x is being_a_sum_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm38;
hence thesis by A2,Lm64;
end;
theorem
x is being_a_product_of_squares & y is generated_from_squares implies
x+y is generated_from_squares
proof
assume that
A1: x is being_a_product_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm49;
hence thesis by A2,Lm64;
end;
theorem
x is being_a_product_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x+y is generated_from_squares
proof
assume
x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49,Th1;
hence thesis by Lm64;
end;
theorem
x is being_a_product_of_squares & y is being_an_amalgam_of_squares
implies x+y is generated_from_squares
proof
assume x is being_a_product_of_squares & y is being_an_amalgam_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Lm49;
hence thesis by Lm64;
end;
theorem
x is being_a_product_of_squares & y is
being_a_sum_of_products_of_squares implies x+y is generated_from_squares
proof
assume
x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49,Lm54;
hence thesis by Lm64;
end;
theorem
x is being_a_product_of_squares & y is being_a_product_of_squares
implies x+y is generated_from_squares
proof
assume x is being_a_product_of_squares & y is being_a_product_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49;
hence thesis by Lm64;
end;
theorem
x is being_a_product_of_squares & y is being_a_sum_of_squares implies
x+y is generated_from_squares
proof
assume x is being_a_product_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm49;
hence thesis by Lm64;
end;
theorem
x is being_a_product_of_squares & y is being_a_square implies x+y is
generated_from_squares
proof
assume x is being_a_product_of_squares & y is being_a_square;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm49;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_products_of_squares & y is generated_from_squares
implies x+y is generated_from_squares
proof
assume that
A1: x is being_a_sum_of_products_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm54;
hence thesis by A2,Lm64;
end;
theorem
x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares
implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm54;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_products_of_squares implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm54;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_an_amalgam_of_squares implies x+y is generated_from_squares
proof
assume
x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Lm54;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm54,Th1;
hence thesis by Lm64;
end;
theorem
x is being_an_amalgam_of_squares & y is generated_from_squares implies
x+y is generated_from_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm40;
hence thesis by A2,Lm64;
end;
theorem
x is being_an_amalgam_of_squares & y is being_a_square implies x+y is
generated_from_squares
proof
assume x is being_an_amalgam_of_squares & y is being_a_square;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm40;
hence thesis by Lm64;
end;
theorem
x is being_an_amalgam_of_squares & y is being_a_sum_of_squares implies
x+y is generated_from_squares
proof
assume x is being_an_amalgam_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm40;
hence thesis by Lm64;
end;
theorem
x is being_an_amalgam_of_squares & y is
being_a_sum_of_products_of_squares implies x+y is generated_from_squares
proof
assume
x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Lm54;
hence thesis by Lm64;
end;
theorem
x is being_an_amalgam_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x+y is generated_from_squares
proof
assume
x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Th1;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares
implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Th1;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_products_of_squares implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm54,Th1;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x+y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Th1;
hence thesis by Lm64;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is generated_from_squares
implies x+y is generated_from_squares
proof
assume that
A1: x is being_a_sum_of_amalgams_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Th1;
hence thesis by A2,Lm64;
end;
Lm76: x is generated_from_squares & y is being_a_sum_of_squares implies x+y is
generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_sum_of_squares;
y is generated_from_squares by A2,Lm38;
hence thesis by A1,Lm64;
end;
Lm77: x is generated_from_squares & y is being_a_product_of_squares implies x+
y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_product_of_squares;
y is generated_from_squares by A2,Lm49;
hence thesis by A1,Lm64;
end;
Lm78: x is generated_from_squares & y is being_a_sum_of_products_of_squares
implies x+y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_sum_of_products_of_squares;
y is generated_from_squares by A2,Lm54;
hence thesis by A1,Lm64;
end;
Lm79: x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares
implies x+y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_sum_of_amalgams_of_squares;
y is generated_from_squares by A2,Th1;
hence thesis by A1,Lm64;
end;
theorem
x is generated_from_squares & y is being_a_square or x is
generated_from_squares & y is being_a_sum_of_squares or x is
generated_from_squares & y is being_a_product_of_squares or x is
generated_from_squares & y is being_a_sum_of_products_of_squares or x is
generated_from_squares & y is being_an_amalgam_of_squares or x is
generated_from_squares & y is being_a_sum_of_amalgams_of_squares or x is
generated_from_squares & y is generated_from_squares implies x+y is
generated_from_squares by Lm36,Lm43,Lm64,Lm76,Lm77,Lm78,Lm79;
begin :: O_RING_3
Lm80: f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares
implies f^g is being_an_Amalgam_of_squares
proof
assume that
A1: f is being_an_Amalgam_of_squares and
A2: g is being_an_Amalgam_of_squares;
A3: for n st n<>0 & n<=len (f^g) holds (f^g)/.n is
being_a_product_of_squares or ex i,j st (f^g)/.n=(f^g)/.i*(f^g)/.j & i<>0 & i<n
& j<>0 & j<n
proof
let n;
assume that
A4: n<>0 and
A5: n<=len (f^g);
A6: n<=len f+len g by A5,FINSEQ_1:22;
A7: now
assume
A8: len f<n;
then consider m be Nat such that
A9: n=len f+m by NAT_1:10;
len f+m<=len f+len g by A5,A9,FINSEQ_1:22;
then
A10: m<=len g by XREAL_1:6;
A11: m<>0 by A8,A9;
A12: m<=len g by A6,A9,XREAL_1:6;
A13: now
given k,l be Nat such that
A14: g/.m=g/.k*g/.l and
A15: k<>0 and
A16: k<m and
A17: l<>0 and
A18: l<m;
A19: len f+k<>0 & len f+l<>0 by A15,A17;
A20: len f+k<n & len f+l<n by A9,A16,A18,XREAL_1:6;
(f^g)/.n=g/.k*g/.l by A9,A11,A10,A14,Lm5
.=(f^g)/.(len f+k)*g/.l by A12,A15,A16,Lm5,XXREAL_0:2
.=(f^g)/.(len f+k)*(f^g)/.(len f+l) by A12,A17,A18,Lm5,XXREAL_0:2;
hence thesis by A19,A20;
end;
g/.m is being_a_product_of_squares implies thesis by A9,A11,A10,Lm5;
hence thesis by A2,A11,A10,A13;
end;
now
assume
A21: n<=len f;
A22: now
given k,l be Nat such that
A23: f/.n=f/.k*f/.l and
A24: k<>0 & k<n and
A25: l<>0 & l<n;
(f^g)/.n=f/.k*f/.l by A4,A21,A23,Lm4
.=(f^g)/.k*f/.l by A21,A24,Lm4,XXREAL_0:2
.=(f^g)/.k*(f^g)/.l by A21,A25,Lm4,XXREAL_0:2;
hence thesis by A24,A25;
end;
f/.n is being_a_product_of_squares implies thesis by A4,A21,Lm4;
hence thesis by A1,A4,A21,A22;
end;
hence thesis by A7;
end;
len f<>0 by A1;
then len f+len g<>0;
then len(f^g)<>0 by FINSEQ_1:22;
hence thesis by A3;
end;
Lm81: f is being_an_Amalgam_of_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f/.i*f/.j*> is being_an_Amalgam_of_squares
proof
assume that
A1: f is being_an_Amalgam_of_squares and
A2: i<>0 and
A3: i<=len f and
A4: j<>0 and
A5: j<=len f;
set g=f^<*f/.i*f/.j*>;
A6: len g=len f+len<*f/.i*f/.j*> by FINSEQ_1:22
.=len f+1 by Lm2;
A7: for n st n<>0 & n<=len g holds g/.n is being_a_product_of_squares or ex
i,j st g/.n=g/.i*g/.j & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A8: n<>0 and
A9: n<=len g;
A10: now
assume n<len g;
then
A11: n<=len f by A6,NAT_1:13;
A12: now
given k,m be Nat such that
A13: f/.n=f/.k*f/.m and
A14: k<>0 & k<n and
A15: m<>0 & m<n;
g/.n=f/.k*f/.m by A8,A11,A13,Lm4
.=g/.k*f/.m by A11,A14,Lm4,XXREAL_0:2
.=g/.k*g/.m by A11,A15,Lm4,XXREAL_0:2;
hence thesis by A14,A15;
end;
f/.n is being_a_product_of_squares implies thesis by A8,A11,Lm4;
hence thesis by A1,A8,A11,A12;
end;
now
assume
A16: n=len g;
then
A17: i<n & j<n by A3,A5,A6,NAT_1:13;
g/.n=f/.i*f/.j by A6,A16,Lm3
.=g/.i*f/.j by A2,A3,Lm4
.=g/.i*g/.j by A4,A5,Lm4;
hence thesis by A2,A4,A17;
end;
hence thesis by A9,A10,XXREAL_0:1;
end;
len f<>0 by A1;
then len f+len<*f/.i*f/.j*><>0;
then len (f^<*f/.i*f/.j*>)<>0 by FINSEQ_1:22;
hence thesis by A7;
end;
Lm82: f is being_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f/.i*f/.j*> is being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: i<>0 and
A3: i<=len f and
A4: j<>0 and
A5: j<=len f;
set g=f^<*f/.i*f/.j*>;
A6: len g=len f+len<*f/.i*f/.j*> by FINSEQ_1:22
.=len f+1 by Lm2;
A7: for n st n<>0 & n<=len g holds g/.n is being_an_amalgam_of_squares or
ex i,j st (g/.n=g/.i*g/.j or g/.n=g/.i+g/. j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that
A8: n<>0 and
A9: n<=len g;
A10: now
assume n<len g;
then
A11: n<=len f by A6,NAT_1:13;
then
A12: g/.n=f/.n by A8,Lm4;
A13: now
given k,m be Nat such that
A14: f/.n=f/.k*f/.m or f/.n=f/.k+f/.m and
A15: k<>0 & k<n & m<>0 & m<n;
f/.k=g/.k & f/.m=g/.m by A11,A15,Lm4,XXREAL_0:2;
hence thesis by A12,A14,A15;
end;
f/.n is being_an_amalgam_of_squares implies thesis by A8,A11,Lm4;
hence thesis by A1,A8,A11,A13;
end;
now
assume
A16: n=len g;
then
A17: i<n & j<n by A3,A5,A6,NAT_1:13;
g/.n=f/.i*f/.j by A6,A16,Lm3
.=g/.i*f/.j by A2,A3,Lm4
.=g/.i*g/.j by A4,A5,Lm4;
hence thesis by A2,A4,A17;
end;
hence thesis by A9,A10,XXREAL_0:1;
end;
len f<>0 by A1;
then len f+len<*f/.i*f/.j*><>0;
then len (f^<*f/.i*f/.j*>)<>0 by FINSEQ_1:22;
hence thesis by A7;
end;
Lm83: f is being_a_Product_of_squares & x is being_a_square implies f^<*f/.len
f*x*> is being_a_Product_of_squares
proof
assume that
A1: f is being_a_Product_of_squares and
A2: x is being_a_square;
set g=f^<*f/.len f*x*>;
A3: len g=len f+len <*f/.len f*x*> by FINSEQ_1:22
.=len f+1 by Lm2;
A4: for n st n<>0 & n<len g holds f/.n=g/.n
proof
let n;
assume n<>0 & n<len g;
then 1<=n & n<=len f by A3,NAT_1:13,25;
then n in dom f by FINSEQ_3:25;
hence thesis by Lm1;
end;
A5: for n st n<>0 & n<len g ex y st y is being_a_square & g/.(n+1)=g/.n*y
proof
let n;
assume that
A6: n<>0 and
A7: n<len g;
A8: now
A9: f/.n=g/.n by A4,A6,A7;
assume
A10: n<len f;
then n+1<>0 & n+1<len g by A3,XREAL_1:6;
then f/.(n+1)=g/.(n+1) by A4;
hence thesis by A1,A6,A10,A9;
end;
A11: now
assume
A12: n=len f;
1<=n by A6,NAT_1:25;
then
A13: n in dom f by A12,FINSEQ_3:25;
g/.(n+1)=f/.n*x by A12,Lm3;
then g/.(n+1)=g/.n*x by A13,Lm1;
hence thesis by A2;
end;
n<=len f by A3,A7,NAT_1:13;
hence thesis by A8,A11,XXREAL_0:1;
end;
len f<>0 by A1;
then 1<=len f by NAT_1:25;
then 1<len g by A3,NAT_1:13;
then g/.1=f/.1 by A4;
then
A14: g/.1 is being_a_square by A1;
len g<>0 by A3;
hence thesis by A14,A5;
end;
Lm84: f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares
implies (f^g)^<*f/.len f*g/.len g*> is being_an_Amalgam_of_squares
proof
assume that
A1: f is being_an_Amalgam_of_squares and
A2: g is being_an_Amalgam_of_squares;
len f<>0 by A1;
then
A3: len f+len g<=len(f^g) & (f^g)/.len f=f/.len f by Lm4,FINSEQ_1:22;
len g<>0 by A2;
then
A4: len f+len g<>0 & (f^g)/.(len f+len g)=g/.len g by Lm5;
len f<=len f+len g by NAT_1:11;
then
A5: len f<=len(f^g) by FINSEQ_1:22;
len f<>0 & f^g is being_an_Amalgam_of_squares by A1,A2,Lm80;
hence thesis by A5,A3,A4,Lm81;
end;
Lm85: f is being_a_generation_from_squares & g is
being_a_generation_from_squares implies (f^g)^<*f/.len f*g/.len g*> is
being_a_generation_from_squares
proof
assume that
A1: f is being_a_generation_from_squares and
A2: g is being_a_generation_from_squares;
A3: len g<>0 by A2;
len f<>0 by A1;
then 1<=len f by NAT_1:25;
then len f in dom f by FINSEQ_3:25;
then
A4: len f+len g<=len(f^g) & (f^g)/.len f=f/.len f by Lm1,FINSEQ_1:22;
len f<=len f+len g by NAT_1:11;
then
A5: len f<=len(f^g) by FINSEQ_1:22;
1<=len g by A3,NAT_1:25;
then len g in dom g by FINSEQ_3:25;
then
A6: (f^g)/.(len f+len g)=g/.len g by Lm1;
f^g is being_a_generation_from_squares & len f<>0 by A1,A2,Lm33;
hence thesis by A5,A4,A6,Lm82;
end;
theorem
x is being_a_product_of_squares & y is being_a_square implies x*y is
being_a_product_of_squares
proof
assume that
A1: x is being_a_product_of_squares and
A2: y is being_a_square;
consider f such that
A3: f is being_a_Product_of_squares & x=f/.len f by A1;
take g=f^<*x*y*>;
len g=len f+len <*x*y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm83;
end;
theorem
x is being_a_square & y is being_a_square implies x*y is
being_a_product_of_squares
proof
assume that
A1: x is being_a_square and
A2: y is being_a_square;
x is being_a_product_of_squares by A1,Lm9;
then consider f such that
A3: f is being_a_Product_of_squares & x=f/.len f;
take g=f^<*x*y*>;
len g=len f+len <*x*y*> by FINSEQ_1:22
.=len f+1 by Lm2;
hence thesis by A2,A3,Lm3,Lm83;
end;
Lm86: x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares
implies x*y is being_an_amalgam_of_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is being_an_amalgam_of_squares;
consider f such that
A3: f is being_an_Amalgam_of_squares & x=f/.len f by A1;
consider g such that
A4: g is being_an_Amalgam_of_squares & y=g/.len g by A2;
take h=(f^g)^<*f/.len f*g/.len g*>;
len h=len(f^g)+len<*f/.len f*g/.len g*> by FINSEQ_1:22
.=len(f^g)+1 by Lm2;
hence thesis by A3,A4,Lm3,Lm84;
end;
theorem
x is being_a_square & y is being_a_product_of_squares implies x*y is
being_an_amalgam_of_squares
proof
assume x is being_a_square & y is being_a_product_of_squares;
then x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares by
Lm17,Lm19;
hence thesis by Lm86;
end;
theorem
x is being_a_square & y is being_an_amalgam_of_squares implies x*y is
being_an_amalgam_of_squares
proof
assume that
A1: x is being_a_square and
A2: y is being_an_amalgam_of_squares;
x is being_an_amalgam_of_squares by A1,Lm17;
hence thesis by A2,Lm86;
end;
theorem
x is being_a_product_of_squares & y is being_a_product_of_squares
implies x*y is being_an_amalgam_of_squares
proof
assume x is being_a_product_of_squares & y is being_a_product_of_squares;
then x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares by
Lm19;
hence thesis by Lm86;
end;
theorem
x is being_a_product_of_squares & y is being_an_amalgam_of_squares
implies x*y is being_an_amalgam_of_squares
proof
assume that
A1: x is being_a_product_of_squares and
A2: y is being_an_amalgam_of_squares;
x is being_an_amalgam_of_squares by A1,Lm19;
hence thesis by A2,Lm86;
end;
theorem
x is being_an_amalgam_of_squares & y is being_a_square implies x*y is
being_an_amalgam_of_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is being_a_square;
y is being_an_amalgam_of_squares by A2,Lm17;
hence thesis by A1,Lm86;
end;
theorem
x is being_an_amalgam_of_squares & y is being_a_product_of_squares
implies x*y is being_an_amalgam_of_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is being_a_product_of_squares;
y is being_an_amalgam_of_squares by A2,Lm19;
hence thesis by A1,Lm86;
end;
theorem
x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares
implies x*y is being_an_amalgam_of_squares by Lm86;
Lm87: x is generated_from_squares & y is generated_from_squares implies x*y is
generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is generated_from_squares;
consider f such that
A3: f is being_a_generation_from_squares and
A4: x=f/.len f by A1;
consider g such that
A5: g is being_a_generation_from_squares and
A6: y=g/.len g by A2;
set h=(f^g)^<*f/.len f*g/.len g*>;
len h=len(f^g)+len<*f/.len f*g/.len g*> by FINSEQ_1:22
.=len(f^g)+1 by Lm2;
then
A7: h/.len h=x*g/.len g by A4,Lm3;
h is being_a_generation_from_squares by A3,A5,Lm85;
hence thesis by A6,A7;
end;
theorem
x is being_a_square & y is being_a_sum_of_squares implies x*y is
generated_from_squares
proof
assume x is being_a_square & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm38;
hence thesis by Lm87;
end;
theorem
x is being_a_square & y is being_a_sum_of_products_of_squares implies
x*y is generated_from_squares
proof
assume x is being_a_square & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_square & y is being_a_sum_of_amalgams_of_squares implies
x*y is generated_from_squares
proof
assume x is being_a_square & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm31,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_square & y is generated_from_squares implies x*y is
generated_from_squares
proof
assume that
A1: x is being_a_square and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm31;
hence thesis by A2,Lm87;
end;
theorem
x is being_a_sum_of_squares & y is being_a_square implies x*y is
generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_square;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm38;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_squares & y is being_a_sum_of_squares implies x*y
is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_squares & y is being_a_product_of_squares implies
x*y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_product_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm49;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares
implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_squares & y is being_an_amalgam_of_squares implies
x*y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_an_amalgam_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm40;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares
implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_squares & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_squares & y is generated_from_squares implies x*y
is generated_from_squares
proof
assume that
A1: x is being_a_sum_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm38;
hence thesis by A2,Lm87;
end;
theorem
x is being_a_product_of_squares & y is being_a_sum_of_squares implies
x*y is generated_from_squares
proof
assume x is being_a_product_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm49;
hence thesis by Lm87;
end;
theorem
x is being_a_product_of_squares & y is
being_a_sum_of_products_of_squares implies x*y is generated_from_squares
proof
assume
x is being_a_product_of_squares & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_product_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x*y is generated_from_squares
proof
assume
x is being_a_product_of_squares & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_product_of_squares & y is generated_from_squares implies
x*y is generated_from_squares
proof
assume that
A1: x is being_a_product_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm49;
hence thesis by A2,Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is being_a_square implies
x*y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is being_a_square;
then x is generated_from_squares & y is generated_from_squares by Lm31,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares
implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_a_product_of_squares implies x*y is generated_from_squares
proof
assume
x is being_a_sum_of_products_of_squares & y is being_a_product_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_products_of_squares implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_an_amalgam_of_squares implies x*y is generated_from_squares
proof
assume
x is being_a_sum_of_products_of_squares & y is being_an_amalgam_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_products_of_squares & y is
being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm54,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_products_of_squares & y is generated_from_squares
implies x*y is generated_from_squares
proof
assume that
A1: x is being_a_sum_of_products_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm54;
hence thesis by A2,Lm87;
end;
theorem
x is being_an_amalgam_of_squares & y is being_a_sum_of_squares implies
x*y is generated_from_squares
proof
assume x is being_an_amalgam_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Lm40;
hence thesis by Lm87;
end;
theorem
x is being_an_amalgam_of_squares & y is
being_a_sum_of_products_of_squares implies x*y is generated_from_squares
proof
assume
x is being_an_amalgam_of_squares & y is being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Lm54;
hence thesis by Lm87;
end;
theorem
x is being_an_amalgam_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x*y is generated_from_squares
proof
assume
x is being_an_amalgam_of_squares & y is being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Th1;
hence thesis by Lm87;
end;
theorem
x is being_an_amalgam_of_squares & y is generated_from_squares implies
x*y is generated_from_squares
proof
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Lm40;
hence thesis by A2,Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is being_a_square implies
x*y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is being_a_square;
then x is generated_from_squares & y is generated_from_squares by Lm31,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares
implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is being_a_sum_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm38,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is
being_a_product_of_squares implies x*y is generated_from_squares
proof
assume
x is being_a_sum_of_amalgams_of_squares & y is being_a_product_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm49,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_products_of_squares implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_products_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm54,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is
being_an_amalgam_of_squares implies x*y is generated_from_squares
proof
assume
x is being_a_sum_of_amalgams_of_squares & y is being_an_amalgam_of_squares;
then x is generated_from_squares & y is generated_from_squares by Lm40,Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_amalgams_of_squares implies x*y is generated_from_squares
proof
assume x is being_a_sum_of_amalgams_of_squares & y is
being_a_sum_of_amalgams_of_squares;
then x is generated_from_squares & y is generated_from_squares by Th1;
hence thesis by Lm87;
end;
theorem
x is being_a_sum_of_amalgams_of_squares & y is generated_from_squares
implies x*y is generated_from_squares
proof
assume that
A1: x is being_a_sum_of_amalgams_of_squares and
A2: y is generated_from_squares;
x is generated_from_squares by A1,Th1;
hence thesis by A2,Lm87;
end;
theorem
x is generated_from_squares & y is being_a_square implies x*y is
generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_square;
y is generated_from_squares by A2,Lm31;
hence thesis by A1,Lm87;
end;
theorem
x is generated_from_squares & y is being_an_amalgam_of_squares implies
x*y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_an_amalgam_of_squares;
y is generated_from_squares by A2,Lm40;
hence thesis by A1,Lm87;
end;
theorem
x is generated_from_squares & y is being_a_sum_of_squares implies x*y
is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_sum_of_squares;
y is generated_from_squares by A2,Lm38;
hence thesis by A1,Lm87;
end;
theorem
x is generated_from_squares & y is being_a_product_of_squares implies
x*y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_product_of_squares;
y is generated_from_squares by A2,Lm49;
hence thesis by A1,Lm87;
end;
theorem
x is generated_from_squares & y is being_a_sum_of_products_of_squares
implies x*y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_sum_of_products_of_squares;
y is generated_from_squares by A2,Lm54;
hence thesis by A1,Lm87;
end;
theorem
x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares
implies x*y is generated_from_squares
proof
assume that
A1: x is generated_from_squares and
A2: y is being_a_sum_of_amalgams_of_squares;
y is generated_from_squares by A2,Th1;
hence thesis by A1,Lm87;
end;