let k be Nat; :: thesis: for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds

ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

let n be non zero Element of NAT ; :: thesis: ( support (ppf n) c= Seg (k + 1) implies ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) )

assume A1: support (ppf n) c= Seg (k + 1) ; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

let n be non zero Element of NAT ; :: thesis: ( support (ppf n) c= Seg (k + 1) implies ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) )

assume A1: support (ppf n) c= Seg (k + 1) ; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

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

end;

suppose A2:
support (ppf n) c= Seg k
; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

take
n
; :: thesis: ex e being Element of NAT st

( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )

take e = 0 ; :: thesis: ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )

(k + 1) |^ e = 1 by NEWTON:4;

hence ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) ) by A2; :: thesis: verum

end;( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )

take e = 0 ; :: thesis: ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )

(k + 1) |^ e = 1 by NEWTON:4;

hence ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) ) by A2; :: thesis: verum

suppose A3:
not support (ppf n) c= Seg k
; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

reconsider r = k + 1 as non zero Element of NAT ;

set e = r |-count n;

set s = r |^ (r |-count n);

then A7: r is Prime by NAT_3:34;

then A8: r > 1 by INT_2:def 4;

then r |^ (r |-count n) divides n by NAT_3:def 7;

then consider t being Nat such that

A9: n = (r |^ (r |-count n)) * t by NAT_D:def 3;

reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by A9, ORDINAL1:def 12;

A10: support (ppf t) = support (pfexp t) by NAT_3:def 9;

A11: support (ppf t) c= Seg k

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

take e = (k + 1) |-count n; :: thesis: ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

support (ppf s) = support (pfexp s) by NAT_3:def 9;

then A20: support (ppf s) = {r} by A7, A19, NAT_3:42;

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) by A9, A11; :: thesis: verum

end;set e = r |-count n;

set s = r |^ (r |-count n);

now :: thesis: k + 1 in support (ppf n)

then
k + 1 in support (pfexp n)
by NAT_3:def 9;assume A4:
not k + 1 in support (ppf n)
; :: thesis: contradiction

support (ppf n) c= Seg k

end;support (ppf n) c= Seg k

proof

hence
contradiction
by A3; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg k )

assume A5: x in support (ppf n) ; :: thesis: x in Seg k

then reconsider m = x as Nat ;

x in support (pfexp n) by A5, NAT_3:def 9;

then x is Prime by NAT_3:34;

then A6: 1 <= m by INT_2:def 4;

m <= k + 1 by A1, A5, FINSEQ_1:1;

then m < k + 1 by A4, A5, XXREAL_0:1;

then m <= k by NAT_1:13;

hence x in Seg k by A6, FINSEQ_1:1; :: thesis: verum

end;assume A5: x in support (ppf n) ; :: thesis: x in Seg k

then reconsider m = x as Nat ;

x in support (pfexp n) by A5, NAT_3:def 9;

then x is Prime by NAT_3:34;

then A6: 1 <= m by INT_2:def 4;

m <= k + 1 by A1, A5, FINSEQ_1:1;

then m < k + 1 by A4, A5, XXREAL_0:1;

then m <= k by NAT_1:13;

hence x in Seg k by A6, FINSEQ_1:1; :: thesis: verum

then A7: r is Prime by NAT_3:34;

then A8: r > 1 by INT_2:def 4;

then r |^ (r |-count n) divides n by NAT_3:def 7;

then consider t being Nat such that

A9: n = (r |^ (r |-count n)) * t by NAT_D:def 3;

reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by A9, ORDINAL1:def 12;

A10: support (ppf t) = support (pfexp t) by NAT_3:def 9;

A11: support (ppf t) c= Seg k

proof

A19:
r |-count n <> 0
set f = r |-count t;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf t) or x in Seg k )

assume A12: x in support (ppf t) ; :: thesis: x in Seg k

then reconsider m = x as Nat ;

A13: x in support (pfexp t) by A12, NAT_3:def 9;

then support (ppf t) c= support (ppf n) by A10, NAT_3:def 9;

then m in support (ppf n) by A12;

then m <= k + 1 by A1, FINSEQ_1:1;

then m < r by A14, XXREAL_0:1;

then A18: m <= k by NAT_1:13;

x is Prime by A13, NAT_3:34;

then 1 <= m by INT_2:def 4;

hence x in Seg k by A18, FINSEQ_1:1; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf t) or x in Seg k )

assume A12: x in support (ppf t) ; :: thesis: x in Seg k

then reconsider m = x as Nat ;

A13: x in support (pfexp t) by A12, NAT_3:def 9;

