:: Ordered Rings - Part I
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received October 11, 1990
:: Copyright (c) 1990-2016 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, BOOLE;
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*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** 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 is being_a_Sum_of_squares
proof
A1: for n st n<>0 & n 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;
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 is being_a_Product_of_squares
proof
A1: for n st n<>0 & n 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;
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 is being_a_Sum_of_products_of_squares
proof
A1: for n st n<>0 & n 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;
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 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;
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 & n0 & n0 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 & i0 & j 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 & i0 & j0 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 & i0 & j0 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 is being_a_Sum_of_amalgams_of_squares
proof
A1: for n st n<>0 & n 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;
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 & n0 & n0 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 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;
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 & n0 & n0 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 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;
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 & i0 & j 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 & i0 & j0 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 & i0 & j0 and
A9: n<=len g;
A10: now
assume n0 & k0 & m0 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 & i0 & j0 and
A5: n<=len (f^g);
A6: n<=len f+len g by A5,FINSEQ_1:22;
A7: now
assume
A8: len f0 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: k0 and
A18: l0 & 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+k0 & k0 & l0 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: i0;
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 & i0 & j 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 & i0 & j0 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;
i0 & 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 & i0 & j0 and
A9: n<=len g;
A10: now
assume n0 & k0 & m0 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: i0;
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 & i0 & j0 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: i0;
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 & n0 & n0 & n0 and
A7: n0 & n+10 by A1;
then 1<=len f by NAT_1:25;
then 10 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 & n0 & n0 & n0 and
A7: n0 & n+10 by A1;
then 1<=len f by NAT_1:25;
then 10 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 & n0 & n0 & n0 and
A7: n0 & n+10 by A1;
then 1<=len f by NAT_1:25;
then 10 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 & i0 & j0 and
A9: n<=len g;
A10: now
assume n0 & k0 & m0 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 & i0 & j0 and
A5: n<=len (f^g);
A6: n<=len f+len g by A5,FINSEQ_1:22;
A7: now
assume
A8: len f0 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: k0 and
A18: l0 & len f+l<>0 by A15,A17;
A20: len f+k0 & k0 & l0 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 & i0 & j0 and
A9: n<=len g;
A10: now
assume n0 & k0 & m0 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 & i0 & j0 and
A9: n<=len g;
A10: now
assume n0 & k0 & m0 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 & n0 & n0 & n0 and
A7: n0 & n+10 by A1;
then 1<=len f by NAT_1:25;
then 10 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;
*