defpred S1[ Nat] means for n being non zero Nat st support (PFactors n) c= Seg $1 holds
Radical n divides n;
let n be non zero Nat; :: thesis: Radical n divides n
A1: ex mS being Element of NAT st support (ppf n) c= Seg mS by Th14;
A2: support (ppf n) = support (pfexp n) by NAT_3:def 9
.= support (PFactors n) by Def6 ;
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 (PFactors n) c= Seg (k + 1) implies Radical n divides n )
assume A5: support (PFactors n) c= Seg (k + 1) ; :: thesis: Radical n divides n
A6: support (pfexp n) = support (PFactors n) by Def6;
per cases ( not support (PFactors n) c= Seg k or support (PFactors n) c= Seg k ) ;
suppose A7: not support (PFactors n) c= Seg k ; :: thesis: Radical 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 (PFactors n)
assume A9: not k + 1 in support (PFactors n) ; :: thesis: contradiction
support (PFactors n) c= Seg k
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (PFactors n) or x in Seg k )
assume A10: x in support (PFactors 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 by NAT_D:def 3;
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 (PFactors s) = Product f and
A16: f = (PFactors s) * (canFS (support (PFactors s))) by NAT_3:def 5;
A17: dom (PFactors s) = SetPrimes by PARTFUN1:def 2;
A18: support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A19: support (ppf s) = support (PFactors s) by Def6;
(pfexp n) . (k + 1) = (k + 1) |-count n by A12, NAT_3:def 8;
then A20: (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 (PFactors 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 (PFactors t) or x in Seg k )
assume A24: x in support (PFactors t) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
A25: x in support (pfexp t) by A24, Def6;
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 by NAT_D:def 3;
reconsider g = g as Element of NAT by ORDINAL1:def 12;
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 by NAT_D:def 3;
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 (PFactors t) c= support (PFactors n) by A6, Def6;
then m in support (PFactors 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: Radical t divides t by A4;
support (PFactors s) = {(k + 1)} by A18, A21, Def6;
then f = (PFactors s) * <*(k + 1)*> by A16, FINSEQ_1:94
.= <*((PFactors s) . (k + 1))*> by A8, A17, FINSEQ_2:34 ;
then Product (PFactors s) = (PFactors s) . (k + 1) by A15, RVSUM_1:95
.= k + 1 by A22, Def6 ;
then A32: Radical s divides s by A20, NAT_3:3;
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 (PFactors t) by Def6;
s1,t1 are_coprime
proof
set u = s1 gcd t1;
A38: s1 gcd t1 divides t1 by NAT_D:def 5;
s1 gcd t1 <> 0 by INT_2:5;
then A39: 0 + 1 <= s1 gcd t1 by NAT_1:13;
assume not s1,t1 are_coprime ; :: thesis: contradiction
then s1 gcd t1 <> 1 by INT_2:def 3;
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 divides k + 1 by A40, NAT_3:5;
then ( r = 1 or r = k + 1 ) by A12, INT_2:def 4;
then k + 1 divides t1 by A40, A41, A38, INT_2:def 4, NAT_D:4;
then k + 1 in support (pfexp t) by A12, NAT_3:37;
then k + 1 in support (PFactors t) by Def6;
then k + 1 <= k by A23, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum
end;
then Radical n = Product ((PFactors s) + (PFactors t)) by A14, Th50
.= (Radical s) * (Radical t) by A34, A19, A33, NAT_3:19 ;
hence Radical n divides n by A14, A32, A31, NAT_3:1; :: thesis: verum
end;
end;
end;
A42: S1[ 0 ]
proof
let n be non zero Nat; :: thesis: ( support (PFactors n) c= Seg 0 implies Radical n divides n )
A43: {} c= support (PFactors n) ;
assume support (PFactors n) c= Seg 0 ; :: thesis: Radical n divides n
then support (PFactors n) = {} by A43;
then PFactors n = EmptyBag SetPrimes by PRE_POLY:81;
then Radical n = 1 by NAT_3:20;
hence Radical 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 Radical n divides n by A1, A2; :: thesis: verum