let n be Element of NAT ; :: thesis: for p being Prime st n >= 3 holds
( ( p > 2 * n implies p |-count ((2 * n) choose n) = 0 ) & ( n < p & p <= 2 * n implies p |-count ((2 * n) choose n) <= 1 ) & ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) & ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) )
let p be Prime; :: thesis: ( n >= 3 implies ( ( p > 2 * n implies p |-count ((2 * n) choose n) = 0 ) & ( n < p & p <= 2 * n implies p |-count ((2 * n) choose n) <= 1 ) & ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) & ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) ) )
assume A1: n >= 3 ; :: thesis: ( ( p > 2 * n implies p |-count ((2 * n) choose n) = 0 ) & ( n < p & p <= 2 * n implies p |-count ((2 * n) choose n) <= 1 ) & ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) & ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) )
A2: for n, r being Element of NAT
for p being Prime st n >= 2 & p |^ r <= 2 * n & 2 * n < p |^ (r + 1) holds
p |-count ((2 * n) choose n) <= r

proof

let n, r be Element of NAT ; :: thesis: for p being Prime st n >= 2 & p |^ r <= 2 * n & 2 * n < p |^ (r + 1) holds
p |-count ((2 * n) choose n) <= r
let p be Prime; :: thesis: ( n >= 2 & p |^ r <= 2 * n & 2 * n < p |^ (r + 1) implies p |-count ((2 * n) choose n) <= r )
assume A3: ( n >= 2 & p |^ r <= 2 * n & 2 * n < p |^ (r + 1) ) ; :: thesis: p |-count ((2 * n) choose n) <= r
consider f being FinSequence of REAL such that
A4: len f = 2 * n and
A5: for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) and
A6: p |-count ((2 * n) choose n) = Sum f by Th49;
thus p |-count ((2 * n) choose n) <= r by A3, A4, A5, A6, Lm8; :: thesis: verum

end;

thus ( p > 2 * n implies p |-count ((2 * n) choose n) = 0 ) :: thesis: ( ( n < p & p <= 2 * n implies p |-count ((2 * n) choose n) <= 1 ) & ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) & ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) )

proof

assume A7: p > 2 * n ; :: thesis: p |-count ((2 * n) choose n) = 0
set r = 0 ;
A8: n >= 2 by A1, XXREAL_0:2;
then n * 2 >= 2 * 2 by XREAL_1:66;
then 2 * n >= 1 by XXREAL_0:2;
then A9: p |^ 0 <= 2 * n by NEWTON:9;
p |^ (0 + 1) > 2 * n by A7, NEWTON:10;
hence p |-count ((2 * n) choose n) = 0 by A2, A8, A9; :: thesis: verum

end;

thus ( n < p & p <= 2 * n implies p |-count ((2 * n) choose n) <= 1 ) :: thesis: ( ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) & ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) )

proof

assume A10: n < p ; :: thesis: ( not p <= 2 * n or p |-count ((2 * n) choose n) <= 1 )
assume A11: p <= 2 * n ; :: thesis: p |-count ((2 * n) choose n) <= 1
set r = 1;
A12: n >= 2 by A1, XXREAL_0:2;
A13: p |^ 1 <= 2 * n by A11, NEWTON:10;
2 < p by A10, A12, XXREAL_0:2;
then A14: 2 * p < p * p by XREAL_1:70;
n * 2 < p * 2 by A10, XREAL_1:70;
then 2 * n < p * p by A14, XXREAL_0:2;
then 2 * n < (p |^ 1) * p by NEWTON:10;
then 2 * n < p |^ (1 + 1) by NEWTON:11;
hence p |-count ((2 * n) choose n) <= 1 by A2, A12, A13; :: thesis: verum

end;

thus ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) :: thesis: ( ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) )

proof

assume A15: (2 * n) / 3 < p ; :: thesis: ( not p <= n or p |-count ((2 * n) choose n) = 0 )
assume A16: p <= n ; :: thesis: p |-count ((2 * n) choose n) = 0
consider f being FinSequence of REAL such that
A17: len f = 2 * n and
A18: for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) and
A19: p |-count ((2 * n) choose n) = Sum f by Th49;
A20: for k being Element of NAT st k in dom f holds
f . k = 0

proof

let k be Element of NAT ; :: thesis: ( k in dom f implies f . k = 0 )
assume A21: k in dom f ; :: thesis: f . k = 0
then k in Seg (len f) by FINSEQ_1:def 3;
then A22: ( 1 <= k & k <= 2 * n ) by A17, FINSEQ_1:3;
A23: for m being Element of NAT holds (m * p) / p = m

