let n be non zero Nat; :: thesis: ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
defpred S₁[ Nat] means for n being non zero Nat st card (support (ppf n)) = $1 holds
ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2);
A1: S₁[ 0 ]

proof

let n be non zero Nat; :: thesis: ( card (support (ppf n)) = 0 implies ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
assume card (support (ppf n)) = 0 ; :: thesis: ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
then support (ppf n) = {} ;
then A3: ppf n = EmptyBag SetPrimes by PRE_POLY:81;
set x1 = 1;
set x2 = 0 ;
set x3 = 0 ;
set x4 = 0 ;
Product (ppf n) = (((1 ^2) + (0 ^2)) + (0 ^2)) + (0 ^2) by A3, NAT_3:20;
hence ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ; :: thesis: verum

end;

A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
let n be non zero Nat; :: thesis: ( card (support (ppf n)) = k + 1 implies ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
assume A10: card (support (ppf n)) = k + 1 ; :: thesis: ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
then support (ppf n) is non empty set ;
then consider x being 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 |^ (p |-count n);
A14: p > 1 by A13, INT_2:def 4;
reconsider n = n as Integer ;
p |^ (p |-count n) divides n by A14, NAT_3:def 7;
then consider t being Nat such that
A15: n = (p |^ (p |-count n)) * t by NAT_D:def 3;
reconsider n = n as Nat ;
reconsider s = p |^ (p |-count n), t = t as non zero Nat by A15;
A16: p |-count n = (p |-count s) + (p |-count t) by A13, NAT_3:28, A15
.= (p |-count n) + (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 = p |-count n by A13, NAT_3:def 8;
then p |-count n <> 0 by A12, PRE_POLY:def 7;
then support (pfexp (p |^ (p |-count n))) = {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 = s1, t1 = t1 as Integer ;
A23: s1 gcd t1 divides t1 by NAT_D:def 5;
reconsider u = s1 gcd t1 as Integer ;
u <> 0 by INT_2:5;
then A24: 0 + 1 <= u by NAT_1:13;

now :: thesis: not s1 gcd t1 <> 1

assume s1 gcd t1 <> 1 ; :: thesis: contradiction
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 = p as Integer ;
A29: ( r = 1 or r = p ) by A13, A26, A28, NAT_3:5, INT_2:def 4;
reconsider p = 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; :: thesis: verum

end;

hence s1 gcd t1 = 1 ; :: thesis: verum

end;

reconsider s1 = s1, t1 = t1 as Integer ;
A31: support (ppf s) misses support (ppf t) by A19, A20, A22, INT_2:def 3, NAT_3:44;
reconsider n = n, t = 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 being Nat such that
A34: p |^ (p |-count n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by A13, Them7;
consider y1, y2, y3, y4 being 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);
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);
reconsider n1 = |.((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)).|, n2 = |.((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)).|, n3 = |.((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)).|, n4 = |.((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)).| as natural Number ;
reconsider n1 = n1, n2 = n2, n3 = n3, n4 = n4 as Nat by TARSKI:1;
A37: ( n1 ^2 = ((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2 & n2 ^2 = ((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2 & n3 ^2 = ((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2 & n4 ^2 = ((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^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 |^ (p |-count n)) * (Product (ppf t)) by NAT_3:61
.= (((((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2) + (((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2)) + (((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2)) + (((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^2) by A34, A35
.= (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2) by A37 ;
hence ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ; :: thesis: verum

end;

A38: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A8);
reconsider n = n as non zero Nat ;
A39: S₁[ card (support (ppf n))] by A38;
consider x1, x2, x3, x4 being Nat such that
A40: Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by A39;
thus ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by A40; :: thesis: verum