let n be Nat; ( n > 1 implies Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) )
assume A1:
n > 1
; Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))
then A2:
n -' 1 <= (2 * n) -' 3
by Th1;
A3:
2 * 1 <= 2 * n
by A1, XREAL_1:64;
then A4:
(2 * n) -' 2 = (2 * n) - 2
by XREAL_1:233;
A5:
1 + 1 <= n
by A1, NAT_1:13;
then A6:
2 * 2 <= 2 * n
by XREAL_1:64;
then
(2 * n) -' 3 = (2 * n) - 3
by XREAL_1:233, XXREAL_0:2;
then A7: ((2 * n) -' 3) + 1 =
(2 * n) - 2
.=
(2 * n) -' 2
by A3, XREAL_1:233
;
((2 * n) -' 3) - (n -' 1) =
((2 * n) -' 3) - (n - 1)
by A1, XREAL_1:233
.=
((2 * n) - 3) - (n - 1)
by A6, XREAL_1:233, XXREAL_0:2
.=
n - 2
.=
n -' 2
by A5, XREAL_1:233
;
then
((2 * n) -' 3) choose (n -' 1) = (((2 * n) -' 3) !) / (((n -' 1) !) * ((n -' 2) !))
by A2, NEWTON:def 3;
then A8:
4 * (((2 * n) -' 3) choose (n -' 1)) = (4 * (((2 * n) -' 3) !)) / (((n -' 1) !) * ((n -' 2) !))
by XCMPLX_1:74;
A9:
(n -' 2) + 1 = n -' 1
by A1, Th4;
A10:
n -' 1 = n - 1
by A1, XREAL_1:233;
then A11:
(n -' 1) + 1 = n
;
A12:
1 * n < 2 * n
by A1, XREAL_1:68;
then A13:
(2 * n) -' 1 = (2 * n) - 1
by A1, XREAL_1:233, XXREAL_0:2;
1 < 2 * n
by A1, A12, XXREAL_0:2;
then A14:
((2 * n) -' 2) + 1 = (2 * n) -' 1
by Th4;
1 < 2 * n
by A1, A12, XXREAL_0:2;
then A15:
n -' 1 < (2 * n) -' 1
by A12, NAT_D:57;
((2 * n) -' 1) - (n -' 1) =
((2 * n) -' 1) - (n - 1)
by A1, XREAL_1:233
.=
(((2 * n) -' 1) - n) + 1
.=
(((2 * n) - 1) - n) + 1
by A1, A12, XREAL_1:233, XXREAL_0:2
.=
n
;
then
((2 * n) -' 1) choose (n -' 1) = (((2 * n) -' 1) !) / (((n -' 1) !) * (n !))
by A15, NEWTON:def 3;
then A16:
((2 * n) -' 1) choose (n -' 1) = ((((2 * n) -' 2) !) * ((2 * n) -' 1)) / (((n -' 1) !) * (n !))
by A14, NEWTON:15;
n - 1 > 0
by A1, XREAL_1:50;
then 4 * (((2 * n) -' 3) choose (n -' 1)) =
((n * (n - 1)) * (4 * (((2 * n) -' 3) !))) / ((n * (n - 1)) * (((n -' 1) !) * ((n -' 2) !)))
by A1, A8, XCMPLX_1:6, XCMPLX_1:91
.=
(((n - 1) * n) * (4 * (((2 * n) -' 3) !))) / (((n - 1) * (n * ((n -' 1) !))) * ((n -' 2) !))
.=
(((n - 1) * n) * (4 * (((2 * n) -' 3) !))) / (((n - 1) * (n !)) * ((n -' 2) !))
by A11, NEWTON:15
.=
(((n - 1) * n) * (4 * (((2 * n) -' 3) !))) / ((n !) * ((n -' 1) * ((n -' 2) !)))
by A10
.=
((2 * n) * (((2 * n) -' 2) * (((2 * n) -' 3) !))) / ((n !) * ((n -' 1) !))
by A4, A9, NEWTON:15
.=
((2 * n) * (((2 * n) -' 2) !)) / ((n !) * ((n -' 1) !))
by A7, NEWTON:15
;
then (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) =
(((2 * n) * (((2 * n) -' 2) !)) - ((((2 * n) -' 2) !) * ((2 * n) -' 1))) / ((n !) * ((n -' 1) !))
by A16, XCMPLX_1:120
.=
Catalan n
by A1, A13, Th8
;
hence
Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))
; verum