let n be Element of NAT ; :: thesis: for p being Prime ex f being FinSequence of REAL st
( len f = 2 * n & ( for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) & p |-count ((2 * n) choose n) = Sum f )
let p be Prime; :: thesis: ex f being FinSequence of REAL st
( len f = 2 * n & ( for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) & p |-count ((2 * n) choose n) = Sum f )
set f0 = n |-> 0 ;
consider f1 being FinSequence of NAT such that
A1: len f1 = n and
A2: for k being Element of NAT st k in dom f1 holds
f1 . k = [\(n / (p |^ k))/] and
A3: p |-count (n ! ) = Sum f1 by Th48;
consider f2 being FinSequence of NAT such that
A4: len f2 = 2 * n and
A5: for k being Element of NAT st k in dom f2 holds
f2 . k = [\((2 * n) / (p |^ k))/] and
A6: p |-count ((2 * n) ! ) = Sum f2 by Th48;
reconsider f2 = f2 as FinSequence of REAL ;
set f = f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))));
take f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))) ; :: thesis: ( len (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) = 2 * n & ( for k being Element of NAT st k in dom (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) holds
(f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) & p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) )
A7: dom (f1 ^ (n |-> 0 )) = Seg ((len f1) + (len (n |-> 0 ))) by FINSEQ_1:def 7
.= Seg (n + n) by A1, FINSEQ_1:def 18
.= Seg (2 * n) ;
A8: dom ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))) = (dom (- (f1 ^ (n |-> 0 )))) /\ (dom (- (f1 ^ (n |-> 0 )))) by Th41
.= Seg (2 * n) by A7, VALUED_1:8 ;
A9: dom (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) = (dom f2) /\ (dom ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) by Th41
.= (Seg (2 * n)) /\ (Seg (2 * n)) by A4, A8, FINSEQ_1:def 3 ;
hence len (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) = 2 * n by FINSEQ_1:def 3; :: thesis: ( ( for k being Element of NAT st k in dom (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) holds
(f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) & p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) )
thus for k being Element of NAT st k in dom (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) holds
(f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) :: thesis: p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))))

proof

let k be Element of NAT ; :: thesis: ( k in dom (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) implies (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) )
assume A10: k in dom (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) ; :: thesis: (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])
then A11: k in dom f2 by A4, A9, FINSEQ_1:def 3;
A12: (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = (f2 . k) + (((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))) . k) by A10, VALUED_1:def 1
.= (f2 . k) + (((- (f1 ^ (n |-> 0 ))) . k) + ((- (f1 ^ (n |-> 0 ))) . k)) by A8, A9, A10, VALUED_1:def 1
.= (f2 . k) + (2 * ((- (f1 ^ (n |-> 0 ))) . k))
.= (f2 . k) + (2 * (- ((f1 ^ (n |-> 0 )) . k))) by RVSUM_1:35
.= (f2 . k) - (2 * ((f1 ^ (n |-> 0 )) . k))
.= [\((2 * n) / (p |^ k))/] - (2 * ((f1 ^ (n |-> 0 )) . k)) by A5, A11 ;

per cases ( k in dom f1 or ex e being Nat st
( e in dom (n |-> 0 ) & k = (len f1) + e ) ) by A7, A9, A10, FINSEQ_1:38;

suppose A13: k in dom f1 ; :: thesis: (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])

then (f1 ^ (n |-> 0 )) . k = f1 . k by FINSEQ_1:def 7
.= [\(n / (p |^ k))/] by A2, A13 ;
hence (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A12; :: thesis: verum

end;

suppose ex e being Nat st
( e in dom (n |-> 0 ) & k = (len f1) + e ) ; :: thesis: (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])

then consider e being Nat such that
A14: ( e in dom (n |-> 0 ) & k = (len f1) + e ) ;
A15: dom (n |-> 0 ) = Seg n by FUNCOP_1:19;
then e >= 1 by A14, FINSEQ_1:3;
then e + (len f1) >= 1 + (len f1) by XREAL_1:8;
then A16: ( k > 1 + n or k = 1 + n ) by A1, A14, XXREAL_0:1;
p > 1 by INT_2:def 5;
then p to_power k >= p to_power (1 + n) by A16, POWER:44;
then p |^ k >= p to_power (1 + n) by POWER:46;
then A17: p |^ k >= p |^ (1 + n) by POWER:46;
A18: p > 1 by INT_2:def 5;
then p * (p |^ n) > 1 * (p |^ n) by XREAL_1:70;
then p |^ (1 + n) > p |^ n by NEWTON:11;
then A19: p |^ k > p |^ n by A17, XXREAL_0:2;
A20: (f1 ^ (n |-> 0 )) . k = (n |-> 0 ) . e by A14, FINSEQ_1:def 7
.= 0 by A14, A15, FUNCOP_1:13 ;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])

