let n be Nat; :: thesis: ( (2 |^ n) - 1 <= 1000000 implies not not n = 0 & ... & not n = 19 )
assume A1: (2 |^ n) - 1 <= 1000000 ; :: thesis: not not n = 0 & ... & not n = 19
A2: 2 |^ 20 = ((((((((((((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2 by Th10
.= 1048576 ;

per cases ( n <= 19 or n > 19 ) ;

suppose n <= 19 ; :: thesis: not not n = 0 & ... & not n = 19

hence not not n = 0 & ... & not n = 19 ; :: thesis: verum

end;

suppose n > 19 ; :: thesis: not not n = 0 & ... & not n = 19

then n >= 19 + 1 by NAT_1:13;
then 2 |^ n >= 2 |^ 20 by PREPOWER:93;
then (2 |^ n) - 1 >= (2 |^ 20) - 1 by XREAL_1:9;
hence not not n = 0 & ... & not n = 19 by A1, A2, XXREAL_0:2; :: thesis: verum

end;

end;