let a, b, n be Nat; :: thesis: ( a = 1 implies (a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2) )
assume A1: a = 1 ; :: thesis: (a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2)
A5: 2 + 0 <= 2 + n by XREAL_1:6;
assume A2: not (a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2) ; :: thesis: contradiction
2 + n < 2 |^ (2 + n) by NEWTON:86;
then ( b |^ (2 + n) > 1 |^ (2 + n) & b |^ (2 + n) < 2 |^ (2 + n) ) by A1, A5, A2, XXREAL_0:2;
then ( b > 1 & b < 1 + 1 ) by Lm3a;
hence contradiction by NAT_1:13; :: thesis: verum