defpred S₁[ Nat] means (2 to_power (2 * $1)) / ($1 !) < 1 / (2 to_power ($1 - 9));
A1: not 4096 / 14175 >= 1 / 2 ;
A2: 7 = 8 - 1 ;
A3: 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
A4: k >= 10 and
A5: (2 to_power (2 * k)) / (k !) < 1 / (2 to_power (k - 9)) ; :: thesis: S₁[k + 1]
A6: 2 to_power 1 > 0 by POWER:39;

A7: 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)) * ((k + 1) ") >= (1 / (2 to_power 1)) * (2 to_power 1) by POWER:32;
then 8 / (k + 1) >= 1 by A6, POWER:69, 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 A2, XREAL_1:21;
hence contradiction by A4, XXREAL_0:2; :: thesis: verum

end;

2 to_power (- (k - 9)) > 0 by POWER:39;
then 1 / (2 to_power (k - 9)) > 0 by POWER:33;
then A8: ((2 to_power 2) / (k + 1)) * (1 / (2 to_power (k - 9))) < (1 / (2 to_power 1)) * (1 / (2 to_power (k - 9))) by A7, XREAL_1:70;
2 to_power 2 > 0 by POWER:39;
then A9: (2 to_power 2) * ((k + 1) ") > 0 * ((k + 1) ") by XREAL_1:70;
(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 (2 to_power (2 * (k + 1))) / ((k + 1) !) < ((2 to_power 2) / (k + 1)) * (1 / (2 to_power (k - 9))) by A5, 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 A8, 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;

(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 POWER:32, POWER:69
.= (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 Lm26, POWER:32
.= ((8 * (2 to_power 1)) * 4096) / (45 * ((6 + 1) * (6 !))) by POWER:32, POWER:69
.= ((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 Lm33 ;
then A10: S₁[10] by A1, POWER:30;
for n being Nat st n >= 10 holds
S₁[n] from NAT_1:sch 8(A10, A3);
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