defpred S₁[ Nat] means ($1 + 1) to_power 6 < 2 * ($1 to_power 6);
A1: S₁[9]

proof

A2: 9 to_power 2 = 9 to_power (1 + 1)
.= (9 to_power 1) * (9 to_power 1) by POWER:32
.= 9 * (9 to_power 1) by POWER:30
.= 9 * 9 by POWER:30
.= 81 ;
A3: 2 * (9 to_power 4) = 2 * (9 to_power (2 + 2))
.= 2 * (81 * 81) by A2, POWER:32
.= 13122 ;
consider t6 being Element of NAT such that
A4: t6 = ((((10 * 10) * 10) * 10) * 10) * 10 ;
A5: 10 to_power 3 = 10 to_power (2 + 1)
.= (10 to_power 2) * (10 to_power 1) by POWER:32
.= (10 to_power (1 + 1)) * 10 by POWER:30
.= ((10 to_power 1) * (10 to_power 1)) * 10 by POWER:32
.= (10 * (10 to_power 1)) * 10 by POWER:30
.= (10 * 10) * 10 by POWER:30 ;
A6: 10 to_power 6 = 10 to_power (3 + 3)
.= ((10 * 10) * 10) * ((10 * 10) * 10) by A5, POWER:32
.= t6 by A4 ;
(13122 * 9) * 9 = (2 * ((9 to_power 4) * 9)) * 9 by A3
.= (2 * ((9 to_power 4) * (9 to_power 1))) * 9 by POWER:30
.= (2 * (9 to_power (4 + 1))) * 9 by POWER:32
.= 2 * ((9 to_power 5) * 9)
.= 2 * ((9 to_power 5) * (9 to_power 1)) by POWER:30
.= 2 * (9 to_power (5 + 1)) by POWER:32
.= 2 * (9 to_power 6) ;
hence S₁[9] by A4, A6; :: thesis: verum

end;

A7: 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
A8: n >= 9 and
A9: (n + 1) to_power 6 < 2 * (n to_power 6) ; :: thesis: S₁[n + 1]
A10: n to_power 6 > 0 by A8, POWER:39;
A11: (n + 1) to_power 6 > 0 by POWER:39;
(n + 2) * ((n + 1) " ) > 0 * ((n + 1) " ) by XREAL_1:70;
then A12: (n + 2) / (n + 1) > 0 ;

now

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:66;
then n + 2 >= ((n + 1) / n) * (n + 1) by XCMPLX_1:88;
then (n + 2) * n >= (((n + 1) / n) * (n + 1)) * n by XREAL_1:66;
then (n + 2) * n >= (((n + 1) / n) * n) * (n + 1) ;
then (n ^2 ) + (2 * n) >= (n + 1) ^2 by A8, XCMPLX_1:88;
then (n ^2 ) + (2 * n) >= ((n ^2 ) + (2 * n)) + (1 * 1) ;
then ((n ^2 ) + (2 * n)) - ((n ^2 ) + (2 * n)) >= 1 by XREAL_1:21;
hence contradiction ; :: thesis: verum

end;

then A13: ((n + 2) / (n + 1)) to_power 6 < ((n + 1) / n) to_power 6 by A12, POWER:42;
((n + 1) to_power 6) / (n to_power 6) < 2 by A9, A10, XREAL_1:85;
then ((n + 1) / n) to_power 6 < 2 by A8, POWER:36;
then ((n + 2) / (n + 1)) to_power 6 < 2 by A13, XXREAL_0:2;
then ((n + 2) to_power 6) / ((n + 1) to_power 6) < 2 by POWER:36;
then (((n + 2) to_power 6) / ((n + 1) to_power 6)) * ((n + 1) to_power 6) < 2 * ((n + 1) to_power 6) by A11, XREAL_1:70;
hence S₁[n + 1] by A11, XCMPLX_1:88; :: thesis: verum

end;

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