defpred S₁[ Nat] means ex n being Element of NAT st
( n ! <= $1 & $1 < (n + 1) ! & ( for m being Element of NAT st m ! <= $1 & $1 < (m + 1) ! holds
m = n ) );
A1: S₁[1]

proof

take 1 ; :: thesis: ( 1 ! <= 1 & 1 < (1 + 1) ! & ( for m being Element of NAT st m ! <= 1 & 1 < (m + 1) ! holds
m = 1 ) )
thus ( 1 ! <= 1 & 1 < (1 + 1) ! ) by NEWTON:19, NEWTON:20; :: thesis: for m being Element of NAT st m ! <= 1 & 1 < (m + 1) ! holds
m = 1
let m be Element of NAT ; :: thesis: ( m ! <= 1 & 1 < (m + 1) ! implies m = 1 )
assume A2: ( m ! <= 1 & 1 < (m + 1) ! ) ; :: thesis: m = 1

A3: now

assume m > 1 ; :: thesis: contradiction
then m >= 1 + 1 by NAT_1:13;
hence contradiction by A2, Lm58; :: thesis: verum

end;

m <> 0 by A2, NEWTON:19;
then m > 0 ;
then m >= 0 + 1 by NAT_1:13;
hence m = 1 by A3, XXREAL_0:1; :: thesis: verum

end;

A4: for k being Nat st k >= 1 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume that
k >= 1 and
A5: ex n being Element of NAT st
( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n ) ) ; :: thesis: S₁[k + 1]
consider n being Element of NAT such that
A6: ( n ! <= k & k < (n + 1) ! ) and
for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n by A5;
A7: k + 1 <= (n + 1) ! by A6, INT_1:20;

per cases ( k + 1 < (n + 1) ! or k + 1 = (n + 1) ! ) by A7, XXREAL_0:1;

suppose A8: k + 1 < (n + 1) ! ; :: thesis: S₁[k + 1]

take n ; :: thesis: ( n ! <= k + 1 & k + 1 < (n + 1) ! & ( for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = n ) )
k + 0 <= k + 1 by XREAL_1:8;
hence n ! <= k + 1 by A6, XXREAL_0:2; :: thesis: ( k + 1 < (n + 1) ! & ( for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = n ) )
thus k + 1 < (n + 1) ! by A8; :: thesis: for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = n
let m be Element of NAT ; :: thesis: ( m ! <= k + 1 & k + 1 < (m + 1) ! implies m = n )
assume that
A9: m ! <= k + 1 and
A10: k + 1 < (m + 1) ! ; :: thesis: m = n

now

assume A11: m <> n ; :: thesis: contradiction
thus contradiction :: thesis: verum

proof

per cases ( m > n or m < n ) by A11, XXREAL_0:1;

suppose m > n ; :: thesis: contradiction

then m >= n + 1 by NAT_1:13;
then m ! >= (n + 1) ! by Lm59;
hence contradiction by A8, A9, XXREAL_0:2; :: thesis: verum

end;

suppose m < n ; :: thesis: contradiction

then m + 1 <= n by NAT_1:13;
then (m + 1) ! <= n ! by Lm59;
then A12: (m + 1) ! <= k by A6, XXREAL_0:2;
k <= k + 1 by NAT_1:11;
hence contradiction by A10, A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

hence m = n ; :: thesis: verum

end;

suppose A13: k + 1 = (n + 1) ! ; :: thesis: S₁[k + 1]

take N = n + 1; :: thesis: ( N ! <= k + 1 & k + 1 < (N + 1) ! & ( for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = N ) )
thus N ! <= k + 1 by A13; :: thesis: ( k + 1 < (N + 1) ! & ( for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = N ) )
A14: N + 1 > 0 + 1 by XREAL_1:8;
N ! > 0 by NEWTON:23;
then (N + 1) * (N ! ) > 1 * (N ! ) by A14, XREAL_1:70;
hence k + 1 < (N + 1) ! by A13, NEWTON:21; :: thesis: for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = N
let m be Element of NAT ; :: thesis: ( m ! <= k + 1 & k + 1 < (m + 1) ! implies m = N )
assume that
A15: m ! <= k + 1 and
A16: k + 1 < (m + 1) ! ; :: thesis: m = N

now

assume A17: m <> N ; :: thesis: contradiction
thus contradiction :: thesis: verum

proof

per cases ( m > N or m < N ) by A17, XXREAL_0:1;

suppose m > N ; :: thesis: contradiction

then m >= N + 1 by NAT_1:13;
then m ! >= (N + 1) ! by Lm59;
then A18: k + 1 >= (N + 1) ! by A15, XXREAL_0:2;
n + 2 >= 0 + 2 by XREAL_1:8;
then A19: N + 1 > 1 by XXREAL_0:2;
N ! > 0 by NEWTON:23;
then (N + 1) * (N ! ) > 1 * (N ! ) by A19, XREAL_1:70;
hence contradiction by A13, A18, NEWTON:21; :: thesis: verum

end;

suppose m < N ; :: thesis: contradiction

then m + 1 <= N by NAT_1:13;
hence contradiction by A13, A16, Lm59; :: thesis: verum

end;

end;

end;

end;

hence m = N ; :: thesis: verum

end;

end;

end;

for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(A1, A4);
hence for k being Element of NAT st k >= 1 holds
ex n being Element of NAT st
( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n ) ) ; :: thesis: verum