:: Lagrange's Four-Square Theorem :: by Yasushige Watase :: :: Received June 4, 2014 :: Copyright (c) 2014-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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; begin :: Preliminaries definition let n be natural number; attr n is a_sum_of_four_squares means :: LAGRA4SQ:def 1 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; end; registration let y be integer object; cluster |.y.| -> natural; end; theorem :: LAGRA4SQ:1 :: 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; end; registration cluster odd for prime Nat; 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 :: LAGRA4SQ:def 2 for x be Element of INT holds it.x = x mod p; end; definition let v; func LAG4SQf(v) -> FinSequence of INT means :: LAGRA4SQ:def 3 len it = v & for i being Nat st i in dom it holds it.i = (i -1)^2; end; definition let v; func LAG4SQg(v) -> FinSequence of INT means :: LAGRA4SQ:def 4 len it = v & for i being Nat st i in dom it holds it.i = -1 - (i -1)^2; end; theorem :: LAGRA4SQ:2 LAG4SQf(v) is one-to-one; theorem :: LAGRA4SQ:3 LAG4SQg v is one-to-one; reserve a for Real; reserve b for Integer; theorem :: LAGRA4SQ:4 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; theorem :: LAGRA4SQ:5 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; begin :: Any prime number can be expressed as the sum of four integer squares theorem :: LAGRA4SQ:6 :: 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; theorem :: LAGRA4SQ:7 ::: 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; theorem :: LAGRA4SQ:8 for i1,i2, c be Nat st i1 <= c & i2 <= c holds i1+i2 < 2*c or (i1 = c & i2 = c); theorem :: LAGRA4SQ:9 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); theorem :: LAGRA4SQ:10 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; theorem :: LAGRA4SQ:11 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; theorem :: LAGRA4SQ:12 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; theorem :: LAGRA4SQ:13 for p be Prime st p is even holds p = 2; theorem :: LAGRA4SQ:14 for p be Prime holds ex x1,x2,x3,x4 be Nat st p = x1^2 + x2^2 + x3^2 + x4^2; theorem :: LAGRA4SQ:15 for p1, p2 be Prime holds ex x1,x2,x3,x4 be Nat st p1*p2 = x1^2 + x2^2 + x3^2 + x4^2; registration let p1,p2 be Prime; cluster p1 * p2 -> a_sum_of_four_squares; end; theorem :: LAGRA4SQ:16 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; registration let p be Prime, n be Nat; cluster p |^ n -> a_sum_of_four_squares; end; begin :: Proof of the Theorem of Sums of Four Squares theorem :: LAGRA4SQ:17 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; ::\$N Lagrange's four-square theorem theorem :: LAGRA4SQ:18 for n be Nat holds ex x1,x2,x3,x4 be Nat st n = x1^2 + x2^2 + x3^2 + x4^2; registration cluster -> a_sum_of_four_squares for Nat; end;