let n be Nat; ( n > 1 implies Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !)) )
assume A1:
n > 1
; Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !))
then A2:
2 * 1 <= 2 * n
by XREAL_1:64;
A3:
(n -' 1) + 1 = n
by A1, XREAL_1:235;
A4:
n -' 1 <= (2 * n) -' 2
by A1, Th2;
((2 * n) -' 2) - (n -' 1) =
((2 * n) -' 2) - (n - 1)
by A1, XREAL_1:233
.=
((2 * n) - 2) - (n - 1)
by A2, XREAL_1:233
.=
n -' 1
by A1, XREAL_1:233
;
then
((2 * n) -' 2) choose (n -' 1) = (((2 * n) -' 2) !) / (((n -' 1) !) * ((n -' 1) !))
by A4, NEWTON:def 3;
then Catalan n =
(((2 * n) -' 2) !) / ((((n -' 1) !) * ((n -' 1) !)) * n)
by XCMPLX_1:78
.=
(((2 * n) -' 2) !) / (((n -' 1) !) * (((n -' 1) !) * n))
.=
(((2 * n) -' 2) !) / (((n -' 1) !) * (n !))
by A3, NEWTON:15
;
hence
Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !))
; verum