A1:
for a, a1, b, b1 being non zero Nat
for x being Prime st ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) & a1 = a div (x |^ (x |-count a)) & b1 = b div (x |^ (x |-count b)) holds
for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1
proof
let a,
a1,
b,
b1 be non
zero Nat;
for x being Prime st ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) & a1 = a div (x |^ (x |-count a)) & b1 = b div (x |^ (x |-count b)) holds
for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1let x be
Prime;
( ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) & a1 = a div (x |^ (x |-count a)) & b1 = b div (x |^ (x |-count b)) implies for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 )
assume A2:
for
p being
Element of
NAT st
p is
prime holds
p |-count a <= p |-count b
;
( not a1 = a div (x |^ (x |-count a)) or not b1 = b div (x |^ (x |-count b)) or for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 )
set xcb =
x |-count b;
set xca =
x |-count a;
assume A3:
a1 = a div (x |^ (x |-count a))
;
( not b1 = b div (x |^ (x |-count b)) or for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1 )
assume A4:
b1 = b div (x |^ (x |-count b))
;
for p being Element of NAT st p is prime holds
p |-count a1 <= p |-count b1
let p be
Element of
NAT ;
( p is prime implies p |-count a1 <= p |-count b1 )
assume A5:
p is
prime
;
p |-count a1 <= p |-count b1
then A6:
p > 1
by INT_2:def 4;
A7:
x > 1
by INT_2:def 4;
then
x |^ (x |-count a) divides a
by NAT_3:def 7;
then A8:
p |-count a1 = (p |-count a) -' (p |-count (x |^ (x |-count a)))
by A3, A5, NAT_3:31;
x |^ (x |-count b) divides b
by A7, NAT_3:def 7;
then A9:
p |-count b1 = (p |-count b) -' (p |-count (x |^ (x |-count b)))
by A4, A5, NAT_3:31;
per cases
( x = p or x <> p )
;
suppose A10:
x <> p
;
p |-count a1 <= p |-count b1p |-count (x |^ (x |-count b)) =
(x |-count b) * (p |-count x)
by A5, NAT_3:32
.=
(x |-count b) * 0
by A6, A10, NAT_3:24
.=
0
;
then A11:
p |-count b1 =
(p |-count b) - 0
by A9, XREAL_1:233
.=
p |-count b
;
p |-count (x |^ (x |-count a)) =
(x |-count a) * (p |-count x)
by A5, NAT_3:32
.=
(x |-count a) * 0
by A6, A10, NAT_3:24
.=
0
;
then p |-count a1 =
(p |-count a) - 0
by A8, XREAL_1:233
.=
p |-count a
;
hence
p |-count a1 <= p |-count b1
by A2, A5, A11;
verum end; end;
end;
A12:
for a being non zero Nat
for x being Prime holds a div (x |^ (x |-count a)) is non zero Nat
defpred S1[ Nat] means for a, b being non zero Nat st card (support (pfexp b)) = $1 & ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) holds
ex c being Element of NAT st b = a * c;
let a, b be non zero Nat; ( ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) implies ex c being Element of NAT st b = a * c )
assume A15:
for p being Element of NAT st p is prime holds
p |-count a <= p |-count b
; ex c being Element of NAT st b = a * c
A16:
ex n1 being Element of NAT st n1 = card (support (pfexp b))
;
A17:
for n1, n2 being non zero Nat st n1 divides n2 holds
(n2 div n1) * n1 = n2
A18:
for b, b1 being non zero Nat
for x being Prime
for n being Element of NAT st card (support (pfexp b)) = n + 1 & b1 = b div (x |^ (x |-count b)) & x in support (pfexp b) holds
card (support (pfexp b1)) = n
A27:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A28:
S1[
n]
;
S1[n + 1]
for
a,
b being non
zero Nat st
card (support (pfexp b)) = n + 1 & ( for
p being
Element of
NAT st
p is
prime holds
p |-count a <= p |-count b ) holds
ex
c being
Element of
NAT st
b = a * c
proof
let a,
b be non
zero Nat;
( card (support (pfexp b)) = n + 1 & ( for p being Element of NAT st p is prime holds
p |-count a <= p |-count b ) implies ex c being Element of NAT st b = a * c )
assume A29:
card (support (pfexp b)) = n + 1
;
( ex p being Element of NAT st
( p is prime & not p |-count a <= p |-count b ) or ex c being Element of NAT st b = a * c )
then
support (pfexp b) <> {}
;
then consider x being
object such that A30:
x in support (pfexp b)
;
reconsider x =
x as
Prime by A30, NAT_3:34;
set a1 =
a div (x |^ (x |-count a));
set b1 =
b div (x |^ (x |-count b));
reconsider a1 =
a div (x |^ (x |-count a)),
b1 =
b div (x |^ (x |-count b)) as non
zero Nat by A12;
assume A31:
for
p being
Element of
NAT st
p is
prime holds
p |-count a <= p |-count b
;
ex c being Element of NAT st b = a * c
then A32:
for
p being
Element of
NAT st
p is
prime holds
p |-count a1 <= p |-count b1
by A1;
set xca =
x |-count a;
set xcb =
x |-count b;
x in NAT
by ORDINAL1:def 12;
then A33:
(x |-count b) - (x |-count a) = (x |-count b) -' (x |-count a)
by A31, XREAL_1:233;
n in NAT
by ORDINAL1:def 12;
then
card (support (pfexp b1)) = n
by A18, A29, A30;
then consider d being
Element of
NAT such that A34:
b1 = a1 * d
by A28, A32;
reconsider e =
d * (x |^ ((x |-count b) -' (x |-count a))) as
Element of
NAT by ORDINAL1:def 12;
take
e
;
b = a * e
A35:
x <> 1
by INT_2:def 4;
then A36:
x |^ (x |-count a) divides a
by NAT_3:def 7;
x |^ (x |-count b) divides b
by A35, NAT_3:def 7;
then b =
(d * (a div (x |^ (x |-count a)))) * (x |^ ((x |-count a) + ((x |-count b) -' (x |-count a))))
by A17, A34, A33
.=
(d * (a div (x |^ (x |-count a)))) * ((x |^ (x |-count a)) * (x |^ ((x |-count b) -' (x |-count a))))
by NEWTON:8
.=
(d * ((a div (x |^ (x |-count a))) * (x |^ (x |-count a)))) * (x |^ ((x |-count b) -' (x |-count a)))
.=
(d * a) * (x |^ ((x |-count b) -' (x |-count a)))
by A17, A36
.=
a * (d * (x |^ ((x |-count b) -' (x |-count a))))
;
hence
b = a * e
;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A37:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A37, A27);
hence
ex c being Element of NAT st b = a * c
by A15, A16; verum