let A be set ; :: thesis: ( A = { n where n is non zero Nat : n gcd ((2 |^ n) - 1) > 1 } implies ( A is infinite & ( for k being Nat st k in A holds
k >= 6 ) ) )
assume A0: A = { n where n is non zero Nat : n gcd ((2 |^ n) - 1) > 1 } ; :: thesis: ( A is infinite & ( for k being Nat st k in A holds
k >= 6 ) )
Co: for k being non zero Nat holds (6 * k) gcd ((2 |^ (6 * k)) - 1) >= 3

proof

let k be non zero Nat; :: thesis: (6 * k) gcd ((2 |^ (6 * k)) - 1) >= 3
ra: 3 divides 3 * (2 * k) ;
rr: 2 divides 2 * (3 * k) ;
SS: 2 |^ 2 = 2 * 2 by NEWTON:81
.= 4 ;
3 = (2 |^ 2) - 1 by SS;
then 3 divides (2 |^ (6 * k)) - 1 by rr, NUMBER05:19;
then 3 divides (6 * k) gcd ((2 |^ (6 * k)) - 1) by ra, NAT_D:def 5;
hence (6 * k) gcd ((2 |^ (6 * k)) - 1) >= 3 by NAT_D:7; :: thesis: verum

end;

HU: for k being non zero Nat holds 6 * k in A

proof

let k be non zero Nat; :: thesis: 6 * k in A
(6 * k) gcd ((2 |^ (6 * k)) - 1) >= 3 by Co;
then (6 * k) gcd ((2 |^ (6 * k)) - 1) > 1 by XXREAL_0:2;
hence 6 * k in A by A0; :: thesis: verum

end;

for m being Nat ex n being Nat st
( n >= m & n in A )

proof

let m be Nat; :: thesis: ex n being Nat st
( n >= m & n in A )
take n = 6 * (m + 1); :: thesis: ( n >= m & n in A )
Y1: 1 * m <= 6 * m by XREAL_1:64;
m <= m + 1 by NAT_1:13;
then 6 * m <= 6 * (m + 1) by XREAL_1:64;
hence ( n >= m & n in A ) by HU, Y1, XXREAL_0:2; :: thesis: verum

end;

hence A is infinite by PYTHTRIP:9; :: thesis: for k being Nat st k in A holds
k >= 6
for k being Nat st k in A holds
k >= 6

proof

let k be Nat; :: thesis: ( k in A implies k >= 6 )
assume k in A ; :: thesis: k >= 6
then consider kk being non zero Nat such that
A1: ( kk = k & kk gcd ((2 |^ kk) - 1) > 1 ) by A0;
V2: k <> 2

proof

assume k = 2 ; :: thesis: contradiction
then k gcd ((2 |^ k) - 1) = 2 gcd ((2 * 2) - 1) by NEWTON:81
.= 2 gcd (2 + 1)
.= 1 ;
hence contradiction by A1; :: thesis: verum

end;

v3: 3,7 are_coprime by NUMBER06:3, XPRIMES1:3, XPRIMES1:7;
V4: k <> 4

proof

assume k = 4 ; :: thesis: contradiction
then k gcd ((2 |^ k) - 1) = 4 gcd ((3 * 4) + 3) by POWER:62
.= (3 + 1) gcd 3 by NEWTON02:5
.= 1 ;
hence contradiction by A1; :: thesis: verum

end;

v5: 5,31 are_coprime by NUMBER06:3, XPRIMES1:5, XPRIMES1:31;
not k <= 5

proof

assume k <= 5 ; :: thesis: contradiction
then not not k = 0 & ... & not k = 5 ;
hence contradiction by A1, V2, v3, V4, v5, POWER:61, POWER:63; :: thesis: verum

end;

then k >= 5 + 1 by NAT_1:13;
hence k >= 6 ; :: thesis: verum

end;

hence for k being Nat st k in A holds
k >= 6 ; :: thesis: verum