environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions ;
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;
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;
constructors HIDDEN, ARYTM_2, RELSET_1, ARYTM_0, XXREAL_1, ORDINAL3, ABIAN, NAT_D, PEPIN, CARD_2, XXREAL_2, UPROOTS, NAT_3;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM;
equalities ORDINAL1, SQUARE_1, FINSEQ_1;
expansions TARSKI, XBOOLE_0, PBOOLE;
theorem
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) ;
lem3:
for p being odd prime Nat holds p > 2
lem3a:
for p being odd prime Nat holds p + 1 > 3
theorem lem7:
for
i1,
i2,
c being
Nat st
i1 <= c &
i2 <= c & not
i1 + i2 < 2
* c holds
(
i1 = c &
i2 = c )
theorem lem8:
for
i1,
i2,
i3,
i4,
c being
Nat st
i1 <= c &
i2 <= c &
i3 <= c &
i4 <= c & not
((i1 + i2) + i3) + i4 < 4
* c holds
(
i1 = c &
i2 = c &
i3 = c &
i4 = c )
Them3:
for p being odd prime Nat ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
Them4:
for p being Prime st p is even holds
ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
theorem Prime4Sq:
for
p1,
p2 being
Prime ex
x1,
x2,
x3,
x4 being
Nat st
p1 * p2 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
theorem Lagrange4Squares:
for
n being
Nat ex
x1,
x2,
x3,
x4 being
Nat st
n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)