let k be Nat; :: thesis: ( 2 <= k implies 2 < Radix k )

defpred S_{1}[ Nat] means 2 < Radix $1;

A1: for kk being Nat st kk >= 2 & S_{1}[kk] holds

S_{1}[kk + 1]

.= (2 to_power 1) * (2 to_power 1) by POWER:27

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

.= 2 * 2 by POWER:25

.= 4 ;

then A4: S_{1}[2]
;

for k being Nat st 2 <= k holds

S_{1}[k]
from NAT_1:sch 8(A4, A1);

hence ( 2 <= k implies 2 < Radix k ) ; :: thesis: verum

defpred S

A1: for kk being Nat st kk >= 2 & S

S

proof

Radix 2 =
2 to_power (1 + 1)
let kk be Nat; :: thesis: ( kk >= 2 & S_{1}[kk] implies S_{1}[kk + 1] )

assume that

2 <= kk and

A2: 2 < Radix kk ; :: thesis: S_{1}[kk + 1]

A3: Radix (kk + 1) = (2 to_power 1) * (2 to_power kk) by POWER:27

.= 2 * (Radix kk) by POWER:25 ;

Radix kk > 1 by A2, XXREAL_0:2;

hence S_{1}[kk + 1]
by A3, XREAL_1:155; :: thesis: verum

end;assume that

2 <= kk and

A2: 2 < Radix kk ; :: thesis: S

A3: Radix (kk + 1) = (2 to_power 1) * (2 to_power kk) by POWER:27

.= 2 * (Radix kk) by POWER:25 ;

Radix kk > 1 by A2, XXREAL_0:2;

hence S

.= (2 to_power 1) * (2 to_power 1) by POWER:27

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

.= 2 * 2 by POWER:25

.= 4 ;

then A4: S

for k being Nat st 2 <= k holds

S

hence ( 2 <= k implies 2 < Radix k ) ; :: thesis: verum