let l be Nat; :: thesis: ( l >= 2 implies ex p being Element of NAT st
( p is prime & p divides l ) )
defpred S1[ 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
S1[n] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( k >= 2 & ( for n being Nat st n >= 2 & n < k holds
S1[n] ) implies S1[k] )
assume A2: k >= 2 ; :: thesis: ( ex n being Nat st
( n >= 2 & n < k & not S1[n] ) or S1[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: S1[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 ) )
proof
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;
hence S1[k] ; :: thesis: verum
end;
A10: for k being Nat st k >= 2 holds
S1[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