let X be finite set ; for k being Nat
for x, y being object st x <> y holds
card (Choose (X,k,x,y)) = (card X) choose k
let k be Nat; for x, y being object st x <> y holds
card (Choose (X,k,x,y)) = (card X) choose k
let x, y be object ; ( x <> y implies card (Choose (X,k,x,y)) = (card X) choose k )
defpred S1[ Nat] means for k being Nat
for X being finite set st k + (card X) <= $1 holds
card (Choose (X,k,x,y)) = (card X) choose k;
assume A1:
x <> y
; card (Choose (X,k,x,y)) = (card X) choose k
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
let k be
Nat;
for X being finite set st k + (card X) <= n + 1 holds
card (Choose (X,k,x,y)) = (card X) choose klet X be
finite set ;
( k + (card X) <= n + 1 implies card (Choose (X,k,x,y)) = (card X) choose k )
assume A4:
k + (card X) <= n + 1
;
card (Choose (X,k,x,y)) = (card X) choose k
per cases
( k + (card X) < n + 1 or k + (card X) = n + 1 )
by A4, XXREAL_0:1;
suppose A5:
k + (card X) = n + 1
;
card (Choose (X,k,x,y)) = (card X) choose kper cases
( ( k = 0 & card X >= 0 ) or ( k > 0 & card X = 0 ) or ( k > 0 & card X > 0 ) )
;
suppose A8:
(
k > 0 &
card X > 0 )
;
card (Choose (X,k,x,y)) = (card X) choose kthen reconsider cXz =
(card X) - 1 as
Element of
NAT by NAT_1:20;
reconsider k1 =
k - 1 as
Element of
NAT by A8, NAT_1:20;
consider z being
object such that A9:
z in X
by A8, CARD_1:27, XBOOLE_0:def 1;
set Xz =
X \ {z};
z in {z}
by TARSKI:def 1;
then A10:
not
z in X \ {z}
by XBOOLE_0:def 5;
(X \ {z}) \/ {z} = X
by A9, ZFMISC_1:116;
then A11:
card (Choose (X,(k1 + 1),x,y)) = (card (Choose ((X \ {z}),(k1 + 1),x,y))) + (card (Choose ((X \ {z}),k1,x,y)))
by A1, A10, Th14;
card X = cXz + 1
;
then A12:
card (X \ {z}) = cXz
by A9, STIRL2_1:55;
cXz < cXz + 1
by NAT_1:13;
then A13:
card (X \ {z}) < card X
by A9, STIRL2_1:55;
then
k + (card (X \ {z})) < n + 1
by A5, XREAL_1:8;
then
k + (card (X \ {z})) <= n
by NAT_1:13;
then A14:
card (Choose ((X \ {z}),(k1 + 1),x,y)) = (card (X \ {z})) choose (k1 + 1)
by A3;
k1 < k1 + 1
by NAT_1:13;
then
k1 + (card (X \ {z})) < n + 1
by A5, A13, XREAL_1:8;
then
k1 + (card (X \ {z})) <= n
by NAT_1:13;
then A15:
card (Choose ((X \ {z}),k1,x,y)) = (card (X \ {z})) choose k1
by A3;
card X = cXz + 1
;
hence
card (Choose (X,k,x,y)) = (card X) choose k
by A14, A15, A11, A12, NEWTON:22;
verum end; end; end; end;
end;
A16:
S1[ 0 ]
proof
let k be
Nat;
for X being finite set st k + (card X) <= 0 holds
card (Choose (X,k,x,y)) = (card X) choose klet X be
finite set ;
( k + (card X) <= 0 implies card (Choose (X,k,x,y)) = (card X) choose k )
A17:
0 choose 0 = 1
by NEWTON:19;
assume
k + (card X) <= 0
;
card (Choose (X,k,x,y)) = (card X) choose k
then
(
k + (card X) = 0 &
card X = 0 )
;
hence
card (Choose (X,k,x,y)) = (card X) choose k
by A1, Th10, A17;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A16, A2);
then
S1[k + (card X)]
;
hence
card (Choose (X,k,x,y)) = (card X) choose k
; verum