defpred S₁[ Nat] means (2 to_power (2 * $1)) / ($1 ! ) < 1 / (2 to_power ($1 - 9));
A1: 7 = 8 - 1 ;
A2: S₁[10]

proof

A3: (2 to_power (2 * 10)) / (10 ! ) = (2 to_power 20) / ((9 + 1) * (9 ! )) by NEWTON:21
.= (2 to_power (1 + 19)) / (10 * (9 ! ))
.= ((2 to_power 1) * (2 to_power 19)) / (10 * (9 ! )) by POWER:32
.= (2 * (2 to_power 19)) / (2 * (5 * (9 ! ))) by POWER:30
.= (2 to_power 19) / (5 * (9 ! )) by XCMPLX_1:92
.= (2 to_power 19) / (5 * ((8 + 1) * (8 ! ))) by NEWTON:21
.= (2 to_power 19) / ((5 * 9) * (8 ! ))
.= (2 to_power 19) / (45 * ((7 + 1) * (7 ! ))) by NEWTON:21
.= (2 to_power (3 + 16)) / (8 * (45 * (7 ! )))
.= (8 * (2 to_power 16)) / (8 * (45 * (7 ! ))) by Lm8, POWER:32
.= (2 to_power 16) / (45 * (7 ! )) by XCMPLX_1:92
.= (2 to_power (4 + 12)) / (45 * ((6 + 1) * (6 ! ))) by NEWTON:21
.= ((2 to_power (3 + 1)) * 4096) / (45 * ((6 + 1) * (6 ! ))) by Lm32, POWER:32
.= ((8 * (2 to_power 1)) * 4096) / (45 * ((6 + 1) * (6 ! ))) by Lm8, POWER:32
.= ((8 * 2) * 4096) / (45 * ((6 + 1) * (6 ! ))) by POWER:30
.= (16 * 4096) / ((45 * 7) * (6 ! ))
.= (16 * 4096) / (315 * ((5 + 1) * (5 ! ))) by NEWTON:21
.= 4096 / 14175 by Lm39 ;
not 4096 / 14175 >= 1 / 2 ;
hence S₁[10] by A3, POWER:30; :: thesis: verum

end;

A4: for k being Nat st k >= 10 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 10 & S₁[k] implies S₁[k + 1] )
assume that
A5: k >= 10 and
A6: (2 to_power (2 * k)) / (k ! ) < 1 / (2 to_power (k - 9)) ; :: thesis: S₁[k + 1]
A7: 2 to_power 2 > 0 by POWER:39;
(2 to_power 2) * ((k + 1) " ) > 0 * ((k + 1) " ) by A7, XREAL_1:70;
then A8: (2 to_power 2) / (k + 1) > 0 ;
2 to_power (- (k - 9)) > 0 by POWER:39;
then A9: 1 / (2 to_power (k - 9)) > 0 by POWER:33;
(2 to_power (2 * (k + 1))) / ((k + 1) ! ) = (2 to_power ((2 * k) + (2 * 1))) / ((k + 1) ! )
.= ((2 to_power (2 * k)) * (2 to_power 2)) / ((k + 1) ! ) by POWER:32
.= ((2 to_power (2 * k)) * (2 to_power 2)) / ((k + 1) * (k ! )) by NEWTON:21
.= ((2 to_power 2) / (k + 1)) * ((2 to_power (2 * k)) / (k ! )) by XCMPLX_1:77 ;
then A10: (2 to_power (2 * (k + 1))) / ((k + 1) ! ) < ((2 to_power 2) / (k + 1)) * (1 / (2 to_power (k - 9))) by A6, A8, XREAL_1:70;
A11: 2 to_power 1 > 0 by POWER:39;

now

assume (2 to_power 2) / (k + 1) >= 1 / (2 to_power 1) ; :: thesis: contradiction
then (2 to_power 1) * ((2 to_power 2) / (k + 1)) >= (1 / (2 to_power 1)) * (2 to_power 1) by XREAL_1:66;
then (2 to_power 1) * ((2 to_power 2) * ((k + 1) " )) >= (1 / (2 to_power 1)) * (2 to_power 1) ;
then ((2 to_power 1) * (2 to_power 2)) * ((k + 1) " ) >= (1 / (2 to_power 1)) * (2 to_power 1) ;
then (2 to_power (1 + 2)) * ((k + 1) " ) >= (1 / (2 to_power 1)) * (2 to_power 1) by POWER:32;
then 8 / (k + 1) >= (1 / (2 to_power 1)) * (2 to_power 1) by Lm8;
then 8 / (k + 1) >= 1 by A11, XCMPLX_1:107;
then (8 / (k + 1)) * (k + 1) >= 1 * (k + 1) by XREAL_1:66;
then 8 >= k + 1 by XCMPLX_1:88;
then 7 >= k by A1, XREAL_1:21;
hence contradiction by A5, XXREAL_0:2; :: thesis: verum

end;

then ((2 to_power 2) / (k + 1)) * (1 / (2 to_power (k - 9))) < (1 / (2 to_power 1)) * (1 / (2 to_power (k - 9))) by A9, XREAL_1:70;
then (2 to_power (2 * (k + 1))) / ((k + 1) ! ) < (1 / (2 to_power 1)) * (1 / (2 to_power (k - 9))) by A10, XXREAL_0:2;
then (2 to_power (2 * (k + 1))) / ((k + 1) ! ) < 1 / ((2 to_power 1) * (2 to_power (k - 9))) by XCMPLX_1:103;
then (2 to_power (2 * (k + 1))) / ((k + 1) ! ) < 1 / (2 to_power (1 + (k + (- 9)))) by POWER:32;
hence (2 to_power (2 * (k + 1))) / ((k + 1) ! ) < 1 / (2 to_power ((k + 1) - 9)) ; :: thesis: verum

end;

for n being Nat st n >= 10 holds
S₁[n] from NAT_1:sch 8(A2, A4);
hence for n being Element of NAT st n >= 10 holds
(2 to_power (2 * n)) / (n ! ) < 1 / (2 to_power (n - 9)) ; :: thesis: verum