reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
set f2a = <*jj*>;
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 )
reconsider f1 = Newton_Coeff n as FinSequence of REAL ;
reconsider nm = n choose m as Element of REAL by XREAL_0:def 1;
set f2b = (n -' 1) |-> nm;
reconsider f2 = (<*jj*> ^ ((n -' 1) |-> nm)) ^ <*jj*> as FinSequence of REAL ;
A2: Sum ((n -' 1) |-> nm) = (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 f2 = (len (<*jj*> ^ ((n -' 1) |-> nm))) + (len <*jj*>) by FINSEQ_1:22
.= (len (<*jj*> ^ ((n -' 1) |-> nm))) + 1 by FINSEQ_1:39
.= ((len <*jj*>) + (len ((n -' 1) |-> nm))) + 1 by FINSEQ_1:22
.= ((len <*jj*>) + (n - 1)) + 1 by A4, CARD_1:def 7
.= (1 + (n - 1)) + 1 by FINSEQ_1:39
.= n + 1 ;
len f1 = n + 1 by NEWTON:def 5;
then dom f1 = Seg (n + 1) by FINSEQ_1:def 3;
then A6: dom f1 = dom f2 by A5, FINSEQ_1:def 3;
A7: for i being Element of NAT st i in dom f1 holds
f1 . i <= f2 . i

proof

let i be Element of NAT ; :: thesis: ( i in dom f1 implies f1 . i <= f2 . i )
assume A8: i in dom f1 ; :: thesis: f1 . i <= f2 . i

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

suppose A9: i in dom (<*jj*> ^ ((n -' 1) |-> nm)) ; :: thesis: f1 . i <= f2 . i

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

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

suppose A11: i in dom <*jj*> ; :: thesis: f1 . i <= f2 . i

set k = 1 - 1;
1 - 1 = 0 ;
then reconsider k = 1 - 1 as Element of NAT ;
A12: f2 . i = <*jj*> . 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 f1 . i = n choose k by A8, NEWTON:def 5
.= 1 by NEWTON:19 ;
hence f1 . i <= f2 . i by A12, A13; :: thesis: verum

end;

suppose A14: ex j being Nat st
( j in dom ((n -' 1) |-> nm) & i = (len <*jj*>) + j ) ; :: thesis: f1 . i <= f2 . i

set k = i -' 1;
consider j being Nat such that
A15: j in dom ((n -' 1) |-> nm) and
A16: i = (len <*jj*>) + 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;
f2 . i = ((n -' 1) |-> nm) . j by A10, A15, A16, FINSEQ_1:def 7;
then A19: f2 . 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;
f1 . i = n choose (i -' 1) by A8, A18, NEWTON:def 5;
hence f1 . i <= f2 . i by A1, A19, A20, Th4; :: thesis: verum

end;

end;

end;

suppose A21: ex j being Nat st
( j in dom <*jj*> & i = (len (<*jj*> ^ ((n -' 1) |-> nm))) + j ) ; :: thesis: f1 . i <= f2 . i

reconsider k = (n + 1) - 1 as Element of NAT by ORDINAL1:def 12;
consider j being Nat such that
A22: j in dom <*jj*> and
A23: i = (len (<*jj*> ^ ((n -' 1) |-> nm))) + 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 (<*jj*> ^ ((n -' 1) |-> nm))) + 1 by A23, A24, FINSEQ_1:2, TARSKI:def 1
.= ((len <*jj*>) + (len ((n -' 1) |-> nm))) + 1 by FINSEQ_1:22
.= ((len <*jj*>) + (n - 1)) + 1 by A4, CARD_1:def 7
.= (1 + (n - 1)) + 1 by FINSEQ_1:39
.= n + 1 ;
then A26: f1 . i = n choose k by A8, NEWTON:def 5
.= 1 by NEWTON:21 ;
f2 . i = <*jj*> . j by A22, A23, FINSEQ_1:def 7;
hence f1 . i <= f2 . i by A25, A26; :: 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 f2 = (Sum (<*jj*> ^ ((n -' 1) |-> nm))) + 1 by RVSUM_1:74
.= (1 + (Sum ((n -' 1) |-> nm))) + 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 f1 = len f2 by A5, NEWTON:def 5;
then Sum f1 <= Sum f2 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