:: Lagrange's Four-Square Theorem
:: by Yasushige Watase
::
:: Received June 4, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, FUNCT_1, RELAT_1, ARYTM_3, SUBSET_1, ARYTM_1,
XXREAL_0, INT_2, NAT_1, INT_1, REAL_1, COMPLEX1, SQUARE_1, XCMPLX_0,
ABIAN, FINSEQ_1, CARD_3, ORDINAL4, XBOOLE_0, CARD_2, ORDINAL2, XXREAL_1,
NEWTON, NAT_3, PRE_POLY, LAGRA4SQ, ORDINAL1, TARSKI;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
BINOP_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_1,
FINSEQ_1, SQUARE_1, ARYTM_0, XREAL_0, INT_2, NAT_D, ABIAN, ARYTM_3,
CARD_2, ORDINAL3, XTUPLE_0, XXREAL_1, PEPIN, ABSVALUE, PARTFUN1, NAT_3,
PRE_POLY, VALUED_0, MEMBERED, NEWTON, RVSUM_1, UPROOTS, XXREAL_2;
constructors ARYTM_2, RELSET_1, ARYTM_0, XXREAL_1, ORDINAL3, ABIAN, NAT_D,
PEPIN, CARD_2, XXREAL_2, UPROOTS, NAT_3;
registrations XBOOLE_0, XREAL_0, ORDINAL1, NAT_1, INT_1, FINSET_1, XXREAL_0,
NEWTON, CARD_1, VALUED_0, RELSET_1, NUMBERS, XCMPLX_0, SQUARE_1, FUNCT_2,
FINSEQ_1, ABIAN, NAT_3, PRE_POLY, PREPOWER;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities ORDINAL1, SQUARE_1, FINSEQ_1;
expansions TARSKI, PBOOLE;
theorems XBOOLE_0, AXIOMS, FUNCT_1, FUNCT_2, INT_1, NAT_1, NAT_D, NUMBERS,
XXREAL_0, COMPLEX1, ABIAN, INT_2, XREAL_1, FINSEQ_1, NEWTON, INT_4,
INT_6, CARD_1, CARD_2, RELAT_1, ORDINAL1, FINSEQ_4, POLYFORM, PEPIN,
XXREAL_1, XCMPLX_0, SQUARE_1, NAT_3, XBOOLE_1, PRE_POLY, TARSKI;
schemes FUNCT_2, FINSEQ_1, NAT_1;
begin :: Preliminaries
definition let n be natural number;
attr n is a_sum_of_four_squares means :Sum4Sq:
ex n1,n2,n3,n4 being Nat st n = n1^2 + n2^2 + n3^2 + n4^2;
end;
registration
cluster a_sum_of_four_squares for Nat;
existence
proof
take n = 0;
take 0,0,0,0;
thus thesis;
end;
end;
registration let y be integer object;
cluster |.y.| -> natural;
coherence;
end;
theorem :: Lagrange identity
for n1,n2,n3,n4,m1,m2,m3,m4 being Nat holds
(n1^2 + n2^2 + n3^2 + n4^2) *
(m1^2 + m2^2 + m3^2 + m4^2) =
(n1 * m1 - n2 * m2 - n3 * m3 - n4 * m4) ^2 +
(n1 * m2 + n2 * m1 + n3 * m4 - n4 * m3) ^2 +
(n1 * m3 - n2 * m4 + n3 * m1 + n4 * m2) ^2 +
(n1 * m4 + n2 * m3 - n3 * m2 + n4 * m1) ^2;
registration let m,n be a_sum_of_four_squares Nat;
cluster m * n -> a_sum_of_four_squares;
coherence
proof
consider n1,n2,n3,n4 being Nat such that
A1: n = n1^2 + n2^2 + n3^2 + n4^2 by Sum4Sq;
consider m1,m2,m3,m4 being Nat such that
A2: m = m1^2 + m2^2 + m3^2 + m4^2 by Sum4Sq;
WW: n * m =
(n1 * m1 - n2 * m2 - n3 * m3 - n4 * m4) ^2 +
(n1 * m2 + n2 * m1 + n3 * m4 - n4 * m3) ^2 +
(n1 * m3 - n2 * m4 + n3 * m1 + n4 * m2) ^2 +
(n1 * m4 + n2 * m3 - n3 * m2 + n4 * m1) ^2 by A1,A2;
set z1 = n1 * m1 - n2 * m2 - n3 * m3 - n4 * m4;
set z2 = (n1 * m2 + n2 * m1 + n3 * m4 - n4 * m3);
set z3 = (n1 * m3 - n2 * m4 + n3 * m1 + n4 * m2);
set z4 = (n1 * m4 + n2 * m3 - n3 * m2 + n4 * m1);
reconsider N1 = |. z1 .|, N2 = |. z2 .|, N3 = |. z3 .|, N4 = |. z4 .|
as natural Number;
reconsider N1,N2,N3,N4 as Nat by TARSKI:1;
N1^2 = z1^2 & N2^2 = z2^2 & N3^2 = z3^2 & N4^2 = z4^2 by COMPLEX1:75;
hence thesis by WW;
end;
end;
registration
cluster odd for Prime;
existence by PEPIN:41,POLYFORM:6;
end;
reserve i,j, k,v, w for Nat;
reserve j1,j2, m, n, s, t, x, y for Integer;
reserve p for odd Prime;
definition let p;
func MODMAP_p -> Function of INT, Segm p means :Def1:
for x be Element of INT holds it.x = x mod p;
existence
proof
reconsider p as non zero Nat;
defpred P[Element of INT,object] means $2 = $1 mod p;
A1: for x being Element of INT ex y being Element of Segm p st P[x,y]
proof
let i be Element of INT;
i mod p >= 0 & i mod p < p by NAT_D:62;
reconsider j = i mod p as Element of NAT by INT_1:3;
A3: j < p by NAT_D:62;
reconsider j = i mod p as Element of Segm p by A3,NAT_1:44;
take j;
thus thesis;
end;
consider f being Function of INT, Segm p such that
A4: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1);
thus thesis by A4;
end;
uniqueness
proof
let f,g be Function of INT, Segm p;
assume that
A5: for x be Element of INT holds f.x = x mod p and
A6: for x be Element of INT holds g.x = x mod p;
now
let x be Element of INT;
f.x = x mod p by A5;
hence f.x = g.x by A6;
end;
hence thesis;
end;
end;
definition let v;
func LAG4SQf(v) -> FinSequence of INT means :Def2:
len it = v & for i being Nat st i in dom it holds it.i = (i -1)^2;
existence
proof
defpred P[Nat,object] means $2 = ($1 -1)^2;
A1: for k st k in Seg v ex x being Element of INT st P[k,x]
proof
let k;
assume k in Seg v;
reconsider j = (k - 1)^2 as Element of INT by INT_1:def 2;
take j;
thus thesis;
end;
consider f being FinSequence of INT such that
A2: dom f = Seg v & for k being Nat st k in Seg v holds P[k,f.k]
from FINSEQ_1:sch 5(A1);
take f;
Seg len f = Seg v by FINSEQ_1:def 3,A2;
hence len f = v by FINSEQ_1:6;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of INT;
assume that
A3: len z1 = v and
A4: for i st i in dom z1 holds z1.i = (i-1)^2 and
A5: len z2 = v and
A6: for i st i in dom z2 holds z2.i = (i-1)^2;
A7: dom z1 = Seg len z1 by FINSEQ_1:def 3 .= dom z2 by A3,A5,FINSEQ_1:def 3;
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A8: x in dom z1; then
reconsider x9 = x as Element of NAT;
thus z1.x = (x9 -1)^2 by A4,A8 .= z2.x by A6,A7,A8;
end;
hence thesis by A7,FINSEQ_1:13;
end;
end;
definition let v;
func LAG4SQg(v) -> FinSequence of INT means :Def3:
len it = v & for i being Nat st i in dom it holds it.i = -1 - (i -1)^2;
existence
proof
defpred P[Nat,object] means $2 = -1 - ($1 -1)^2;
A1: for k being Nat st k in Seg v ex x being Element of INT st P[k,x]
proof
let k;
assume k in Seg v;
reconsider j = -1 - (k - 1)^2 as Element of INT by INT_1:def 2;
take j;
thus thesis;
end;
consider f being FinSequence of INT such that
A2: dom f = Seg v & for k being Nat st k in Seg v holds P[k,f.k]
from FINSEQ_1:sch 5(A1);
take f;
Seg len f = Seg v by A2,FINSEQ_1:def 3;
hence len f = v by FINSEQ_1:6;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence of INT;
assume that
A3: len z1 = v and
A4: for i st i in dom z1 holds z1.i = -1 - (i-1)^2 and
A5: len z2 = v and
A6: for i st i in dom z2 holds z2.i = -1 - (i-1)^2;
A7: dom z1 = Seg len z1 by FINSEQ_1:def 3 .= dom z2 by A3,A5,FINSEQ_1:def 3;
for x be Nat st x in dom z1 holds z1.x = z2.x
proof
let x be Nat;
assume
A8: x in dom z1;
thus z1.x = -1 - (x -1)^2 by A4,A8 .= z2.x by A6,A7,A8;
end;
hence thesis by A7,FINSEQ_1:13;
end;
end;
theorem lem1:
LAG4SQf(v) is one-to-one
proof
set f = LAG4SQf v;
for n1, n2 be object st n1 in dom f & n2 in dom f
& f.n1 = f.n2 holds n1 = n2
proof
let n1, n2 be object such that
A1: n1 in dom f and
A2: n2 in dom f and
A3: f.n1 = f.n2;
A4: dom f = Seg len f by FINSEQ_1:def 3.= Seg v by Def2;
consider m1 be Nat such that
A5: n1 = m1 and
A6: 1 <= m1 and
m1 <= v by A1,A4;
consider m2 be Nat such that
A7: n2 = m2 and
A8: 1 <= m2 and
m2 <= v by A2,A4;
f.m1 = f.m2 implies m1 = m2
proof
assume
A11: f.m1 = f.m2;
assume
A12: m1 <> m2;
A13: f.m1 = (m1 - 1)^2 by Def2,A5,A1;
A14: f.m1 - f.m2 =
(m1 - 1)^2 -(m2 - 1)^2 by A13,Def2,A2,A7 .= (m2 + m1 - 2)*(m1 -m2);
A16: m1 + m2 -2 > 0
proof
per cases by A8,XXREAL_0:1;
suppose m2 = 1; then
m1 > 1 by A12,A6,XXREAL_0:1; then
A17: m1 + m2 > 1 + 1 by A8, XREAL_1:8;
m1 + m2 + (-2) > 2 + (-2) by A17,XREAL_1:8;
hence m1 + m2 -2 > 0;
end;
suppose m2 >1; then
A19: m1 + m2 > 1 + 1 by A6,XREAL_1:8;
m1 + m2 + (-2) > 2 + (-2) by A19,XREAL_1:8;
hence m1 + m2 -2 > 0;
end;
end;
m1 - m2 <> 0 by A12;
hence contradiction by A11,A16,A14;
end;
hence thesis by A3,A5,A7;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem lem2:
LAG4SQg v is one-to-one
proof
for n1, n2 be object st n1 in dom LAG4SQg v & n2 in dom LAG4SQg v
& (LAG4SQg v).n1 = (LAG4SQg v).n2 holds n1 = n2
proof
let n1, n2 be object such that
A1: n1 in dom LAG4SQg v and
A2: n2 in dom LAG4SQg v and
A3: (LAG4SQg v).n1 = (LAG4SQg v).n2;
A4: dom LAG4SQg v = Seg len LAG4SQg v by FINSEQ_1:def 3
.= Seg v by Def3;
consider m1 be Nat such that
A5: n1 = m1 and
A6: 1 <= m1 and
m1 <= v by A1,A4;
consider m2 be Nat such that
A7: n2 = m2 and
A8: 1 <= m2 and
m2 <= v by A2,A4;
(LAG4SQg v).m1 = (LAG4SQg v).m2 implies m1 = m2
proof
assume
A11: (LAG4SQg v).m1 = (LAG4SQg v).m2;
assume
A12: m1 <> m2;
A13: (LAG4SQg v).m1 = -1- (m1 - 1)^2 by Def3,A5,A1;
(LAG4SQg v).m2 =-1 - (m2 - 1)^2 by Def3,A2,A7; then
A14: (LAG4SQg v).m1 - (LAG4SQg v).m2 = (m2 + m1 - 2)*(m2 -m1) by A13;
A16: m2 + m1 -2 > 0
proof
per cases by A8,XXREAL_0:1;
suppose m2 = 1; then
A18: m1 > 1 by A6,A12,XXREAL_0:1;
A19: m1 + m2 > 1 + 1 by A8,A18, XREAL_1:8;
m1 + m2 + (-2) > 2 + (-2) by A19,XREAL_1:8;
hence thesis;
end;
suppose m2 >1; then
A20: m1 + m2 > 1 + 1 by A6,XREAL_1:8;
m1 + m2 + (-2) > 2 + (-2) by A20,XREAL_1:8;
hence thesis;
end;
end;
m2 - m1 <> 0 by A12;
hence contradiction by A11,A14,A16;
end;
hence thesis by A5,A7,A3;
end;
hence thesis by FUNCT_1:def 4;
end;
lem3:
p > 2
proof
p > 1 by INT_2:def 4; then
p >= 1 + 1 by INT_1:7;
hence thesis by POLYFORM:5,XXREAL_0:1;
end;
lem3a:
p + 1 > 3
proof
p + 1 > 2 + 1 by lem3,XREAL_1:8;
hence thesis;
end;
reserve a for Real;
reserve b for Integer;
theorem lem4:
for p be odd Prime, s be Nat, j1, j2
st 2*s = p+1 & j1 in rng LAG4SQf s & j2 in rng LAG4SQf s holds
j1 = j2 or j1 mod p <> j2 mod p
proof
let p;
consider s such that
A1: p+1 = 2 * s by ABIAN:11;
s > 0 by A1; then
s in NAT by INT_1:3; then
reconsider s as Nat;
A3: 2*(p - s) = p -1 by A1;
A4: p -1 > 2 -1 by lem3, XREAL_1:14;
A5: p - s > 0 by A3,A4;
A6: p -s + s > 0 + s by A5,XREAL_1:8;
A7: dom (LAG4SQf(s))=Seg len (LAG4SQf(s)) by FINSEQ_1:def 3
.= Seg s by Def2;
for j1, j2 be Integer st j1 in rng (LAG4SQf(s))
& j2 in rng (LAG4SQf s) & j1 <> j2 holds j1 mod p <> j2 mod p
proof
let j1, j2 such that
A8: j1 in rng (LAG4SQf s) and
A9: j2 in rng (LAG4SQf s) and
A10: j1 <> j2;
consider i1 be object such that
A11: i1 in dom (LAG4SQf s) and
A12: j1 = (LAG4SQf s).i1 by A8,FUNCT_1:def 3;
consider i2 be object such that
A13: i2 in dom (LAG4SQf s) and
A14: j2 = (LAG4SQf s).i2 by A9,FUNCT_1:def 3;
reconsider i1,i2 as Nat by A11,A13;
A15: j1 = (i1-1)^2 by A11,A12,Def2;
A16: j2 = (i2-1)^2 by A13,A14,Def2;
A17: j1 - j2 = (i1-1)^2 - (i2-1)^2 by A11,A12,A16,Def2
.= (i1 + i2 -2)*(i1-i2);
A18: j2 - j1 = (i2-1)^2 - (i1-1)^2 by A11,A12,A16,Def2
.= (i2 + i1 -2)*(i2-i1);
consider i9 be Nat such that
A19: i1 = i9 and
A20: 1 <= i9 and
A21: i9 <= s by A7,A11;
consider i0 be Nat such that
A22: i2 = i0 and
A23: 1 <= i0 and
A24: i0 <= s by A7,A13;
A25: i1 + i2 -2 < p
proof
A26: i1 + i2 <= s + s by A19,A21,A22,A24, XREAL_1:7;
i1 + i2 + (-2) < p+1 + (-1) by A1,A26, XREAL_1:8;
hence thesis;
end;
A27: i1 + i2 -2 > 0
proof
per cases by A22,A23,XXREAL_0:1;
suppose i2 = 1; then
A29: i1 > 1 by A10,A12,A14,A19,A20,XXREAL_0:1;
A30: i1 + i2 > 1 + 1 by A22,A23,A29,XREAL_1:8;
i1 + i2 + (-2) > 2 + (-2) by XREAL_1:8,A30;
hence i1 + i2 -2 > 0;
end;
suppose i2 >1; then
A32: i1 + i2 > 1 + 1 by A19,A20,XREAL_1:8;
i1 + i2 + (-2) > 2 + (-2) by A32,XREAL_1:8;
hence i1 + i2 -2 > 0;
end;
end;
A33: i1 - i2 < p & i2 -i1 < p
proof
i1 - i2 <= i1 by XREAL_1:43; then
A34: i1 - i2 <= s by A19,A21, XXREAL_0:2;
i2 - i1 <= i2 by XREAL_1:43; then
i2 - i1 <= s by A22,A24,XXREAL_0:2;
hence thesis by A6,A34,XXREAL_0:2;
end;
j1 mod p <> j2 mod p
proof
per cases by A10,A12,A14,XXREAL_0:1;
suppose i1 > i2; then
A39: i1 - i2 > 0 by XREAL_1:50;
reconsider i1,i2 as Nat;
A40: i1 + i2 -2 in NAT by A27,INT_1:3;
A41: i1 - i2 in NAT by A39, INT_1:3;
(i1 + i2 -2)*(i1-i2) mod p <> 0
proof
assume (i1 + i2 -2)*(i1-i2) mod p = 0; then
A44: (i1 + i2 -2)*(i1-i2) = p * ((i1 + i2 -2)*(i1-i2) div p) + 0
by A40,A41,NAT_D:2;
A45: (i1 + i2 -2)*(i1-i2) div p in NAT by A40,A41,INT_1:3;
p divides (i1 + i2 -2) or p divides (i1-i2)
by A40,A41,A44,A45,NEWTON:80,NAT_D:def 3;
hence contradiction by A25,A27,A33,A39,A40,A41,NAT_D:7;
end;
hence thesis by A15,A16,A17,INT_4:22;
end;
suppose i2 > i1; then
A47: i2 - i1 > 0 by XREAL_1:50;
reconsider i1,i2 as Nat;
reconsider p as Nat;
A48: i2 + i1 -2 in NAT by A27,INT_1:3;
A49: i2 - i1 in NAT by A47,INT_1:3;
(i2 + i1 -2)*(i2-i1) mod p <> 0
proof
assume (i2 + i1 -2)*(i2-i1) mod p = 0; then
A52: (i2 + i1 -2)*(i2-i1) = p * ((i2 + i1 -2)*(i2-i1) div p) + 0
by A48,A49,NAT_D:2;
A53: (i2 + i1 -2)*(i2-i1) div p in NAT by A48,A49,INT_1:3;
p divides (i2 + i1 -2) or p divides (i2-i1)
by A48,A49,A52,A53,NEWTON:80,NAT_D:def 3;
hence contradiction by A25,A27,A47,A33,A48,A49,NAT_D:7;
end;
hence thesis by A15,A16,A18,INT_4:22;
end;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem lem5:
for p be odd Prime, s be Nat, j1, j2
st 2*s = p+1 & j1 in rng LAG4SQg s & j2 in rng LAG4SQg s holds
j1 = j2 or j1 mod p <> j2 mod p
proof
let p;
consider s such that
A1: p+1 = 2 * s by ABIAN:11;
s > 0 by A1; then
s in NAT by INT_1:3; then
reconsider s as Nat;
A4: 2*(p - s) = p - 1 by A1;
p -1 > 2 -1 by lem3, XREAL_1:14; then
p - s > 0 by A4; then
A7: p -s + s > 0 + s by XREAL_1:8;
A8: dom LAG4SQg s = Seg len LAG4SQg s by FINSEQ_1:def 3
.= Seg s by Def3;
for j1, j2 st j1 in rng LAG4SQg s
& j2 in rng LAG4SQg s & j1 <> j2 holds j1 mod p <> j2 mod p
proof
let j1, j2 such that
A9: j1 in rng LAG4SQg s and
A10: j2 in rng LAG4SQg s and
A11: j1 <> j2;
consider i1 be object such that
A12: i1 in dom LAG4SQg s and
A13: j1 = (LAG4SQg s).i1 by A9,FUNCT_1:def 3;
consider i2 be object such that
A14: i2 in dom (LAG4SQg s) and
A15: j2 = (LAG4SQg s).i2 by A10,FUNCT_1:def 3;
reconsider i1,i2 as Nat by A12,A14;
A16: j2 = -1-(i2-1)^2 by A14,A15,Def3;
A17: j2 - j1 = -1-(i2-1)^2 -(-1- (i1-1)^2) by A12,A13,A16,Def3
.= (i1 + i2 -2)*(i1-i2);
A18: j1 - j2 = -1-(i1-1)^2 - (-1-(i2-1)^2) by A12,A13,A16,Def3
.= (i2 + i1 -2)*(i2-i1);
consider i9 be Nat such that
A19: i1 = i9 and
A20: 1 <= i9 and
A21: i9 <= s by A8,A12;
consider i0 be Nat such that
A28: i2 = i0 and
A29: 1 <= i0 and
A30: i0 <= s by A8,A14;
A31: i1 + i2 -2 < p
proof
s + s = p+1 by A1; then
i1 + i2 <= p+1 by A19,A21,A28,A30,XREAL_1:7; then
i1 + i2 + -2 < p+1 + -1 by XREAL_1:8;
hence thesis;
end;
A34: i1 + i2 -2 > 0
proof
per cases by A28,A29,XXREAL_0:1;
suppose i2 = 1; then
i1 > 1 by A11,A13,A15,A19,A20,XXREAL_0:1; then
i1 + i2 > 1 + 1 by A28,A29,XREAL_1:8; then
i1 + i2 + (-2) > 2 + (-2) by XREAL_1:8;
hence i1 + i2 -2 > 0;
end;
suppose i2 > 1; then
i1 + i2 > 1 + 1 by A19,A20,XREAL_1:8; then
i1 + i2 + (-2) > 2 + (-2) by XREAL_1:8;
hence i1 + i2 -2 > 0;
end;
end;
A40: i1 - i2 < p & i2 -i1 < p
proof
i1 - i2 <= i1 by XREAL_1:43; then
A41: i1 - i2 <= s by A19,A21,XXREAL_0:2;
i2 - i1 <= i2 by XREAL_1:43; then
i2 - i1 <= s by A28,A30,XXREAL_0:2;
hence thesis by A7,A41,XXREAL_0:2;
end;
j1 mod p <> j2 mod p
proof
per cases by A11,A13,A15,XXREAL_0:1;
suppose i1 > i2; then
A45: i1 - i2 > 0 by XREAL_1:50;
reconsider i1,i2 as Nat;
reconsider p as Nat;
A46: i1 + i2 -2 in NAT by A34,INT_1:3;
A47: i1 - i2 in NAT by A45, INT_1:3;
A48: (i1 + i2 -2)*(i1-i2) mod p <> 0
proof
assume
A49: (i1 + i2 -2)*(i1-i2) mod p = 0;
A51: (i1 + i2 -2)*(i1-i2) div p in NAT by A46,A47,INT_1:3;
(i1 + i2 -2)*(i1-i2) = p*((i1 + i2 -2)*(i1-i2) div p)+0
by A46,A47,A49,NAT_D:2; then
p divides (i1 + i2 -2) or p divides (i1-i2)
by A46,A47,A51,NAT_D:def 3,NEWTON:80;
hence contradiction by A31,A34,A40,A45,A46,A47,NAT_D:7;
end;
j1 mod p = j2 mod p implies (j2 -j1) mod p = 0
proof
assume
A53: j1 mod p = j2 mod p;
(j2 - j1) mod p = ((j2 mod p) - (j1 mod p)) mod p by INT_6:7
.= 0 by NAT_D:26,A53;
hence thesis;
end;
hence thesis by A17,A48;
end;
suppose i2 > i1; then
A55: i2 - i1 > 0 by XREAL_1:50;
A56: i2 + i1 -2 in NAT by A34,INT_1:3;
A57: i2 - i1 in NAT by A55,INT_1:3;
A58: (i2 + i1 -2)*(i2-i1) mod p <> 0
proof
assume
A59: (i2 + i1 -2)*(i2-i1) mod p = 0;
A61: (i2 + i1 -2)*(i2-i1) div p in NAT by A56,A57,INT_1:3;
(i2 + i1 -2)*(i2-i1) = p * ((i2 + i1 -2)*(i2-i1) div p) + 0
by A56,A57,A59,NAT_D:2; then
p divides (i2 + i1 -2) or p divides (i2-i1)
by A56,A57,A61,NAT_D:def 3,NEWTON:80;
hence contradiction by A31,A34,A40,A55,A56,A57,NAT_D:7;
end;
j1 mod p = j2 mod p implies (j1 -j2) mod p = 0
proof
assume
A63: j1 mod p = j2 mod p;
(j1 - j2) mod p = ((j1 mod p) - (j2 mod p)) mod p by INT_6:7
.= 0 by NAT_D:26,A63;
hence thesis;
end;
hence thesis by A18,A58;
end;
end;
hence thesis;
end;
hence thesis by A1;
end;
begin :: Any prime number can be expressed as the sum of four integer squares
theorem Them1: :: Lagrange lemma
for p holds
ex x1,x2,x3,x4, h be Nat st 0 < h & h < p &
h*p = x1^2 + x2^2 + x3^2 + x4^2
proof
let p;
consider s such that
A1: 2*s = p+1 by ABIAN:11;
s > 0 by A1;then
s in NAT by INT_1:3; then
reconsider s as Nat;
set f = LAG4SQf(s);
set g = LAG4SQg(s);
A5: dom f = Seg len f by FINSEQ_1:def 3 .= Seg s by Def2;
A6: dom g = Seg len g by FINSEQ_1:def 3 .= Seg s by Def3;
A7: f is one-to-one by lem1;
A8: g is one-to-one by lem2;
A9: rng f misses rng g
proof
assume rng f meets rng g; then
consider y be object such that
A12: y in rng f & y in rng g by XBOOLE_0:3;
consider i1 be object such that
A13: i1 in dom f and
A14: y = f.i1 by A12,FUNCT_1:def 3;
consider i2 be object such that
A15: i2 in dom g and
A16: y = g.i2 by A12,FUNCT_1:def 3;
reconsider i1,i2 as Nat by A13,A15;
reconsider y as Integer by A14;
A17: y = (i1 - 1)^2 by A13,Def2,A14;
y = -1 - (i2 - 1)^2 by A15,Def3,A16;
hence contradiction by A17;
end;
A19: card rng (g^f) = p+1
proof
A20: card rng f = card dom f by A7,CARD_1:70
.= card (Seg len f) by FINSEQ_1:def 3 .= card (Seg s) by Def2
.= s by FINSEQ_1:57;
A21: card rng g = card dom g by A8,CARD_1:70
.= card (Seg len g) by FINSEQ_1:def 3 .= card (Seg s) by Def3
.= s by FINSEQ_1:57;
card(rng(g^f)) = card (rng g \/ rng f) by FINSEQ_1:31
.= card rng g +` card rng f by A9,CARD_2:35
.= card (s +^ s) by CARD_2:def 1,A20,A21
.= card (s + s) by CARD_2:36 .= p+1 by A1;
hence thesis;
end;
A23: rng(g^f) = rng g \/ rng f by FINSEQ_1:31;
A24: dom MODMAP_p = INT by FUNCT_2:def 1;
AAA: rng (g^f) c= INT by RELAT_1:def 19;
then
A25: card dom ((MODMAP_p)|rng (g^f)) = p+1 by A19,A24,RELAT_1:62;
A26: card rng ((MODMAP_p)|rng (g^f)) <= card Segm p by NAT_1:43;
set s1 = card rng ((MODMAP_p)|rng (g^f));
set t1 = card dom ((MODMAP_p)|rng (g^f));
s1 < t1 by A25,A26,NAT_1:13; then
A28: s1 in { i where i is Nat: i < t1 };
A29: dom ((MODMAP_p)|rng (g^f)) <> {} by A25;
set A = dom ((MODMAP_p)|rng (g^f));
set B = rng ((MODMAP_p)|rng (g^f));
defpred P[object,object] means
ex m1 being Element of INT st $1 in A &
$2=m1 & ((MODMAP_p)|rng (g^f)).$1 = m1;
A30: card B in card A by A28,AXIOMS:4;
A31: for x being object st x in A ex y being object st y in B & P[x,y]
proof
let x be object;
assume
A32: x in A;
take y = ((MODMAP_p)|rng (g^f)).x;
y in B by A32,FUNCT_1:3; then
y in Segm p; then
y in { i where i is Nat : i < p } by AXIOMS:4; then
consider j be Nat such that
A36: y = j & j < p;
y in INT by A36,ORDINAL1:def 12, NUMBERS:17;
hence thesis by FUNCT_1:3,A32;
end;
consider h be Function of A,B such that
A38: for x being object st x in A holds P[x,h.x] from FUNCT_2:sch 1(A31);
consider m1,m2 be object such that
A39: m1 in A and
A40: m2 in A and
A41: m1 <> m2 and
A42: h.m1 = h.m2 by A29,A30,RELAT_1:42,FINSEQ_4:65;
A43: P[m1,h.m1] by A38,A39;
A44: P[m2,h.m2] by A38,A40;
reconsider m1,m2 as Element of INT by A39,A40;
A46: ((MODMAP_p)|rng (g^f)).m1 = (MODMAP_p).m1 by A39,FUNCT_1:47
.= m1 mod p by Def1;
A47: ((MODMAP_p)|rng (g^f)).m2 = (MODMAP_p).m2 by A40,FUNCT_1:47
.= m2 mod p by Def1;
A49: A = dom (MODMAP_p) /\ rng (g^f) by RELAT_1:61
.= rng (g^f) by AAA,A24,XBOOLE_1:28;
A50: m1 in rng f implies m2 in rng g
proof
assume
A51: m1 in rng f;
assume not m2 in rng g; then
m2 in rng f by A23,A40,A49,XBOOLE_0:def 3;
hence contradiction by A1,A41,A47,A44,A42,A43,A46,A51,lem4;
end;
A54: m1 in rng g implies m2 in rng f
proof
assume
A55: m1 in rng g;
assume not m2 in rng f; then
m2 in rng g by A23,A40,A49,XBOOLE_0:def 3;
hence contradiction by A1,A41,A47,A44,A42,A43,A46,A55,lem5;
end;
ex x1, x2, x3,x4,h be Nat st h > 0 & h < p &
h*p = x1^2 + x2^2 + x3^2 + x4^2
proof
A60: p*p" = 1 by XCMPLX_0:def 7;
per cases by A23,A39,A49,XBOOLE_0:def 3;
suppose
A61: m1 in rng f; then
consider x0 be object such that
A62: x0 in dom f and
A63: m1 = f.x0 by FUNCT_1:def 3;
reconsider x0 as Nat by A62;
A64: m1 = (x0-1)^2 by Def2,A62,A63;
consider y0 be object such that
A65: y0 in dom g and
A66: m2 = g.y0 by A50,A61,FUNCT_1:def 3;
reconsider y0 as Nat by A65;
A67: m2 = -1 - (y0-1)^2 by Def3,A65,A66;
(m1 - m2) mod p = ((m1 mod p) - (m2 mod p)) mod p by INT_6:7
.= 0 by A47,A44,A42,A43,A46,NAT_D:26; then
A69: (m1 - m2) - ((m1 - m2) div p) * p = 0 by INT_1:def 10;
A70: (m1 - m2) div p > 0 by A64,A67,A69;
consider x9 be Nat such that
A71: x0 = x9 and
A72: 1 <= x9 and
A73: x9 <= s by A5,A62;
A74: 1-1 <= x9 - 1 by A72,XREAL_1:9;
consider y9 be Nat such that
A75: y0 = y9 and
A76: 1 <= y9 and
A77: y9 <= s by A6,A65;
A78: 1-1 <= y9 - 1 by A76,XREAL_1:9;
x9 - 1 <= s - 1 by A73,XREAL_1:9; then
A80: (x9 - 1)^2 <= (s - 1)^2 by A74,XREAL_1:66;
y9-1 <= s -1 by A77,XREAL_1:9; then
(y9 - 1)^2 <= (s-1)^2 by A78,XREAL_1:66; then
(x9 - 1)^2 + (y9 - 1)^2 <= (s-1)^2+(s-1)^2 by A80,XREAL_1:7; then
A84: (x0 - 1)^2 + (y0 - 1)^2 + 1 <= (s-1)^2 + (s-1)^2 + 1
by A71,A75,XREAL_1:7;
A85: p^2 = (2*s -1)^2 by A1;
2*s -2 > 3 -2 by A1,XREAL_1:9,lem3a; then
A86: (s+1)*(2*s-2) > 0;
A87: p^2 - ((s-1)^2 + (s-1)^2 + 1) + ((s-1)^2 + (s-1)^2 + 1)
> 0 + ((s-1)^2 + (s-1)^2 + 1) by A85,A86,XREAL_1:6;
A89: x0 -1 in NAT by A71,A74,INT_1:3;
A90: y0 -1 in NAT by A75,A78,INT_1:3;
set h = (m1 - m2) div p;
h in NAT by A70,INT_1:3; then
reconsider h as Nat;
A92: h > 0 by A69,A64,A67;
consider x1,x2,x3,x4 be Nat such that
A93: x1 = x0 -1 and
A94: x2 = y0 -1 and
A95: x3 = 1 and
A96: x4 = 0 by A89,A90;
A97: (x0-1)^2 + (y0-1)^2 + 1 = x1^2 + x2^2 + x3^2 + x4^2
by A96,A95,A94,A93;
h*p < p*p by A69,A64,A67,A84,A87,XXREAL_0:2; then
h*p*p" < p*p*p" by XREAL_1:68; then
h*(p*p") < p*(p*p");
hence thesis by A92,A69,A64,A67,A97,A60;
end;
suppose
A101: m1 in rng g;
consider x0 be object such that
A102: x0 in dom f and
A103: m2 = f.x0 by A54,A101,FUNCT_1:def 3;
reconsider x0 as Nat by A102;
consider y0 be object such that
A104: y0 in dom g and
A105: m1 = g.y0 by A101,FUNCT_1:def 3;
reconsider y0 as Nat by A104;
A106: m1 = -1 - (y0-1)^2 by A104,A105,Def3;
(m2 - m1) mod p = ((m2 mod p) - (m1 mod p)) mod p by INT_6:7
.= 0 by A47,A44,A42,A43,A46,NAT_D:26; then
(m2 - m1) - ((m2 - m1) div p) * p = 0 by INT_1:def 10; then
A109: (x0-1)^2-(-1-(y0-1)^2)=((m2-m1) div p) * p by A102,A103,A106,Def2;
A110: (m2 - m1) div p >= 0 by A109;
consider x9 be Nat such that
A111: x0 = x9 and
A112: 1 <= x9 and
A113: x9 <= s by A102,A5;
A114: 1-1 <= x9 - 1 by A112,XREAL_1:9;
consider y9 be Nat such that
A115: y0 = y9 and
A116: 1 <= y9 and
A117: y9 <= s by A6,A104;
A118: 1-1 <= y9 - 1 by A116,XREAL_1:9;
x9 - 1 <= s - 1 by A113,XREAL_1:9; then
A120: (x9 - 1)^2 <=(s - 1)^2 by A114,XREAL_1:66;
y9-1 <= s -1 by A117,XREAL_1:9; then
(y9 - 1)^2 <=(s-1)^2 by A118,XREAL_1:66; then
(x9 - 1)^2 + (y9-1)^2 <= (s-1)^2+(s-1)^2 by A120,XREAL_1:7; then
A124: (x0 - 1)^2 + (y0-1)^2+1<=(s-1)^2+(s-1)^2+1 by A111,A115,XREAL_1:7;
A125: p^2 = (2*s -1)^2 by A1;
2*s -2 > 3 -2 by A1,XREAL_1:9,lem3a; then
(s+1)*(2*s-2) > 0; then
A127: p^2 - ((s-1)^2 + (s-1)^2 + 1) + ((s-1)^2 + (s-1)^2 + 1)
> 0 + ((s-1)^2 + (s-1)^2 + 1) by A125,XREAL_1:6;
set h = (m2 - m1) div p;
h in NAT by A110,INT_1:3; then
reconsider h as Nat;
A129: x0 -1 in NAT by A114,A111,INT_1:3;
A130: y0 -1 in NAT by INT_1:3, A115,A118;
A132: h > 0 by A109;
consider x1,x2,x3,x4 be Nat such that
A133: x1 = x0 -1 & x2 = y0 -1 & x3 = 1 & x4 = 0 by A129,A130;
A134: (x0-1)^2 + (y0-1)^2 + 1 = x1^2 + x2^2 + x3^2 + x4^2 by A133;
h*p < p*p by A109,A124,A127,XXREAL_0:2; then
h*p*p" < p*p*p" by XREAL_1:68; then
h*(p*p") < p*(p*p");
hence thesis by A60,A109,A132,A134;
end;
end;
hence thesis;
end;
theorem Them2: ::: Lagrange Lemma
for x1, h be Nat st 1 < h holds
ex y1 be Integer st x1 mod h = y1 mod h & -h < 2*y1 & 2*y1 <= h &
x1^2 mod h = y1^2 mod h
proof
let x1,h be Nat;
assume
A1: 1 < h;
reconsider h1 = h as Real;
consider q1,r1 be Integer such that
A2: x1 = (h*q1) + r1 and
A3: 0 <= r1 and
A4: r1 < h by INT_4:13,A1;
A5: r1 in [.0,h1.[ by A3,A4,XXREAL_1:3;
h1/2 < h1 by A1,XREAL_1:216; then
A7: [.0,h1.[ = [.0,h1/2.] \/ ].h1/2,h1.[ by XXREAL_1:169;
ex y1 be Integer st x1 mod h = y1 mod h & -h < 2*y1 & 2*y1 <= h &
x1^2 mod h = y1^2 mod h
proof
per cases by A5,A7,XBOOLE_0:def 3;
suppose
A9: r1 in [.0,h1/2.]; then
A10: 0 <= r1 & r1 <= h1/2 by XXREAL_1:1;
r1 <= h1/2 & 0<= 2 by A9,XXREAL_1:1; then
A12: 2*r1 <= 2*(h1/2) by XREAL_1:64;
A13: r1 in NAT by A10,INT_1:3;
consider y1 be Integer such that
A14: y1 = r1;
A15: 0 <= y1 & 2*y1 <= h1 by A9,A12,A14,XXREAL_1:1;
h divides (x1 - y1) by A2,A14,INT_1:def 3; then
A17: x1 mod h = y1 mod h by A1,A13,A14,INT_4:23;
x1^2 mod h = ((x1 mod h)*(x1 mod h)) mod h by NAT_D:67 .=
y1^2 mod h by NAT_D:67,A17;
hence thesis by A1,A15,A17;
end;
suppose
A19: r1 in ].h1/2,h1.[; then
A20: h1/2 < r1 & r1 < h1 by XXREAL_1:4;
r1 > 0 by A19,XXREAL_1:4; then
A22: r1 in NAT by INT_1:3;
set y1 = r1 - h;
h divides (x1 - (y1 + h)) by A2,INT_1:def 3; then
A24: x1 mod h = (y1 + h) mod h by A1,A22,INT_4:23
.= ( (y1 mod h) + (h mod h)) mod h by NAT_D:66
.= ( (y1 mod h) + 0) mod h by NAT_D:25
.= y1 mod h by NAT_D:65;
A25: x1^2 mod h = ((x1 mod h)*(x1 mod h)) mod h by NAT_D:67 .=
y1^2 mod h by NAT_D:67,A24;
A26: h1/2 -h < r1 - h by A20,XREAL_1:9;
r1 - h < h1 - h by A20,XREAL_1:9; then
2*(-h1/2) < 2*y1 & 2*y1 <= 2*(h1/2) by A26,XREAL_1:68;
hence thesis by A24,A25;
end;
end;
hence thesis;
end;
theorem lem7:
for i1,i2, c be Nat st i1 <= c & i2 <= c holds
i1+i2 < 2*c or (i1 = c & i2 = c)
proof
let i1,i2, c be Nat;
assume that
A1: i1 <= c and
A2: i2 <= c;
i1 in [.0,c.] by A1,XXREAL_1:1; then
A3: i1 in [.0,c.[ or i1 = c by XXREAL_1:7;
i2 in [.0,c.] by A2,XXREAL_1:1; then
A4: i2 in [.0,c.[ or i2 = c by XXREAL_1:7;
per cases by A3,XXREAL_1:3,A4;
suppose i1 = c & i2 = c;
hence thesis;
end;
suppose 0 <= i1 & i1 < c & 0 <= i2 & i2 < c; then
i1 + i2 < c + c by XREAL_1:8;
hence thesis;
end;
suppose 0 <= i1 & i1 < c & i2 = c; then
i1 + i2 < c + c by XREAL_1:8;
hence thesis;
end;
suppose 0 <= i2 & i2 < c & i1 = c; then
i1 + i2 < c + c by XREAL_1:8;
hence thesis;
end;
end;
theorem lem8:
for i1,i2,i3,i4, c be Nat st i1 <= c & i2 <= c & i3 <= c & i4 <= c holds
i1+i2 + i3 + i4 < 4*c or (i1 = c & i2 = c & i3 = c & i4 = c)
proof
let i1,i2,i3,i4, c be Nat;
assume that
A1: i1 <= c and
A2: i2 <= c and
A3: i3 <= c and
A4: i4 <= c;
per cases by A1,A2, A3,A4,lem7;
suppose i1+i2 < 2*c & i3+i4 < 2*c; then
(i1 + i2) + (i3 + i4) < 2*c +2*c by XREAL_1:8;
hence thesis;
end;
suppose i1+i2 < 2*c & i3 = c & i4 = c; then
(i1+i2) + (i3 +i4) < 2*c + 2*c by XREAL_1:8;
hence thesis;
end;
suppose (i1 = c & i2 = c) & i3+i4 < 2*c; then
(i1+i2) + (i3 +i4) < 2*c + 2*c by XREAL_1:8;
hence thesis;
end;
suppose i1 = c & i2 = c & i3 = c & i4 = c;
hence thesis;
end;
end;
theorem lem9:
for x1,h be Nat, y1 be Integer st 1 < h & x1 mod h = y1 mod h & -h < 2*y1
& (2*y1)^2 = h^2 holds 2*y1 = h
& ex m1 be Nat st 2*x1 = (2*m1 +1) * h
proof
let x1, h be Nat, y1 be Integer;
assume that
A1: 1 < h and
A2: x1 mod h = y1 mod h and
A3: -h < 2*y1 and
A4: (2*y1)^2 = h^2;
A7: 2*y1 = h by A3,A4,SQUARE_1:40;
reconsider h as Integer;
set h1 = h;
y1 > 0 by A1,A3,A4,SQUARE_1:40; then
y1 in NAT by INT_1:3; then
h divides (x1 -y1) by A1,A2,INT_4:23; then
consider m1 be Integer such that
A9: (x1 - y1) = h*m1 by INT_1:def 3;
A10: x1 = (2*m1 +1)*h1/2 by A7,A9;
A12: (2*m1 +1)*(h1/2)*(h1/2)" >= 0*(h1/2)" by A7,A9;
(h1/2)*(h1/2)" = 1 by A1,XCMPLX_0:def 7; then
(2*m1 +1) = (2*m1 +1)*((h1/2)*(h1/2)"); then
2*m1 +1 +(- 1) >= 0+(-1) by A12,XREAL_1:6; then
2*m1*2" >= (-1)*2" by XREAL_1:64; then
m1 > -1 by XXREAL_0:2; then
m1 >= -1 +1 by INT_1:7; then
m1 in NAT by INT_1:3;
hence thesis by A3,A4,A10,SQUARE_1:40;
end;
theorem lem10:
for x1,h be Nat, y1 be Integer st 1 < h & x1 mod h = y1 mod h
& y1 = 0 holds ex m1 be Integer st x1 = h*m1
proof
let x1, h be Nat, y1 be Integer;
assume that
A1: 1 < h and
A2: x1 mod h = y1 mod h and
A3: y1 = 0;
A5: x1 mod h = 0 by NAT_D:26,A2,A3;
reconsider x1 as Integer;
A6: h divides x1 by A1,A5,INT_1:62;
reconsider h as Integer;
thus thesis by A6,INT_1:def 3;
end;
theorem Them5:
for p be odd Prime, x1,x2,x3,x4, h be Nat
st 1 < h & h < p & h*p = x1^2 + x2^2 + x3^2 + x4^2
holds ex y1,y2,y3,y4 be Integer, r be Nat st 0 < r & r < h &
r*p = y1^2 + y2^2 + y3^2 + y4^2
proof
let p;
let x1, x2,x3,x4, h be Nat;
assume that
A1: 1 < h and
A2: h < p and
A3: h*p = x1^2 + x2^2 + x3^2 + x4^2;
set h1 = h;
consider y1 be Integer such that
A4: x1 mod h = y1 mod h and
A5: -h < 2*y1 and
A6: 2*y1 <= h and
A7: x1^2 mod h = y1^2 mod h by A1,Them2;
consider y2 be Integer such that
A8: x2 mod h = y2 mod h and
A9: -h < 2*y2 and
A10: 2*y2 <= h and
A11: x2^2 mod h = y2^2 mod h by A1,Them2;
consider y3 be Integer such that
A12: x3 mod h = y3 mod h and
A13: -h < 2*y3 and
A14: 2*y3 <= h and
A15: x3^2 mod h = y3^2 mod h by A1,Them2;
consider y4 be Integer such that
A16: x4 mod h = y4 mod h and
A17: -h < 2*y4 and
A18: 2*y4 <= h and
A19: x4^2 mod h = y4^2 mod h by A1,Them2;
A20: (x1^2 + x2^2) mod h = ((x1^2 mod h) +( x2^2 mod h)) mod h by NAT_D:66
.= (y1^2 + y2^2) mod h by NAT_D:66,A11,A7;
A21: (x3^2 + x4^2) mod h = ((x3^2 mod h) +( x4^2 mod h)) mod h by NAT_D:66
.= (y3^2 + y4^2) mod h by NAT_D:66,A19,A15;
0 = ((x1^2 + x2^2) + (x3^2 + x4^2)) mod h by A3
.= (((x1^2 + x2^2) mod h) + ((x3^2 + x4^2) mod h)) mod h by NAT_D:66
.= ((y1^2 + y2^2) + (y3^2 + y4^2)) mod h by NAT_D:66,A21,A20
.= (y1^2 + y2^2 + y3^2 + y4^2) mod h; then
A22: 0 = (y1^2 + y2^2 + y3^2 + y4^2)-((y1^2 + y2^2 + y3^2 + y4^2) div h)*h
by A1,INT_1:def 10;
set r = (y1^2 + y2^2 + y3^2 + y4^2) div h;
set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4;
set z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3;
set z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2;
set z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
A25: z1^2 + z2^2 + z3^2 + z4^2
= (x1^2 + x2^2 +x3^2 + x4^2)*(y1^2 + y2^2 +y3^2 + y4^2)
.= (h*p) * (r*h) by A22,A3 .= p*h^2*r;
A26: x1^2 mod h = ((x1 mod h)*(x1 mod h)) mod h by NAT_D:67
.= x1*y1 mod h by NAT_D:67,A4;
A27: x2^2 mod h = ((x2 mod h)*(x2 mod h)) mod h by NAT_D:67
.= x2*y2 mod h by NAT_D:67,A8;
A28: x3^2 mod h = ((x3 mod h)*(x3 mod h)) mod h by NAT_D:67
.= x3*y3 mod h by NAT_D:67,A12;
A29: x4^2 mod h = ((x4 mod h)*(x4 mod h)) mod h by NAT_D:67
.= x4*y4 mod h by NAT_D:67,A16;
A30: (x1*y1 + x2*y2)mod h =((x1*y1 mod h) + (x2*y2 mod h)) mod h by NAT_D:66
.= (x1^2 + x2^2) mod h by NAT_D:66,A27,A26;
A31: (x3*y3 + x4*y4)mod h =((x3*y3 mod h) + (x4*y4 mod h)) mod h by NAT_D:66
.= (x3^2 + x4^2) mod h by NAT_D:66,A29,A28;
A32: z1 mod h = ((x1*y1+x2*y2)+(x3*y3+x4*y4)) mod h
.= ( ((x1*y1+x2*y2) mod h)+ ((x3*y3 + x4*y4) mod h)) mod h by NAT_D:66
.= ( (x1^2 + x2^2) + (x3^2 + x4^2)) mod h by NAT_D:66,A31,A30
.= 0 by A3;
A33: x1*y2 mod h = ((x1 mod h)*(y2 mod h)) mod h by NAT_D:67
.= x1*x2 mod h by NAT_D:67,A8;
A34: x2*y1 mod h = ((x2 mod h)*(y1 mod h)) mod h by NAT_D:67
.= x2*x1 mod h by NAT_D:67,A4;
A35: x3*y4 mod h = ((x3 mod h)*(y4 mod h)) mod h by NAT_D:67
.= x3*x4 mod h by NAT_D:67,A16;
A36: x4*y3 mod h = ((x4 mod h)*(y3 mod h)) mod h by NAT_D:67
.= x4*x3 mod h by NAT_D:67,A12;
A37: (-x1*y2 + x2*y1)mod h = (x2*y1 -x1*y2) mod h .=
((x2*y1 mod h) - (x1*y2 mod h)) mod h by INT_6:7 .=
0 by NAT_D:26,A33,A34;
A38: (- x3*y4 + x4*y3) mod h = (x4*y3 -x3*y4) mod h .=
((x4*x3 mod h) - (x3*x4 mod h)) mod h by A35,A36,INT_6:7
.= 0 by NAT_D:26;
A39: z2 mod h = ((-x1*y2 + x2*y1) + (-x3*y4 + x4*y3)) mod h
.= (((-x1*y2+x2*y1) mod h)+((-x3*y4 + x4*y3) mod h)) mod h by NAT_D:66
.= 0 by NAT_D:26,A38,A37;
A40: x1*y3 mod h = ((x1 mod h)*(y3 mod h)) mod h by NAT_D:67
.= x1*x3 mod h by NAT_D:67,A12;
A41: x2*y4 mod h = ((x2 mod h)*(y4 mod h)) mod h by NAT_D:67
.= x2*x4 mod h by NAT_D:67,A16;
A42: x3*y1 mod h = ((x3 mod h)*(y1 mod h)) mod h by NAT_D:67
.= x3*x1 mod h by NAT_D:67,A4;
A43: x4*y2 mod h = ((x4 mod h)*(y2 mod h)) mod h by NAT_D:67
.= x4*x2 mod h by NAT_D:67,A8;
A44: (x1*y3 - x3*y1)mod h = ((x1*y3 mod h) - (x3*y1 mod h))mod h by INT_6:7
.= 0 by NAT_D:26,A42,A40;
A45: (x4*y2 - x2*y4) mod h = ((x4*y2 mod h) - (x2*y4 mod h))mod h by INT_6:7
.= 0 by NAT_D:26,A41,A43;
A46: z3 mod h = ((x1*y3 - x3*y1) + (x4*y2 - x2*y4)) mod h
.= (((x1*y3 - x3*y1) mod h)+((x4*y2 - x2*y4) mod h)) mod h by NAT_D:66
.= 0 by NAT_D:26,A45,A44;
A47: x1*y4 mod h = ((x1 mod h)*(y4 mod h)) mod h by NAT_D:67
.= x1*x4 mod h by NAT_D:67,A16;
A48: x2*y3 mod h = ((x2 mod h)*(y3 mod h)) mod h by NAT_D:67
.= x2*x3 mod h by NAT_D:67,A12;
A49: x3*y2 mod h = ((x3 mod h)*(y2 mod h)) mod h by NAT_D:67
.= x3*x2 mod h by NAT_D:67,A8;
A50: x4*y1 mod h = ((x4 mod h)*(y1 mod h)) mod h by NAT_D:67
.= x4*x1 mod h by NAT_D:67,A4;
A51: (x1*y4 - x4*y1)mod h = ((x1*y4 mod h) - (x4*y1 mod h))mod h by INT_6:7
.= 0 by NAT_D:26,A50,A47;
A52: (x2*y3 - x3*y2) mod h = ((x2*y3 mod h) - (x3*y2 mod h))mod h by INT_6:7
.= 0 by NAT_D:26,A49,A48;
A53: z4 mod h = ((x1*y4 - x4*y1) + (x2*y3 - x3*y2)) mod h
.= (((x1*y4 - x4*y1) mod h)+((x2*y3 - x3*y2) mod h)) mod h by NAT_D:66
.= 0 by NAT_D:26,A52,A51;
h divides z1 by A1,A32,INT_1:62; then
consider t1 be Integer such that
A55: z1 = h*t1 by INT_1:def 3;
h divides z2 by A1,A39,INT_1:62; then
consider t2 be Integer such that
A57: z2 = h*t2 by INT_1:def 3;
h divides z3 by A1,A46,INT_1:62; then
consider t3 be Integer such that
A59: z3 = h*t3 by INT_1:def 3;
h divides z4 by A1,A53,INT_1:62; then
consider t4 be Integer such that
A61: z4 = h*t4 by INT_1:def 3;
A62: h^2*p*r = (h*t1)^2+(h*t2)^2+(h*t3)^2+(h*t4)^2 by A61,A59,A57,A55,A25
.= h1^2*(t1^2 + t2^2 + t3^2 + t4^2);
(h^2)"*h^2 = 1 by A1,XCMPLX_0:def 7; then
A64: p*r = (h^2)"*h^2 *p*r .=(h^2)"*(h^2 *p*r)
.=(h^2)"* ( h^2*(t1^2 + t2^2 + t3^2 + t4^2)) by A62
.=(h^2)"* h^2*(t1^2 + t2^2 + t3^2 + t4^2)
.= 1*(t1^2 + t2^2 + t3^2 + t4^2) by A1,XCMPLX_0:def 7
.= t1^2 + t2^2 + t3^2 + t4^2;
A65: (2*y1)^2 <= h^2 by A5,A6,SQUARE_1:49;
A66: (2*y2)^2 <= h^2 by A9,A10,SQUARE_1:49;
A67: (2*y3)^2 <= h^2 by A13,A14,SQUARE_1:49;
A68: (2*y4)^2 <= h^2 by A17,A18,SQUARE_1:49;
A69: r <= h
proof
A70: 4*y1^2 + 4*y2^2 <= h^2 + h^2 by A65,A66,XREAL_1:7;
4*y3^2 + 4*y4^2 <= h^2 + h^2 by A67,A68,XREAL_1:7; then
(4*y1^2 + 4*y2^2) + (4*y3^2 + 4*y4^2) <= (h^2 + h^2) + (h^2 + h^2)
by A70,XREAL_1:7; then
4"*(4*r*h) <= 4"*(4*h^2) by A22,XREAL_1:64;then
(r*h)*h" <= (h^2)*h" by XREAL_1:64; then
A74: r*(h*h") <= h*(h*h");
h*h" = 1 by A1,XCMPLX_0:def 7;
hence thesis by A74;
end;
A76: r <> h
proof
assume
A77: r = h;
per cases by A65,A66,A67,A68,lem8;
suppose (2*y1)^2 + (2*y2)^2 + (2*y3)^2 + (2*y4)^2 < 4*h^2;
hence contradiction by A22,A77;
end;
suppose that
A79: (2*y1)^2 = h^2 and
A80: (2*y2)^2 = h^2 and
A81: (2*y3)^2 = h^2 and
A82: (2*y4)^2 = h^2;
reconsider h as Integer;
reconsider h1 = h as Real;
A83: h is even by A79;
consider m1 be Nat such that
A84: 2*x1 = (2*m1 +1) * h by A1,A4,A5,A79,lem9;
consider m2 be Nat such that
A85: 2*x2 = (2*m2 +1) * h by A1,A8,A9,A80,lem9;
consider m3 be Nat such that
A86: 2*x3 = (2*m3 +1) * h by A1,A12,A13,A81,lem9;
consider m4 be Nat such that
A87: 2*x4 = (2*m4 +1) * h by A1,A16,A17,A82,lem9;
p*h1 = ((2*m1 +1) * h1/2)^2 + ((2*m2 +1) * h1/2)^2 +
((2*m3 +1) * h1/2)^2 + ((2*m4 +1) * h1/2)^2 by A84,A85,A86,A87,A3
.= (m1^2+m1+m2^2+m2+m3^2+m3+m4^2+m4+1)*h1*h1; then
p*h1*h1" = (m1^2+m1+m2^2+m2+m3^2+m3+m4^2+m4+1)*h1*h1*h1";then
A88: p*(h1*h1") = (m1^2+m1+m2^2+m2+m3^2+m3+m4^2+m4+1)*h1*(h1*h1");
h1*h1" = 1 by A1,XCMPLX_0:def 7;
hence contradiction by A83,A88;
end;
end;
reconsider x1 as Integer;
A90: r <> 0
proof
assume r = 0; then
A92: y1 = 0 & y2 = 0 & y3 = 0 & y4 = 0 by A22; then
consider m1 be Integer such that
A93: x1 = h*m1 by A1,A4,lem10;
consider m2 be Integer such that
A94: x2 = h*m2 by A1,A8,A92,lem10;
consider m3 be Integer such that
A95: x3 = h*m3 by A1,A12,A92,lem10;
consider m4 be Integer such that
A96: x4 = h*m4 by A1,A16,A92,lem10;
h*p*h" = ((m1^2) + (m2^2) + (m3^2) + (m4^2))*h*h*h"
by A93,A94,A95,A96,A3; then
A99: (h*h")*p = ((m1^2) + (m2^2) + (m3^2) + (m4^2))*h*(h*h");
A100: h*h" = 1 by A1,XCMPLX_0:def 7;
reconsider p as Integer;
A101: h divides p by A99,A100,INT_1:def 3;
reconsider p as odd Prime;
per cases by A101,INT_2:def 4;
suppose h = 1;
hence contradiction by A1;
end;
suppose h = p;
hence contradiction by A2;
end;
end;
r < h by A69,A76,XXREAL_0:1;
hence thesis by A90,A64;
end;
Them3:
for p holds ex x1,x2,x3,x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2
proof
let p;
defpred P[Nat]
means ex x1,x2,x3,x4 be Integer st 0 < $1 & $1 < p &
$1*p = x1^2 + x2^2 + x3^2 + x4^2;
A1: ex h be Nat st P[h]
proof
consider x1, x2,x3,x4, h1 be Nat such that
A3: h1 > 0 and
A4: h1 < p and
A5: h1*p = x1^2 + x2^2 + x3^2 + x4^2 by Them1;
thus thesis by A3,A4,A5;
end;
A7: ex h being Nat st P[h] & for n being Nat st P[n] holds h <= n from
NAT_1:sch 5(A1);
consider h0 be Nat such that
A8: P[h0] and
A9: for n be Nat st P[n] holds h0 <= n by A7;
consider x1,x2,x3,x4 be Integer such that
A11: h0*p = x1^2 + x2^2 + x3^2 + x4^2 by A8;
A13: h0 >= 0 + 1 by A8,INT_1:7;
reconsider z1 = |. x1 .|, z2 = |. x2 .|, z3 = |. x3 .|,z4 = |. x4 .|
as natural set by TARSKI:1;
A16: z1^2 = x1^2 & z2^2 = x2^2 & z3^2 = x3^2 & z4^2 = x4^2
by COMPLEX1:75;
h0 = 1
proof
assume
A19: h0 <> 1;
per cases by A19,XXREAL_0:1;
suppose
A21: h0 > 1;
consider y1,y2,y3,y4 be Integer, h1 be Nat such that
A23: 0 < h1 and
A24: h1 < h0 and
A25: h1*p = y1^2 + y2^2 + y3^2 + y4^2 by A8,A11,A16,A21,Them5;
h1 < p by A24,A8,XXREAL_0:2;
hence contradiction by A9,A23,A24,A25;
end;
suppose h0 < 1;
hence contradiction by A13;
end;
end;
hence thesis by A11,A16;
end;
theorem
for p be Prime st p is even holds p = 2 by ABIAN:def 1,INT_2:def 4;
Them4:
for p be Prime st p is even holds
ex x1, x2, x3, x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2
proof
let p be Prime;
assume
A1: p is even;
reconsider p as Integer;
set x1 = 1, x2 = 1, x3 = 0, x4 = 0;
p = x1^2 + x2^2 + x3^2 + x4^2 by A1,ABIAN:def 1,INT_2:def 4;
hence thesis;
end;
theorem Them5:
for p be Prime holds
ex x1,x2,x3,x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2
proof
let p be Prime;
per cases;
suppose p is even;
hence thesis by Them4;
end;
suppose p is odd;
hence thesis by Them3;
end;
end;
theorem Prime4Sq:
for p1, p2 be Prime holds
ex x1,x2,x3,x4 be Nat st p1*p2 = x1^2 + x2^2 + x3^2 + x4^2
proof
let p1, p2 be Prime;
consider x1,x2,x3,x4 be Nat such that
A3: p1 = x1^2 + x2^2 + x3^2 + x4^2 by Them5;
consider y1,y2,y3,y4 be Nat such that
A4: p2 = y1^2 + y2^2 + y3^2 + y4^2 by Them5;
set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4,
z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3,
z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2,
z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
reconsider n1 = |. z1 .|, n2 = |. z2 .|, n3 = |. z3 .|,n4 = |. z4 .|
as natural Number;
reconsider n1,n2,n3,n4 as Nat by TARSKI:1;
A7: n1^2 = z1^2 & n2^2 = z2^2 & n3^2 = z3^2 & n4^2 = z4^2 by COMPLEX1:75;
p1*p2 = z1^2 + z2^2 + z3^2 + z4^2 by A3,A4
.= n1^2 + n2^2 + n3^2 + n4^2 by A7;
hence thesis;
end;
registration let p1,p2 be Prime;
cluster p1 * p2 -> a_sum_of_four_squares;
coherence by Prime4Sq;
end;
theorem Them7:
for p be Prime, n be Nat holds
ex x1,x2,x3,x4 be Nat st p|^n = x1^2 + x2^2 + x3^2 + x4^2
proof
let p be Prime, n be Nat;
defpred P[Nat] means ex x1,x2,x3,x4 be Nat
st p|^$1 = x1^2 + x2^2 + x3^2 + x4^2;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat; assume P[n]; then
consider x1,x2,x3,x4 be Nat such that
A3: p|^n = x1^2 + x2^2 + x3^2 + x4^2;
consider y1,y2,y3,y4 be Nat such that
A4: p = y1^2 + y2^2 + y3^2 + y4^2 by Them5;
set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4,
z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3,
z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2,
z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
reconsider n1 = |. z1 .|, n2 = |. z2 .|, n3 = |. z3 .|, n4 = |. z4 .|
as natural Number;
reconsider n1,n2,n3,n4 as Nat by TARSKI:1;
A6: n1^2 = z1^2 & n2^2 = z2^2 & n3^2 = z3^2 & n4^2 = z4^2 by COMPLEX1:75;
p|^(n + 1) = p|^n * p by NEWTON:6
.= z1^2 + z2^2 + z3^2 + z4^2 by A3,A4
.= n1^2 + n2^2 + n3^2 + n4^2 by A6;
hence thesis;
end;
A8: P[0]
proof
consider x1,x2,x3,x4 be Nat such that
A9: x1 = 1 & x2 = 0 & x3 = 0 & x4 = 0;
p|^0 = x1^2 + x2^2 + x3^2 + x4^2 by A9,NEWTON:4;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A8,A1);
hence thesis;
end;
registration let p be Prime, n be Nat;
cluster p |^ n -> a_sum_of_four_squares;
coherence by Them7;
end;
begin :: Proof of the Theorem of Sums of Four Squares
theorem Them8:
for n being non zero Nat holds
ex x1,x2,x3,x4 be Nat st Product ppf n = x1^2 + x2^2 + x3^2 + x4^2
proof
let n be non zero Nat;
defpred P[Nat] means for n being non zero Nat st card support ppf n = $1
holds
ex x1,x2,x3,x4 be Nat st Product ppf n = x1^2 + x2^2 + x3^2 + x4^2;
A1: P[ 0 ]
proof
let n be non zero Nat;
assume card support ppf n = 0; then
support ppf n = {}; then
A3: ppf n = EmptyBag SetPrimes by PRE_POLY:81;
set x1 = 1, x2 = 0, x3 = 0, x4 = 0;
Product ppf n = x1^2 + x2^2 + x3^2 + x4^2 by A3,NAT_3:20;
hence thesis;
end;
A8: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A9: P[k];
let n be non zero Nat; assume
A10: card support ppf n = k+1; then
support ppf n is non empty set; then
consider x be object such that
A11: x in support ppf n by XBOOLE_0:def 1;
A12: x in support pfexp n by A11,NAT_3:def 9;
A13: x is Prime by A12,NAT_3:34;
reconsider p = x as Nat by A12,NAT_3:34;
set e = p |-count n;
set s = p |^ e;
A14: p > 1 by A13,INT_2:def 4;
reconsider n as Integer;
s divides n by A14,NAT_3:def 7; then
consider t being Nat such that
A15: n = s * t by NAT_D:def 3;
reconsider n as Nat;
reconsider s, t as non zero Nat by A15;
A16: e = (p |-count s) + (p |-count t) by A13,NAT_3:28,A15
.= e + (p |-count t) by A13,INT_2:def 4,NAT_3:25;
A17: (p |-count t) = 0 by A16;
A19: support ppf t = support pfexp t by NAT_3:def 9;
A20: support ppf s = support pfexp s by NAT_3:def 9;
(pfexp n).p = e by A13,NAT_3:def 8; then
e <> 0 by A12,PRE_POLY:def 7; then
support pfexp p|^e = {p} by A13,NAT_3:42; then
A21: card support pfexp s = 1 by CARD_1:30;
reconsider s1 = s, t1 = t as non zero Nat;
A22: s1 gcd t1 = 1
proof
set u = s1 gcd t1;
reconsider s1, t1 as Integer;
A23: (s1 gcd t1) divides t1 by NAT_D:def 5;
reconsider u as Integer;
u <> 0 by INT_2:5; then
A24: 0+1 <= u by NAT_1:13;
now assume s1 gcd t1 <> 1; then
u > 1 by A24,XXREAL_0:1;then
u >= 1+1 by NAT_1:13; then
consider r being Element of NAT such that
A26: r is prime and
A27: r divides u by INT_2:31;
u divides s1 by NAT_D:def 5; then
A28: r divides s1 by A27,NAT_D:4;
reconsider p as Integer;
A29: r = 1 or r = p by A13,A26,A28,NAT_3:5,INT_2:def 4;
reconsider p as Prime by A12,NAT_3:34;
reconsider q = p as non zero Nat;
1 = p |-count q by NAT_3:22,INT_2:def 4;
hence contradiction
by A17,A23,A27,A26,A29,INT_2:def 4,NAT_D:4,NAT_3:30;
end;
hence thesis;
end;
reconsider s1,t1 as Integer;
A31: support ppf s misses support ppf t by A19,A20,A22,INT_2:def 3,NAT_3:44;
reconsider n,t as non zero Nat;
A32: k+1 = card support pfexp n by A10,NAT_3:def 9
.= card support pfexp s + card support pfexp t
by NAT_3:47,A22,INT_2:def 3,A15;
A33: card support ppf t = k by A21,A32,NAT_3:def 9;
consider x1,x2,x3,x4 be Nat such that
A34: p |^ e = x1^2 + x2^2 + x3^2 + x4^2 by A13,Them7;
consider y1,y2,y3,y4 be Nat such that
A35: Product ppf t = y1^2 + y2^2 + y3^2 + y4^2 by A9,A33;
set z1 = x1*y1 + x2*y2 +x3*y3 + x4*y4,
z2 = -x1*y2 + x2*y1 - x3*y4 + x4*y3,
z3 = x1*y3 - x2*y4 - x3*y1 + x4*y2,
z4 = x1*y4 + x2*y3 - x3*y2 - x4*y1;
reconsider n1 = |. z1 .|, n2 = |. z2 .|, n3 = |. z3 .|, n4 = |. z4 .|
as natural Number;
reconsider n1, n2, n3, n4 as Nat by TARSKI:1;
A37: n1^2 = z1^2 & n2^2 = z2^2 & n3^2 = z3^2 & n4^2 = z4^2 by COMPLEX1:75;
Product ppf n = Product (ppf s + ppf t) by A15,A22,INT_2:def 3,NAT_3:58
.= (Product ppf s) * Product ppf t by NAT_3:19,A31
.= (p |^ e)*Product ppf t by NAT_3:61
.= z1^2 + z2^2 + z3^2 + z4^2 by A34,A35
.= n1^2 + n2^2 + n3^2 + n4^2 by A37;
hence thesis;
end;
A38: for k be Nat holds P[k] from NAT_1:sch 2(A1,A8);
reconsider n as non zero Nat;
A39: P[card support ppf n] by A38;
consider x1,x2,x3,x4 be Nat such that
A40: Product ppf n = x1^2 + x2^2 + x3^2 + x4^2 by A39;
thus thesis by A40;
end;
::$N Lagrange's four-square theorem
::$L https://en.wikipedia.org/wiki/Lagrange's_four-square_theorem Lagrange's four-square theorem
theorem Lagrange4Squares:
for n be Nat holds
ex x1,x2,x3,x4 be Nat st n = x1^2 + x2^2 + x3^2 + x4^2
proof
let n be Nat;
per cases;
suppose n <> 0; then
reconsider n as non zero Nat;
consider x1,x2,x3,x4 be Nat such that
A1: Product ppf n = x1^2 + x2^2 + x3^2 + x4^2 by Them8;
n = x1^2 + x2^2 + x3^2 + x4^2 by A1,NAT_3:61;
hence thesis;
end;
suppose
A2: n = 0;
set x1 = 0, x2 = 0, x3 = 0, x4 = 0;
n = x1^2 + x2^2 + x3^2 + x4^2 by A2;
hence thesis;
end;
end;
registration
cluster -> a_sum_of_four_squares for Nat;
coherence by Lagrange4Squares;
end;