hereby :: thesis: ( not value ((<%1%> ^ (8 --> 3)),10) is prime & { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } is infinite )
let n be non zero Nat; :: thesis: ( n < 6 implies value ((<%1%> ^ (b1 --> 3)),10) is prime )
assume A1: n < 6 ; :: thesis: value ((<%1%> ^ (b1 --> 3)),10) is prime
then A2: not not n = 0 & ... & not n = 6 ;
A3: value ((<%1%> ^ (n --> 3)),10) = ((10 |^ (n + 1)) - 7) / 3 by Th16;
10 |^ (0 + 1) = 10 ;
then A4: 10 |^ (1 + 1) = 10 * 10 by NEWTON:6;
then A5: 10 |^ (2 + 1) = (10 * 10) * 10 by NEWTON:6;
then A6: 10 |^ (3 + 1) = ((10 * 10) * 10) * 10 by NEWTON:6;
then A7: 10 |^ (4 + 1) = (((10 * 10) * 10) * 10) * 10 by NEWTON:6;
then A8: 10 |^ (5 + 1) = ((((10 * 10) * 10) * 10) * 10) * 10 by NEWTON:6;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A1, A2;
suppose n = 1 ; :: thesis: value ((<%1%> ^ (b1 --> 3)),10) is prime
hence value ((<%1%> ^ (n --> 3)),10) is prime by A3, A4, XPRIMES1:31; :: thesis: verum
end;
suppose n = 2 ; :: thesis: value ((<%1%> ^ (b1 --> 3)),10) is prime
hence value ((<%1%> ^ (n --> 3)),10) is prime by A3, A5, XPRIMES1:331; :: thesis: verum
end;
suppose n = 3 ; :: thesis: value ((<%1%> ^ (b1 --> 3)),10) is prime
hence value ((<%1%> ^ (n --> 3)),10) is prime by A3, A6, XPRIMES1:3331; :: thesis: verum
end;
suppose n = 4 ; :: thesis: value ((<%1%> ^ (b1 --> 3)),10) is prime
hence value ((<%1%> ^ (n --> 3)),10) is prime by A3, A7, Th18; :: thesis: verum
end;
suppose n = 5 ; :: thesis: value ((<%1%> ^ (b1 --> 3)),10) is prime
hence value ((<%1%> ^ (n --> 3)),10) is prime by A3, A8, Th19; :: thesis: verum
end;
end;
end;
consider v being Nat such that
A9: ( 17 divides v & v = ((10 |^ ((16 * 0) + 9)) - 7) / 3 ) by Th17;
value ((<%1%> ^ (8 --> 3)),10) = ((10 |^ (8 + 1)) - 7) / 3 by Th16;
hence not value ((<%1%> ^ (8 --> 3)),10) is prime by A9, Lm1; :: thesis: { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } is infinite
set V = { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } ;
deffunc H1( Nat) -> set = ((10 |^ ((16 * $1) + 9)) - 7) / 3;
consider f being Function such that
A10: ( dom f = NAT & ( for d being Element of NAT holds f . d = H1(d) ) ) from FUNCT_1:sch 4();
 A11: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A12: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Element of NAT by A12, A10;
( ((10 |^ ((16 * n1) + 9)) - 7) / 3 = f . n1 & f . n2 = ((10 |^ ((16 * n2) + 9)) - 7) / 3 ) by A10;
then ((10 |^ ((16 * n1) + 9)) - 7) / 3 = ((10 |^ ((16 * n2) + 9)) - 7) / 3 by A12;
then (16 * n1) + 9 = (16 * n2) + 9 by PEPIN:30;
hence x1 = x2 ; :: thesis: verum
end;
rng f c= { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } )
assume y in rng f ; :: thesis: y in { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime }
then consider x being object such that
A13: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A13, A10;
( f . x = ((10 |^ ((16 * x) + 9)) - 7) / 3 & ((10 |^ ((16 * x) + 9)) - 7) / 3 = ((10 |^ (((16 * x) + 8) + 1)) - 7) / 3 ) by A13, A10;
then A14: f . x = value ((<%1%> ^ (((16 * x) + 8) --> 3)),10) by Th16;
consider v being Nat such that
A15: ( 17 divides v & v = ((10 |^ ((16 * x) + 9)) - 7) / 3 ) by Th17;
value ((<%1%> ^ (((16 * x) + 8) --> 3)),10) = ((10 |^ (((16 * x) + 8) + 1)) - 7) / 3 by Th16;
then not value ((<%1%> ^ (((16 * x) + 8) --> 3)),10) is prime by A15, Lm1;
hence y in { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } by A14, A13; :: thesis: verum
end;
hence { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } is infinite by A11, FUNCT_1:def 4, A10, CARD_1:59; :: thesis: verum