deffunc H₁( non zero Nat) -> Element of NAT = (Product (SqFactors $1)) |^ 2;
deffunc H₂( non zero Nat) -> Element of NAT = Product (SqFactors $1);
deffunc H₃( non zero Nat) -> set = SqFactors $1;
defpred S₁[ Nat] means for n being non zero Nat st support H₃(n) c= Seg $1 holds
H₁(n) divides n;
let n be non zero Nat; :: thesis: (SqF n) |^ 2 divides n
A1: ex mS being Element of NAT st support (ppf n) c= Seg mS by MOEBIUS1:14;
A2: support (ppf n) = support (pfexp n) by NAT_3:def 9
.= support H₃(n) by MOEBIUS2:def 3 ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let n be non zero Nat; :: thesis: ( support H₃(n) c= Seg (k + 1) implies H₁(n) divides n )
assume A5: support H₃(n) c= Seg (k + 1) ; :: thesis: H₁(n) divides n
A6: support (pfexp n) = support H₃(n) by MOEBIUS2:def 3;

per cases ( not support H₃(n) c= Seg k or support H₃(n) c= Seg k ) ;

suppose A7: not support H₃(n) c= Seg k ; :: thesis: H₁(n) divides n

set p = k + 1;
set e = (k + 1) |-count n;
set s = (k + 1) |^ ((k + 1) |-count n);

A8: now :: thesis: k + 1 in support H₃(n)

assume A9: not k + 1 in support H₃(n) ; :: thesis: contradiction
support H₃(n) c= Seg k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support H₃(n) or x in Seg k )
assume A10: x in support H₃(n) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
m <= k + 1 by A5, A10, FINSEQ_1:1;
then m < k + 1 by A9, A10, XXREAL_0:1;
then A11: m <= k by NAT_1:13;
x is Prime by A6, A10, NAT_3:34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A11, FINSEQ_1:1; :: thesis: verum

end;

hence contradiction by A7; :: thesis: verum

end;

then A12: k + 1 is Prime by A6, NAT_3:34;
then A13: k + 1 > 1 by INT_2:def 4;
then (k + 1) |^ ((k + 1) |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A14: n = ((k + 1) |^ ((k + 1) |-count n)) * t ;
reconsider s = (k + 1) |^ ((k + 1) |-count n), t = t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product H₃(s) = Product f and
A16: f = H₃(s) * (canFS (support H₃(s))) by NAT_3:def 5;
A17: dom H₃(s) = SetPrimes by PARTFUN1:def 2;
A18: support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A19: support (ppf s) = support H₃(s) by MOEBIUS2:def 3;
(pfexp n) . (k + 1) = (k + 1) |-count n by A12, NAT_3:def 8;
then (k + 1) |-count n <> 0 by A6, A8, PRE_POLY:def 7;
then A21: support (ppf s) = {(k + 1)} by A12, A18, NAT_3:42;
then A22: k + 1 in support (pfexp s) by A18, TARSKI:def 1;
A23: support H₃(t) c= Seg k

proof

set f = (k + 1) |-count t;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support H₃(t) or x in Seg k )
assume A24: x in support H₃(t) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
A25: x in support (pfexp t) by A24, MOEBIUS2:def 3;

A26: now :: thesis: not m = k + 1

assume A27: m = k + 1 ; :: thesis: contradiction
(pfexp t) . (k + 1) = (k + 1) |-count t by A12, NAT_3:def 8;
then (k + 1) |-count t <> 0 by A25, A27, PRE_POLY:def 7;
then (k + 1) |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A28: (k + 1) |-count t = 1 + g by NAT_1:10;
(k + 1) |^ ((k + 1) |-count t) divides t by A13, NAT_3:def 7;
then consider u being Nat such that
A29: t = ((k + 1) |^ ((k + 1) |-count t)) * u ;
n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A14, A28, A29, NEWTON:6
.= (s * (k + 1)) * (((k + 1) |^ g) * u)
.= ((k + 1) |^ (((k + 1) |-count n) + 1)) * (((k + 1) |^ g) * u) by NEWTON:6 ;
then (k + 1) |^ (((k + 1) |-count n) + 1) divides n ;
hence contradiction by A13, NAT_3:def 7; :: thesis: verum

end;

