defpred S1[ Nat] means for p being Prime ex f being FinSequence of NAT st
( len f = $1 & ( for k being Element of NAT st k in dom f holds
f . k = [\($1 / (p |^ k))/] ) & p |-count ($1 !) = Sum f );
let n be Element of NAT ; for p being Prime ex f being FinSequence of NAT st
( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n !) = Sum f )
let p be Prime; ex f being FinSequence of NAT st
( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n !) = Sum f )
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
for
p being
Prime ex
f being
FinSequence of
NAT st
(
len f = n + 1 & ( for
k being
Element of
NAT st
k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] ) &
p |-count ((n + 1) !) = Sum f )
proof
let p be
Prime;
ex f being FinSequence of NAT st
( len f = n + 1 & ( for k being Element of NAT st k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] ) & p |-count ((n + 1) !) = Sum f )
consider fn being
FinSequence of
NAT such that A3:
len fn = n
and A4:
for
k being
Element of
NAT st
k in dom fn holds
fn . k = [\(n / (p |^ k))/]
and A5:
p |-count (n !) = Sum fn
by A2;
reconsider fnn =
fn as
FinSequence of
REAL by FINSEQ_2:24, NUMBERS:19;
set fn0 =
fnn ^ <*(In (0,REAL))*>;
consider fn1 being
FinSequence of
NAT such that A6:
len fn1 = n + 1
and A7:
for
k being
Element of
NAT st
k in dom fn1 holds
( (
fn1 . k = 1 implies
p |^ k divides n + 1 ) & (
p |^ k divides n + 1 implies
fn1 . k = 1 ) & (
fn1 . k = 0 implies not
p |^ k divides n + 1 ) & ( not
p |^ k divides n + 1 implies
fn1 . k = 0 ) )
and A8:
p |-count (n + 1) = Sum fn1
by Th46;
A9:
Seg (n + 1) = dom fn1
by A6, FINSEQ_1:def 3;
set f =
(fn ^ <*0*>) + fn1;
for
y being
object st
y in rng ((fn ^ <*0*>) + fn1) holds
y in NAT
by ORDINAL1:def 12;
then
rng ((fn ^ <*0*>) + fn1) c= NAT
;
then reconsider f =
(fn ^ <*0*>) + fn1 as
FinSequence of
NAT by FINSEQ_1:def 4;
take
f
;
( len f = n + 1 & ( for k being Element of NAT st k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] ) & p |-count ((n + 1) !) = Sum f )
reconsider fn0 =
fnn ^ <*(In (0,REAL))*> as
FinSequence of
REAL ;
reconsider fn1 =
fn1 as
FinSequence of
REAL by FINSEQ_2:24, NUMBERS:19;
A10:
dom f = (dom fn0) /\ (dom fn1)
by VALUED_1:def 1;
A11:
len fn0 =
(len fn) + (len <*0*>)
by FINSEQ_1:22
.=
n + 1
by A3, FINSEQ_1:39
;
then
Seg (n + 1) = dom fn0
by FINSEQ_1:def 3;
hence
len f = n + 1
by A10, A9, FINSEQ_1:def 3;
( ( for k being Element of NAT st k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] ) & p |-count ((n + 1) !) = Sum f )
thus
for
k being
Element of
NAT st
k in dom f holds
f . k = [\((n + 1) / (p |^ k))/]
p |-count ((n + 1) !) = Sum fproof
let k be
Element of
NAT ;
( k in dom f implies f . k = [\((n + 1) / (p |^ k))/] )
A12:
(p |^ k) / (p |^ k) = 1
by XCMPLX_1:60;
assume A13:
k in dom f
;
f . k = [\((n + 1) / (p |^ k))/]
then A14:
f . k = (fn0 . k) + (fn1 . k)
by VALUED_1:def 1;
A15:
k in dom fn0
by A10, A13, XBOOLE_0:def 4;
A16:
fn0 . k = [\(n / (p |^ k))/]
proof
per cases
( k in dom fn or ex n1 being Nat st
( n1 in dom <*0*> & k = (len fn) + n1 ) )
by A15, FINSEQ_1:25;
suppose
ex
n1 being
Nat st
(
n1 in dom <*0*> &
k = (len fn) + n1 )
;
fn0 . k = [\(n / (p |^ k))/]then consider n1 being
Nat such that A18:
n1 in dom <*0*>
and A19:
k = (len fn) + n1
;
n1 in Seg 1
by A18, FINSEQ_1:38;
then A20:
n1 = 1
by FINSEQ_1:2, TARSKI:def 1;
p > 1
by INT_2:def 4;
then A21:
(
p * (p |^ n) > 1
* (p |^ n) &
p |^ n > n )
by Th3, XREAL_1:68;
p |^ (n + 1) = (p |^ n) * p
by NEWTON:6;
then
p |^ k > n
by A3, A19, A20, A21, XXREAL_0:2;
then
n / (p |^ k) < 1
by XREAL_1:189;
then A22:
(n / (p |^ k)) - 1
< 1
- 1
by XREAL_1:9;
fn0 . (n + 1) = <*0*> . 1
by A3, A18, A20, FINSEQ_1:def 7;
then
fn0 . k = 0
by A3, A19, A20, FINSEQ_1:40;
hence
fn0 . k = [\(n / (p |^ k))/]
by A22, INT_1:def 6;
verum end; end;
end;
A23:
k in dom fn1
by A10, A13, XBOOLE_0:def 4;
per cases
( p |^ k divides n + 1 or not p |^ k divides n + 1 )
;
suppose A28:
not
p |^ k divides n + 1
;
f . k = [\((n + 1) / (p |^ k))/]set m =
(n + 1) mod (p |^ k);
set d =
(n + 1) div (p |^ k);
A29:
n + 1
= ((p |^ k) * ((n + 1) div (p |^ k))) + ((n + 1) mod (p |^ k))
by NAT_D:2;
then
not
(n + 1) mod (p |^ k) = 0
by A28, NAT_D:def 3;
then
((n + 1) mod (p |^ k)) + 1
> 0 + 1
by XREAL_1:6;
then
(n + 1) mod (p |^ k) >= 1
by NAT_1:13;
then A30:
((n + 1) mod (p |^ k)) - 1
>= 1
- 1
by XREAL_1:9;
(
(n + 1) mod (p |^ k) < p |^ k &
0 + (p |^ k) < 1
+ (p |^ k) )
by NAT_D:1, XREAL_1:6;
then
(n + 1) mod (p |^ k) < (p |^ k) + 1
by XXREAL_0:2;
then
((n + 1) mod (p |^ k)) - 1
< ((p |^ k) + 1) - 1
by XREAL_1:9;
then
(((n + 1) mod (p |^ k)) - 1) / (p |^ k) < (p |^ k) / (p |^ k)
by XREAL_1:74;
then A31:
((((n + 1) mod (p |^ k)) - 1) / (p |^ k)) - 1
< 1
- 1
by A12, XREAL_1:9;
((n + 1) mod (p |^ k)) / (p |^ k) < (p |^ k) / (p |^ k)
by NAT_D:1, XREAL_1:74;
then A32:
(((n + 1) mod (p |^ k)) / (p |^ k)) - 1
< 1
- 1
by A12, XREAL_1:9;
A33:
fn1 . k = 0
by A7, A23, A28;
n = ((p |^ k) * ((n + 1) div (p |^ k))) + (((n + 1) mod (p |^ k)) - 1)
by A29;
then [\(n / (p |^ k))/] =
[\((((p |^ k) * ((n + 1) div (p |^ k))) / (p |^ k)) + ((((n + 1) mod (p |^ k)) - 1) / (p |^ k)))/]
by XCMPLX_1:62
.=
[\((((n + 1) div (p |^ k)) * ((p |^ k) / (p |^ k))) + ((((n + 1) mod (p |^ k)) - 1) / (p |^ k)))/]
by XCMPLX_1:74
.=
[\((((n + 1) div (p |^ k)) * 1) + ((((n + 1) mod (p |^ k)) - 1) / (p |^ k)))/]
by XCMPLX_1:60
.=
((n + 1) div (p |^ k)) + [\((((n + 1) mod (p |^ k)) - 1) / (p |^ k))/]
by INT_1:28
.=
((n + 1) div (p |^ k)) + 0
by A30, A31, INT_1:def 6
.=
((n + 1) div (p |^ k)) + [\(((n + 1) mod (p |^ k)) / (p |^ k))/]
by A32, INT_1:def 6
.=
[\((((n + 1) div (p |^ k)) * 1) + (((n + 1) mod (p |^ k)) / (p |^ k)))/]
by INT_1:28
.=
[\((((n + 1) div (p |^ k)) * ((p |^ k) / (p |^ k))) + (((n + 1) mod (p |^ k)) / (p |^ k)))/]
by XCMPLX_1:60
.=
[\((((p |^ k) * ((n + 1) div (p |^ k))) / (p |^ k)) + (((n + 1) mod (p |^ k)) / (p |^ k)))/]
by XCMPLX_1:74
.=
[\((((p |^ k) * ((n + 1) div (p |^ k))) + ((n + 1) mod (p |^ k))) / (p |^ k))/]
by XCMPLX_1:62
.=
[\((n + 1) / (p |^ k))/]
by NAT_D:2
;
hence
f . k = [\((n + 1) / (p |^ k))/]
by A14, A16, A33;
verum end; end;
end;
reconsider fn1 =
fn1 as
Element of
(n + 1) -tuples_on REAL by A6, FINSEQ_2:92;
reconsider fn0 =
fn0 as
Element of
(n + 1) -tuples_on REAL by A11, FINSEQ_2:92;
A34:
(p |-count (n !)) + (p |-count (n + 1)) =
p |-count ((n !) * (n + 1))
by NAT_3:28
.=
p |-count ((n + 1) !)
by NEWTON:15
;
Sum f =
(Sum fn0) + (Sum fn1)
by RVSUM_1:89
.=
((Sum fn) + 0) + (p |-count (n + 1))
by A8, RVSUM_1:74
.=
(p |-count (n !)) + (p |-count (n + 1))
by A5
;
hence
p |-count ((n + 1) !) = Sum f
by A34;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A35:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A35, A1);
then consider f being FinSequence of NAT such that
A36:
( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n !) = Sum f )
;
take
f
; ( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n !) = Sum f )
thus
( len f = n & ( for k being Element of NAT st k in dom f holds
f . k = [\(n / (p |^ k))/] ) & p |-count (n !) = Sum f )
by A36; verum