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: 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; :: thesis: 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( ( 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))/] :: thesis: p |-count ((n + 1) !) = Sum f

proof

let k be Element of NAT ; :: thesis: ( 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 ; :: thesis: 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 A17: k in dom fn ; :: thesis: fn0 . k = [\(n / (p |^ k))/]

then fn . k = [\(n / (p |^ k))/] by A4;
hence fn0 . k = [\(n / (p |^ k))/] by A17, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ex n1 being Nat st
( n1 in dom <*0*> & k = (len fn) + n1 ) ; :: thesis: 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;
hence fn0 . k = [\(n / (p |^ k))/] by A22, INT_1:def 6; :: thesis: 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 A24: p |^ k divides n + 1 ; :: thesis: f . k = [\((n + 1) / (p |^ k))/]

then consider r being Nat such that
A25: n + 1 = (p |^ k) * r by NAT_D:def 3;
A26: (n + 1) / (p |^ k) = r / ((p |^ k) / (p |^ k)) by A25, XCMPLX_1:77
.= r / (1 / 1) by XCMPLX_1:60
.= r ;
(((p |^ k) / (p |^ k)) + ((- 1) / (p |^ k))) - 1 < 0 by A12;
then A27: (((p |^ k) + (- 1)) / (p |^ k)) - 1 < 0 by XCMPLX_1:62;
[\(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 A26, INT_1:28
.= ((n + 1) / (p |^ k)) + 0 by A27, INT_1:def 6
.= [\((n + 1) / (p |^ k))/] by A26 ;
hence f . k = [\((n + 1) / (p |^ k))/] by A7, A14, A23, A16, A24; :: thesis: verum

end;

suppose A28: not p |^ k divides n + 1 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

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

end;

A35: S₁[ 0 ]

proof

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

end;

for n being Nat holds S₁[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 ; :: thesis: ( 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; :: thesis: verum