defpred S₁[ Nat] means for p being Prime st $1 < p holds
not p divides $1 ! ;
let p be Prime; :: thesis: for n being Nat st n < p holds
not p divides n !
let n be Nat; :: thesis: ( n < p implies not p divides n ! )
assume A1: n < p ; :: thesis: not p divides n !
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
for p being Prime st n + 1 < p holds
not p divides (n + 1) !

proof

let p be Prime; :: thesis: ( n + 1 < p implies not p divides (n + 1) ! )
assume A4: n + 1 < p ; :: thesis: not p divides (n + 1) !
assume p divides (n + 1) ! ; :: thesis: contradiction
then A5: p divides (n !) * (n + 1) by NEWTON:15;
n + 0 < n + 1 by XREAL_1:6;
then n < p by A4, XXREAL_0:2;
then not p divides n ! by A3;
then p divides n + 1 by A5, NEWTON:80;
hence contradiction by A4, NAT_D:7; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ] by NAT_D:7, NEWTON:12, INT_2:def 4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A2);
hence not p divides n ! by A1; :: thesis: verum