defpred S₁[ Nat] means ($1 + 1) to_power 6 < 2 * ($1 to_power 6);
A1: for n being Nat st n >= 9 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 9 & S₁[n] implies S₁[n + 1] )
assume that
A2: n >= 9 and
A3: (n + 1) to_power 6 < 2 * (n to_power 6) ; :: thesis: S₁[n + 1]
((n + 1) to_power 6) / (n to_power 6) < 2 by A2, A3, POWER:34, XREAL_1:83;
then A4: ((n + 1) / n) to_power 6 < 2 by A2, POWER:31;

A5: now :: thesis: not (n + 2) / (n + 1) >= (n + 1) / n

assume (n + 2) / (n + 1) >= (n + 1) / n ; :: thesis: contradiction
then ((n + 2) / (n + 1)) * (n + 1) >= ((n + 1) / n) * (n + 1) by XREAL_1:64;
then n + 2 >= ((n + 1) / n) * (n + 1) by XCMPLX_1:87;
then (n + 2) * n >= (((n + 1) / n) * (n + 1)) * n by XREAL_1:64;
then (n + 2) * n >= (((n + 1) / n) * n) * (n + 1) ;
then (n ^2) + (2 * n) >= (n + 1) ^2 by A2, XCMPLX_1:87;
then (n ^2) + (2 * n) >= ((n ^2) + (2 * n)) + (1 * 1) ;
then ((n ^2) + (2 * n)) - ((n ^2) + (2 * n)) >= 1 by XREAL_1:19;
hence contradiction ; :: thesis: verum

end;

A6: (n + 1) to_power 6 > 0 by POWER:34;
(n + 2) * ((n + 1) ") > 0 * ((n + 1) ") by XREAL_1:68;
then ((n + 2) / (n + 1)) to_power 6 < ((n + 1) / n) to_power 6 by A5, POWER:37;
then ((n + 2) / (n + 1)) to_power 6 < 2 by A4, XXREAL_0:2;
then ((n + 2) to_power 6) / ((n + 1) to_power 6) < 2 by POWER:31;
then (((n + 2) to_power 6) / ((n + 1) to_power 6)) * ((n + 1) to_power 6) < 2 * ((n + 1) to_power 6) by A6, XREAL_1:68;
hence S₁[n + 1] by A6, XCMPLX_1:87; :: thesis: verum

end;

A7: S₁[9]

proof

A8: 9 to_power 2 = 9 to_power (1 + 1)
.= (9 to_power 1) * (9 to_power 1) by POWER:27
.= 9 * (9 to_power 1) by POWER:25
.= 9 * 9 by POWER:25
.= 81 ;
2 * (9 to_power 4) = 2 * (9 to_power (2 + 2))
.= 2 * (81 * 81) by A8, POWER:27
.= 13122 ;
then A9: (13122 * 9) * 9 = (2 * ((9 to_power 4) * 9)) * 9
.= (2 * ((9 to_power 4) * (9 to_power 1))) * 9 by POWER:25
.= (2 * (9 to_power (4 + 1))) * 9 by POWER:27
.= 2 * ((9 to_power 5) * 9)
.= 2 * ((9 to_power 5) * (9 to_power 1)) by POWER:25
.= 2 * (9 to_power (5 + 1)) by POWER:27
.= 2 * (9 to_power 6) ;
consider t6 being Element of NAT such that
A10: t6 = ((((10 * 10) * 10) * 10) * 10) * 10 ;
A11: 10 to_power 3 = 10 to_power (2 + 1)
.= (10 to_power 2) * (10 to_power 1) by POWER:27
.= (10 to_power (1 + 1)) * 10 by POWER:25
.= ((10 to_power 1) * (10 to_power 1)) * 10 by POWER:27
.= (10 * (10 to_power 1)) * 10 by POWER:25
.= (10 * 10) * 10 by POWER:25 ;
10 to_power 6 = 10 to_power (3 + 3)
.= ((10 * 10) * 10) * ((10 * 10) * 10) by A11, POWER:27
.= t6 by A10 ;
hence S₁[9] by A10, A9; :: thesis: verum

end;

for n being Nat st n >= 9 holds
S₁[n] from NAT_1:sch 8(A7, A1);
hence for n being Nat st n >= 9 holds
(n + 1) to_power 6 < 2 * (n to_power 6) ; :: thesis: verum