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 that
n >= 2 and
A3: ( p |^ r <= 2 * n & 2 * n < p |^ (r + 1) ) ; :: thesis: p |-count ((2 * n) choose n) <= r
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 ) by Th48;
hence p |-count ((2 * n) choose n) <= r by A3, 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

set r = 0 ;
assume p > 2 * n ; :: thesis: p |-count ((2 * n) choose n) = 0
then A4: p |^ (0 + 1) > 2 * n ;
A5: n >= 2 by A1, XXREAL_0:2;
then n * 2 >= 2 * 2 by XREAL_1:64;
then 2 * n >= 1 by XXREAL_0:2;
then p |^ 0 <= 2 * n by NEWTON:4;
hence p |-count ((2 * n) choose n) = 0 by A2, A5, A4; :: 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

set r = 1;
assume A6: n < p ; :: thesis: ( not p <= 2 * n or p |-count ((2 * n) choose n) <= 1 )
then A7: n * 2 < p * 2 by XREAL_1:68;
A8: n >= 2 by A1, XXREAL_0:2;
then 2 < p by A6, XXREAL_0:2;
then 2 * p < p * p by XREAL_1:68;
then 2 * n < p * p by A7, XXREAL_0:2;
then 2 * n < (p |^ 1) * p ;
then A9: 2 * n < p |^ (1 + 1) by NEWTON:6;
assume p <= 2 * n ; :: thesis: p |-count ((2 * n) choose n) <= 1
then p |^ 1 <= 2 * n ;
hence p |-count ((2 * n) choose n) <= 1 by A2, A8, A9; :: 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

set q = (2 * n) |-> 0;
assume A10: (2 * n) / 3 < p ; :: thesis: ( not p <= n or p |-count ((2 * n) choose n) = 0 )
consider f being FinSequence of REAL such that
A11: len f = 2 * n and
A12: for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) and
A13: p |-count ((2 * n) choose n) = Sum f by Th48;
A14: dom f = Seg (2 * n) by A11, FINSEQ_1:def 3;
assume A15: p <= n ; :: thesis: p |-count ((2 * n) choose n) = 0
A16: 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 )
A17: 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:74; :: thesis: verum

end;

p * 2 <= n * 2 by A15, XREAL_1:64;
then (2 * p) / p <= (2 * n) / p by XREAL_1:72;
then A18: 2 <= (2 * n) / p by A17;
assume A19: k in dom f ; :: thesis: f . k = 0
then A20: k in Seg (len f) by FINSEQ_1:def 3;
then A21: 1 <= k by FINSEQ_1:1;
A22: ((2 * n) / 3) * 3 < p * 3 by A10, XREAL_1:68;
then (2 * n) / p < (3 * p) / p by XREAL_1:74;
then (2 * n) / p < 3 by A17;
then A23: ((2 * n) / p) - 1 < 3 - 1 by XREAL_1:9;

per cases ( k = 1 or ( 1 < k & k <= 2 * n ) ) by A11, A20, A21, FINSEQ_1:1, XXREAL_0:1;

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

3 * p < 4 * p by XREAL_1:68;
then 2 * n < 4 * p by A22, XXREAL_0:2;
then (n * 2) / 2 < ((2 * p) * 2) / 2 by XREAL_1:74;
then n / p < (2 * p) / p by XREAL_1:74;
then n / p < 2 by A17;
then A25: (n / p) - 1 < 2 - 1 by XREAL_1:9;
(1 * p) / p <= n / p by A15, XREAL_1:72;
then 1 <= n / p by A17;
then A26: [\(n / p)/] = 1 by A25, INT_1:def 6;
f . k = [\((2 * n) / (p |^ 1))/] - (2 * [\(n / (p |^ 1))/]) by A12, A19, A24
.= [\((2 * n) / p)/] - (2 * [\(n / (p |^ 1))/])
.= [\((2 * n) / p)/] - (2 * [\(n / p)/])
.= 2 - (2 * 1) by A18, A23, A26, INT_1:def 6 ;
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:6;
then 2 <= k by NAT_1:13;
then A27: ( k = 2 or 2 < k ) by XXREAL_0:1;
3 * 2 <= n * 2 by A1, XREAL_1:64;
then 2 * 3 < 3 * p by A22, XXREAL_0:2;
then (2 * 3) / 3 < (p * 3) / 3 by XREAL_1:74;
then 2 + 1 < p + 1 by XREAL_1:6;
then 3 <= p by NAT_1:13;
then 3 * p <= p * p by XREAL_1:64;
then 2 * n < p * p by A22, XXREAL_0:2;
then 2 * n < (p |^ 1) * p ;
then A28: 2 * n < p |^ (1 + 1) by NEWTON:6;
p > 1 by INT_2:def 4;
then p to_power 2 <= p to_power k by A27, POWER:39;
then p |^ 2 <= p to_power k by POWER:41;
then A29: p |^ 2 <= p |^ k by POWER:41;
then 2 * n < p |^ k by A28, XXREAL_0:2;
then (2 * n) / (p |^ k) < (p |^ k) / (p |^ k) by XREAL_1:74;
then (2 * n) / (p |^ k) < 1 by XCMPLX_1:60;
then ((2 * n) / (p |^ k)) - 1 < 1 - 1 by XREAL_1:9;
then A30: [\((2 * n) / (p |^ k))/] = 0 by INT_1:def 6;
1 * n <= 2 * n by XREAL_1:64;
then n < p |^ 2 by A28, XXREAL_0:2;
then n < p |^ k by A29, XXREAL_0:2;
then n / (p |^ k) < (p |^ k) / (p |^ k) by XREAL_1:74;
then n / (p |^ k) < 1 by XCMPLX_1:60;
then A31: (n / (p |^ k)) - 1 < 1 - 1 by XREAL_1:9;
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) by A12, A19
.= 0 - (2 * 0) by A31, A30, INT_1:def 6 ;
hence f . k = 0 ; :: thesis: verum

