let n be natural number ; ( 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:66;
then A4:
(2 * n) -' 2 = (2 * n) - 2
by XREAL_1:235;
A5:
1 + 1 <= n
by A1, NAT_1:13;
then A6:
2 * 2 <= 2 * n
by XREAL_1:66;
then
(2 * n) -' 3 = (2 * n) - 3
by XREAL_1:235, XXREAL_0:2;
then A7: ((2 * n) -' 3) + 1 =
(2 * n) - 2
.=
(2 * n) -' 2
by A3, XREAL_1:235
;
((2 * n) -' 3) - (n -' 1) =
((2 * n) -' 3) - (n - 1)
by A1, XREAL_1:235
.=
((2 * n) - 3) - (n - 1)
by A6, XREAL_1:235, XXREAL_0:2
.=
n - 2
.=
n -' 2
by A5, XREAL_1:235
;
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:75;
A9:
(n -' 2) + 1 = n -' 1
by A1, Th4;
A10:
n -' 1 = n - 1
by A1, XREAL_1:235;
then A11:
(n -' 1) + 1 = n
;
A12:
1 * n < 2 * n
by A1, XREAL_1:70;
then A13:
(2 * n) -' 1 = (2 * n) - 1
by A1, XREAL_1:235, 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:235
.=
(((2 * n) -' 1) - n) + 1
.=
(((2 * n) - 1) - n) + 1
by A1, A12, XREAL_1:235, 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:21;
n - 1 > 0
by A1, XREAL_1:52;
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:92
.=
(((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:21
.=
(((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:21
.=
((2 * n) * (((2 * n) -' 2) ! )) / ((n ! ) * ((n -' 1) ! ))
by A7, NEWTON:21
;
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:121
.=
Catalan n
by A1, A13, Th8
;
hence
Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1))
; verum