let n be Nat; :: thesis: (2 * n) choose n >= (4 |^ n) / (2 * n)

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

suppose A1: n = 0 ; :: thesis: (2 * n) choose n >= (4 |^ n) / (2 * n)

thus (2 * n) choose n >= (4 |^ n) / (2 * n) by A1; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (2 * n) choose n >= (4 |^ n) / (2 * n)

then A2: 2 * n >= 2 * 1 by NAT_1:14, XREAL_1:66;
A3: 2 |^ 2 = Product <*2,2*> by FINSEQ_2:75
.= 2 * 2 by RVSUM_1:129
.= 4 ;
set m = [\((2 * n) / 2)/];
A4: [\((2 * n) / 2)/] = n by INT_1:47;
then reconsider m = [\((2 * n) / 2)/] as Element of NAT by ORDINAL1:def 13;
(2 * n) choose m >= (2 |^ (2 * n)) / (2 * n) by A2, Th5;
hence (2 * n) choose n >= (4 |^ n) / (2 * n) by A3, A4, NEWTON:14; :: thesis: verum

end;

end;