let n be Nat; :: thesis: for a being non trivial odd Nat holds (a |^ n) + (a |^ n) < a |^ (n + 1)
let a be non trivial odd Nat; :: thesis: (a |^ n) + (a |^ n) < a |^ (n + 1)
( a - 1 <> 1 & a - 1 <> 0 ) ;
then reconsider b = a - 1 as non trivial Nat by NAT_2:def 1;
((b + 1) |^ n) + ((b + 1) |^ n) < (b + 1) |^ (n + 1) by LmNT;
hence (a |^ n) + (a |^ n) < a |^ (n + 1) ; :: thesis: verum