defpred S₁[ Nat] means ( ex k being Nat st $1 = (4 * k) + 3 implies ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides $1 ) );
let k be Integer; :: thesis: for n being Nat st n = (4 * k) + 3 holds
ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides n )
let n be Nat; :: thesis: ( n = (4 * k) + 3 implies ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides n ) )
assume A1: n = (4 * k) + 3 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides n )

now :: thesis: not k < 0

assume k < 0 ; :: thesis: contradiction
then B2: k + 1 <= 0 by INT_1:7;
((4 * k) + 3) - 3 >= 0 - 3 by A1, XREAL_1:9;
then (4 * k) / 4 >= (- 3) / 4 by XREAL_1:72;
then k + 1 >= (- (3 / 4)) + 1 by XREAL_1:7;
hence contradiction by B2, XXREAL_0:2; :: thesis: verum

end;

then reconsider k = k as Element of NAT by INT_1:3;
B1: n = (4 * k) + 3 by A1;
A2: for m being Nat st ( for l being Nat st l < m holds
S₁[l] ) holds
S₁[m]

proof

let m be Nat; :: thesis: ( ( for l being Nat st l < m holds
S₁[l] ) implies S₁[m] )
assume A3: for l being Nat st l < m holds
S₁[l] ; :: thesis: S₁[m]
given k being Nat such that A4: m = (4 * k) + 3 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )
( m <> 0 & m <> 1 ) by A4, NAT_1:11;
then not m is trivial by NAT_2:28;
then consider l being prime Nat such that
A5: l divides m by NEWTON03:29;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
consider t being Nat such that
A6: m = l * t by A5, NAT_D:def 3;
A7: t divides m by A6;
consider u being Element of NAT such that
A8: ( l = 4 * u or l = (4 * u) + 1 or l = (4 * u) + 2 or l = (4 * u) + 3 ) by SCHEME1:3;

per cases ( l = 4 * u or l = (4 * u) + 1 or l = (4 * u) + 2 or l = (4 * u) + 3 ) by A8;

suppose l = 4 * u ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

then 4 divides l ;
then 4 divides m by A5, NAT_D:4;
hence ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m ) by A4, NUMBER02:32; :: thesis: verum

end;

suppose A9: l = (4 * u) + 1 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

reconsider t = t as Element of NAT by ORDINAL1:def 12;
consider v being Element of NAT such that
A10: ( t = 4 * v or t = (4 * v) + 1 or t = (4 * v) + 2 or t = (4 * v) + 3 ) by SCHEME1:3;

per cases ( t = 4 * v or t = (4 * v) + 1 or t = (4 * v) + 2 or t = (4 * v) + 3 ) by A10;

suppose t = 4 * v ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

then 4 divides t ;
then 4 divides m by A7, NAT_D:4;
hence ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m ) by A4, NUMBER02:32; :: thesis: verum

end;

suppose t = (4 * v) + 1 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

then m = (4 * ((((4 * u) * v) + u) + v)) + 1 by A6, A9;
then A11: m mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24 ;
m mod 4 = 3 mod 4 by A4, NAT_D:21
.= 3 by NAT_D:24 ;
hence ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m ) by A11; :: thesis: verum

end;

suppose t = (4 * v) + 2 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

then t = 2 * ((2 * v) + 1) ;
then A12: 2 divides t ;
m = (2 * ((2 * k) + 1)) + 1 by A4;
hence ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m ) by A12, A7; :: thesis: verum

end;

suppose A13: t = (4 * v) + 3 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

A14: t <= m by A6, NAT_D:def 3, INT_2:27;

now :: thesis: not t = m

assume t = m ; :: thesis: contradiction
then l = 1 by A6, A4, XCMPLX_1:7;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

then t < m by A14, XXREAL_0:1;
then consider p, q being Nat such that
A15: ( p = (4 * q) + 3 & p is prime & p divides t ) by A13, A3;
take p ; :: thesis: ex q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )
take q ; :: thesis: ( p = (4 * q) + 3 & p is prime & p divides m )
thus ( p = (4 * q) + 3 & p is prime & p divides m ) by A15, A7, NAT_D:4; :: thesis: verum

end;

end;

end;

suppose l = (4 * u) + 2 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

then l = 2 * ((2 * u) + 1) ;
then A16: 2 divides l ;
m = (2 * ((2 * k) + 1)) + 1 by A4;
hence ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m ) by A16, A5; :: thesis: verum

end;

suppose l = (4 * u) + 3 ; :: thesis: ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m )

hence ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides m ) by A5; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
then consider p, q being Nat such that
A17: ( p = (4 * q) + 3 & p is prime & p divides n ) by B1;
take p ; :: thesis: ex q being Nat st
( p = (4 * q) + 3 & p is prime & p divides n )
take q ; :: thesis: ( p = (4 * q) + 3 & p is prime & p divides n )
thus ( p = (4 * q) + 3 & p is prime & p divides n ) by A17; :: thesis: verum