:: Lagrange's Four-Square Theorem :: by Yasushige Watase :: :: Received June 4, 2014 :: Copyright (c) 2014-2018 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; 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, SUBSET_1, 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, XBOOLE_0, 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 Nat; 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 Nat; 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; then 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 Nat, 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,55; 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,55; 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 Nat, 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,55; (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,55; (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; 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 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; A58: A = dom(MODMAP_p) /\ rng (g^f) by RELAT_1:61 .= rng (g^f) by A24,XBOOLE_1:28; 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,A58,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,NAT_D:13 .= (((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 NAT_D:13,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 Nat; 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 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;