defpred S1[ 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; ( ( 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 S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let m,
n be non
zero Element of
NAT ;
( 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
;
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 )
;
m divides nreconsider r =
k + 1 as non
zero Element of
NAT ;
set e =
r |-count n;
set s =
r |^ (r |-count n);
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
A26:
support (ppf s) = support (pfexp s)
by NAT_3:def 9;
r |-count n <> 0
then A27:
support (ppf s) = {r}
by A13, A26, NAT_3:42;
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
then
support (ppf m) c= support (ppf t)
by Th17;
hence
m divides n
by A16, A18, A33, A31, NAT_D:4;
verum end; suppose A37:
( not
support (ppf n) c= Seg k & not
support (ppf m) c= Seg k )
;
m divides nthen 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
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;
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 A46:
(
p in support (ppf m1) & not
p in support (ppf m2) )
;
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;
verum end; end;
end; then A51:
m1 divides m2
by A4, A38, A41;
A52:
not
w divides m1
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;
verum end; end;
end;
A56:
S1[ 0 ]
A59:
for k being Nat holds S1[k]
from NAT_1:sch 2(A56, A3);
assume A60:
for p being Prime holds p |-count m <= p |-count n
; 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; verum