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

( (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 )
;

end;

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;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

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;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