let n be Nat; for a being non trivial Nat holds (a |^ (n + 1)) + (a |^ n) < a |^ (n + 2)
let a be non trivial Nat; (a |^ (n + 1)) + (a |^ n) < a |^ (n + 2)
A0:
( not a = 0 & not a = 1 )
by NAT_2:def 1;
then A0a:
a >= 2
by NAT_1:23;
A1:
a |^ ((n + 1) + 1) = a * (a |^ (n + 1))
by NEWTON:6;
A2:
a * (a |^ (n + 1)) >= 2 * (a |^ (n + 1))
by A0, NAT_1:23, XREAL_1:64;
a > 1
by A0a, XXREAL_0:2;
then
a * (a |^ n) > 1 * (a |^ n)
by XREAL_1:68;
then
a |^ (n + 1) > a |^ n
by NEWTON:6;
then
(a |^ (n + 1)) + (a |^ (n + 1)) > (a |^ (n + 1)) + (a |^ n)
by XREAL_1:6;
hence
(a |^ (n + 1)) + (a |^ n) < a |^ (n + 2)
by A1, A2, XXREAL_0:2; verum