( 3 = (4 * 0) + 3 & 3 is prime ) by PEPIN:41;
then A1: 3 in 4k+3_Primes by Def1;
assume 4k+3_Primes is finite ; :: thesis: contradiction
then consider n being Element of NAT such that
A2: 4k+3_Primes c= (Seg n) \/ {0} by A1, HEYTING3:1;
A3: 4k+3_Primes c= Seg n by A2, ZFMISC_1:135, Th4;
set X = 4k+3_Primes \ {3};
4k+3_Primes \ {3} c= 4k+3_Primes by XBOOLE_1:36;
then 4k+3_Primes \ {3} c= Seg n by A3, XBOOLE_1:1;
then a4: 4k+3_Primes \ {3} is included_in_Seg by FINSEQ_1:def 13;
set N = (4 * (Product (Sgm (4k+3_Primes \ {3})))) + 3;
consider p, q being Nat such that
A5: ( p = (4 * q) + 3 & p is prime & p divides (4 * (Product (Sgm (4k+3_Primes \ {3})))) + 3 ) by Th3;
A6: p in 4k+3_Primes by Def1, A5;
rng (Sgm (4k+3_Primes \ {3})) c= SetPrimes

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (Sgm (4k+3_Primes \ {3})) or a in SetPrimes )
assume A7: a in rng (Sgm (4k+3_Primes \ {3})) ; :: thesis: a in SetPrimes
then a in 4k+3_Primes \ {3} by a4, FINSEQ_1:def 14;
then A8: a in 4k+3_Primes by XBOOLE_0:def 5;
reconsider n = a as Nat by A7;
consider k being Nat such that
A9: ( n = (4 * k) + 3 & n is prime ) by A8, Def1;
thus a in SetPrimes by A9, NEWTON:def 6; :: thesis: verum

end;

then reconsider SX = Sgm (4k+3_Primes \ {3}) as FinSequence of SetPrimes by FINSEQ_1:def 4;
for p being prime Nat st p in 4k+3_Primes holds
not p divides (4 * (Product (Sgm (4k+3_Primes \ {3})))) + 3

proof

let p be prime Nat; :: thesis: ( p in 4k+3_Primes implies not p divides (4 * (Product (Sgm (4k+3_Primes \ {3})))) + 3 )
assume A10: p in 4k+3_Primes ; :: thesis: not p divides (4 * (Product (Sgm (4k+3_Primes \ {3})))) + 3
assume A11: p divides (4 * (Product (Sgm (4k+3_Primes \ {3})))) + 3 ; :: thesis: contradiction
p >= 3 by A10, Th4;

per cases then ( p = 3 or p > 3 ) by XXREAL_0:1;

suppose A12: p = 3 ; :: thesis: contradiction

2,3 are_coprime by INT_2:30, INT_2:28, PEPIN:41;
then A13: 2 * 2,3 are_coprime by EULER_1:14;
p divides 4 * (Product (Sgm (4k+3_Primes \ {3}))) by A11, A12, INT_2:1;
then p in rng SX by A12, A13, EULER_1:13, NAT_3:8;
then p in 4k+3_Primes \ {3} by a4, FINSEQ_1:def 14;
then not p in {3} by XBOOLE_0:def 5;
hence contradiction by A12, TARSKI:def 1; :: thesis: verum

end;

suppose A14: p > 3 ; :: thesis: contradiction

then not p in {3} by TARSKI:def 1;
then p in 4k+3_Primes \ {3} by A10, XBOOLE_0:def 5;
then p in rng SX by a4, FINSEQ_1:def 14;
then p divides 4 * (Product (Sgm (4k+3_Primes \ {3}))) by NAT_D:9, NAT_3:7;
hence contradiction by A14, INT_2:1, INT_2:27, A11; :: thesis: verum

end;

end;

end;

hence contradiction by A5, A6; :: thesis: verum