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 Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of 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;
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: ( y in rng ((fn ^ <*0 *>) + fn1) implies y in NAT )
assume y in rng ((fn ^ <*0 *>) + fn1) ; :: thesis: y in NAT
then ex x being set st
( x in dom ((fn ^ <*0 *>) + fn1) & y = ((fn ^ <*0 *>) + fn1) . x ) by FUNCT_1:def 5;
hence y in NAT ; :: thesis: verum

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: ( 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 )
A10: dom f = (dom (fn ^ <*0 *>)) /\ (dom fn1) by Th41;
A11: len (fn ^ <*0 *>) = (len fn) + (len <*0 *>) by FINSEQ_1:35
.= n + 1 by A3, FINSEQ_1:56 ;
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: ( ( 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;
p > 1 by INT_2:def 5;
then A13: p |^ k >= 1 by PREPOWER:19;
assume A14: k in dom f ; :: thesis: f . k = [\((n + 1) / (p |^ k))/]
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 ( k in dom fn or ex n1 being Nat st
( n1 in dom <*0 *> & k = (len fn) + n1 ) ) by A16, FINSEQ_1:38;

suppose A18: k in dom fn ; :: thesis: (fn ^ <*0 *>) . k = [\(n / (p |^ k))/]

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

end;

suppose ex n1 being Nat st
( n1 in dom <*0 *> & k = (len fn) + n1 ) ; :: thesis: (fn ^ <*0 *>) . k = [\(n / (p |^ k))/]

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:55;
then A21: n1 = 1 by FINSEQ_1:4, TARSKI:def 1;
p > 1 by INT_2:def 5;
then A22: ( p * (p |^ n) > 1 * (p |^ n) & p |^ n > n ) by Th3, XREAL_1:70;
p |^ (n + 1) = (p |^ n) * p by NEWTON:11;
then p |^ k > n by A3, A20, A21, A22, XXREAL_0:2;
then n / (p |^ k) < 1 by XREAL_1:191;
then A23: (n / (p |^ k)) - 1 < 1 - 1 by XREAL_1:11;
(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:57;
hence (fn ^ <*0 *>) . k = [\(n / (p |^ k))/] by A23, INT_1:def 4; :: thesis: verum

end;

end;

end;

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

per cases ( p |^ k divides n + 1 or not p |^ k divides n + 1 ) ;

suppose A25: p |^ k divides n + 1 ; :: thesis: f . k = [\((n + 1) / (p |^ k))/]

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:78
.= 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:63;
A29: (p |^ k) - 1 >= 1 - 1 by A13, XREAL_1:11;
[\(n / (p |^ k))/] + 1 = [\((n / (p |^ k)) + 1)/] by INT_1:51
.= [\((n / (p |^ k)) + ((p |^ k) / (p |^ k)))/] by XCMPLX_1:60
.= [\((n + (p |^ k)) / (p |^ k))/] by XCMPLX_1:63
.= [\(((n + 1) + ((p |^ k) - 1)) / (p |^ k))/]
.= [\(((n + 1) / (p |^ k)) + (((p |^ k) - 1) / (p |^ k)))/] by XCMPLX_1:63
.= ((n + 1) / (p |^ k)) + [\(((p |^ k) - 1) / (p |^ k))/] by A27, INT_1:51
.= ((n + 1) / (p |^ k)) + 0 by A29, A28, INT_1:def 4
.= [\((n + 1) / (p |^ k))/] by A27, INT_1:47 ;
hence f . k = [\((n + 1) / (p |^ k))/] by A7, A15, A24, A17, A25; :: thesis: verum

end;

suppose A30: 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);
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:8;
then (n + 1) mod (p |^ k) >= 1 by NAT_1:13;
then A32: ((n + 1) mod (p |^ k)) - 1 >= 1 - 1 by XREAL_1:11;
( (n + 1) mod (p |^ k) < p |^ k & 0 + (p |^ k) < 1 + (p |^ k) ) by NAT_D:1, XREAL_1:8;
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:11;
then (((n + 1) mod (p |^ k)) - 1) / (p |^ k) < (p |^ k) / (p |^ k) by XREAL_1:76;
then A33: ((((n + 1) mod (p |^ k)) - 1) / (p |^ k)) - 1 < 1 - 1 by A12, XREAL_1:11;
((n + 1) mod (p |^ k)) / (p |^ k) < (p |^ k) / (p |^ k) by NAT_D:1, XREAL_1:76;
then A34: (((n + 1) mod (p |^ k)) / (p |^ k)) - 1 < 1 - 1 by A12, XREAL_1:11;
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:63
.= [\((((n + 1) div (p |^ k)) * ((p |^ k) / (p |^ k))) + ((((n + 1) mod (p |^ k)) - 1) / (p |^ k)))/] by XCMPLX_1:75
.= [\((((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:51
.= ((n + 1) div (p |^ k)) + 0 by A32, A33, INT_1:def 4
.= ((n + 1) div (p |^ k)) + [\(((n + 1) mod (p |^ k)) / (p |^ k))/] by A34, INT_1:def 4
.= [\((((n + 1) div (p |^ k)) * 1) + (((n + 1) mod (p |^ k)) / (p |^ k)))/] by INT_1:51
.= [\((((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:75
.= [\((((p |^ k) * ((n + 1) div (p |^ k))) + ((n + 1) mod (p |^ k))) / (p |^ k))/] by XCMPLX_1:63
.= [\((n + 1) / (p |^ k))/] by NAT_D:2 ;
hence f . k = [\((n + 1) / (p |^ k))/] by A15, A17, A35; :: thesis: verum

end;

end;

end;

reconsider fn1 = fn1 as Element of (n + 1) -tuples_on REAL by A6, FINSEQ_2:110;
reconsider fn0 = fn ^ <*0 *> as Element of (n + 1) -tuples_on REAL by A11, FINSEQ_2:110;
A36: (p |-count (n ! )) + (p |-count (n + 1)) = p |-count ((n ! ) * (n + 1)) by NAT_3:28
.= p |-count ((n + 1) ! ) by NEWTON:21 ;
Sum f = (Sum fn0) + (Sum fn1) by RVSUM_1:119
.= ((Sum fn) + 0 ) + (p |-count (n + 1)) by A8, RVSUM_1:104
.= (p |-count (n ! )) + (p |-count (n + 1)) by A5 ;
hence p |-count ((n + 1) ! ) = Sum f by A36; :: thesis: verum

end;

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

end;

A37: 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 5;
hence p |-count (0 ! ) = Sum (<*> NAT ) by NAT_3:21, NEWTON:18, RVSUM_1:102; :: thesis: verum

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: ( 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 A38; :: thesis: verum