defpred S1[ Nat] means for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ $1 & Product p = Product q holds
p = q;
A1:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A2:
S1[
k]
;
S1[k + 1]now for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ (k + 1) & Product p = Product q holds
p = qlet p,
q be
bag of
SetPrimes ;
( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ (k + 1) & Product p = Product q implies p = q )assume that A3:
p is
prime-factorization-like
and A4:
q is
prime-factorization-like
and A5:
Product p <= 2
|^ (k + 1)
and A6:
Product p = Product q
;
p = qnow p = qper cases
( support p = {} or support p <> {} )
;
suppose
support p <> {}
;
p = qthen consider x being
object such that A8:
x in support p
by XBOOLE_0:def 1;
reconsider x =
x as
Prime by A8, NEWTON:def 6;
A9:
x divides Product p
by A3, A8, Lm4;
then A10:
x in support q
by A4, A6, Lm7;
per cases
( p . x <> x or p . x = x )
;
suppose
p . x <> x
;
p = qthen consider p1,
r1 being
bag of
SetPrimes such that A11:
p1 is
prime-factorization-like
and
support r1 = {x}
and
Product r1 = x
and A12:
support p1 = support p
and A13:
p1 | ((support p1) \ {x}) = p | ((support p1) \ {x})
and A14:
p . x = (p1 . x) * x
and A15:
Product p = (Product p1) * x
by A3, A8, Lm10;
per cases
( q . x <> x or q . x = x )
;
suppose A16:
q . x <> x
;
p = q
1
< x
by INT_2:def 4;
then
1
+ 1
<= x
by NAT_1:13;
then A17:
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2
by XREAL_1:118;
consider q1,
r2 being
bag of
SetPrimes such that A18:
q1 is
prime-factorization-like
and
support r2 = {x}
and
Product r2 = x
and A19:
support q1 = support q
and A20:
q1 | ((support q1) \ {x}) = q | ((support q1) \ {x})
and A21:
q . x = (q1 . x) * x
and A22:
Product q = (Product q1) * x
by A4, A6, A9, A16, Lm7, Lm10;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x
by A5, A15, XREAL_1:72;
then
((Product p1) * x) / x <= (2 |^ (k + 1)) / 2
by A17, XXREAL_0:2;
then
Product p1 <= (2 |^ (k + 1)) / 2
by XCMPLX_1:89;
then
Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2
by NEWTON:8;
then A23:
Product p1 <= ((2 |^ k) * 2) / 2
;
then A24:
p1 = q1
by A2, A6, A11, A15, A18, A22, XCMPLX_1:5;
A25:
now for z being set st z in support p holds
p . z = q . zlet z be
set ;
( z in support p implies p . b1 = q . b1 )assume A26:
z in support p
;
p . b1 = q . b1per cases
( not z in {x} or z in {x} )
;
suppose A28:
z in {x}
;
p . b1 = q . b1hence p . z =
(p1 . x) * x
by A14, TARSKI:def 1
.=
(q1 . x) * x
by A2, A6, A11, A15, A18, A22, A23, XCMPLX_1:5
.=
q . z
by A21, A28, TARSKI:def 1
;
verum end; end; end; A29:
dom p =
SetPrimes
by PARTFUN1:def 2
.=
dom q
by PARTFUN1:def 2
;
support p = support q
by A2, A6, A11, A12, A15, A18, A19, A22, A23, XCMPLX_1:5;
then
p | (support p) = q | (support q)
by A29, A25, FUNCT_1:96;
hence
p = q
by Th3;
verum end; suppose A30:
q . x = x
;
p = q
1
< x
by INT_2:def 4;
then
1
+ 1
<= x
by NAT_1:13;
then A31:
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2
by XREAL_1:118;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x
by A5, A15, XREAL_1:72;
then
((Product p1) * x) / x <= (2 |^ (k + 1)) / 2
by A31, XXREAL_0:2;
then
Product p1 <= (2 |^ (k + 1)) / 2
by XCMPLX_1:89;
then
Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2
by NEWTON:8;
then A32:
Product p1 <= ((2 |^ k) * 2) / 2
;
ex
q1,
r2 being
bag of
SetPrimes st
(
q1 is
prime-factorization-like &
support r2 = {x} &
Product r2 = x &
support q1 = (support q) \ {x} &
q1 | (support q1) = q | (support q1) &
Product q = (Product q1) * x )
by A4, A6, A9, A30, Lm7, Lm9;
then
support p = (support q) \ {x}
by A2, A6, A11, A12, A15, A32, XCMPLX_1:5;
then
not
x in {x}
by A8, XBOOLE_0:def 5;
hence
p = q
by TARSKI:def 1;
verum end; end; end; suppose A33:
p . x = x
;
p = qthen consider p1,
r1 being
bag of
SetPrimes such that A34:
p1 is
prime-factorization-like
and
support r1 = {x}
and
Product r1 = x
and A35:
support p1 = (support p) \ {x}
and A36:
p1 | (support p1) = p | (support p1)
and A37:
Product p = (Product p1) * x
by A3, A8, Lm9;
per cases
( q . x <> x or q . x = x )
;
suppose A38:
q . x <> x
;
p = q
1
< x
by INT_2:def 4;
then
1
+ 1
<= x
by NAT_1:13;
then A39:
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2
by XREAL_1:118;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x
by A5, A37, XREAL_1:72;
then
((Product p1) * x) / x <= (2 |^ (k + 1)) / 2
by A39, XXREAL_0:2;
then
Product p1 <= (2 |^ (k + 1)) / 2
by XCMPLX_1:89;
then
Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2
by NEWTON:8;
then A40:
Product p1 <= ((2 |^ k) * 2) / 2
;
ex
q1,
r2 being
bag of
SetPrimes st
(
q1 is
prime-factorization-like &
support r2 = {x} &
Product r2 = x &
support q1 = support q &
q1 | ((support q1) \ {x}) = q | ((support q1) \ {x}) &
q . x = (q1 . x) * x &
Product q = (Product q1) * x )
by A4, A6, A9, A38, Lm7, Lm10;
then
(support p) \ {x} = support q
by A2, A6, A34, A35, A37, A40, XCMPLX_1:5;
then
not
x in {x}
by A10, XBOOLE_0:def 5;
hence
p = q
by TARSKI:def 1;
verum end; suppose A41:
q . x = x
;
p = q
1
< x
by INT_2:def 4;
then
1
+ 1
<= x
by NAT_1:13;
then A42:
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2
by XREAL_1:118;
consider q1,
r2 being
bag of
SetPrimes such that A43:
q1 is
prime-factorization-like
and
support r2 = {x}
and
Product r2 = x
and A44:
support q1 = (support q) \ {x}
and A45:
q1 | (support q1) = q | (support q1)
and A46:
Product q = (Product q1) * x
by A4, A6, A9, A41, Lm7, Lm9;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x
by A5, A37, XREAL_1:72;
then
((Product p1) * x) / x <= (2 |^ (k + 1)) / 2
by A42, XXREAL_0:2;
then
Product p1 <= (2 |^ (k + 1)) / 2
by XCMPLX_1:89;
then
Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2
by NEWTON:8;
then A47:
Product p1 <= ((2 |^ k) * 2) / 2
;
then
(support p) \ {x} = (support q) \ {x}
by A2, A6, A34, A35, A37, A43, A44, A46, XCMPLX_1:5;
then
(support p) \/ {x} = ((support q) \ {x}) \/ {x}
by XBOOLE_1:39;
then A48:
(support p) \/ {x} = (support q) \/ {x}
by XBOOLE_1:39;
A49:
p1 = q1
by A2, A6, A34, A37, A43, A46, A47, XCMPLX_1:5;
A54:
{x} c= support q
by A10, ZFMISC_1:31;
{x} c= support p
by A8, ZFMISC_1:31;
then A55:
support p = (support q) \/ {x}
by A48, XBOOLE_1:12;
dom p =
SetPrimes
by PARTFUN1:def 2
.=
dom q
by PARTFUN1:def 2
;
then p | (support p) =
q | (support p)
by A50, FUNCT_1:96
.=
q | (support q)
by A54, A55, XBOOLE_1:12
;
hence
p = q
by Th3;
verum end; end; end; end; end; end; end; hence
p = q
;
verum end; hence
S1[
k + 1]
;
verum end;
A56:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A56, A1);
hence
for n being Element of NAT
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ n & Product p = Product q holds
p = q
; verum