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, CARD_1:def 7
.= 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:17
.= (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:25;

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) and
A15: k = (len f1) + e ;
A16: dom (n |-> 0) = Seg n by FUNCOP_1:13;
then e >= 1 by A14, FINSEQ_1:1;
then e + (len f1) >= 1 + (len f1) by XREAL_1:6;
then A17: ( k > 1 + n or k = 1 + n ) by A1, A15, XXREAL_0:1;
A18: (f1 ^ (n |-> 0)) . k = (n |-> 0) . e by A14, A15, FINSEQ_1:def 7
.= 0 by A14, A16, FUNCOP_1:7 ;
p > 1 by INT_2:def 4;
then p to_power k >= p to_power (1 + n) by A17, POWER:39;
then p |^ k >= p to_power (1 + n) by POWER:41;
then A19: p |^ k >= p |^ (1 + n) by POWER:41;
A20: p > 1 by INT_2:def 4;
then p * (p |^ n) > 1 * (p |^ n) by XREAL_1:68;
then p |^ (1 + n) > p |^ n by NEWTON:6;
then A21: p |^ k > p |^ n by A19, XXREAL_0:2;

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, A18, INT_1:25; :: thesis: verum

end;

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

(p |^ n) / (p |^ n) > n / (p |^ n) by A20, Th3, XREAL_1:74;
then A23: 1 > n / (p |^ n) by XCMPLX_1:60;
n / (p |^ n) > n / (p |^ k) by A21, A22, XREAL_1:76;
then 1 > n / (p |^ k) by A23, XXREAL_0:2;
then 1 - 1 > (n / (p |^ k)) - 1 by XREAL_1:9;
hence (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A12, A18, INT_1:def 6; :: 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 A24: n = 0 ; :: thesis: p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))))

then A25: (2 * n) choose n = 1 by NEWTON:19;
p > 1 by INT_2:def 4;
then A26: p |-count ((2 * n) choose n) = 0 by A25, NAT_3:21;
len (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) = 0 by A9, A24, FINSEQ_1:def 3;
hence p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) by A26, PROB_3:62; :: thesis: verum

end;

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

A28: (2 * n) - n = n ;
A29: n + n > n + 0 by A27, XREAL_1:6;
then ((2 * n) choose n) * ((n !) * (n !)) = (((2 * n) !) / ((n !) * (n !))) * ((n !) * (n !)) by A28, NEWTON:def 3
.= (2 * n) ! by XCMPLX_1:87 ;
then A30: (n !) * (n !) divides (2 * n) ! by NAT_D:def 3;
(2 * n) choose n = ((2 * n) !) / ((n !) * (n !)) by A29, A28, NEWTON:def 3;
then A31: (2 * n) choose n = (((n !) * (n !)) * (((2 * n) !) div ((n !) * (n !)))) / ((n !) * (n !)) by A30, NAT_D:3
.= ((2 * n) !) div ((n !) * (n !)) by XCMPLX_1:89 ;
A32: - (f1 ^ (n |-> 0)) is Element of (len (- (f1 ^ (n |-> 0)))) -tuples_on REAL by FINSEQ_2:92;
A33: p |-count (((2 * n) !) div ((n !) * (n !))) = (p |-count ((2 * n) !)) -' (p |-count ((n !) * (n !))) by A30, NAT_3:31
.= (p |-count ((2 * n) !)) - (p |-count ((n !) * (n !))) by A30, NAT_3:30, XREAL_1:233 ;
A34: (- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))) is Element of (len ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) -tuples_on REAL by FINSEQ_2:92;
( len ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))) = len f2 & f2 is Element of (len f2) -tuples_on REAL ) by A4, A8, FINSEQ_1:def 3, FINSEQ_2:92;
then Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) = (Sum f2) + (Sum ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) by A34, RVSUM_1:89
.= (Sum f2) + ((Sum (- (f1 ^ (n |-> 0)))) + (Sum (- (f1 ^ (n |-> 0))))) by A32, RVSUM_1:89
.= (Sum f2) + ((- (Sum (f1 ^ (n |-> 0)))) + (Sum (- (f1 ^ (n |-> 0))))) by RVSUM_1:88
.= (Sum f2) + ((- (Sum (f1 ^ (n |-> 0)))) + (- (Sum (f1 ^ (n |-> 0))))) by RVSUM_1:88
.= (Sum f2) - (2 * (Sum (f1 ^ (n |-> 0))))
.= (Sum f2) - (2 * ((Sum f1) + (Sum (n |-> 0)))) by RVSUM_1:75
.= (Sum f2) - (2 * ((Sum f1) + (n * 0))) by RVSUM_1:80
.= (p |-count ((2 * n) !)) - ((p |-count (n !)) + (p |-count (n !))) by A3, A6
.= p |-count (((2 * n) !) div ((n !) * (n !))) by A33, NAT_3:28 ;
hence p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))) by A31; :: thesis: verum

end;

end;

end;

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