support (pfexp t) c= support (pfexp n) by A14, NAT_3:45;
then support H₃(t) c= support H₃(n) by A6, MOEBIUS2:def 3;
then m in support H₃(n) by A24;
then m <= k + 1 by A5, FINSEQ_1:1;
then m < k + 1 by A26, XXREAL_0:1;
then A30: m <= k by NAT_1:13;
x is Prime by A25, NAT_3:34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A30, FINSEQ_1:1; :: thesis: verum

end;

then A31: H₁(t) divides t by A4;
support H₃(s) = {(k + 1)} by A18, A21, MOEBIUS2:def 3;
then f = H₃(s) * <*(k + 1)*> by A16, FINSEQ_1:94
.= <*(H₃(s) . (k + 1))*> by FINSEQ_2:34, A17, A8 ;
then h1: Product H₃(s) = H₃(s) . (k + 1) by A15, RVSUM_1:95
.= (k + 1) |^ (((k + 1) |-count s) div 2) by A22, MOEBIUS2:def 3 ;
H2: (k + 1) |-count s <= (k + 1) |-count n by A12, NAT_3:25, INT_2:def 4;
set j = (k + 1) |-count s;
(k + 1) |-count s = (2 * (((k + 1) |-count s) div 2)) + (((k + 1) |-count s) mod 2) by NAT_D:2;
then Sb: 2 * (((k + 1) |-count s) div 2) <= (k + 1) |-count s by NAT_1:11;
((k + 1) |^ (((k + 1) |-count s) div 2)) |^ 2 = (k + 1) |^ ((((k + 1) |-count s) div 2) * 2) by NEWTON:9;
then ZZ: ((k + 1) |^ (((k + 1) |-count s) div 2)) |^ 2 divides (k + 1) |^ ((k + 1) |-count n) by Sb, NEWTON:89, H2, XXREAL_0:2;
reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 12;
support (ppf t) = support (pfexp t) by NAT_3:def 9;
then A33: support (ppf t) = support H₃(t) by MOEBIUS2:def 3;

A34: now :: thesis: not support (ppf s) meets support (ppf t)

assume support (ppf s) meets support (ppf t) ; :: thesis: contradiction
then consider x being object such that
A35: x in support (ppf s) and
A36: x in support (ppf t) by XBOOLE_0:3;
x in support (pfexp t) by A36, NAT_3:def 9;
then A37: x in support H₃(t) by MOEBIUS2:def 3;
x = k + 1 by A21, A35, TARSKI:def 1;
then k + 1 <= k by A23, A37, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

s1,t1 are_coprime

proof

set u = s1 gcd t1;
A38: s1 gcd t1 divides t1 by NAT_D:def 5;
A39: 0 + 1 <= s1 gcd t1 by NAT_1:13;
assume not s1,t1 are_coprime ; :: thesis: contradiction
then s1 gcd t1 > 1 by A39, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider r being Element of NAT such that
A40: r is prime and
A41: r divides s1 gcd t1 by INT_2:31;
s1 gcd t1 divides s1 by NAT_D:def 5;
then r divides s1 by A41, NAT_D:4;
then ( r = 1 or r = k + 1 ) by A12, INT_2:def 4, A40, NAT_3:5;
then k + 1 in support (pfexp t) by NAT_3:37, A40, A41, A38, NAT_D:4;
then k + 1 in support H₃(t) by MOEBIUS2:def 3;
then k + 1 <= k by A23, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then H₁(n) = (Product (H₃(s) + H₃(t))) |^ 2 by A14, MOEBIUS2:44
.= (H₂(s) * H₂(t)) |^ 2 by A34, A19, A33, NAT_3:19
.= H₁(s) * H₁(t) by NEWTON:7 ;
hence H₁(n) divides n by A14, h1, ZZ, A31, NAT_3:1; :: thesis: verum

end;

suppose support H₃(n) c= Seg k ; :: thesis: H₁(n) divides n

hence H₁(n) divides n by A4; :: thesis: verum

end;

end;

end;

A42: S₁[ 0 ]

proof

let n be non zero Nat; :: thesis: ( support H₃(n) c= Seg 0 implies H₁(n) divides n )
assume support H₃(n) c= Seg 0 ; :: thesis: H₁(n) divides n
then support H₃(n) = {} ;
then H₃(n) = EmptyBag SetPrimes by PRE_POLY:81;
then H₁(n) = 1 |^ 2 by NAT_3:20
.= 1 ;
hence H₁(n) divides n by NAT_D:6; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A42, A3);
hence (SqF n) |^ 2 divides n by A1, A2; :: thesis: verum