set A = { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } ;
set B = {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)};
A1: 10 |^ 6 = ((((10 * 10) * 10) * 10) * 10) * 10 by NUMBER02:2;
thus { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } c= {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} :: according to XBOOLE_0:def 10 :: thesis: {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} c= { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } or x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} )
assume x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}
then consider n being Nat such that
A2: x = (2 |^ n) - 1 and
A3: (2 |^ n) - 1 <= 10 |^ 6 and
A4: (2 |^ n) - 1 is a_product_of_two_primes ;

A5: now :: thesis: ( n < 2 + 1 implies not 2 = 3 - 1 )

assume ( n < 2 + 1 & 2 = 3 - 1 ) ; :: thesis: contradiction
then not not n = 0 & ... & not n = 2 by NUMBER02:7;
hence contradiction by A4, Th19, Lm1, Lm2; :: thesis: verum

end;

A6: now :: thesis: ( n is even implies not n > 4 )

assume n is even ; :: thesis: not n > 4
then consider k being Nat such that
A7: n = 2 * k ;
A8: (2 |^ k) + 1 <> 0 + 1 ;

now :: thesis: not 2 |^ k = 2 |^ 1

assume 2 |^ k = 2 |^ 1 ; :: thesis: contradiction
then k = 1 by PEPIN:30;
hence contradiction by A7, A4, Th19, Lm2; :: thesis: verum

end;

then A9: (2 |^ k) - 1 <> 2 - 1 ;
2 |^ (2 * k) = (2 |^ k) |^ 2 by NEWTON:9
.= (2 |^ k) ^2 by WSIERP_1:1 ;
then (2 |^ n) - 1 = ((2 |^ k) + 1) * ((2 |^ k) - 1) by A7;
then ( (2 |^ k) + 1 is prime & (2 |^ k) - 1 is prime ) by A4, A8, A9, NUMBER07:59;
then k = 2 by Th22;
hence not n > 4 by A7; :: thesis: verum

end;

not not n = 0 & ... & not n = 19 by A1, A3, Lm25;

per cases then ( n = 3 or n = 4 or n = 5 or n = 2 * 3 or n = 7 or n = 2 * 4 or n = 9 or n = 2 * 5 or n = 11 or n = 2 * 6 or n = 13 or n = 2 * 7 or n = 15 or n = 2 * 8 or n = 17 or n = 2 * 9 or n = 19 ) by A5;

suppose n = 3 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, Lm3, XPRIMES1:7; :: thesis: verum

end;

suppose n = 4 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A2, ENUMSET1:def 1; :: thesis: verum

end;

suppose n = 5 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, Lm5, XPRIMES1:31; :: thesis: verum

end;

suppose n = 2 * 3 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose n = 7 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, Lm7, XPRIMES1:127; :: thesis: verum

end;

suppose n = 2 * 4 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose n = 9 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A2, ENUMSET1:def 1; :: thesis: verum

end;

suppose n = 2 * 5 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose n = 11 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A2, ENUMSET1:def 1; :: thesis: verum

end;

suppose n = 2 * 6 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose n = 13 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, Lm11, XPRIMES2:8191; :: thesis: verum

end;

suppose n = 2 * 7 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose A10: n = 15 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

(2 |^ 15) - 1 = (7 * 31) * 151 by Lm12;
hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, A10, XPRIMES1:7, XPRIMES1:31, XPRIMES1:151; :: thesis: verum

end;

suppose n = 2 * 8 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose n = 17 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, Th24; :: thesis: verum

end;

suppose n = 2 * 9 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A6; :: thesis: verum

end;

suppose n = 19 ; :: thesis: x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)}

hence x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} by A4, Th25; :: thesis: verum

end;

end;

end;

thus {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} c= { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} or x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } )
assume x in {((2 |^ 4) - 1),((2 |^ 9) - 1),((2 |^ 11) - 1)} ; :: thesis: x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) }

per cases then ( x = (2 |^ 4) - 1 or x = (2 |^ 9) - 1 or x = (2 |^ 11) - 1 ) by ENUMSET1:def 1;

suppose A11: x = (2 |^ 4) - 1 ; :: thesis: x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) }

(2 |^ 4) - 1 = 3 * 5 by Lm4;
hence x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } by A1, A11, XPRIMES1:3, XPRIMES1:5; :: thesis: verum

end;

suppose A12: x = (2 |^ 9) - 1 ; :: thesis: x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) }

(2 |^ 9) - 1 = 7 * 73 by Lm9;
hence x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } by A1, A12, XPRIMES1:7, XPRIMES1:73; :: thesis: verum

end;

suppose A13: x = (2 |^ 11) - 1 ; :: thesis: x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) }

(2 |^ 11) - 1 = 23 * 89 by Lm10;
hence x in { ((2 |^ n) - 1) where n is Nat : ( (2 |^ n) - 1 <= 10 |^ 6 & (2 |^ n) - 1 is a_product_of_two_primes ) } by A1, A13, XPRIMES1:23, XPRIMES1:89; :: thesis: verum

end;

end;

end;