let p be Prime; for n being Element of NAT
for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let n be Element of NAT ; for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let m be non zero Element of NAT ; for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let X be set ; ( X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } & p |^ (p |-count m) in X implies p |-count (Product (Sgm X)) = p |-count m )
set XX = Seg m;
defpred S1[ Element of NAT , Element of NAT , Prime] means ( P1[$1,$2,$3] & $3 |^ ($3 |-count $2) <= p |^ (p |-count $2) );
defpred S2[ Element of NAT , Element of NAT , Prime] means ( P1[$1,$2,$3] & $3 |^ ($3 |-count $2) > p |^ (p |-count $2) );
set X1 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } ;
set X2 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } ;
A1:
now for k1, k2 being Nat st k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } holds
k1 < k2let k1,
k2 be
Nat;
( k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } implies k1 < k2 )assume
(
k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } &
k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )
;
k1 < k2then
( ex
p1 being
prime Element of
NAT st
(
p1 |^ (p1 |-count m) = k1 &
S1[
n,
m,
p1] ) & ex
p2 being
prime Element of
NAT st
(
p2 |^ (p2 |-count m) = k2 &
S2[
n,
m,
p2] ) )
;
hence
k1 < k2
by XXREAL_0:2;
verum end;
set m1 = p |^ (p |-count m);
defpred S3[ Element of NAT , Element of NAT , Prime] means ( P1[$1,$2,$3] & $3 |^ ($3 |-count $2) = p |^ (p |-count $2) );
defpred S4[ Element of NAT , Element of NAT , Prime] means ( P1[$1,$2,$3] & $3 |^ ($3 |-count $2) < p |^ (p |-count $2) );
set X11 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } ;
set X12 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } ;
A3:
now for k1, k2 being Nat st k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } holds
k1 < k2let k1,
k2 be
Nat;
( k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } & k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } implies k1 < k2 )assume
(
k1 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } &
k2 in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )
;
k1 < k2then
( ex
p1 being
prime Element of
NAT st
(
p1 |^ (p1 |-count m) = k1 &
S4[
n,
m,
p1] ) & ex
p2 being
prime Element of
NAT st
(
p2 |^ (p2 |-count m) = k2 &
S3[
n,
m,
p2] ) )
;
hence
k1 < k2
;
verum end;
now for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } let x be
object ;
( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )assume
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
;
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } then consider p9 being
prime Element of
NAT such that A4:
(
p9 |^ (p9 |-count m) = x &
S1[
n,
m,
p9] )
;
( (
p9 |^ (p9 |-count m) = x &
S4[
n,
m,
p9] ) or (
p9 |^ (p9 |-count m) = x &
S3[
n,
m,
p9] ) )
by A4, XXREAL_0:1;
then
(
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } or
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )
;
hence
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] }
by XBOOLE_0:def 3;
verum end;
then A5:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] }
;
assume A6:
X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] }
; ( not p |^ (p |-count m) in X or p |-count (Product (Sgm X)) = p |-count m )
then A7:
X c= Seg m
;
then A8:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } c= {(p |^ (p |-count m))}
;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } holds
Product (Sgm X) > 0
from NAT_4:sch 1();
then A9:
Product (Sgm X) <> 0
by A6;
A10:
1 < p
by INT_2:def 4;
A11: p |-count (p |^ (p |-count m)) =
(p |-count m) * (p |-count p)
by NAT_3:32
.=
(p |-count m) * 1
by A10, NAT_3:22
;
then A12:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } c= X
;
then A13:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } c= Seg m
by A7;
now for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } let x be
object ;
( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } )assume
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] }
;
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } then
ex
p9 being
prime Element of
NAT st
(
p9 |^ (p9 |-count m) = x &
S3[
n,
m,
p9] )
;
hence
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
;
verum end;
then A14:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
;
then A15:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } c= Seg m
by A13;
now for x being object st x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } let x be
object ;
( x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } )assume
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] }
;
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } then
ex
p9 being
prime Element of
NAT st
(
p9 |^ (p9 |-count m) = x &
S4[
n,
m,
p9] )
;
hence
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
;
verum end;
then A16:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
;
then A17:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } c= Seg m
by A13;
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
by A16, A14, XBOOLE_1:13;
then A18: Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } )) =
Sum (p |-count (Sgm ( { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )))
by A5, XBOOLE_0:def 10
.=
Sum (p |-count ((Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } ) ^ (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )))
by A17, A15, A3, FINSEQ_3:42
.=
Sum ((p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } )) ^ (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )))
by Th50
.=
(Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } ))) + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )))
by RVSUM_1:75
;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X2 being set st X2 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } & not p |^ (p |-count m) in X2 holds
p |-count (Product (Sgm X2)) = 0
from NAT_4:sch 2();
then A19:
p |-count (Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )) = 0
by A2;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X2 being set st X2 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } holds
Product (Sgm X2) > 0
from NAT_4:sch 1();
then A20:
Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } ) <> 0
;
now for x being object st x in X holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } let x be
object ;
( x in X implies x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )assume
x in X
;
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } then consider p9 being
prime Element of
NAT such that A21:
(
p9 |^ (p9 |-count m) = x &
P1[
n,
m,
p9] )
by A6;
( (
p9 |^ (p9 |-count m) = x &
S1[
n,
m,
p9] ) or (
p9 |^ (p9 |-count m) = x &
S2[
n,
m,
p9] ) )
by A21;
then
(
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } or
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )
;
hence
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] }
by XBOOLE_0:def 3;
verum end;
then A22:
X c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] }
;
then A23:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } c= X
;
then A24:
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } c= Seg m
by A7;
reconsider m1 = p |^ (p |-count m) as non zero Element of NAT by ORDINAL1:def 12;
assume
p |^ (p |-count m) in X
; p |-count (Product (Sgm X)) = p |-count m
then
p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] }
by A22, A2, XBOOLE_0:def 3;
then
p |^ (p |-count m) in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] }
by A5, A25, XBOOLE_0:def 3;
then
for x being object st x in {(p |^ (p |-count m))} holds
x in { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] }
by TARSKI:def 1;
then A26:
{(p |^ (p |-count m))} c= { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] }
;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X11 being set st X11 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } & not p |^ (p |-count m) in X11 holds
p |-count (Product (Sgm X11)) = 0
from NAT_4:sch 2();
then A27:
p |-count (Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } )) = 0
by A25;
for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X11 being set st X11 = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } holds
Product (Sgm X11) > 0
from NAT_4:sch 1();
then A28:
Product (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S4[n,m,p9] } ) <> 0
;
{ (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } c= X \/ X
by A12, A23, XBOOLE_1:13;
then Sum (p |-count (Sgm X)) =
Sum (p |-count (Sgm ( { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } \/ { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )))
by A22, XBOOLE_0:def 10
.=
Sum (p |-count ((Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } ) ^ (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )))
by A13, A24, A1, FINSEQ_3:42
.=
Sum ((p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } )) ^ (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )))
by Th50
.=
(Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } ))) + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )))
by RVSUM_1:75
;
then p |-count (Product (Sgm X)) =
(Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } ))) + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S2[n,m,p9] } )))
by A9, Th52
.=
(Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S1[n,m,p9] } ))) + 0
by A20, A19, Th52
.=
0 + (Sum (p |-count (Sgm { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : S3[n,m,p9] } )))
by A18, A28, A27, Th52
.=
Sum (p |-count (Sgm {(p |^ (p |-count m))}))
by A26, A8, XBOOLE_0:def 10
.=
Sum (p |-count <*m1*>)
by FINSEQ_3:44
.=
Sum <*(p |-count m1)*>
by Th51
.=
p |-count m1
by RVSUM_1:73
;
hence
p |-count (Product (Sgm X)) = p |-count m
by A11; verum