Copyright (c) 1990 Association of Mizar Users
environ
vocabulary VECTSP_1, FINSEQ_1, RELAT_1, FUNCT_1, SQUARE_1, O_RING_1;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, FUNCT_1, FINSEQ_1,
STRUCT_0, RLVECT_1, VECTSP_1;
constructors NAT_1, VECTSP_1, XREAL_0, XBOOLE_0;
clusters VECTSP_1, STRUCT_0, RELSET_1, NAT_1, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, ARITHM;
theorems REAL_1, NAT_1, FINSEQ_1, FUNCT_1, AXIOMS, FINSEQ_3;
schemes NAT_1;
begin
reserve i,j,k,m,n for Nat;
Lm1:
n<1 implies n=0
proof
assume n<1;
then n<0+1;
then 0<=n & n<=0 by NAT_1:18,38;
hence thesis by AXIOMS:21;
end;
Lm2:
n<=1 implies n=0 or n=1
proof
assume n<=1;
then n<1 or n=1 by REAL_1:def 5;
hence thesis by Lm1;
end;
::
:: FIELD-LIKE ALGEBRAS
::
reserve R for non empty doubleLoopStr;
reserve x,y for Scalar of R;
reserve f,g,h for FinSequence of the carrier of R;
definition let D be non empty set,
f be FinSequence of D,
k be Nat;
assume
A1: 0<>k & k<=len f;
func f.:k -> Element of D equals
:Def1: f.k;
coherence
proof
0<k by A1,NAT_1:19;
then 0+1<=k by NAT_1:38;
then k in dom f by A1,FINSEQ_3:27;
then A2:f.k in rng f by FUNCT_1:def 5;
rng f c= D by FINSEQ_1:def 4;
hence thesis by A2;
end;
end;
Lm3:
h=f^g iff ( dom h = Seg(len f + len g) &
(for k st k in dom f holds h.:k=f.:k) &
(for k st k in dom g holds h.:(len f + k)=g.:k))
proof
thus h=f^g implies
(dom h = Seg(len f + len g) &
(for k st k in dom f holds h.:k=f.:k) &
(for k st k in dom g holds h.:(len f + k)=g.:k))
proof
assume A1: h=f^g;
hence dom h = Seg(len f + len g) by FINSEQ_1:def 7;
then A2:len h=len f+len g by FINSEQ_1:def 3;
thus for k st k in dom f holds h.:k=f.:k
proof
let k such that A3:k in dom f;
A4:len f<=len f+len g by NAT_1:29;
A5:0<>k & k<=len f by A3,FINSEQ_3:27;
then 0<>k & k<=len h by A2,A4,AXIOMS:22;
then h.:k=h.k by Def1
.=f.k by A1,A3,FINSEQ_1:def 7
.=f.:k by A5,Def1;
hence thesis;
end;
thus for k st k in dom g holds h.:(len f + k)=g.:k
proof
let k; assume A6:k in dom g;
then A7:0<>k & k<=len g by FINSEQ_3:27;
then 0<>len f+k & len f+k<=len f+len g by NAT_1:23,REAL_1:55;
then h.:(len f + k)=h.(len f+k) by A2,Def1
.=g.k by A1,A6,FINSEQ_1:def 7
.=g.:k by A7,Def1;
hence thesis;
end;
end;
thus (dom h = Seg(len f + len g) &
(for k st k in dom f holds h.:k=f.:k) &
(for k st k in dom g holds h.:(len f + k)=g.:k)) implies
h=f^g
proof
assume that
A8:dom h = Seg(len f + len g) and
A9:for k st k in dom f holds h.:k=f.:k and
A10:for k 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 st k in dom f holds h.k=f.k
proof
let k such that A13:k in dom f;
A14:len f<=len f+len g by NAT_1:29;
A15:0<>k & k<=len f by A13,FINSEQ_3:27;
then 0<>k & k<=len h by A11,A14,AXIOMS:22;
then h.k=h.:k by Def1
.=f.:k by A9,A13
.=f.k by A15,Def1;
hence thesis;
end;
for k st k in dom g holds h.(len f + k)=g.k
proof
let k; assume A16:k in dom g;
then A17:0<>k & k<=len g by FINSEQ_3:27;
then 0<>len f+k & len f+k<=len f+len g by NAT_1:23,REAL_1:55;
then h.(len f + k)=h.:(len f+k) by A11,Def1
.=g.:k by A10,A16
.=g.k by A17,Def1;
hence thesis;
end;
hence h=f^g by A8,A12,FINSEQ_1:def 7;
end;
end;
Lm4:
f=<*x*> iff len f =1 & f.:1=x
proof
thus f=<*x*> implies len f=1 & f.:1=x
proof
assume A1:f=<*x*>;
hence len f=1 by FINSEQ_1:57;
then f.:1=f.1 by Def1
.=x by A1,FINSEQ_1:57;
hence thesis;
end;
thus len f=1 & f.:1=x implies f=<*x*>
proof
assume that
A2:len f=1 and
A3:f.:1=x;
f.1=x by A2,A3,Def1;
hence thesis by A2,FINSEQ_1:57;
end;
end;
Lm5:
(f^<*x*>).:(len f + 1)=x
proof
len f+1=len f+len<*x*> by FINSEQ_1:56
.=len(f^<*x*>) by FINSEQ_1:35;
then 0<>len f+1 & len f+1<=len(f^<*x*>) by NAT_1:21;
then (f^<*x*>).:(len f+1)=(f^<*x*>).(len f+1) by Def1
.=x by FINSEQ_1:59;
hence thesis;
end;
Lm6:
i<>0 & i<=len f implies (f^g).:i=f.:i
proof
assume A1: i<>0 & i<=len f;
then 0<>i & 0<=i by NAT_1:18;
then 0<i by REAL_1:def 5;
then 0+1<=i by NAT_1:38;
then i in dom f by A1,FINSEQ_3:27;
hence thesis by Lm3;
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;
synonym x is_a_square;
end;
definition let R,f;
attr f is being_a_Sum_of_squares means:Def4:
len f<>0 & f.:1 is_a_square &
(for n st n<>0 & n<len f ex y st y is_a_square & f.:(n+1)=f.:n+y);
synonym f is_a_Sum_of_squares;
end;
definition let R be non empty doubleLoopStr, x be Scalar of R;
attr x is being_a_sum_of_squares means:Def5:
ex f being FinSequence of the carrier of R st
f is_a_Sum_of_squares & x=f.:len f;
synonym x is_a_sum_of_squares;
end;
Lm7:
x is_a_square implies <*x*> is_a_Sum_of_squares
proof
assume A1:x is_a_square;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_a_square by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_a_square & <*x*>.:(n+1)=<*x*>.:n+y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def4;
end;
Lm8:
x is_a_square implies x is_a_sum_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_a_Sum_of_squares by Lm7;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def5;
end;
definition let R,f;
attr f is being_a_Product_of_squares means:Def6:
len f<>0 & f.:1 is_a_square &
(for n st n<>0 & n<len f ex y
st y is_a_square & f.:(n+1)=f.:n*y);
synonym f is_a_Product_of_squares;
end;
definition let R,x;
attr x is being_a_product_of_squares means:Def7:
ex f st f is_a_Product_of_squares & x=f.:len f;
synonym x is_a_product_of_squares;
end;
Lm9:
x is_a_square implies <*x*> is_a_Product_of_squares
proof
assume A1:x is_a_square;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_a_square by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_a_square & <*x*>.:(n+1)=<*x*>.:n*y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def6;
end;
Lm10:
x is_a_square implies x is_a_product_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_a_Product_of_squares by Lm9;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def7;
end;
definition let R,f;
attr f is being_a_Sum_of_products_of_squares means:Def8:
len f<>0 & (f.:1 is_a_product_of_squares) &
(for n st n<>0 & n<len f ex y
st y is_a_product_of_squares & f.:(n+1)=f.:n+y);
synonym f is_a_Sum_of_products_of_squares;
end;
definition let R,x;
attr x is being_a_sum_of_products_of_squares means:Def9:
ex f st f is_a_Sum_of_products_of_squares & x=f.:len f;
synonym x is_a_sum_of_products_of_squares;
end;
Lm11:
x is_a_square implies <*x*> is_a_Sum_of_products_of_squares
proof
assume x is_a_square;
then A1:x is_a_product_of_squares by Lm10;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_a_product_of_squares by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_a_product_of_squares & <*x*>.:(n+1)=<*x*>.:n+y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def8;
end;
Lm12:
x is_a_square implies x is_a_sum_of_products_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_a_Sum_of_products_of_squares by Lm11;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def9;
end;
Lm13:
x is_a_product_of_squares implies <*x*> is_a_Sum_of_products_of_squares
proof
assume A1:x is_a_product_of_squares;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_a_product_of_squares
by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_a_product_of_squares & <*x*>.:(n+1)=<*x*>.:n+y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def8;
end;
Lm14:
x is_a_product_of_squares implies x is_a_sum_of_products_of_squares
proof
assume x is_a_product_of_squares;
then A1:<*x*> is_a_Sum_of_products_of_squares by Lm13;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def9;
end;
Lm15:
f is_a_Sum_of_squares implies f is_a_Sum_of_products_of_squares
proof
assume A1:f is_a_Sum_of_squares;
then len f<>0 & f.:1 is_a_square by Def4;
then A2:len f<>0 & f.:1 is_a_product_of_squares by Lm10;
for n st n<>0 & n<len f ex y
st y is_a_product_of_squares & f.:(n+1)=f.:n+y
proof
let n; assume n<>0 & n<len f;
then consider y such that A3:y is_a_square & f.:(n+1)=f.:n+y
by A1,Def4;
y is_a_product_of_squares & f.:(n+1)=f.:n+y by A3,Lm10;
hence thesis;
end;
hence thesis by A2,Def8;
end;
Lm16:
x is_a_sum_of_squares implies x is_a_sum_of_products_of_squares
proof
assume x is_a_sum_of_squares;
then consider f such that A1:f is_a_Sum_of_squares & x=f.:len f
by Def5;
f is_a_Sum_of_products_of_squares by A1,Lm15;
hence thesis by A1,Def9;
end;
definition let R,f;
attr f is being_an_Amalgam_of_squares means:Def10:
len f<>0 &
(for n st n<>0 & n<=len f holds f.:n is_a_product_of_squares or
ex i,j st f.:n=f.:i*f.:j & i<>0 & i<n & j<>0 & j<n);
synonym f is_an_Amalgam_of_squares;
end;
definition let R,x;
attr x is being_an_amalgam_of_squares means:Def11:
ex f st f is_an_Amalgam_of_squares & x=f.:len f;
synonym x is_an_amalgam_of_squares;
end;
Lm17:
x is_a_square implies <*x*> is_an_Amalgam_of_squares
proof
assume x is_a_square;
then A1:x is_a_product_of_squares by Lm10;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_a_product_of_squares by A1,Lm4;
for n st n<>0 & n<=len <*x*> holds <*x*>.:n is_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 n<>0 & n<=len <*x*>;
then n<>0 & n<=1 by Lm4;
hence thesis by A3,Lm2;
end;
hence thesis by A2,Def10;
end;
Lm18:
x is_a_square implies x is_an_amalgam_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_an_Amalgam_of_squares by Lm17;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def11;
end;
Lm19:
x is_a_product_of_squares implies <*x*> is_an_Amalgam_of_squares
proof
assume A1:x is_a_product_of_squares;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_a_product_of_squares by A1,Lm4;
for n st n<>0 & n<=len <*x*> holds <*x*>.:n is_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 n<>0 & n<=len <*x*>;
then n<>0 & n<=1 by Lm4;
hence thesis by A3,Lm2;
end;
hence thesis by A2,Def10;
end;
Lm20:
x is_a_product_of_squares implies x is_an_amalgam_of_squares
proof
assume x is_a_product_of_squares;
then A1:<*x*> is_an_Amalgam_of_squares by Lm19;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def11;
end;
definition let R,f;
attr f is being_a_Sum_of_amalgams_of_squares means
:Def12:
len f<>0 & (f.:1 is_an_amalgam_of_squares) &
(for n st n<>0 & n<len f ex y
st y is_an_amalgam_of_squares & f.:(n+1)=f.:n+y);
synonym f is_a_Sum_of_amalgams_of_squares;
end;
definition let R,x;
attr x is being_a_sum_of_amalgams_of_squares means
:Def13:
ex f st f is_a_Sum_of_amalgams_of_squares & x=f.:len f;
synonym x is_a_sum_of_amalgams_of_squares;
end;
Lm21:
x is_a_square implies <*x*> is_a_Sum_of_amalgams_of_squares
proof
assume x is_a_square;
then A1:x is_an_amalgam_of_squares by Lm18;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_an_amalgam_of_squares by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_an_amalgam_of_squares & <*x*>.:(n+1)=<*x*>.:n+y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def12;
end;
Lm22:
x is_a_square implies x is_a_sum_of_amalgams_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_a_Sum_of_amalgams_of_squares by Lm21;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def13;
end;
Lm23:
f is_a_Sum_of_squares
implies f is_a_Sum_of_amalgams_of_squares
proof
assume A1:f is_a_Sum_of_squares;
then A2:len f<>0 by Def4;
f.:1 is_a_square by A1,Def4;
then A3:f.:1 is_an_amalgam_of_squares by Lm18;
for n st n<>0 & n<len f ex y
st y is_an_amalgam_of_squares & f.:(n+1)=f.:n+y
proof
let n; assume n<>0 & n<len f;
then consider y such that
A4:y is_a_square & f.:(n+1)=f.:n+y
by A1,Def4;
y is_an_amalgam_of_squares & f.:(n+1)=f.:n+y by A4,Lm18;
hence thesis;
end;
hence thesis by A2,A3,Def12;
end;
Lm24:
x is_a_sum_of_squares
implies x is_a_sum_of_amalgams_of_squares
proof
assume x is_a_sum_of_squares;
then consider f such that
A1:f is_a_Sum_of_squares & x=f.:len f
by Def5;
f is_a_Sum_of_amalgams_of_squares & x=f.:len f by A1,Lm23;
hence thesis by Def13;
end;
Lm25:
x is_a_product_of_squares implies <*x*> is_a_Sum_of_amalgams_of_squares
proof
assume x is_a_product_of_squares;
then A1:x is_an_amalgam_of_squares by Lm20;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_an_amalgam_of_squares by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_an_amalgam_of_squares & <*x*>.:(n+1)=<*x*>.:n+y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def12;
end;
Lm26:
x is_a_product_of_squares implies x is_a_sum_of_amalgams_of_squares
proof
assume x is_a_product_of_squares;
then A1:<*x*> is_a_Sum_of_amalgams_of_squares by Lm25;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def13;
end;
Lm27:
f is_a_Sum_of_products_of_squares
implies f is_a_Sum_of_amalgams_of_squares
proof
assume A1:f is_a_Sum_of_products_of_squares;
then A2:len f<>0 by Def8;
f.:1 is_a_product_of_squares by A1,Def8;
then A3:f.:1 is_an_amalgam_of_squares by Lm20;
for n st n<>0 & n<len f ex y
st y is_an_amalgam_of_squares & f.:(n+1)=f.:n+y
proof
let n; assume n<>0 & n<len f;
then consider y such that
A4:y is_a_product_of_squares & f.:(n+1)=f.:n+y
by A1,Def8;
y is_an_amalgam_of_squares & f.:(n+1)=f.:n+y by A4,Lm20;
hence thesis;
end;
hence thesis by A2,A3,Def12;
end;
Lm28:
x is_a_sum_of_products_of_squares
implies x is_a_sum_of_amalgams_of_squares
proof
assume x is_a_sum_of_products_of_squares;
then consider f such that
A1:f is_a_Sum_of_products_of_squares & x=f.:len f
by Def9;
f is_a_Sum_of_amalgams_of_squares & x=f.:len f by A1,Lm27;
hence thesis by Def13;
end;
Lm29:
x is_an_amalgam_of_squares
implies <*x*> is_a_Sum_of_amalgams_of_squares
proof
assume A1:x is_an_amalgam_of_squares;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_an_amalgam_of_squares by A1,Lm4;
for n st n<>0 & n<len <*x*>
ex y st y is_an_amalgam_of_squares & <*x*>.:(n+1)=<*x*>.:n+y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm4;
hence thesis by Lm1;
end;
hence thesis by A2,A3,Def12;
end;
Lm30:
x is_an_amalgam_of_squares implies x is_a_sum_of_amalgams_of_squares
proof
assume x is_an_amalgam_of_squares;
then A1:<*x*> is_a_Sum_of_amalgams_of_squares by Lm29;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def13;
end;
definition let R,f;
attr f is being_a_generation_from_squares means:Def14:
len f<>0 &
(for n st n<>0 & n<=len f holds f.:n is_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);
synonym f is_a_generation_from_squares;
end;
definition let R,x;
attr x is generated_from_squares means:Def15:
ex f st f is_a_generation_from_squares & x=f.:len f;
synonym x is_generated_from_squares;
end;
Lm31:
x is_a_square implies <*x*> is_a_generation_from_squares
proof
assume x is_a_square;
then A1:x is_an_amalgam_of_squares by Lm18;
A2: len<*x*>=1 by Lm4;
A3:<*x*>.:1 is_an_amalgam_of_squares by A1,Lm4;
for n st n<>0 & n<=len <*x*> holds <*x*>.:n is_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 n<>0 & n<=len <*x*>;
then n<>0 & n<=1 by Lm4;
hence thesis by A3,Lm2;
end;
hence thesis by A2,Def14;
end;
Lm32:
x is_a_square implies x is_generated_from_squares
proof
assume x is_a_square;
then A1:<*x*> is_a_generation_from_squares by Lm31;
len<*x*>=1 & <*x*>.:1=x by Lm4;
hence thesis by A1,Def15;
end;
Lm33:f is_a_generation_from_squares & x is_an_amalgam_of_squares
implies f^<*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
x is_an_amalgam_of_squares;
then len f<>0 by Def14;
then len f+len<*x*><>0 by NAT_1:23;
then A2:len (f^<*x*>)<>0 by FINSEQ_1:35;
set g=f^<*x*>;
A3:len g=len f+len<*x*> by FINSEQ_1:35
.=len f+1 by Lm4;
for n st n<>0 & n<=len g holds
g.:n is_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 A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm6;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm6;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm6;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm6;
hence thesis by A7,A9,A10;
end;
hence thesis by A1,A4,A6,A8,Def14;
end;
n=len g implies thesis by A1,A3,Lm5;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,Def14;
end;
Lm34:
f is_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f.:i+f.:j*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
i<>0 & i<=len f & j<>0 & j<=len f;
then len f<>0 by Def14;
then len f+len<*f.:i+f.:j*><>0 by NAT_1:23;
then A2:len (f^<*f.:i+f.:j*>)<>0 by FINSEQ_1:35;
set g=f^<*f.:i+f.:j*>;
A3:len g=len f+len<*f.:i+f.:j*> by FINSEQ_1:35
.=len f+1 by Lm4;
for n st n<>0 & n<=len g holds
g.:n is_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 A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm6;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm6;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm6;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm6;
hence thesis by A7,A9,A10;
end;
hence thesis by A1,A4,A6,A8,Def14;
end;
now assume A11: n=len g;
then g.:n=f.:i+f.:j by A3,Lm5
.=g.:i+f.:j by A1,Lm6
.=g.:i+g.:j by A1,Lm6;
then g.:n=g.:i+g.:j & i<n & j<n by A1,A3,A11,NAT_1:38;
hence thesis by A1;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,Def14;
end;
Lm35:
f is_a_generation_from_squares & x is_a_square
implies f^<*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares & x is_a_square;
then len f<>0 by Def14;
then len f+len<*x*><>0 by NAT_1:23;
then A2:len (f^<*x*>)<>0 by FINSEQ_1:35;
set g=f^<*x*>;
A3:len g=len f+len<*x*> by FINSEQ_1:35
.=len f+1 by Lm4;
for n st n<>0 & n<=len g holds
g.:n is_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 A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm6;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm6;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm6;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm6;
hence thesis by A7,A9,A10;
end;
hence thesis
by A1,A4,A6,A8,Def14;
end;
now assume n=len g;
then g.:n=x by A3,Lm5;
hence thesis by A1,Lm18;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,Def14;
end;
Lm36:
f is_a_generation_from_squares & x is_a_square
implies (f^<*x*>)^<*f.:len f+x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares & x is_a_square;
then A2:f^<*x*> is_a_generation_from_squares by Lm35;
A3:len<*x*>=1 by Lm4;
A4:len f<>0 by A1,Def14;
A5: len f<=len f+1 by NAT_1:29;
A6:
len f+1<>0 & len f+1=len(f^<*x*>) by A3,FINSEQ_1:35,NAT_1:21;
A7:(f^<*x*>).:len f=f.:len f by A4,Lm6;
(f^<*x*>).:(len f+1)=x by Lm5;
hence thesis by A2,A4,A5,A6,A7,Lm34;
end;
Lm37:
x is_generated_from_squares & y is_a_square
implies x+y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_square;
consider f such that
A3:f is_a_generation_from_squares & x=f.:len f
by A1,Def15;
take g=(f^<*y*>)^<*f.:len f+y*>;
len g=len(f^<*y*>)+len<*f.:len f+y*> by FINSEQ_1:35
.=len(f^<*y*>)+1 by Lm4;
hence thesis by A2,A3,Lm5,Lm36;
end;
Lm38:
f is_a_Sum_of_squares & 0<>i & i<=len f
implies f.:i is_generated_from_squares
proof
assume that
A1:f is_a_Sum_of_squares and
A2:0<>i and
A3:i<=len f;
defpred P[Nat] means 0<>$1 & $1<=len f implies f.:$1
is_generated_from_squares;
A4: P[0];
A5: for i st P[i] holds P[i+1]
proof
let i such that
A6:0<>i & i<=len f implies f.:i is_generated_from_squares;
assume that
0<>(i+1) and
A7:(i+1)<=len f;
A8:i<len f by A7,NAT_1:38;
A9:now assume i=0;
then f.:(i+1) is_a_square by A1,Def4;
hence thesis by Lm32;
end;
now assume A10:i<>0;
then ex y st
y is_a_square & f.:(i+1)=f.:i+y by A1,A8,Def4;
hence thesis by A6,A7,A10,Lm37,NAT_1:38;
end;
hence thesis by A9;
end;
for i holds P[i] from Ind(A4,A5);
hence thesis by A2,A3;
end;
Lm39:
x is_a_sum_of_squares
implies x is_generated_from_squares
proof
assume x is_a_sum_of_squares;
then consider f such that
A1:f is_a_Sum_of_squares & x=f.:len f
by Def5;
0<>len f & len f<=len f by A1,Def4;
hence thesis by A1,Lm38;
end;
Lm40:f is_a_generation_from_squares & x is_an_amalgam_of_squares
implies (f^<*x*>)^<*f.:len f+x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
x is_an_amalgam_of_squares;
then A2:f^<*x*> is_a_generation_from_squares by Lm33;
A3:len<*x*>=1 by Lm4;
A4:len f<>0 by A1,Def14;
A5: len f<=len f+1 by NAT_1:29;
A6:
len f+1<>0 & len f+1=len(f^<*x*>) by A3,FINSEQ_1:35,NAT_1:21;
A7:(f^<*x*>).:len f=f.:len f by A4,Lm6;
(f^<*x*>).:(len f+1)=x by Lm5;
hence thesis by A2,A4,A5,A6,A7,Lm34;
end;
Lm41:
x is_generated_from_squares & y is_an_amalgam_of_squares
implies x+y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_an_amalgam_of_squares;
consider f such that
A3:f is_a_generation_from_squares & x=f.:len f
by A1,Def15;
take g=(f^<*y*>)^<*f.:len f+y*>;
len g=len(f^<*y*>)+len<*f.:len f+y*> by FINSEQ_1:35
.=len(f^<*y*>)+1 by Lm4;
hence thesis by A2,A3,Lm5,Lm40;
end;
Lm42:
f is_an_Amalgam_of_squares implies f is_a_generation_from_squares
proof
assume A1:f is_an_Amalgam_of_squares;
hence len f<>0 by Def10;
thus thesis
proof
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_a_product_of_squares implies thesis by Lm20;
hence thesis by A1,A2,A3,Def10;
end;
end;
Lm43:
x is_an_amalgam_of_squares implies x is_generated_from_squares
proof
assume x is_an_amalgam_of_squares;
then consider f such that
A1:f is_an_Amalgam_of_squares & x=f.:len f by Def11;
f is_a_generation_from_squares & x=f.:len f by A1,Lm42;
hence thesis by Def15;
end;
Lm44:f is_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f.:i*f.:j*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
i<>0 & i<=len f & j<>0 & j<=len f;
then len f<>0 by Def14;
then len f+len<*f.:i*f.:j*><>0 by NAT_1:23;
then A2:len (f^<*f.:i*f.:j*>)<>0 by FINSEQ_1:35;
set g=f^<*f.:i*f.:j*>;
A3:len g=len f+len<*f.:i*f.:j*> by FINSEQ_1:35
.=len f+1 by Lm4;
for n st n<>0 & n<=len g holds
g.:n is_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 A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm6;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm6;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm6;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm6;
hence thesis by A7,A9,A10;
end;
hence thesis by A1,A4,A6,A8,Def14;
end;
now assume A11: n=len g;
then g.:n=f.:i*f.:j by A3,Lm5
.=g.:i*f.:j by A1,Lm6
.=g.:i*g.:j by A1,Lm6;
then g.:n=g.:i*g.:j & i<n & j<n by A1,A3,A11,NAT_1:38;
hence thesis by A1;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,Def14;
end;
Lm45:
f is_a_generation_from_squares & x is_a_square
implies (f^<*x*>)^<*f.:len f*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares & x is_a_square;
then A2:f^<*x*> is_a_generation_from_squares by Lm35;
A3:len<*x*>=1 by Lm4;
A4:len f<>0 by A1,Def14;
A5: len f<=len f+1 by NAT_1:29;
A6:
len f+1<>0 & len f+1=len(f^<*x*>) by A3,FINSEQ_1:35,NAT_1:21;
A7:(f^<*x*>).:len f=f.:len f by A4,Lm6;
(f^<*x*>).:(len f+1)=x by Lm5;
hence thesis by A2,A4,A5,A6,A7,Lm44;
end;
Lm46:
x is_generated_from_squares & y is_a_square
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_square;
consider f such that
A3:f is_a_generation_from_squares & x=f.:len f
by A1,Def15;
take g=(f^<*y*>)^<*f.:len f*y*>;
len g=len(f^<*y*>)+len<*f.:len f*y*> by FINSEQ_1:35
.=len(f^<*y*>)+1 by Lm4;
hence thesis by A2,A3,Lm5,Lm45;
end;
Lm47:
f is_a_Product_of_squares & 0<>i & i<=len f
implies f.:i is_generated_from_squares
proof
assume that
A1:f is_a_Product_of_squares and
A2:0<>i and
A3:i<=len f;
defpred P[Nat] means
0<>$1 & $1<=len f implies f.:$1 is_generated_from_squares;
A4: P[0];
A5:for i st P[i] holds P[i+1]
proof
let i such that
A6:0<>i & i<=len f implies f.:i is_generated_from_squares;
assume that
0<>(i+1) and
A7:(i+1)<=len f;
A8:i<len f by A7,NAT_1:38;
A9:now assume i=0;
then f.:(i+1) is_a_square by A1,Def6;
hence thesis by Lm32;
end;
now assume A10:i<>0;
then ex y st y is_a_square & f.:(i+1)=f.:i*y
by A1,A8,Def6;
hence thesis by A6,A7,A10,Lm46,NAT_1:38;
end;
hence thesis by A9;
end;
for i holds P[i] from Ind(A4,A5);
hence thesis by A2,A3;
end;
Lm48:
x is_a_product_of_squares
implies x is_generated_from_squares
proof
assume x is_a_product_of_squares;
then consider f such that
A1:f is_a_Product_of_squares & x=f.:len f
by Def7;
0<>len f & len f<=len f by A1,Def6;
hence thesis by A1,Lm47;
end;
Lm49:f is_a_generation_from_squares & x is_a_product_of_squares
implies f^<*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
x is_a_product_of_squares;
then len f<>0 by Def14;
then len f+len<*x*><>0 by NAT_1:23;
then A2:len (f^<*x*>)<>0 by FINSEQ_1:35;
set g=f^<*x*>;
A3:len g=len f+len<*x*> by FINSEQ_1:35
.=len f+1 by Lm4;
for n st n<>0 & n<=len g holds
g.:n is_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 A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm6;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm6;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm6;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm6;
hence thesis by A7,A9,A10;
end;
hence thesis by A1,A4,A6,A8,Def14;
end;
now assume n=len g;
then g.:n=x by A3,Lm5;
hence thesis by A1,Lm20;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,Def14;
end;
Lm50:f is_a_generation_from_squares & x is_a_product_of_squares
implies (f^<*x*>)^<*f.:len f+x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
x is_a_product_of_squares;
then A2:f^<*x*> is_a_generation_from_squares by Lm49;
A3:len<*x*>=1 by Lm4;
A4:len f<>0 by A1,Def14;
A5: len f<=len f+1 by NAT_1:29;
A6: len f+1<>0 & len f+1=len(f^<*x*>) by A3,FINSEQ_1:35,NAT_1:21;
A7:(f^<*x*>).:len f=f.:len f by A4,Lm6;
(f^<*x*>).:(len f+1)=x by Lm5;
hence thesis by A2,A4,A5,A6,A7,Lm34;
end;
Lm51:
x is_generated_from_squares & y is_a_product_of_squares
implies x+y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_product_of_squares;
consider f such that
A3:f is_a_generation_from_squares & x=f.:len f
by A1,Def15;
take g=(f^<*y*>)^<*f.:len f+y*>;
len g=len(f^<*y*>)+len<*f.:len f+y*> by FINSEQ_1:35
.=len(f^<*y*>)+1 by Lm4;
hence thesis by A2,A3,Lm5,Lm50;
end;
Lm52:
f is_a_Sum_of_products_of_squares & 0<>i & i<=len f
implies f.:i is_generated_from_squares
proof
assume that
A1:f is_a_Sum_of_products_of_squares and
A2:0<>i and
A3:i<=len f;
defpred P[Nat] means
0<>$1 & $1<=len f implies f.:$1 is_generated_from_squares;
A4: P[0];
A5:for i st P[i] holds P[i+1]
proof
let i such that
A6:0<>i & i<=len f implies f.:i is_generated_from_squares;
assume that
0<>(i+1) and
A7:(i+1)<=len f;
A8:i<len f by A7,NAT_1:38;
A9:now assume i=0;
then f.:(i+1) is_a_product_of_squares
by A1,Def8;
hence thesis by Lm48;
end;
now assume A10:i<>0;
then ex y st y is_a_product_of_squares & f.:(i+1)=f.:i+y
by A1,A8,Def8;
hence thesis by A6,A7,A10,Lm51,NAT_1:38;
end;
hence thesis by A9;
end;
for i holds P[i] from Ind(A4,A5);
hence thesis by A2,A3;
end;
Lm53:
x is_a_sum_of_products_of_squares
implies x is_generated_from_squares
proof
assume x is_a_sum_of_products_of_squares;
then consider f such that
A1:f is_a_Sum_of_products_of_squares & x=f.:len f
by Def9;
0<>len f & len f<=len f by A1,Def8;
hence thesis by A1,Lm52;
end;
theorem
x is_a_square implies
x is_a_sum_of_squares &
x is_a_product_of_squares &
x is_a_sum_of_products_of_squares &
x is_an_amalgam_of_squares &
x is_a_sum_of_amalgams_of_squares &
x is_generated_from_squares
by Lm8,Lm10,Lm12,Lm18,Lm22,Lm32;
theorem
x is_a_sum_of_squares implies
x is_a_sum_of_products_of_squares &
x is_a_sum_of_amalgams_of_squares &
x is_generated_from_squares by Lm16,Lm24,Lm39;
theorem
x is_a_product_of_squares implies
x is_a_sum_of_products_of_squares &
x is_an_amalgam_of_squares &
x is_a_sum_of_amalgams_of_squares &
x is_generated_from_squares by Lm14,Lm20,Lm26,Lm48;
theorem
x is_a_sum_of_products_of_squares implies
x is_a_sum_of_amalgams_of_squares &
x is_generated_from_squares by Lm28,Lm53;
theorem
x is_an_amalgam_of_squares implies
x is_a_sum_of_amalgams_of_squares &
x is_generated_from_squares by Lm30,Lm43;
Lm54:
f is_a_Sum_of_amalgams_of_squares implies
for i holds i<>0 & i<=len f implies f.:i is_generated_from_squares
proof
assume A1:f is_a_Sum_of_amalgams_of_squares;
defpred P[Nat] means
$1<>0 & $1<=len f implies f.:$1 is_generated_from_squares;
A2: P[0];
A3:for i st P[i] holds P[i+1]
proof
let i such that
A4:i<>0 & i<=len f implies f.:i is_generated_from_squares;
assume A5:(i+1)<>0 & (i+1)<=len f;
A6:now assume i=0;
then f.:(i+1) is_an_amalgam_of_squares
by A1,Def12;
hence thesis by Lm43;
end;
now assume A7: i<>0;
then i<>0 & i<len f by A5,NAT_1:38;
then ex y st
y is_an_amalgam_of_squares & f.:(i+1)=f.:i+y
by A1,Def12;
hence thesis by A4,A5,A7,Lm41,NAT_1:38;
end;
hence thesis by A6;
end;
thus for i holds P[i] from Ind(A2,A3);
end;
theorem
x is_a_sum_of_amalgams_of_squares implies x is_generated_from_squares
proof
assume x is_a_sum_of_amalgams_of_squares;
then consider f such that
A1:f is_a_Sum_of_amalgams_of_squares & x=f.:len f
by Def13;
len f<>0 & len f<=len f by A1,Def12;
hence thesis by A1,Lm54;
end;