defpred S₁[ Nat] means for k, l being non zero Element of NAT st support (ppf k) c= Seg $1 & support (ppf l) c= Seg $1 & ( for p being Prime holds p |-count k <= p |-count l ) holds
k divides l;
let m, n be non zero Nat; :: thesis: ( ( for p being Prime holds p |-count m <= p |-count n ) implies m divides n )
A1: ( m is Element of NAT & n is Element of NAT ) by ORDINAL1:def 12;
consider k being Element of NAT such that
A2: support (ppf n) c= Seg k by Th14;
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 m, n be non zero Element of NAT ; :: thesis: ( support (ppf m) c= Seg (k + 1) & support (ppf n) c= Seg (k + 1) & ( for p being Prime holds p |-count m <= p |-count n ) implies m divides n )
assume that
A5: support (ppf m) c= Seg (k + 1) and
A6: support (ppf n) c= Seg (k + 1) and
A7: for p being Prime holds p |-count m <= p |-count n ; :: thesis: m divides n

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

suppose A8: ( not support (ppf n) c= Seg k & support (ppf m) c= Seg k ) ; :: thesis: m divides n

reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);

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

assume A9: 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 A10: x in support (ppf n) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
x in support (pfexp n) by A10, NAT_3:def 9;
then x is Prime by NAT_3:34;
then A11: 1 <= m by INT_2:def 4;
m <= k + 1 by A6, A10, FINSEQ_1:1;
then m < k + 1 by A9, A10, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A11, FINSEQ_1:1; :: thesis: verum

end;

hence contradiction by A8; :: thesis: verum

end;

then A12: k + 1 in support (pfexp n) by NAT_3:def 9;
then A13: r is Prime by NAT_3:34;
then A14: 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
A15: n = (r |^ (r |-count n)) * t by NAT_D:def 3;
A16: t divides n by A15, NAT_D:def 3;
reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by A15, ORDINAL1:def 12;
A17: support (ppf t) = support (pfexp t) by NAT_3:def 9;
A18: support (ppf t) c= Seg k

proof

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 A19: x in support (ppf t) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
A20: x in support (pfexp t) by A19, NAT_3:def 9;

A21: now :: thesis: not m = r

assume A22: m = r ; :: thesis: contradiction
(pfexp t) . r = r |-count t by A13, NAT_3:def 8;
then r |-count t <> 0 by A20, A22, PRE_POLY:def 7;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A23: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by A14, NAT_3:def 7;
then consider u being Nat such that
A24: 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 A15, A23, A24, 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 A14, NAT_3:def 7; :: thesis: verum

end;

support (pfexp t) c= support (pfexp n) by A15, NAT_3:45;
then support (ppf t) c= support (ppf n) by A17, NAT_3:def 9;
then m in support (ppf n) by A19;
then m <= k + 1 by A6, FINSEQ_1:1;
then m < r by A21, XXREAL_0:1;
then A25: m <= k by NAT_1:13;
x is Prime by A20, NAT_3:34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A25, FINSEQ_1:1; :: thesis: verum

end;

A26: support (ppf s) = support (pfexp s) by NAT_3:def 9;
r |-count n <> 0

proof

assume r |-count n = 0 ; :: thesis: contradiction
then not r divides n by A14, NAT_3:27;
hence contradiction by A12, NAT_3:36; :: thesis: verum

end;

then A27: support (ppf s) = {r} by A13, A26, NAT_3:42;

A28: 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
A29: x in support (ppf s) and
A30: x in support (ppf t) by XBOOLE_0:3;
x = r by A27, A29, TARSKI:def 1;
then r <= k by A18, A30, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

A31: ( support (ppf m) c= Seg k & support (ppf t) c= Seg k & ( for p being Prime holds p |-count m <= p |-count t ) implies m divides t ) by A4;
( support (ppf n) = support (pfexp n) & support (ppf t) = support (pfexp t) ) by NAT_3:def 9;
then A32: support (ppf n) = (support (ppf s)) \/ (support (ppf t)) by A15, A26, NAT_3:46;
A33: for p being Prime holds p |-count m <= p |-count t

