set f2a = <*1*>;
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 )
set f1 = Newton_Coeff n;
set f2b = (n -' 1) |-> (n choose m);
set f2 = (<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>;
A2: Sum ((n -' 1) |-> (n choose m)) = (n -' 1) * (n choose m) by RVSUM_1:80;
assume A3: n >= 2 ; :: thesis: n choose m >= (2 |^ n) / n
then A4: n -' 1 = n - 1 by XREAL_1:233, XXREAL_0:2;
A5: len ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + (len <*1*>) by FINSEQ_1:22
.= (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + 1 by FINSEQ_1:39
.= ((len <*1*>) + (len ((n -' 1) |-> (n choose m)))) + 1 by FINSEQ_1:22
.= ((len <*1*>) + (n - 1)) + 1 by A4, CARD_1:def 7
.= (1 + (n - 1)) + 1 by FINSEQ_1:39
.= n + 1 ;
len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
then dom (Newton_Coeff n) = Seg (n + 1) by FINSEQ_1:def 3;
then A6: dom (Newton_Coeff n) = dom ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) by A5, FINSEQ_1:def 3;
A7: 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 A6, A8, FINSEQ_1:25;

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:25;

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

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

end;

suppose A14: 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

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

end;

end;

end;

suppose A21: 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

reconsider k = (n + 1) - 1 as Element of NAT by ORDINAL1:def 12;
consider j being Nat such that
A22: j in dom <*1*> and
A23: i = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + j by A21;
A24: j in Seg 1 by A22, FINSEQ_1:38;
then A25: j = 1 by FINSEQ_1:2, TARSKI:def 1;
i = (len (<*1*> ^ ((n -' 1) |-> (n choose m)))) + 1 by A23, A24, FINSEQ_1:2, TARSKI:def 1
.= ((len <*1*>) + (len ((n -' 1) |-> (n choose m)))) + 1 by FINSEQ_1:22
.= ((len <*1*>) + (n - 1)) + 1 by A4, CARD_1:def 7
.= (1 + (n - 1)) + 1 by FINSEQ_1:39
.= n + 1 ;
then A26: (Newton_Coeff n) . i = n choose k by A8, NEWTON:def 5
.= 1 by NEWTON:21 ;
((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i = <*1*> . j by A22, A23, FINSEQ_1:def 7;
hence (Newton_Coeff n) . i <= ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) . i by A25, A26, FINSEQ_1:40; :: thesis: verum

end;

end;

end;

1 <= n by A3, XXREAL_0:2;
then A27: n choose 1 <= n choose m by A1, Th4;
2 <= n choose 1 by A3, NEWTON:23, XXREAL_0:2;
then 2 <= n choose m by A27, XXREAL_0:2;
then A28: 2 + ((n - 1) * (n choose m)) <= (n choose m) + ((n - 1) * (n choose m)) by XREAL_1:6;
A29: Sum ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) = (Sum (<*1*> ^ ((n -' 1) |-> (n choose m)))) + 1 by RVSUM_1:74
.= (1 + (Sum ((n -' 1) |-> (n choose m)))) + 1 by RVSUM_1:76
.= 2 + ((n -' 1) * (n choose m)) by A2
.= 2 + ((n - 1) * (n choose m)) by A3, XREAL_1:233, XXREAL_0:2 ;
len (Newton_Coeff n) = len ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) by A5, NEWTON:def 5;
then Sum (Newton_Coeff n) <= Sum ((<*1*> ^ ((n -' 1) |-> (n choose m))) ^ <*1*>) by A7, INTEGRA5:3;
then 2 |^ n <= 2 + ((n - 1) * (n choose m)) by A29, NEWTON:32;
then 2 |^ n <= n * (n choose m) by A28, XXREAL_0:2;
then (2 |^ n) / n <= (n * (n choose m)) / n by XREAL_1:72;
hence n choose m >= (2 |^ n) / n by A3, XCMPLX_1:89; :: thesis: verum