proof

let m be Element of NAT ; :: thesis: (m * p) / p = m
p / p = 1 by XCMPLX_1:60;
then m * (p / p) = m ;
hence (m * p) / p = m by XCMPLX_1:75; :: thesis: verum

end;

p * 2 <= n * 2 by A16, XREAL_1:66;
then (2 * p) / p <= (2 * n) / p by XREAL_1:74;
then A24: 2 <= (2 * n) / p by A23;
A25: ((2 * n) / 3) * 3 < p * 3 by A15, XREAL_1:70;
then (2 * n) / p < (3 * p) / p by XREAL_1:76;
then (2 * n) / p < 3 by A23;
then A26: ((2 * n) / p) - 1 < 3 - 1 by XREAL_1:11;

per cases ( k = 1 or ( 1 < k & k <= 2 * n ) ) by A22, XXREAL_0:1;

suppose A27: k = 1 ; :: thesis: f . k = 0

(1 * p) / p <= n / p by A16, XREAL_1:74;
then A28: 1 <= n / p by A23;
3 * p < 4 * p by XREAL_1:70;
then 2 * n < 4 * p by A25, XXREAL_0:2;
then (n * 2) / 2 < ((2 * p) * 2) / 2 by XREAL_1:76;
then n / p < (2 * p) / p by XREAL_1:76;
then n / p < 2 by A23;
then (n / p) - 1 < 2 - 1 by XREAL_1:11;
then A29: [\(n / p)/] = 1 by A28, INT_1:def 4;
f . k = [\((2 * n) / (p |^ 1))/] - (2 * [\(n / (p |^ 1))/]) by A18, A21, A27
.= [\((2 * n) / p)/] - (2 * [\(n / (p |^ 1))/]) by NEWTON:10
.= [\((2 * n) / p)/] - (2 * [\(n / p)/]) by NEWTON:10
.= 2 - (2 * 1) by A24, A26, A29, INT_1:def 4 ;
hence f . k = 0 ; :: thesis: verum

end;

suppose ( 1 < k & k <= 2 * n ) ; :: thesis: f . k = 0

then 1 + 1 < k + 1 by XREAL_1:8;
then A30: 2 <= k by NAT_1:13;
3 * 2 <= n * 2 by A1, XREAL_1:66;
then 2 * 3 < 3 * p by A25, XXREAL_0:2;
then (2 * 3) / 3 < (p * 3) / 3 by XREAL_1:76;
then 2 + 1 < p + 1 by XREAL_1:8;
then 3 <= p by NAT_1:13;
then 3 * p <= p * p by XREAL_1:66;
then 2 * n < p * p by A25, XXREAL_0:2;
then 2 * n < (p |^ 1) * p by NEWTON:10;
then A31: 2 * n < p |^ (1 + 1) by NEWTON:11;
( p > 1 & ( k = 2 or 2 < k ) ) by A30, INT_2:def 5, XXREAL_0:1;
then p to_power 2 <= p to_power k by POWER:44;
then p |^ 2 <= p to_power k by POWER:46;
then A32: p |^ 2 <= p |^ k by POWER:46;
then 2 * n < p |^ k by A31, XXREAL_0:2;
then (2 * n) / (p |^ k) < (p |^ k) / (p |^ k) by XREAL_1:76;
then (2 * n) / (p |^ k) < 1 by XCMPLX_1:60;
then A33: ((2 * n) / (p |^ k)) - 1 < 1 - 1 by XREAL_1:11;
1 * n <= 2 * n by XREAL_1:66;
then n < p |^ 2 by A31, XXREAL_0:2;
then n < p |^ k by A32, XXREAL_0:2;
then n / (p |^ k) < (p |^ k) / (p |^ k) by XREAL_1:76;
then n / (p |^ k) < 1 by XCMPLX_1:60;
then A34: (n / (p |^ k)) - 1 < 1 - 1 by XREAL_1:11;
A35: [\((2 * n) / (p |^ k))/] = 0 by A33, INT_1:def 4;
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A18, A21
.= 0 - (2 * 0 ) by A34, A35, INT_1:def 4 ;
hence f . k = 0 ; :: thesis: verum

end;

end;

end;

set q = (2 * n) |-> 0 ;
A36: dom ((2 * n) |-> 0 ) = Seg (2 * n) by FUNCOP_1:19;
A37: dom f = Seg (2 * n) by A17, FINSEQ_1:def 3;
for k being Nat st k in dom f holds
f . k = ((2 * n) |-> 0 ) . k

proof

