let p be bag of SetPrimes ; for x being Prime st p is prime-factorization-like & x in support p & p . x <> x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
let x be Prime; ( p is prime-factorization-like & x in support p & p . x <> x implies ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x ) )
assume that
A1:
p is prime-factorization-like
and
A2:
x in support p
and
A3:
p . x <> x
; ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
consider nx being Nat such that
A4:
0 < nx
and
A5:
p . x = x |^ nx
by A1, A2;
consider mx being Nat such that
A6:
nx = mx + 1
by A4, NAT_1:6;
A7:
mx <> 0
by A3, A5, A6;
A8:
dom (SetPrimes --> 0) = SetPrimes
by FUNCOP_1:13;
then A9:
x in dom (SetPrimes --> 0)
by NEWTON:def 6;
set r10 = (SetPrimes --> 0) +* (x,x);
x is Element of NAT
by ORDINAL1:def 12;
then A10:
ex r1 being bag of SetPrimes st
( r1 = (SetPrimes --> 0) +* (x,x) & support r1 = {x} & Product r1 = x )
by Lm8;
A11:
{x} c= support p
by A2, ZFMISC_1:31;
then consider q, r being bag of SetPrimes such that
A12:
support q = (support p) \ {x}
and
A13:
support r = {x}
and
A14:
support q misses support r
and
A15:
q | (support q) = p | (support q)
and
A16:
r | (support r) = p | (support r)
and
A17:
q + r = p
by Lm3;
A18:
x in support r
by A13, TARSKI:def 1;
then A19: r . x =
(r | (support r)) . x
by FUNCT_1:49
.=
p . x
by A16, A18, FUNCT_1:49
;
then A20: (r . x) / x =
((x |^ mx) * x) / x
by A5, A6, NEWTON:6
.=
x |^ mx
by XCMPLX_1:89
;
then reconsider rxx = (r . x) / x as Element of NAT by ORDINAL1:def 12;
set r20 = (SetPrimes --> 0) +* (x,rxx);
rxx <> 0
then consider r2 being bag of SetPrimes such that
A22:
r2 = (SetPrimes --> 0) +* (x,rxx)
and
A23:
support r2 = {x}
and
A24:
Product r2 = rxx
by Lm8;
set p1 = q + r2;
A25:
r = (SetPrimes --> 0) +* (x,(r . x))
by A13, Th1;
A26:
now for z being set st z in (support (q + r2)) \ {x} holds
(q + r2) . z = p . zlet z be
set ;
( z in (support (q + r2)) \ {x} implies (q + r2) . z = p . z )A27:
(q + r2) . z = (q . z) + (r2 . z)
by PRE_POLY:def 5;
assume A28:
z in (support (q + r2)) \ {x}
;
(q + r2) . z = p . zthen
not
z in {x}
by XBOOLE_0:def 5;
then A29:
r2 . z = 0
by A23, PRE_POLY:def 7;
z in support (q + r2)
by A28, XBOOLE_0:def 5;
then
z in (support q) \/ (support r2)
by PRE_POLY:38;
then A30:
(
z in support q or
z in support r2 )
by XBOOLE_0:def 3;
then q . z =
(q | (support q)) . z
by A23, A28, FUNCT_1:49, XBOOLE_0:def 5
.=
p . z
by A15, A23, A28, A30, FUNCT_1:49, XBOOLE_0:def 5
;
hence
(q + r2) . z = p . z
by A27, A29;
verum end;
dom (q + r2) =
SetPrimes
by PARTFUN1:def 2
.=
dom p
by PARTFUN1:def 2
;
then A31:
(q + r2) | ((support (q + r2)) \ {x}) = p | ((support (q + r2)) \ {x})
by A26, FUNCT_1:96;
A32:
(support q) /\ (support r) = {}
by A14, XBOOLE_0:def 7;
now for z being Prime st z in support (q + r2) holds
ex n being Nat st
( 0 < n & (q + r2) . z = z |^ n )let z be
Prime;
( z in support (q + r2) implies ex n being Nat st
( 0 < b2 & (q + r2) . n = n |^ b2 ) )A33:
(q + r2) . z = (q . z) + (r2 . z)
by PRE_POLY:def 5;
assume
z in support (q + r2)
;
ex n being Nat st
( 0 < b2 & (q + r2) . n = n |^ b2 )then A34:
z in (support q) \/ (support r2)
by PRE_POLY:38;
per cases
( z in support q or z in support r2 )
by A34, XBOOLE_0:def 3;
suppose A35:
z in support q
;
ex n being Nat st
( 0 < b2 & (q + r2) . n = n |^ b2 )then
not
z in {x}
by A12, XBOOLE_0:def 5;
then A36:
r2 . z = 0
by A23, PRE_POLY:def 7;
A37:
support q c= support p
by A12, XBOOLE_1:36;
q . z =
(q | (support q)) . z
by A35, FUNCT_1:49
.=
p . z
by A15, A35, FUNCT_1:49
;
hence
ex
n being
Nat st
(
0 < n &
(q + r2) . z = z |^ n )
by A1, A33, A35, A37, A36;
verum end; suppose A38:
z in support r2
;
ex mx being Nat st
( 0 < b2 & (q + r2) . mx = mx |^ b2 )take mx =
mx;
( 0 < mx & (q + r2) . z = z |^ mx )thus
0 < mx
by A7;
(q + r2) . z = z |^ mxA39:
z = x
by A23, A38, TARSKI:def 1;
A40:
not
z in support q
by A13, A32, A23, A38, XBOOLE_0:def 4;
(q + r2) . z =
(q . z) + (r2 . z)
by PRE_POLY:def 5
.=
0 + (r2 . z)
by A40, PRE_POLY:def 7
.=
z |^ mx
by A20, A22, A8, A38, A39, FUNCT_7:31
;
hence
(q + r2) . z = z |^ mx
;
verum end; end;
then A41:
q + r2 is prime-factorization-like
;
x in {x}
by TARSKI:def 1;
then A42:
not x in support q
by A12, XBOOLE_0:def 5;
(q + r2) . x =
(q . x) + (r2 . x)
by PRE_POLY:def 5
.=
0 + (r2 . x)
by A42, PRE_POLY:def 7
.=
rxx
by A22, A9, FUNCT_7:31
;
then A43:
p . x = ((q + r2) . x) * x
by A19, XCMPLX_1:87;
r . x = rxx * x
by XCMPLX_1:87;
then
ex rr1 being bag of SetPrimes st
( rr1 = r & support rr1 = {x} & Product rr1 = rxx * x )
by A5, A19, A25, Lm8;
then A44: Product p =
(Product q) * ((Product r2) * x)
by A14, A17, A24, NAT_3:19
.=
((Product q) * (Product r2)) * x
.=
(Product (q + r2)) * x
by A13, A14, A23, NAT_3:19
;
support (q + r2) =
((support p) \ {x}) \/ {x}
by A12, A23, PRE_POLY:38
.=
(support p) \/ {x}
by XBOOLE_1:39
.=
support p
by A11, XBOOLE_1:12
;
hence
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
by A10, A43, A44, A41, A31; verum