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

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

assume A1: 1 <= k ; :: thesis: 2 <= Radix k

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

S_{1}[kk + 1]
_{1}[1]
by POWER:25;

for k being Nat st 1 <= k holds

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

hence 2 <= Radix k by A1; :: thesis: verum

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

assume A1: 1 <= k ; :: thesis: 2 <= Radix k

A2: for kk being Nat st kk >= 1 & S

S

proof

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

assume that

1 <= kk and

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

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

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

Radix kk > 1 by A3, XXREAL_0:2;

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

end;assume that

1 <= kk and

A3: 2 <= Radix kk ; :: thesis: S

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

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

Radix kk > 1 by A3, XXREAL_0:2;

hence S

for k being Nat st 1 <= k holds

S

hence 2 <= Radix k by A1; :: thesis: verum