deffunc H1( non zero Nat) -> Element of omega = Product (SqFactors $1);
deffunc H2( non zero Nat) -> ManySortedSet of SetPrimes = SqFactors $1;
defpred S1[ Nat] means for n being non zero Nat st support H2(n) c= Seg $1 holds
H1(n) divides n;
let n be non zero Nat; :: thesis: SqF n 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 H2(n) by SqDef ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let n be non zero Nat; :: thesis: ( support H2(n) c= Seg (k + 1) implies H1(n) divides n )
assume A5: support H2(n) c= Seg (k + 1) ; :: thesis: H1(n) divides n
A6: support (pfexp n) = support H2(n) by SqDef;
per cases ( not support H2(n) c= Seg k or support H2(n) c= Seg k ) ;
suppose A7: not support H2(n) c= Seg k ; :: thesis: H1(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 H2(n)
assume A9: not k + 1 in support H2(n) ; :: thesis: contradiction
support H2(n) c= Seg k
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support H2(n) or x in Seg k )
assume A10: x in support H2(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 H2(s) = Product f and
A16: f = H2(s) * (canFS (support H2(s))) by NAT_3:def 5;
A17: dom H2(s) = SetPrimes by PARTFUN1:def 2;
A18: support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A19: support (ppf s) = support H2(s) by SqDef;
(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 H2(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 H2(t) or x in Seg k )
assume A24: x in support H2(t) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
A25: x in support (pfexp t) by A24, SqDef;
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 H2(t) c= support H2(n) by A6, SqDef;
then m in support H2(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: H1(t) divides t by A4;
support H2(s) = {(k + 1)} by A18, A21, SqDef;
then f = H2(s) * <*(k + 1)*> by A16, FINSEQ_1:94
.= <*(H2(s) . (k + 1))*> by FINSEQ_2:34, A17, A8 ;
then h1: Product H2(s) = H2(s) . (k + 1) by A15
.= (k + 1) |^ (((k + 1) |-count s) div 2) by A22, SqDef ;
H2: (k + 1) |-count s <= (k + 1) |-count n by A12, NAT_3:25, INT_2:def 4;
( (k + 1) |-count s = 0 iff not k + 1 divides s ) by NAT_3:27, A13;
then ((k + 1) |-count s) div 2 <= (k + 1) |-count s by INT_1:56;
then ZZ: (k + 1) |^ (((k + 1) |-count s) div 2) divides (k + 1) |^ ((k + 1) |-count n) by 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 H2(t) by SqDef;
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 H2(t) by SqDef;
then k + 1 <= k by A23, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum
end;
then H1(n) = Product (H2(s) + H2(t)) by A14, MB150
.= H1(s) * H1(t) by A34, A19, A33, NAT_3:19 ;
hence H1(n) divides n by A14, h1, ZZ, A31, NAT_3:1; :: thesis: verum
end;
end;
end;
A42: S1[ 0 ]
proof
let n be non zero Nat; :: thesis: ( support H2(n) c= Seg 0 implies H1(n) divides n )
assume support H2(n) c= Seg 0 ; :: thesis: H1(n) divides n
then support H2(n) = {} ;
then H2(n) = EmptyBag SetPrimes by PRE_POLY:81;
then H1(n) = 1 by NAT_3:20;
hence H1(n) divides n by NAT_D:6; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A42, A3);
 hence SqF n divides n by A1, A2; :: thesis: verum