let n be Element of NAT ; 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; 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 Th47;
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 Th47;
reconsider f2 = f2 as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
set f = f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))));
take
f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0))))
; ( 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 VALUED_1:def 1
.=
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 VALUED_1:def 1
.=
(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; ( ( 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))/])
p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))))
p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))))
proof
per cases
( n = 0 or n <> 0 )
;
suppose A26:
n <> 0
;
p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))))A27:
(2 * n) - n = n
;
A28:
n + n > n + 0
by A26, XREAL_1:6;
then ((2 * n) choose n) * ((n !) * (n !)) =
(((2 * n) !) / ((n !) * (n !))) * ((n !) * (n !))
by A27, NEWTON:def 3
.=
(2 * n) !
by XCMPLX_1:87
;
then A29:
(n !) * (n !) divides (2 * n) !
by NAT_D:def 3;
(2 * n) choose n = ((2 * n) !) / ((n !) * (n !))
by A28, A27, NEWTON:def 3;
then A30:
(2 * n) choose n =
(((n !) * (n !)) * (((2 * n) !) div ((n !) * (n !)))) / ((n !) * (n !))
by A29, NAT_D:3
.=
((2 * n) !) div ((n !) * (n !))
by XCMPLX_1:89
;
A31:
- (f1 ^ (n |-> 0)) is
Element of
(len (- (f1 ^ (n |-> 0)))) -tuples_on REAL
by FINSEQ_2:92;
A32:
p |-count (((2 * n) !) div ((n !) * (n !))) =
(p |-count ((2 * n) !)) -' (p |-count ((n !) * (n !)))
by A29, NAT_3:31
.=
(p |-count ((2 * n) !)) - (p |-count ((n !) * (n !)))
by A29, NAT_3:30, XREAL_1:233
;
A33:
(- (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 A33, RVSUM_1:89
.=
(Sum f2) + ((Sum (- (f1 ^ (n |-> 0)))) + (Sum (- (f1 ^ (n |-> 0)))))
by A31, 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 A32, NAT_3:28
;
hence
p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))))
by A30;
verum end; end;
end;
hence
p |-count ((2 * n) choose n) = Sum (f2 + ((- (f1 ^ (n |-> 0))) + (- (f1 ^ (n |-> 0)))))
; verum