let n be Nat; :: thesis: for a, b being non negative Real holds (a + b) |^ n >= Sum ((a,b) Subnomial n)
let a, b be non negative Real; :: thesis: (a + b) |^ n >= Sum ((a,b) Subnomial n)
for i being Nat holds ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i by ILS;
then Sum ((a,b) In_Power n) >= Sum ((a,b) Subnomial n) by NYS;
hence (a + b) |^ n >= Sum ((a,b) Subnomial n) by NEWTON:30; :: thesis: verum