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: 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
A2: 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
A3: n ! <= k and
A4: k < (n + 1) ! and
for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n by A2;
A5: k + 1 <= (n + 1) ! by A4, INT_1:7;

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

suppose A6: 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:6;
hence n ! <= k + 1 by A3, 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 A6; :: 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
A7: m ! <= k + 1 and
A8: k + 1 < (m + 1) ! ; :: thesis: m = n

now :: thesis: not m <> n

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

proof

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

suppose m > n ; :: thesis: contradiction

then m >= n + 1 by NAT_1:13;
then m ! >= (n + 1) ! by Lm51;
hence contradiction by A6, A7, XXREAL_0:2; :: thesis: verum

end;

suppose m < n ; :: thesis: contradiction

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

end;

end;

end;

end;

hence m = n ; :: thesis: verum

end;

suppose A11: 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 A11; :: thesis: ( k + 1 < (N + 1) ! & ( for m being Element of NAT st m ! <= k + 1 & k + 1 < (m + 1) ! holds
m = N ) )
A12: N ! > 0 by NEWTON:17;
N + 1 > 0 + 1 by XREAL_1:6;
then (N + 1) * (N !) > 1 * (N !) by A12, XREAL_1:68;
hence k + 1 < (N + 1) ! by A11, NEWTON:15; :: 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
A13: m ! <= k + 1 and
A14: k + 1 < (m + 1) ! ; :: thesis: m = N

now :: thesis: not m <> N

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

proof

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

suppose m > N ; :: thesis: contradiction

then m >= N + 1 by NAT_1:13;
then m ! >= (N + 1) ! by Lm51;
then A16: k + 1 >= (N + 1) ! by A13, XXREAL_0:2;
n + 2 >= 0 + 2 by XREAL_1:6;
then A17: N + 1 > 1 by XXREAL_0:2;
N ! > 0 by NEWTON:17;
then (N + 1) * (N !) > 1 * (N !) by A17, XREAL_1:68;
hence contradiction by A11, A16, NEWTON:15; :: thesis: verum

end;

suppose m < N ; :: thesis: contradiction

then m + 1 <= N by NAT_1:13;
hence contradiction by A11, A14, Lm51; :: thesis: verum

end;

end;

end;

end;

hence m = N ; :: thesis: verum

end;

end;

end;

A18: 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:13, NEWTON:14; :: 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 that
A19: m ! <= 1 and
A20: 1 < (m + 1) ! ; :: thesis: m = 1

A21: now :: thesis: not m > 1

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

end;

m <> 0 by A20, NEWTON:13;
then m >= 0 + 1 by NAT_1:13;
hence m = 1 by A21, XXREAL_0:1; :: thesis: verum

end;

for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(A18, A1);
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