defpred S1[ 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 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 10 & S1[k] implies S1[k + 1] )
assume that
A4: k >= 10 and
A5: (2 to_power (2 * k)) / (k !) < 1 / (2 to_power (k - 9)) ; :: thesis: S1[k + 1]
A6: 2 to_power 1 > 0 by POWER:34;
A7: now :: thesis: not (2 to_power 2) / (k + 1) >= 1 / (2 to_power 1)
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:64;
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:27;
then 8 / (k + 1) >= 1 by A6, POWER:61, XCMPLX_1:106;
then (8 / (k + 1)) * (k + 1) >= 1 * (k + 1) by XREAL_1:64;
then 8 >= k + 1 by XCMPLX_1:87;
then 7 >= k by A2, XREAL_1:19;
hence contradiction by A4, XXREAL_0:2; :: thesis: verum
end;
2 to_power (- (k - 9)) > 0 by POWER:34;
then 1 / (2 to_power (k - 9)) > 0 by POWER:28;
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:68;
2 to_power 2 > 0 by POWER:34;
then A9: (2 to_power 2) * ((k + 1) ") > 0 * ((k + 1) ") by XREAL_1:68;
(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:27
.= ((2 to_power (2 * k)) * (2 to_power 2)) / ((k + 1) * (k !)) by NEWTON:15
.= ((2 to_power 2) / (k + 1)) * ((2 to_power (2 * k)) / (k !)) by XCMPLX_1:76 ;
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:68;
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:102;
then (2 to_power (2 * (k + 1))) / ((k + 1) !) < 1 / (2 to_power (1 + (k + (- 9)))) by POWER:27;
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:15
.= (2 to_power (1 + 19)) / (10 * (9 !))
.= ((2 to_power 1) * (2 to_power 19)) / (10 * (9 !)) by POWER:27
.= (2 * (2 to_power 19)) / (2 * (5 * (9 !))) by POWER:25
.= (2 to_power 19) / (5 * (9 !)) by XCMPLX_1:91
.= (2 to_power 19) / (5 * ((8 + 1) * (8 !))) by NEWTON:15
.= (2 to_power 19) / ((5 * 9) * (8 !))
.= (2 to_power 19) / (45 * ((7 + 1) * (7 !))) by NEWTON:15
.= (2 to_power (3 + 16)) / (8 * (45 * (7 !)))
.= (8 * (2 to_power 16)) / (8 * (45 * (7 !))) by POWER:27, POWER:61
.= (2 to_power 16) / (45 * (7 !)) by XCMPLX_1:91
.= (2 to_power (4 + 12)) / (45 * ((6 + 1) * (6 !))) by NEWTON:15
.= ((2 to_power (3 + 1)) * 4096) / (45 * ((6 + 1) * (6 !))) by Lm26, POWER:27
.= ((8 * (2 to_power 1)) * 4096) / (45 * ((6 + 1) * (6 !))) by POWER:27, POWER:61
.= ((8 * 2) * 4096) / (45 * ((6 + 1) * (6 !))) by POWER:25
.= (16 * 4096) / ((45 * 7) * (6 !))
.= (16 * 4096) / (315 * ((5 + 1) * (5 !))) by NEWTON:15
.= 4096 / 14175 by Lm33 ;
then A10: S1[10] by A1, POWER:25;
for n being Nat st n >= 10 holds
S1[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