let l be Nat; :: thesis: ( l >= 2 implies ex p being Element of NAT st

( p is prime & p divides l ) )

defpred S_{1}[ Nat] means ex p being Nat st

( p is prime & p divides $1 );

A1: for k being Nat st k >= 2 & ( for n being Nat st n >= 2 & n < k holds

S_{1}[n] ) holds

S_{1}[k]

S_{1}[k]
from NAT_1:sch 9(A1);

assume l >= 2 ; :: thesis: ex p being Element of NAT st

( p is prime & p divides l )

then consider p being Nat such that

A11: ( p is prime & p divides l ) by A10;

reconsider p = p as Element of NAT by ORDINAL1:def 12;

take p ; :: thesis: ( p is prime & p divides l )

thus ( p is prime & p divides l ) by A11; :: thesis: verum

( p is prime & p divides l ) )

defpred S

( p is prime & p divides $1 );

A1: for k being Nat st k >= 2 & ( for n being Nat st n >= 2 & n < k holds

S

S

proof

A10:
for k being Nat st k >= 2 holds
let k be Nat; :: thesis: ( k >= 2 & ( for n being Nat st n >= 2 & n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A2: k >= 2 ; :: thesis: ( ex n being Nat st

( n >= 2 & n < k & not S_{1}[n] ) or S_{1}[k] )

assume A3: for n being Nat st n >= 2 & n < k holds

ex p being Nat st

( p is prime & p divides n ) ; :: thesis: S_{1}[k]

A4: (k + 1) - 1 > (1 + 1) - 1 by A2, NAT_1:13;

( not k is prime implies ex p being Element of NAT st

( p is prime & p divides k ) )_{1}[k]
; :: thesis: verum

end;S

assume A2: k >= 2 ; :: thesis: ( ex n being Nat st

( n >= 2 & n < k & not S

assume A3: for n being Nat st n >= 2 & n < k holds

ex p being Nat st

( p is prime & p divides n ) ; :: thesis: S

A4: (k + 1) - 1 > (1 + 1) - 1 by A2, NAT_1:13;

( not k is prime implies ex p being Element of NAT st

( p is prime & p divides k ) )

proof

hence
S
assume
not k is prime
; :: thesis: ex p being Element of NAT st

( p is prime & p divides k )

then consider m being Nat such that

A5: m divides k and

A6: m <> 1 and

A7: m <> k by A4;

m <> 0 by A5, A7;

then m > 0 ;

then m >= 0 + 1 by NAT_1:13;

then m > 1 by A6, XXREAL_0:1;

then A8: m >= 1 + 1 by NAT_1:13;

k > 0 by A2;

then m <= k by A5, Th27;

then m < k by A7, XXREAL_0:1;

then consider p1 being Nat such that

A9: ( p1 is prime & p1 divides m ) by A3, A8;

reconsider p1 = p1 as Element of NAT by ORDINAL1:def 12;

take p1 ; :: thesis: ( p1 is prime & p1 divides k )

thus ( p1 is prime & p1 divides k ) by A5, A9, Lm2; :: thesis: verum

end;( p is prime & p divides k )

then consider m being Nat such that

A5: m divides k and

A6: m <> 1 and

A7: m <> k by A4;

m <> 0 by A5, A7;

then m > 0 ;

then m >= 0 + 1 by NAT_1:13;

then m > 1 by A6, XXREAL_0:1;

then A8: m >= 1 + 1 by NAT_1:13;

k > 0 by A2;

then m <= k by A5, Th27;

then m < k by A7, XXREAL_0:1;

then consider p1 being Nat such that

A9: ( p1 is prime & p1 divides m ) by A3, A8;

reconsider p1 = p1 as Element of NAT by ORDINAL1:def 12;

take p1 ; :: thesis: ( p1 is prime & p1 divides k )

thus ( p1 is prime & p1 divides k ) by A5, A9, Lm2; :: thesis: verum

S

assume l >= 2 ; :: thesis: ex p being Element of NAT st

( p is prime & p divides l )

then consider p being Nat such that

A11: ( p is prime & p divides l ) by A10;

reconsider p = p as Element of NAT by ORDINAL1:def 12;

take p ; :: thesis: ( p is prime & p divides l )

thus ( p is prime & p divides l ) by A11; :: thesis: verum