let k be Nat; :: thesis: ( k in dom f implies f . k = ((2 * n) |-> 0 ) . k )
assume A38: k in dom f ; :: thesis: f . k = ((2 * n) |-> 0 ) . k
then f . k = 0 by A20;
hence f . k = ((2 * n) |-> 0 ) . k by A37, A38, FUNCOP_1:13; :: thesis: verum

end;

then (2 * n) |-> 0 = f by A36, A37, FINSEQ_1:17;
then Sum f = (2 * n) * 0 by RVSUM_1:110;
hence p |-count ((2 * n) choose n) = 0 by A19; :: thesis: verum

end;

thus ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) :: thesis: ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n )

proof

assume A39: sqrt (2 * n) < p ; :: thesis: ( not p <= (2 * n) / 3 or p |-count ((2 * n) choose n) <= 1 )
assume A40: p <= (2 * n) / 3 ; :: thesis: p |-count ((2 * n) choose n) <= 1
set r = 1;
A41: n >= 2 by A1, XXREAL_0:2;
A42: (1 / 3) * (2 * n) <= 1 * (2 * n) by XREAL_1:66;
p |^ 1 <= (2 * n) / 3 by A40, NEWTON:10;
then A43: p |^ 1 <= 2 * n by A42, XXREAL_0:2;
sqrt (2 * n) > 0 by SQUARE_1:93, A1;
then A44: (sqrt (2 * n)) * (sqrt (2 * n)) < p * (sqrt (2 * n)) by A39, XREAL_1:70;
(sqrt (2 * n)) * p < p * p by A39, XREAL_1:70;
then (sqrt (2 * n)) ^2 < p * p by A44, XXREAL_0:2;
then 2 * n < p * p by SQUARE_1:def 4;
then 2 * n < (p |^ 1) * p by NEWTON:10;
then 2 * n < p |^ (1 + 1) by NEWTON:11;
hence p |-count ((2 * n) choose n) <= 1 by A2, A41, A43; :: thesis: verum

end;

assume A45: p <= sqrt (2 * n) ; :: thesis: p |^ (p |-count ((2 * n) choose n)) <= 2 * n
set r = [\(log p,(2 * n))/];
A46: p > 1 by INT_2:def 5;
then A47: p * p > 1 * p by XREAL_1:70;
A48: ( [\(log p,(2 * n))/] <= log p,(2 * n) & (log p,(2 * n)) - 1 < [\(log p,(2 * n))/] ) by INT_1:def 4;
A49: (sqrt (2 * n)) * p >= p * p by A45, XREAL_1:66;
(sqrt (2 * n)) * (sqrt (2 * n)) >= p * (sqrt (2 * n)) by A45, XREAL_1:66;
then (sqrt (2 * n)) ^2 >= p * p by A49, XXREAL_0:2;
then A50: 2 * n >= p * p by SQUARE_1:def 4;
then 2 * n > p by A47, XXREAL_0:2;
then log p,(2 * n) > log p,p by A46, POWER:65;
then log p,(2 * n) > 1 by A46, POWER:60;
then (log p,(2 * n)) - 1 > 1 - 1 by XREAL_1:11;
then reconsider r = [\(log p,(2 * n))/] as Element of NAT by A48, INT_1:16;
( r < log p,(2 * n) or r = log p,(2 * n) ) by A48, XXREAL_0:1;
then p to_power r <= p to_power (log p,(2 * n)) by A46, POWER:44;
then p |^ r <= p to_power (log p,(2 * n)) by POWER:46;
then A51: p |^ r <= 2 * n by A46, A50, POWER:def 3;
((log p,(2 * n)) - 1) + 1 < r + 1 by A48, XREAL_1:8;
then p to_power (log p,(2 * n)) < p to_power (r + 1) by A46, POWER:44;
then p to_power (log p,(2 * n)) < p |^ (r + 1) by POWER:46;
then A52: 2 * n < p |^ (r + 1) by A46, POWER:def 3;
set k0 = p |-count ((2 * n) choose n);
n >= 2 by A1, XXREAL_0:2;
then p |-count ((2 * n) choose n) <= r by A2, A51, A52;
then ( p |-count ((2 * n) choose n) = r or p |-count ((2 * n) choose n) < r ) by XXREAL_0:1;
then p to_power (p |-count ((2 * n) choose n)) <= p to_power r by A46, POWER:44;
then p |^ (p |-count ((2 * n) choose n)) <= p to_power r by POWER:46;
then p |^ (p |-count ((2 * n) choose n)) <= p |^ r by POWER:46;
hence p |^ (p |-count ((2 * n) choose n)) <= 2 * n by A51, XXREAL_0:2; :: thesis: verum