let l be Real; :: thesis: for m, n being Nat st l > 1 & n <= m holds
( (l |^ n) * (l |^ (m -' n)) = l |^ m & (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m )
let m, n be Nat; :: thesis: ( l > 1 & n <= m implies ( (l |^ n) * (l |^ (m -' n)) = l |^ m & (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m ) )
assume that
A1: l > 1 and
A2: n <= m ; :: thesis: ( (l |^ n) * (l |^ (m -' n)) = l |^ m & (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m )
consider k being Nat such that
A3: m = n + k by A2, NAT_1:10;
k = m - n by A3;
then k = m -' n by XREAL_0:def 2;
hence A4: (l |^ n) * (l |^ (m -' n)) = l |^ m by A3, NEWTON:8; :: thesis: (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m

per cases ( m -' n = 0 or m -' n <> 0 ) ;

suppose m -' n = 0 ; :: thesis: (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m

then l |^ (m -' n) = 1 by NEWTON:4;
then (l |^ (m -' n)) - 1 = 0 ;
then A5: (l |^ (m -' n)) -' 1 = 0 by XREAL_0:def 2;
l |^ 0 <= l |^ m by A1, PREPOWER:93;
hence (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m by A5, NEWTON:4; :: thesis: verum

end;

suppose m -' n <> 0 ; :: thesis: (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m

then (l |^ (m -' n)) - 1 > 0 by A1, PEPIN:65, XREAL_1:50;
then A6: (l |^ (m -' n)) -' 1 = (l |^ (m -' n)) - 1 by XREAL_0:def 2;
l |^ n > 0 by A1, NEWTON:83;
hence (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m by A4, A6, XREAL_1:44, XREAL_1:68; :: thesis: verum

end;

end;