defpred S₁[ 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 ; :: thesis:
let p be Prime; :: thesis:
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A2: S₁[n] ; :: thesis:
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; :: thesis:
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;
set fn0 = fn ^ <*0*>;
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 Th47;
A9: Seg (n + 1) = dom fn1 by A6, FINSEQ_1:def 3;
set f = (fn ^ <*0*>) + fn1;

now

let y be set ; :: thesis:
assume y in rng ((fn ^ <*0*>) + fn1) ; :: thesis:
then ex x being set st
( x in dom ((fn ^ <*0*>) + fn1) & y = ((fn ^ <*0*>) + fn1) . x ) by FUNCT_1:def 3;
hence y in NAT ; :: thesis:

end;

then rng ((fn ^ <*0*>) + fn1) c= NAT by TARSKI:def 3;
then reconsider f = (fn ^ <*0*>) + fn1 as FinSequence of NAT by FINSEQ_1:def 4;
take f ; :: thesis:
A10: dom f = (dom (fn ^ <*0*>)) /\ (dom fn1) by Th41;
A11: len (fn ^ <*0*>) = (len fn) + (len <*0*>) by FINSEQ_1:22
.= n + 1 by A3, FINSEQ_1:39 ;
then Seg (n + 1) = dom (fn ^ <*0*>) by FINSEQ_1:def 3;
hence len f = n + 1 by A10, A9, FINSEQ_1:def 3; :: thesis:
thus for k being Element of NAT st k in dom f holds
f . k = [\((n + 1) / (p |^ k))/] :: thesis:

proof

let k be Element of NAT ; :: thesis:
A12: (p |^ k) / (p |^ k) = 1 by XCMPLX_1:60;
p > 1 by INT_2:def 4;
then A13: p |^ k >= 1 by PREPOWER:11;
assume A14: k in dom f ; :: thesis:
then A15: f . k = ((fn ^ <*0*>) . k) + (fn1 . k) by VALUED_1:def 1;
A16: k in dom (fn ^ <*0*>) by A10, A14, XBOOLE_0:def 4;
A17: (fn ^ <*0*>) . k = [\(n / (p |^ k))/]

proof

per cases by A16, FINSEQ_1:25;

suppose A18: k in dom fn ; :: thesis:

then fn . k = [\(n / (p |^ k))/] by A4;
hence (fn ^ <*0*>) . k = [\(n / (p |^ k))/] by A18, FINSEQ_1:def 7; :: thesis:

end;

suppose ex n1 being Nat st
( n1 in dom <*0*> & k = (len fn) + n1 ) ; :: thesis:

then consider n1 being Nat such that
A19: n1 in dom <*0*> and
A20: k = (len fn) + n1 ;
n1 in Seg 1 by A19, FINSEQ_1:38;
then A21: n1 = 1 by FINSEQ_1:2, TARSKI:def 1;
p > 1 by INT_2:def 4;
then A22: ( 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, A20, A21, A22, XXREAL_0:2;
then n / (p |^ k) < 1 by XREAL_1:189;
then A23: (n / (p |^ k)) - 1 < 1 - 1 by XREAL_1:9;
(fn ^ <*0*>) . (n + 1) = <*0*> . 1 by A3, A19, A21, FINSEQ_1:def 7;
then (fn ^ <*0*>) . k = 0 by A3, A20, A21, FINSEQ_1:40;
hence (fn ^ <*0*>) . k = [\(n / (p |^ k))/] by A23, INT_1:def 6; :: thesis:

end;

end;

end;

A24: k in dom fn1 by A10, A14, XBOOLE_0:def 4;

per cases ;

suppose A25: p |^ k divides n + 1 ; :: thesis:

then consider r being Nat such that
A26: n + 1 = (p |^ k) * r by NAT_D:def 3;
A27: (n + 1) / (p |^ k) = r / ((p |^ k) / (p |^ k)) by A26, XCMPLX_1:77
.= r / (1 / 1) by XCMPLX_1:60
.= r ;
(((p |^ k) / (p |^ k)) + ((- 1) / (p |^ k))) - 1 < 0 by A12;
then A28: (((p |^ k) + (- 1)) / (p |^ k)) - 1 < 0 by XCMPLX_1:62;
A29: (p |^ k) - 1 >= 1 - 1 by A13, XREAL_1:9;
[\(n / (p |^ k))/] + 1 = [\((n / (p |^ k)) + 1)/] by INT_1:28
.= [\((n / (p |^ k)) + ((p |^ k) / (p |^ k)))/] by XCMPLX_1:60
.= [\((n + (p |^ k)) / (p |^ k))/] by XCMPLX_1:62
.= [\(((n + 1) + ((p |^ k) - 1)) / (p |^ k))/]
.= [\(((n + 1) / (p |^ k)) + (((p |^ k) - 1) / (p |^ k)))/] by XCMPLX_1:62
.= ((n + 1) / (p |^ k)) + [\(((p |^ k) - 1) / (p |^ k))/] by A27, INT_1:28
.= ((n + 1) / (p |^ k)) + 0 by A29, A28, INT_1:def 6
.= [\((n + 1) / (p |^ k))/] by A27, INT_1:25 ;
hence f . k = [\((n + 1) / (p |^ k))/] by A7, A15, A24, A17, A25; :: thesis:

end;

suppose A30: not p |^ k divides n + 1 ; :: thesis:

set m = (n + 1) mod (p |^ k);
set d = (n + 1) div (p |^ k);
A31: 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 A30, 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 A32: ((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 A33: ((((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 A34: (((n + 1) mod (p |^ k)) / (p |^ k)) - 1 < 1 - 1 by A12, XREAL_1:9;
A35: fn1 . k = 0 by A7, A24, A30;
n = ((p |^ k) * ((n + 1) div (p |^ k))) + (((n + 1) mod (p |^ k)) - 1) by A31;
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 A32, A33, INT_1:def 6
.= ((n + 1) div (p |^ k)) + [\(((n + 1) mod (p |^ k)) / (p |^ k))/] by A34, 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 A15, A17, A35; :: thesis:

end;

end;

end;

reconsider fn1 = fn1 as Element of (n + 1) -tuples_on REAL by A6, FINSEQ_2:92;
reconsider fn0 = fn ^ <*0*> as Element of (n + 1) -tuples_on REAL by A11, FINSEQ_2:92;
A36: (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 A36; :: thesis:

end;

hence S₁[n + 1] ; :: thesis:

end;

A37: S₁[ 0 ]

proof

set f = <*> NAT;
let p be Prime; :: thesis:
take <*> NAT ; :: thesis:
thus len (<*> NAT) = 0 ; :: thesis:
thus for k being Element of NAT st k in dom (<*> NAT) holds
(<*> NAT) . k = [\(0 / (p |^ k))/] ; :: thesis:
p <> 1 by INT_2:def 4;
hence p |-count (0 !) = Sum (<*> NAT) by NAT_3:21, NEWTON:12, RVSUM_1:72; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A37, A1);
then consider f being FinSequence of NAT such that
A38: ( 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 ; :: thesis:
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 A38; :: thesis: