let z be non zero Nat; :: thesis: { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } is infinite

set S = { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } ;

deffunc H_{1}( Nat) -> set = (6 * $1) - 1;

consider f being ManySortedSet of NATPLUS such that

A1: for n being Element of NATPLUS holds f . n = H_{1}(n)
from PBOOLE:sch 5();

set R = rng f;

A2: dom f = NATPLUS by PARTFUN1:def 2;

A3: rng f c= { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) }

( n >= m & n in rng f )

set S = { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } ;

deffunc H

consider f being ManySortedSet of NATPLUS such that

A1: for n being Element of NATPLUS holds f . n = H

set R = rng f;

A2: dom f = NATPLUS by PARTFUN1:def 2;

A3: rng f c= { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) }

proof

for m being Element of NAT ex n being Element of NAT st
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } )

assume a in rng f ; :: thesis: a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) }

then consider t being object such that

A4: t in dom f and

A5: a = f . t by FUNCT_1:def 3;

reconsider t = t as Element of NATPLUS by A4, PARTFUN1:def 2;

A6: a = (6 * t) - 1 by A1, A5;

A7: (2 * (3 * t)) - 1 is odd ;

0 + 1 <= t by NAT_1:13;

then (2 |^ (2 |^ z)) + ((6 * t) - 1) is composite by Th64;

hence a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } by A6, A7; :: thesis: verum

end;assume a in rng f ; :: thesis: a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) }

then consider t being object such that

A4: t in dom f and

A5: a = f . t by FUNCT_1:def 3;

reconsider t = t as Element of NATPLUS by A4, PARTFUN1:def 2;

A6: a = (6 * t) - 1 by A1, A5;

A7: (2 * (3 * t)) - 1 is odd ;

0 + 1 <= t by NAT_1:13;

then (2 |^ (2 |^ z)) + ((6 * t) - 1) is composite by Th64;

hence a in { k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } by A6, A7; :: thesis: verum

( n >= m & n in rng f )

proof

hence
{ k where k is Nat : ( k is odd & (2 |^ (2 |^ z)) + k is composite ) } is infinite
by A3, PYTHTRIP:9; :: thesis: verum
let m be Element of NAT ; :: thesis: ex n being Element of NAT st

( n >= m & n in rng f )

1 * m <= 6 * m by XREAL_1:64;

then A8: m + 0 <= (6 * m) + 5 by XREAL_1:7;

reconsider n = H_{1}(m + 1) as Element of NAT by INT_1:3;

take n ; :: thesis: ( n >= m & n in rng f )

thus n >= m by A8; :: thesis: n in rng f

A9: m + 1 in NATPLUS by NAT_LAT:def 6;

then f . (m + 1) = n by A1;

hence n in rng f by A2, A9, FUNCT_1:def 3; :: thesis: verum

end;( n >= m & n in rng f )

1 * m <= 6 * m by XREAL_1:64;

then A8: m + 0 <= (6 * m) + 5 by XREAL_1:7;

reconsider n = H

take n ; :: thesis: ( n >= m & n in rng f )

thus n >= m by A8; :: thesis: n in rng f

A9: m + 1 in NATPLUS by NAT_LAT:def 6;

then f . (m + 1) = n by A1;

hence n in rng f by A2, A9, FUNCT_1:def 3; :: thesis: verum