defpred S_{1}[ Nat] means 2 * $1 <= 2 to_power $1;

P1: S_{1}[ 0 ]
;

P2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(P1, P2);

hence for k being Nat holds 2 * k <= 2 to_power k ; :: thesis: verum

P1: S

P2: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A1: S_{1}[n]
; :: thesis: S_{1}[n + 1]

end;assume A1: S

per cases
( n = 0 or n <> 0 )
;

end;

suppose
n <> 0
; :: thesis: S_{1}[n + 1]

then
n - 1 in NAT
by INT_1:5, NAT_1:14;

then reconsider m = n - 1 as Nat ;

A3: 2 <= 2 to_power (m + 1) by LMC31B;

A2: 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27

.= (2 to_power n) * 2 by POWER:25

.= (2 to_power n) + (2 to_power n) ;

(2 * n) + 2 <= (2 to_power n) + (2 to_power n) by A3, XREAL_1:7, A1;

hence 2 * (n + 1) <= 2 to_power (n + 1) by A2; :: thesis: verum

end;then reconsider m = n - 1 as Nat ;

A3: 2 <= 2 to_power (m + 1) by LMC31B;

A2: 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27

.= (2 to_power n) * 2 by POWER:25

.= (2 to_power n) + (2 to_power n) ;

(2 * n) + 2 <= (2 to_power n) + (2 to_power n) by A3, XREAL_1:7, A1;

hence 2 * (n + 1) <= 2 to_power (n + 1) by A2; :: thesis: verum

hence for k being Nat holds 2 * k <= 2 to_power k ; :: thesis: verum