let L be Real; :: thesis: ( 0 < L & L < 1 implies for k being Nat holds

( L to_power k <= 1 & 0 < L to_power k ) )

assume that

A1: 0 < L and

A2: L < 1 ; :: thesis: for k being Nat holds

( L to_power k <= 1 & 0 < L to_power k )

defpred S_{1}[ Nat] means ( L to_power $1 <= 1 & 0 < L to_power $1 );

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by POWER:24;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A7, A3); :: thesis: verum

( L to_power k <= 1 & 0 < L to_power k ) )

assume that

A1: 0 < L and

A2: L < 1 ; :: thesis: for k being Nat holds

( L to_power k <= 1 & 0 < L to_power k )

defpred S

A3: for k being Nat st S

S

proof

A7:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume that

A4: L to_power k <= 1 and

A5: 0 < L to_power k ; :: thesis: S_{1}[k + 1]

A6: L to_power (k + 1) = (L to_power k) * (L to_power 1) by A1, POWER:27

.= (L to_power k) * L by POWER:25 ;

(L to_power k) * L <= L to_power k by A2, A5, XREAL_1:153;

hence S_{1}[k + 1]
by A1, A4, A5, A6, XREAL_1:129, XXREAL_0:2; :: thesis: verum

end;assume that

A4: L to_power k <= 1 and

A5: 0 < L to_power k ; :: thesis: S

A6: L to_power (k + 1) = (L to_power k) * (L to_power 1) by A1, POWER:27

.= (L to_power k) * L by POWER:25 ;

(L to_power k) * L <= L to_power k by A2, A5, XREAL_1:153;

hence S

thus for k being Nat holds S