proof

let p be Prime; :: thesis: p |-count m <= p |-count t
A34: p |-count n = (p |-count (r |^ (r |-count n))) + (p |-count t) by A15, NAT_3:28;

per cases ( p in support (ppf n) or not p in support (ppf n) ) ;

suppose A35: p in support (ppf n) ; :: thesis: p |-count m <= p |-count t

per cases ( p in support (ppf s) or p in support (ppf t) ) by A32, A35, XBOOLE_0:def 3;

suppose p in support (ppf s) ; :: thesis: p |-count m <= p |-count t

then A36: p = k + 1 by A27, TARSKI:def 1;

per cases ( p in support (ppf m) or not p in support (ppf m) ) ;

suppose p in support (ppf m) ; :: thesis: p |-count m <= p |-count t

then p <= k by A8, FINSEQ_1:1;
hence p |-count m <= p |-count t by A36, NAT_1:13; :: thesis: verum

end;

suppose not p in support (ppf m) ; :: thesis: p |-count m <= p |-count t

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

end;

end;

end;

suppose p in support (ppf t) ; :: thesis: p |-count m <= p |-count t

then not p in support (ppf s) by A28, XBOOLE_0:3;
then p |-count s = 0 by Th15;
hence p |-count m <= p |-count t by A7, A34; :: thesis: verum

end;

end;

end;

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

then p |-count n = 0 by Th15;
hence p |-count m <= p |-count t by A7; :: thesis: verum

end;

end;

end;

then support (ppf m) c= support (ppf t) by Th17;
hence m divides n by A16, A18, A33, A31, NAT_D:4; :: thesis: verum

end;

suppose A37: ( not support (ppf n) c= Seg k & not support (ppf m) c= Seg k ) ; :: thesis: m divides n

then reconsider w = k + 1 as Prime by A5, Th16;
consider m1 being non zero Element of NAT , e1 being Element of NAT such that
A38: support (ppf m1) c= Seg k and
A39: m = m1 * ((k + 1) |^ e1) and
A40: for p being Prime holds
( ( p in support (ppf m1) implies p |-count m1 = p |-count m ) & ( not p in support (ppf m1) implies p |-count m1 <= p |-count m ) ) by A5, Th18;
consider m2 being non zero Element of NAT , e2 being Element of NAT such that
A41: support (ppf m2) c= Seg k and
A42: n = m2 * ((k + 1) |^ e2) and
A43: for p being Prime holds
( ( p in support (ppf m2) implies p |-count m2 = p |-count n ) & ( not p in support (ppf m2) implies p |-count m2 <= p |-count n ) ) by A6, Th18;
A44: not w divides m2

proof

assume w divides m2 ; :: thesis: contradiction
then w in support (pfexp m2) by NAT_3:37;
then w in support (ppf m2) by NAT_3:def 9;
then w <= k by A41, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

A45: k + 1 is Prime by A5, A37, Th16;
for p being Prime holds p |-count m1 <= p |-count m2

proof

let p be Prime; :: thesis: p |-count m1 <= p |-count m2

per cases ( ( p in support (ppf m1) & p in support (ppf m2) ) or ( not p in support (ppf m1) & p in support (ppf m2) ) or ( p in support (ppf m1) & not p in support (ppf m2) ) or ( not p in support (ppf m1) & not p in support (ppf m2) ) ) ;

suppose ( p in support (ppf m1) & p in support (ppf m2) ) ; :: thesis: p |-count m1 <= p |-count m2

then ( p |-count m1 = p |-count m & p |-count m2 = p |-count n ) by A40, A43;
hence p |-count m1 <= p |-count m2 by A7; :: thesis: verum

end;

suppose ( not p in support (ppf m1) & p in support (ppf m2) ) ; :: thesis: p |-count m1 <= p |-count m2

hence p |-count m1 <= p |-count m2 by Th15; :: thesis: verum