end;

end;

end;

A32: for k being Nat st k in dom f holds
f . k = ((2 * n) |-> 0) . k by A16;
dom ((2 * n) |-> 0) = Seg (2 * n) by FUNCOP_1:13;
then (2 * n) |-> 0 = f by A14, A32, FINSEQ_1:13;
then Sum f = (2 * n) * 0 by RVSUM_1:80;
hence p |-count ((2 * n) choose n) = 0 by A13; :: 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

set r = 1;
assume A33: sqrt (2 * n) < p ; :: thesis: ( not p <= (2 * n) / 3 or p |-count ((2 * n) choose n) <= 1 )
then A34: (sqrt (2 * n)) * p < p * p by XREAL_1:68;
sqrt (2 * n) > 0 by A1, SQUARE_1:25;
then (sqrt (2 * n)) * (sqrt (2 * n)) < p * (sqrt (2 * n)) by A33, XREAL_1:68;
then (sqrt (2 * n)) ^2 < p * p by A34, XXREAL_0:2;
then 2 * n < p * p by SQUARE_1:def 2;
then 2 * n < (p |^ 1) * p ;
then A35: 2 * n < p |^ (1 + 1) by NEWTON:6;
assume p <= (2 * n) / 3 ; :: thesis: p |-count ((2 * n) choose n) <= 1
then ( (1 / 3) * (2 * n) <= 1 * (2 * n) & p |^ 1 <= (2 * n) / 3 ) by XREAL_1:64;
then A36: p |^ 1 <= 2 * n by XXREAL_0:2;
n >= 2 by A1, XXREAL_0:2;
hence p |-count ((2 * n) choose n) <= 1 by A2, A36, A35; :: thesis: verum

end;

assume p <= sqrt (2 * n) ; :: thesis: p |^ (p |-count ((2 * n) choose n)) <= 2 * n
then ( (sqrt (2 * n)) * p >= p * p & (sqrt (2 * n)) * (sqrt (2 * n)) >= p * (sqrt (2 * n)) ) by XREAL_1:64;
then (sqrt (2 * n)) ^2 >= p * p by XXREAL_0:2;
then A37: 2 * n >= p * p by SQUARE_1:def 2;
set k0 = p |-count ((2 * n) choose n);
set r = [\(log (p,(2 * n)))/];
A38: [\(log (p,(2 * n)))/] <= log (p,(2 * n)) by INT_1:def 6;
A39: (log (p,(2 * n))) - 1 < [\(log (p,(2 * n)))/] by INT_1:def 6;
A40: p > 1 by INT_2:def 4;
then p * p > 1 * p by XREAL_1:68;
then 2 * n > p by A37, XXREAL_0:2;
then log (p,(2 * n)) > log (p,p) by A40, POWER:57;
then log (p,(2 * n)) > 1 by A40, POWER:52;
then (log (p,(2 * n))) - 1 > 1 - 1 by XREAL_1:9;
then reconsider r = [\(log (p,(2 * n)))/] as Element of NAT by A39, INT_1:3;
( r < log (p,(2 * n)) or r = log (p,(2 * n)) ) by A38, XXREAL_0:1;
then p to_power r <= p to_power (log (p,(2 * n))) by A40, POWER:39;
then p |^ r <= p to_power (log (p,(2 * n))) by POWER:41;
then A41: p |^ r <= 2 * n by A40, A37, POWER:def 3;
((log (p,(2 * n))) - 1) + 1 < r + 1 by A39, XREAL_1:6;
then p to_power (log (p,(2 * n))) < p to_power (r + 1) by A40, POWER:39;
then p to_power (log (p,(2 * n))) < p |^ (r + 1) by POWER:41;
then A42: 2 * n < p |^ (r + 1) by A40, POWER:def 3;
n >= 2 by A1, XXREAL_0:2;
then p |-count ((2 * n) choose n) <= r by A2, A41, A42;
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 A40, POWER:39;
then p |^ (p |-count ((2 * n) choose n)) <= p to_power r by POWER:41;
then p |^ (p |-count ((2 * n) choose n)) <= p |^ r by POWER:41;
hence p |^ (p |-count ((2 * n) choose n)) <= 2 * n by A41, XXREAL_0:2; :: thesis: verum