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

proof

let n be Element of 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:21;
n + 0 < n + 1 by XREAL_1:8;
then n < p by A4, XXREAL_0:2;
then not p divides n ! by A3;
then p divides n + 1 by A5, NEWTON:98;
hence contradiction by A4, NAT_D:7; :: thesis: verum

end;

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

end;

A6: S₁[ 0 ]

proof

let p be Prime; :: thesis: ( 0 < p implies not p divides 0 ! )
assume 0 < p ; :: thesis: not p divides 0 !
assume p divides 0 ! ; :: thesis: contradiction
then p <= 1 by NAT_D:7, NEWTON:18;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A2);
hence not p divides n ! by A1; :: thesis: verum