let p be Prime; :: thesis: for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P1[n,m,p'] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let n be Element of NAT ; :: thesis: for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P1[n,m,p'] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let m be non empty Element of NAT ; :: thesis: for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P1[n,m,p'] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m
let X be set ; :: thesis: ( X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P1[n,m,p'] } & p |^ (p |-count m) in X implies p |-count (Product (Sgm X)) = p |-count m )
assume A1:
X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P1[n,m,p'] }
; :: thesis: ( not p |^ (p |-count m) in X or p |-count (Product (Sgm X)) = p |-count m )
assume A2:
p |^ (p |-count m) in X
; :: thesis: p |-count (Product (Sgm X)) = p |-count m
set XX = Seg m;
then A3:
X c= Seg m
by TARSKI:def 3;
for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X being set st X = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : P1[n,m,p'] } holds
Product (Sgm X) > 0
from NAT_4:sch 1();
then A4:
Product (Sgm X) <> 0
by A1;
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 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } ;
set X2 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } ;
then A5:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } c= X
by TARSKI:def 3;
then A6:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } c= X
by TARSKI:def 3;
A7:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } c= Seg m
by A3, A5, XBOOLE_1:1;
A8:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } c= Seg m
by A3, A6, XBOOLE_1:1;
A9:
now let k1,
k2 be
Element of
NAT ;
:: thesis: ( k1 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } & k2 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } implies k1 < k2 )assume A10:
(
k1 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } &
k2 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )
;
:: thesis: k1 < k2then A11:
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] )
by A10;
hence
k1 < k2
by A11, XXREAL_0:2;
:: thesis: verum end;
A12:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } c= X \/ X
by A5, A6, XBOOLE_1:13;
now let x be
set ;
:: thesis: ( x in X implies x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )assume
x in X
;
:: thesis: x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } then consider p' being
prime Element of
NAT such that A13:
(
p' |^ (p' |-count m) = x &
P1[
n,
m,
p'] )
by A1;
( (
p' |^ (p' |-count m) = x &
S1[
n,
m,
p'] ) or (
p' |^ (p' |-count m) = x &
S2[
n,
m,
p'] ) )
by A13;
then
(
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } or
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )
;
hence
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] }
by XBOOLE_0:def 3;
:: thesis: verum end;
then A14:
X c= { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] }
by TARSKI:def 3;
then A15: Sum (p |-count (Sgm X)) =
Sum (p |-count (Sgm ({ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )))
by A12, XBOOLE_0:def 10
.=
Sum (p |-count ((Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } ) ^ (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )))
by A7, A8, A9, FINSEQ_3:48
.=
Sum ((p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } )) ^ (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )))
by Th51
.=
(Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } ))) + (Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )))
by RVSUM_1:105
;
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 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } ;
set X12 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } ;
now let x be
set ;
:: thesis: ( x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } implies x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } )assume
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] }
;
:: thesis: x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } then
ex
p' being
prime Element of
NAT st
(
p' |^ (p' |-count m) = x &
S3[
n,
m,
p'] )
;
hence
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
;
:: thesis: verum end;
then A16:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } c= { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
by TARSKI:def 3;
now let x be
set ;
:: thesis: ( x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } implies x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } )assume
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] }
;
:: thesis: x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } then
ex
p' being
prime Element of
NAT st
(
p' |^ (p' |-count m) = x &
S4[
n,
m,
p'] )
;
hence
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
;
:: thesis: verum end;
then A17:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } c= { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
by TARSKI:def 3;
A18:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } c= Seg m
by A7, A16, XBOOLE_1:1;
A19:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } c= Seg m
by A7, A17, XBOOLE_1:1;
A20:
now let k1,
k2 be
Element of
NAT ;
:: thesis: ( k1 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } & k2 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } implies k1 < k2 )assume A21:
(
k1 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } &
k2 in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )
;
:: thesis: k1 < k2then A22:
ex
p1 being
prime Element of
NAT st
(
p1 |^ (p1 |-count m) = k1 &
S3[
n,
m,
p1] )
;
ex
p2 being
prime Element of
NAT st
(
p2 |^ (p2 |-count m) = k2 &
S4[
n,
m,
p2] )
by A21;
hence
k1 < k2
by A22;
:: thesis: verum end;
A23:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } c= { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
by A16, A17, XBOOLE_1:13;
now let x be
set ;
:: thesis: ( x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } implies x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )assume
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
;
:: thesis: x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } then consider p' being
prime Element of
NAT such that A24:
(
p' |^ (p' |-count m) = x &
S1[
n,
m,
p'] )
;
( (
p' |^ (p' |-count m) = x &
S3[
n,
m,
p'] ) or (
p' |^ (p' |-count m) = x &
S4[
n,
m,
p'] ) )
by A24, XXREAL_0:1;
then
(
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } or
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )
;
hence
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] }
by XBOOLE_0:def 3;
:: thesis: verum end;
then A25:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } c= { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] }
by TARSKI:def 3;
then A26: Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } )) =
Sum (p |-count (Sgm ({ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } \/ { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )))
by A23, XBOOLE_0:def 10
.=
Sum (p |-count ((Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } ) ^ (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )))
by A18, A19, A20, FINSEQ_3:48
.=
Sum ((p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } )) ^ (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )))
by Th51
.=
(Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } ))) + (Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )))
by RVSUM_1:105
;
for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X11 being set st X11 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } holds
Product (Sgm X11) > 0
from NAT_4:sch 1();
then A28:
Product (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } ) <> 0
;
for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X11 being set st X11 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } & not p |^ (p |-count m) in X11 holds
p |-count (Product (Sgm X11)) = 0
from NAT_4:sch 2();
then A29:
p |-count (Product (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S3[n,m,p'] } )) = 0
by A27;
for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X2 being set st X2 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } holds
Product (Sgm X2) > 0
from NAT_4:sch 1();
then A31:
Product (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } ) <> 0
;
for p being Prime
for n being Element of NAT
for m being non empty Element of NAT
for X2 being set st X2 = { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } & not p |^ (p |-count m) in X2 holds
p |-count (Product (Sgm X2)) = 0
from NAT_4:sch 2();
then A32:
p |-count (Product (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )) = 0
by A30;
p |^ (p |-count m) in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] }
by A2, A14, A30, XBOOLE_0:def 3;
then
p |^ (p |-count m) in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] }
by A25, A27, XBOOLE_0:def 3;
then
for x being set st x in {(p |^ (p |-count m))} holds
x in { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] }
by TARSKI:def 1;
then A33:
{(p |^ (p |-count m))} c= { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] }
by TARSKI:def 3;
then A34:
{ (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } c= {(p |^ (p |-count m))}
by TARSKI:def 3;
set m1 = p |^ (p |-count m);
reconsider m1 = p |^ (p |-count m) as non empty Element of NAT by ORDINAL1:def 13;
A35:
1 < p
by INT_2:def 5;
A36: p |-count (p |^ (p |-count m)) =
(p |-count m) * (p |-count p)
by NAT_3:32
.=
(p |-count m) * 1
by A35, NAT_3:22
;
p |-count (Product (Sgm X)) =
(Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } ))) + (Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S2[n,m,p'] } )))
by A4, A15, Th53
.=
(Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S1[n,m,p'] } ))) + 0
by A31, A32, Th53
.=
0 + (Sum (p |-count (Sgm { (p' |^ (p' |-count m)) where p' is prime Element of NAT : S4[n,m,p'] } )))
by A26, A28, A29, Th53
.=
Sum (p |-count (Sgm {(p |^ (p |-count m))}))
by A33, A34, XBOOLE_0:def 10
.=
Sum (p |-count <*m1*>)
by FINSEQ_3:50
.=
Sum <*(p |-count m1)*>
by Th52
.=
p |-count m1
by RVSUM_1:103
;
hence
p |-count (Product (Sgm X)) = p |-count m
by A36; :: thesis: verum