end;

suppose A46: ( p in support (ppf m1) & not p in support (ppf m2) ) ; :: thesis: p |-count m1 <= p |-count m2

m1 divides m by A39, NAT_D:def 3;
then A47: p |-count m1 <= p |-count m by NAT_3:30;
A48: p > 1 by INT_2:def 4;
p in support (pfexp m1) by A46, NAT_3:def 9;
then p divides m1 by NAT_3:36;
then p |-count m1 <> 0 by A48, NAT_3:27;
then p |-count m1 > 0 ;
then p |-count n > 0 by A7, A47;
then A49: p divides n by A48, NAT_3:27;
p |-count m2 = 0 by A46, Th15;
then not p divides m2 by A48, NAT_3:27;
then p divides (k + 1) |^ e2 by A42, A49, NEWTON:80;
then p divides k + 1 by NAT_3:5;
then A50: p = k + 1 by A45, A48, INT_2:def 4;
k < k + 1 by NAT_1:13;
hence p |-count m1 <= p |-count m2 by A38, A46, A50, FINSEQ_1:1; :: thesis: verum

end;

suppose ( not p in support (ppf m1) & not p in support (ppf m2) ) ; :: thesis: p |-count m1 <= p |-count m2

hence p |-count m1 <= p |-count m2 by Th15; :: thesis: verum

end;

end;

end;

then A51: m1 divides m2 by A4, A38, A41;
A52: not w divides m1

proof

assume w divides m1 ; :: thesis: contradiction
then w in support (pfexp m1) by NAT_3:37;
then w in support (ppf m1) by NAT_3:def 9;
then w <= k by A38, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

A53: w > 1 by INT_2:def 4;
then w |-count (w |^ e2) = e2 by NAT_3:25;
then A54: w |-count n = (w |-count m2) + e2 by A42, NAT_3:28
.= 0 + e2 by A53, A44, NAT_3:27
.= e2 ;
w |-count (w |^ e1) = e1 by A53, NAT_3:25;
then w |-count m = (w |-count m1) + e1 by A39, NAT_3:28
.= 0 + e1 by A53, A52, NAT_3:27
.= e1 ;
then (k + 1) |^ e1 divides (k + 1) |^ e2 by A7, A54, NEWTON:89;
hence m divides n by A39, A42, A51, NAT_3:1; :: thesis: verum

end;

suppose A55: support (ppf n) c= Seg k ; :: thesis: m divides n

support (ppf m) c= support (ppf n) by A7, Th17;
then support (ppf m) c= Seg k by A55;
hence m divides n by A4, A7, A55; :: thesis: verum

end;

end;

end;

A56: S₁[ 0 ]

proof

let k, l be non zero Element of NAT ; :: thesis: ( support (ppf k) c= Seg 0 & support (ppf l) c= Seg 0 & ( for p being Prime holds p |-count k <= p |-count l ) implies k divides l )
assume that
A57: support (ppf k) c= Seg 0 and
support (ppf l) c= Seg 0 and
for p being Prime holds p |-count k <= p |-count l ; :: thesis: k divides l
support (ppf k) = {} by A57, XBOOLE_1:3;
then A58: support (pfexp k) = {} by NAT_3:def 9;

per cases ( k <> 1 or k = 1 ) ;

suppose k <> 1 ; :: thesis: k divides l

then ex p being Prime st p divides k by Lm2;
hence k divides l by A58, NAT_3:37; :: thesis: verum

end;

suppose k = 1 ; :: thesis: k divides l

hence k divides l by NAT_D:6; :: thesis: verum

end;

end;

end;

A59: for k being Nat holds S₁[k] from NAT_1:sch 2(A56, A3);
assume A60: for p being Prime holds p |-count m <= p |-count n ; :: thesis: m divides n
then support (ppf m) c= support (ppf n) by Th17;
then support (ppf m) c= Seg k by A2;
hence m divides n by A60, A59, A2, A1; :: thesis: verum