let n be non zero Nat; :: thesis: Product (ppf n) = n
defpred S1[ Nat] means for n being non zero Nat st support (ppf n) c= Seg $1 holds
Product (ppf n) = n;
A1: support (ppf n) = support (pfexp n) by Def9;
A2: S1[ 0 ]
proof
let n be non zero Nat; :: thesis: ( support (ppf n) c= Seg 0 implies Product (ppf n) = n )
A3: {} c= support (ppf n) ;
assume support (ppf n) c= Seg 0 ; :: thesis: Product (ppf n) = n
then A4: support (ppf n) = {} by A3;
A5: now :: thesis: not n <> 1
reconsider k = n as Nat ;
assume n <> 1 ; :: thesis: contradiction
then k > 1 by NAT_1:53;
then k >= 1 + 1 by NAT_1:13;
then ex p being Element of NAT st
( p is prime & p divides k ) by INT_2:31;
then not support (pfexp n) is empty by Th37;
hence contradiction by A4, Def9; :: thesis: verum
end;
ppf n = EmptyBag SetPrimes by A4, PRE_POLY:81;
hence Product (ppf n) = n by A5, Th20; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
let n be non zero Nat; :: thesis: ( support (ppf n) c= Seg (k + 1) implies Product (ppf n) = n )
assume A8: support (ppf n) c= Seg (k + 1) ; :: thesis: Product (ppf n) = n
A9: support (ppf n) = support (pfexp n) by Def9;
per cases ( not support (ppf n) c= Seg k or support (ppf n) c= Seg k ) ;
suppose A10: not support (ppf n) c= Seg k ; :: thesis: Product (ppf n) = n
set p = k + 1;
set e = (k + 1) |-count n;
set s = (k + 1) |^ ((k + 1) |-count n);
A11: now :: thesis: k + 1 in support (ppf n)
assume A12: not k + 1 in support (ppf n) ; :: thesis: contradiction
support (ppf n) c= Seg k
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg k )
assume A13: x in support (ppf n) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
m <= k + 1 by A8, A13, FINSEQ_1:1;
then m < k + 1 by A12, A13, XXREAL_0:1;
then A14: m <= k by NAT_1:13;
x is Prime by A9, A13, Th34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A14; :: thesis: verum
end;
hence contradiction by A10; :: thesis: verum
end;
then A15: k + 1 is Prime by A9, Th34;
then A16: k + 1 > 1 by INT_2:def 4;
then (k + 1) |^ ((k + 1) |-count n) divides n by Def7;
then consider t being Nat such that
A17: n = ((k + 1) |^ ((k + 1) |-count n)) * t ;
reconsider s = (k + 1) |^ ((k + 1) |-count n), t = t as non zero Nat by A17;
A18: dom (ppf s) = SetPrimes by PARTFUN1:def 2;
(pfexp n) . (k + 1) = (k + 1) |-count n by A15, Def8;
then A19: (k + 1) |-count n <> 0 by A9, A11, PRE_POLY:def 7;
reconsider s1 = s, t1 = t as non zero Nat ;
A20: support (ppf t) = support (pfexp t) by Def9;
A21: support (ppf 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 (ppf t) or x in Seg k )
assume A22: x in support (ppf t) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
A23: x in support (pfexp t) by A22, Def9;
A24: now :: thesis: not m = k + 1
assume A25: m = k + 1 ; :: thesis: contradiction
(pfexp t) . (k + 1) = (k + 1) |-count t by A15, Def8;
then (k + 1) |-count t <> 0 by A23, A25, PRE_POLY:def 7;
then (k + 1) |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A26: (k + 1) |-count t = 1 + g by NAT_1:10;
(k + 1) |^ ((k + 1) |-count t) divides t by A16, Def7;
then consider u being Nat such that
A27: t = ((k + 1) |^ ((k + 1) |-count t)) * u ;
n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A17, A26, A27, 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 A16, Def7; :: thesis: verum
end;
support (ppf t) c= support (ppf n) by A9, A17, A20, Th45;
then m in support (ppf n) by A22;
then m <= k + 1 by A8, FINSEQ_1:1;
then m < k + 1 by A24, XXREAL_0:1;
then A28: m <= k by NAT_1:13;
x is Prime by A23, Th34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A28; :: thesis: verum
end;
s1,t1 are_coprime
proof
set u = s1 gcd t1;
A29: s1 gcd t1 divides t1 by NAT_D:def 5;
s1 gcd t1 <> 0 by INT_2:5;
then A30: 0 + 1 <= s1 gcd t1 by NAT_1:13;
assume s1 gcd t1 <> 1 ; :: according to INT_2:def 3 :: thesis: contradiction
then s1 gcd t1 > 1 by A30, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider r being Element of NAT such that
A31: r is prime and
A32: r divides s1 gcd t1 by INT_2:31;
s1 gcd t1 divides s1 by NAT_D:def 5;
then r divides s1 by A32, NAT_D:4;
then r divides k + 1 by A31, Th5;
then ( r = 1 or r = k + 1 ) by A15, INT_2:def 4;
then k + 1 divides t1 by A31, A32, A29, NAT_D:4;
then k + 1 in support (pfexp t) by A15, Th37;
then k + 1 <= k by A20, A21, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum
end;
then A33: ppf n = (ppf s) + (ppf t) by A17, Th58;
consider f being FinSequence of COMPLEX such that
A34: Product (ppf s) = Product f and
A35: f = (ppf s) * (canFS (support (ppf s))) by Def5;
support (ppf s) = support (pfexp s) by Def9;
then A36: support (ppf s) = {(k + 1)} by A15, A19, Th42;
then f = (ppf s) * <*(k + 1)*> by A35, FINSEQ_1:94
.= <*((ppf s) . (k + 1))*> by A11, A18, FINSEQ_2:34 ;
then A37: Product (ppf s) = (ppf s) . (k + 1) by A34
.= s by A15, A19, Th59 ;
then A40: support (ppf s) misses support (ppf t) ;
Product (ppf t) = t by A7, A21;
hence Product (ppf n) = n by A17, A40, A33, A37, Th19; :: thesis: verum
end;
end;
end;
A41: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A6);
per cases ( support (ppf n) is empty or not support (ppf n) is empty ) ;
suppose support (ppf n) is empty ; :: thesis: Product (ppf n) = n
hence Product (ppf n) = n by A2; :: thesis: verum
end;
suppose not support (ppf n) is empty ; :: thesis: Product (ppf n) = n
then reconsider S = support (ppf n) as non empty finite Subset of NAT by XBOOLE_1:1;
A42: max S is Nat by TARSKI:1;
support (ppf n) c= Seg (max S)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg (max S) )
assume A43: x in support (ppf n) ; :: thesis: x in Seg (max S)
then reconsider m = x as Nat ;
x is Prime by A1, A43, Th34;
then A44: 1 <= m by INT_2:def 4;
m <= max S by A43, XXREAL_2:def 8;
hence x in Seg (max S) by A44; :: thesis: verum
end;
hence Product (ppf n) = n by A42, A41; :: thesis: verum
end;
end;