hence (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A12, A20, INT_1:47; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/])

then A21: n / (p |^ n) > n / (p |^ k) by A19, XREAL_1:78;
(p |^ n) / (p |^ n) > n / (p |^ n) by A18, Th3, XREAL_1:76;
then 1 > n / (p |^ n) by XCMPLX_1:60;
then 1 > n / (p |^ k) by A21, XXREAL_0:2;
then 1 - 1 > (n / (p |^ k)) - 1 by XREAL_1:11;
hence (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A12, A20, INT_1:def 4; :: thesis: verum

end;

end;

end;

end;

end;

p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))))

proof

per cases ( n = 0 or n <> 0 ) ;

suppose A22: n = 0 ; :: thesis: p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))))

p > 1 by INT_2:def 5;
then A23: p |-count ((2 * n) choose n) = 0 by A22, NAT_3:21, NEWTON:27;
len (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) = 0 by A9, A22, FINSEQ_1:def 3;
hence p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) by A23, PROB_3:67; :: thesis: verum

end;

suppose A24: n <> 0 ; :: thesis: p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))))

A25: n ! <> 0 by NEWTON:23;
A27: ( n + n > n + 0 & (2 * n) - n = n ) by A24, XREAL_1:8;
then A28: (2 * n) choose n = ((2 * n) ! ) / ((n ! ) * (n ! )) by NEWTON:def 3;
((2 * n) choose n) * ((n ! ) * (n ! )) = (((2 * n) ! ) / ((n ! ) * (n ! ))) * ((n ! ) * (n ! )) by A27, NEWTON:def 3
.= (2 * n) ! by A25, XCMPLX_1:88 ;
then A29: (n ! ) * (n ! ) divides (2 * n) ! by NAT_D:def 3;
then A30: (2 * n) choose n = (((n ! ) * (n ! )) * (((2 * n) ! ) div ((n ! ) * (n ! )))) / ((n ! ) * (n ! )) by A28, NAT_D:3
.= ((2 * n) ! ) div ((n ! ) * (n ! )) by A25, XCMPLX_1:90 ;
A31: (2 * n) ! <> 0 by NEWTON:23;
then A32: p |-count (((2 * n) ! ) div ((n ! ) * (n ! ))) = (p |-count ((2 * n) ! )) -' (p |-count ((n ! ) * (n ! ))) by A25, A29, NAT_3:31
.= (p |-count ((2 * n) ! )) - (p |-count ((n ! ) * (n ! ))) by A25, A29, A31, NAT_3:30, XREAL_1:235 ;
A33: len ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 )))) = len f2 by A4, A8, FINSEQ_1:def 3;
A34: f2 is Element of (len f2) -tuples_on REAL by FINSEQ_2:110;
A35: (- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))) is Element of (len ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) -tuples_on REAL by FINSEQ_2:110;
A36: - (f1 ^ (n |-> 0 )) is Element of (len (- (f1 ^ (n |-> 0 )))) -tuples_on REAL by FINSEQ_2:110;
Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) = (Sum f2) + (Sum ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) by A33, A34, A35, RVSUM_1:119
.= (Sum f2) + ((Sum (- (f1 ^ (n |-> 0 )))) + (Sum (- (f1 ^ (n |-> 0 ))))) by A36, RVSUM_1:119
.= (Sum f2) + ((- (Sum (f1 ^ (n |-> 0 )))) + (Sum (- (f1 ^ (n |-> 0 ))))) by RVSUM_1:118
.= (Sum f2) + ((- (Sum (f1 ^ (n |-> 0 )))) + (- (Sum (f1 ^ (n |-> 0 ))))) by RVSUM_1:118
.= (Sum f2) - (2 * (Sum (f1 ^ (n |-> 0 ))))
.= (Sum f2) - (2 * ((Sum f1) + (Sum (n |-> 0 )))) by RVSUM_1:105
.= (Sum f2) - (2 * ((Sum f1) + (n * 0 ))) by RVSUM_1:110
.= (p |-count ((2 * n) ! )) - ((p |-count (n ! )) + (p |-count (n ! ))) by A3, A6
.= p |-count (((2 * n) ! ) div ((n ! ) * (n ! ))) by A25, A32, NAT_3:28 ;
hence p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) by A30; :: thesis: verum

end;

end;

end;

hence p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0 ))) + (- (f1 ^ (n |-> 0 ))))) ; :: thesis: verum