A14: now :: thesis: not m = r

support (pfexp t) c= support (pfexp n)
by A9, NAT_3:45;assume A15:
m = r
; :: thesis: contradiction

(pfexp t) . r = r |-count t by A7, NAT_3:def 8;

then r |-count t <> 0 by A13, A15, PRE_POLY:def 7;

then r |-count t >= 0 + 1 by NAT_1:13;

then consider g being Nat such that

A16: r |-count t = 1 + g by NAT_1:10;

r |^ (r |-count t) divides t by A8, NAT_3:def 7;

then consider u being Nat such that

A17: t = (r |^ (r |-count t)) * u by NAT_D:def 3;

reconsider g = g as Element of NAT by ORDINAL1:def 12;

n = s * (((r |^ g) * r) * u) by A9, A16, A17, NEWTON:6

.= (s * r) * ((r |^ g) * u)

.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;

then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;

hence contradiction by A8, NAT_3:def 7; :: thesis: verum

end;(pfexp t) . r = r |-count t by A7, NAT_3:def 8;

then r |-count t <> 0 by A13, A15, PRE_POLY:def 7;

then r |-count t >= 0 + 1 by NAT_1:13;

then consider g being Nat such that

A16: r |-count t = 1 + g by NAT_1:10;

r |^ (r |-count t) divides t by A8, NAT_3:def 7;

then consider u being Nat such that

A17: t = (r |^ (r |-count t)) * u by NAT_D:def 3;

reconsider g = g as Element of NAT by ORDINAL1:def 12;

n = s * (((r |^ g) * r) * u) by A9, A16, A17, NEWTON:6

.= (s * r) * ((r |^ g) * u)

.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;

then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;

hence contradiction by A8, NAT_3:def 7; :: thesis: verum

then support (ppf t) c= support (ppf n) by A10, NAT_3:def 9;

then m in support (ppf n) by A12;

then m <= k + 1 by A1, FINSEQ_1:1;

then m < r by A14, XXREAL_0:1;

then A18: m <= k by NAT_1:13;

x is Prime by A13, NAT_3:34;

then 1 <= m by INT_2:def 4;

hence x in Seg k by A18, FINSEQ_1:1; :: thesis: verum

proof

take m = t; :: thesis: ex e being Element of NAT st
assume
r |-count n = 0
; :: thesis: contradiction

then n = 1 * t by A9, NEWTON:4;

hence contradiction by A3, A11; :: thesis: verum

end;then n = 1 * t by A9, NEWTON:4;

hence contradiction by A3, A11; :: thesis: verum

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

take e = (k + 1) |-count n; :: thesis: ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

support (ppf s) = support (pfexp s) by NAT_3:def 9;

then A20: support (ppf s) = {r} by A7, A19, NAT_3:42;

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

for p being Prime holds assume
support (ppf s) meets support (ppf t)
; :: thesis: contradiction

then consider x being object such that

A22: x in support (ppf s) and

A23: x in support (ppf t) by XBOOLE_0:3;

x = r by A20, A22, TARSKI:def 1;

then r <= k by A11, A23, FINSEQ_1:1;

hence contradiction by NAT_1:13; :: thesis: verum

end;then consider x being object such that

A22: x in support (ppf s) and

A23: x in support (ppf t) by XBOOLE_0:3;

x = r by A20, A22, TARSKI:def 1;

then r <= k by A11, A23, FINSEQ_1:1;

hence contradiction by NAT_1:13; :: thesis: verum

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )

proof

hence
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
let p be Prime; :: thesis: ( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )

hence p |-count m <= p |-count n by Th15; :: thesis: verum

end;hereby :: thesis: ( not p in support (ppf m) implies p |-count m <= p |-count n )

assume
not p in support (ppf m)
; :: thesis: p |-count m <= p |-count nassume
p in support (ppf m)
; :: thesis: p |-count m = p |-count n

then not p in support (ppf s) by A21, XBOOLE_0:3;

then A24: p |-count s = 0 by Th15;

p |-count n = (p |-count (r |^ e)) + (p |-count t) by A9, NAT_3:28;

hence p |-count m = p |-count n by A24; :: thesis: verum

end;then not p in support (ppf s) by A21, XBOOLE_0:3;

then A24: p |-count s = 0 by Th15;

p |-count n = (p |-count (r |^ e)) + (p |-count t) by A9, NAT_3:28;

hence p |-count m = p |-count n by A24; :: thesis: verum

hence p |-count m <= p |-count n by Th15; :: thesis: verum

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) by A9, A11; :: thesis: verum