let n, m be Nat; :: thesis: ( m = [\(n / 2)/] & n >= 2 implies n choose m >= (2 |^ n) / n )
assume A1: m = [\(n / 2)/] ; :: thesis: ( not n >= 2 or n choose m >= (2 |^ n) / n )
assume A2: n >= 2 ; :: thesis: n choose m >= (2 |^ n) / n
then A3: n -' 1 = n - 1 by XREAL_1:235, XXREAL_0:2;
set f2a = <*1*>;
set f2b = (n -' 1) |-> (n choose m);
set f1 = Newton_Coeff n;
set f2 = (<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>;
A4: len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
A5: len ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + (len <*1*>) by FINSEQ_1:35
.= (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + 1 by FINSEQ_1:56
.= ((len <*1*>) + (len ((n -' 1) |-> (n choose m)))) + 1 by FINSEQ_1:35
.= ((len <*1*>) + (n - 1)) + 1 by A3, FINSEQ_1:def 18
.= (1 + (n - 1)) + 1 by FINSEQ_1:56
.= n + 1 ;
then A6: len (Newton_Coeff n) = len ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) by NEWTON:def 5;
dom (Newton_Coeff n) = Seg (n + 1) by A4, FINSEQ_1:def 3;
then A7: dom (Newton_Coeff n) = dom ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) by A5, FINSEQ_1:def 3;
for i being Element of NAT st i in dom (Newton_Coeff n) holds
(Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i

proof

let i be Element of NAT ; :: thesis: ( i in dom (Newton_Coeff n) implies (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i )
assume A8: i in dom (Newton_Coeff n) ; :: thesis: (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i

per cases ( i in dom (<*1*> ^ ((n -' 1) |-> (n choose m))) or ex j being Nat st
( j in dom <*1*> & i = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + j ) ) by A7, A8, FINSEQ_1:38;

suppose A9: i in dom (<*1*> ^ ((n -' 1) |-> (n choose m))) ; :: thesis: (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i

then A10: ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i = (<*1*> ^ ((n -' 1) |-> (n choose m))) . i by FINSEQ_1:def 7;

per cases ( i in dom <*1*> or ex j being Nat st
( j in dom ((n -' 1) |-> (n choose m)) & i = (len <*1*>) + j ) ) by A9, FINSEQ_1:38;

suppose A11: i in dom <*1*> ; :: thesis: (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i

then A12: ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i = <*1*> . i by A10, FINSEQ_1:def 7;
i in Seg 1 by A11, FINSEQ_1:55;
then A13: i = 1 by FINSEQ_1:4, TARSKI:def 1;
set k = 1 - 1;
1 - 1 = 0 ;
then reconsider k = 1 - 1 as Element of NAT ;
(Newton_Coeff n) . i = n choose k by A8, A13, NEWTON:def 5
.= 1 by NEWTON:29 ;
hence (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i by A12, A13, FINSEQ_1:57; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom ((n -' 1) |-> (n choose m)) & i = (len <*1*>) + j ) ; :: thesis: (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i

then consider j being Nat such that
A14: j in dom ((n -' 1) |-> (n choose m)) and
A15: i = (len <*1*>) + j ;
A16: ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i = ((n -' 1) |-> (n choose m)) . j by A10, A14, A15, FINSEQ_1:def 7;
A17: j in Seg (n -' 1) by A14, FUNCOP_1:19;
then A18: ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i = n choose m by A16, FUNCOP_1:13;
A19: j + 1 >= 0 + 1 by XREAL_1:8;
A20: i = 1 + j by A15, FINSEQ_1:56;
A21: i >= 1 by A15, A19, FINSEQ_1:56;
A22: (- 1) + n < 0 + n by XREAL_1:8;
set k = i -' 1;
A23: i -' 1 = i - 1 by A21, XREAL_1:235;
then A24: (Newton_Coeff n) . i = n choose (i -' 1) by A8, NEWTON:def 5;
i - 1 <= n - 1 by A3, A17, A20, FINSEQ_1:3;
then i -' 1 <= n by A22, A23, XXREAL_0:2;
hence (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i by A1, A18, A24, Th4; :: thesis: verum

end;

end;

end;

suppose ex j being Nat st
( j in dom <*1*> & i = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + j ) ; :: thesis: (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i

then consider j being Nat such that
A25: j in dom <*1*> and
A26: i = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + j ;
A27: ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i = <*1*> . j by A25, A26, FINSEQ_1:def 7;
A28: j in Seg 1 by A25, FINSEQ_1:55;
then A29: j = 1 by FINSEQ_1:4, TARSKI:def 1;
A30: i = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + 1 by A26, A28, FINSEQ_1:4, TARSKI:def 1
.= ((len <*1*>) + (len ((n -' 1) |-> (n choose m)))) + 1 by FINSEQ_1:35
.= ((len <*1*>) + (n - 1)) + 1 by A3, FINSEQ_1:def 18
.= (1 + (n - 1)) + 1 by FINSEQ_1:56
.= n + 1 ;
reconsider k = (n + 1) - 1 as Element of NAT by ORDINAL1:def 13;
(Newton_Coeff n) . i = n choose k by A8, A30, NEWTON:def 5
.= 1 by NEWTON:31 ;
hence (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i by A27, A29, FINSEQ_1:57; :: thesis: verum

end;

end;

end;

then A31: Sum (Newton_Coeff n) <= Sum ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) by A6, INTEGRA5:3;
1 <= n by A2, XXREAL_0:2;
then A32: n choose 1 <= n choose m by A1, Th4;
2 <= n choose 1 by A2, NEWTON:33, XXREAL_0:2;
then 2 <= n choose m by A32, XXREAL_0:2;
then A33: 2 + ((n - 1) * (n choose m)) <= (n choose m) + ((n - 1) * (n choose m)) by XREAL_1:8;
A34: Sum ((n -' 1) |-> (n choose m)) = (n -' 1) * (n choose m) by RVSUM_1:110;
Sum ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) = (Sum (<*1*> ^ ((n -' 1) |-> (n choose m)))) + 1 by RVSUM_1:104
.= (1 + (Sum ((n -' 1) |-> (n choose m)))) + 1 by RVSUM_1:106
.= 2 + ((n -' 1) * (n choose m)) by A34
.= 2 + ((n - 1) * (n choose m)) by A2, XREAL_1:235, XXREAL_0:2 ;
then 2 |^ n <= 2 + ((n - 1) * (n choose m)) by A31, NEWTON:44;
then 2 |^ n <= n * (n choose m) by A33, XXREAL_0:2;
then (2 |^ n) / n <= (n * (n choose m)) / n by XREAL_1:74;
hence n choose m >= (2 |^ n) / n by A2, XCMPLX_1:90; :: thesis: verum