let m be Nat; rng (Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)))) misses SetPrimes
set f = Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)));
assume
rng (Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)))) meets SetPrimes
; contradiction
then consider x being object such that
A2:
( x in rng (Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)))) & x in SetPrimes )
by XBOOLE_0:3;
consider n being object such that
A3:
( n in dom (Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)))) & x = (Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)))) . n )
by A2, FUNCT_1:def 3;
A4:
n in Seg (((m !) + 2),((m !) + m))
by A3, RELAT_1:57;
then
n in { i where i is Nat : ( (m !) + 2 <= i & i <= (m !) + m ) }
by SGRAPH1:def 1;
then consider nn being Nat such that
A5:
( n = nn & (m !) + 2 <= nn & nn <= (m !) + m )
;
consider k being Nat such that
C1:
((m !) + 2) + k = nn
by A5, NAT_1:10;
E1:
(m !) + (2 + k) <= (m !) + m
by C1, A5;
set l = k + 2;
A6:
nn = (m !) + (k + 2)
by C1;
2 <= k + 2
by NAT_1:11;
then A7:
( 2 <= k + 2 & k + 2 <= m )
by E1, XREAL_1:6;
AA:
n in NAT
by A5, ORDINAL1:def 12;
BA:
Mersenne nn = (2 |^ nn) - 1
by GR_CY_3:def 3;
x =
Mersenne_sequence . n
by A3, A4, FUNCT_1:49
.=
Mersenne nn
by AA, A5, MerDef
;
then
x is not Prime
by BA, A7, A6, LemmaMersenne;
hence
contradiction
by A2, NEWTON:def 6; verum