let b be Nat; :: thesis: ( b >= 2 implies (b + 1) ! > 2 |^ b )

defpred S_{1}[ Nat] means ($1 + 1) ! > 2 |^ $1;

A1: S_{1}[2]
_{1}[k] holds

S_{1}[k + 1]

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

hence ( b >= 2 implies (b + 1) ! > 2 |^ b ) ; :: thesis: verum

defpred S

A1: S

proof

A2:
for k being Nat st k >= 2 & S
B1:
(2 + 1) ! = 2 * 3
by NEWTON:14, NEWTON:15;

2 |^ 2 = 2 * 2 by NEWTON:81;

hence S_{1}[2]
by B1; :: thesis: verum

end;2 |^ 2 = 2 * 2 by NEWTON:81;

hence S

S

proof

for x being Nat st x >= 2 holds
let k be Nat; :: thesis: ( k >= 2 & S_{1}[k] implies S_{1}[k + 1] )

assume B1: ( k >= 2 & (k + 1) ! > 2 |^ k ) ; :: thesis: S_{1}[k + 1]

then k + 2 > 2 + 0 by XREAL_1:6;

then ((k + 1) !) * ((k + 1) + 1) > (2 |^ k) * 2 by B1, XREAL_1:96;

then ((k + 1) !) * ((k + 1) + 1) > 2 |^ (k + 1) by NEWTON:6;

hence S_{1}[k + 1]
by NEWTON:15; :: thesis: verum

end;assume B1: ( k >= 2 & (k + 1) ! > 2 |^ k ) ; :: thesis: S

then k + 2 > 2 + 0 by XREAL_1:6;

then ((k + 1) !) * ((k + 1) + 1) > (2 |^ k) * 2 by B1, XREAL_1:96;

then ((k + 1) !) * ((k + 1) + 1) > 2 |^ (k + 1) by NEWTON:6;

hence S

S

hence ( b >= 2 implies (b + 1) ! > 2 |^ b ) ; :: thesis: verum