let n be Nat; :: thesis: for a being non trivial Nat holds ((a + 1) |^ n) + ((a + 1) |^ n) < (a + 1) |^ (n + 1)
let a be non trivial Nat; :: thesis: ((a + 1) |^ n) + ((a + 1) |^ n) < (a + 1) |^ (n + 1)
( a <> 0 & a <> 1 ) by NAT_2:def 1;
then a + 1 > 2 by NAT_1:13, NAT_1:23;
then (a + 1) * ((a + 1) |^ n) > 2 * ((a + 1) |^ n) by XREAL_1:68;
hence ((a + 1) |^ n) + ((a + 1) |^ n) < (a + 1) |^ (n + 1) by NEWTON:6; :: thesis: verum