:: CARDFIN2 semantic presentation
begin
registration
let c be real number ;
cluster exp_R c -> positive ;
coherence
exp_R c is positive by SIN_COS:55;
end;
registration
cluster number_e -> positive ;
coherence
number_e is positive by TAYLOR_1:11;
end;
theorem Th1: :: CARDFIN2:1
id {} is without_fixpoints
proof
assume id {} is with_fixpoint ; ::_thesis: contradiction
then consider y being set such that
A1: y is_a_fixpoint_of id {} by ABIAN:def_5;
y in dom (id {}) by A1, ABIAN:def_3;
hence contradiction ; ::_thesis: verum
end;
theorem Th2: :: CARDFIN2:2
for c being real number st c < 0 holds
exp_R c < 1
proof
let c be real number ; ::_thesis: ( c < 0 implies exp_R c < 1 )
assume c < 0 ; ::_thesis: exp_R c < 1
then ( exp_R c <= 1 & exp_R c <> 1 ) by SIN_COS:53, SIN_COS7:29;
hence exp_R c < 1 by XXREAL_0:1; ::_thesis: verum
end;
begin
definition
let n be real number ;
func round n -> Integer equals :: CARDFIN2:def 1
[\(n + (1 / 2))/];
coherence
[\(n + (1 / 2))/] is Integer ;
end;
:: deftheorem defines round CARDFIN2:def_1_:_
for n being real number holds round n = [\(n + (1 / 2))/];
theorem :: CARDFIN2:3
for a being Integer holds round a = a
proof
let a be Integer; ::_thesis: round a = a
a - (1 / 2) < a - 0 by XREAL_1:6;
then ( a + 0 <= a + (1 / 2) & (a + (1 / 2)) - 1 < a - 0 ) by XREAL_1:6;
hence round a = a by INT_1:def_6; ::_thesis: verum
end;
theorem Th4: :: CARDFIN2:4
for a being Integer
for b being real number st |.(a - b).| < 1 / 2 holds
a = round b
proof
let a be Integer; ::_thesis: for b being real number st |.(a - b).| < 1 / 2 holds
a = round b
let b be real number ; ::_thesis: ( |.(a - b).| < 1 / 2 implies a = round b )
assume A1: |.(a - b).| < 1 / 2 ; ::_thesis: a = round b
then a - b < 1 / 2 by SEQ_2:1;
then A2: (a - b) + b < (1 / 2) + b by XREAL_1:8;
- (1 / 2) < a - b by A1, SEQ_2:1;
then - (a - b) < - (- (1 / 2)) by XREAL_1:24;
then (b - a) + a < (1 / 2) + a by XREAL_1:8;
then b - (1 / 2) < (a + (1 / 2)) - (1 / 2) by XREAL_1:14;
then (b + (1 / 2)) - 1 < a ;
hence a = round b by A2, INT_1:def_6; ::_thesis: verum
end;
begin
theorem Th5: :: CARDFIN2:5
for n being Nat
for a, b being real number st a < b holds
ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
proof
let n be Nat; ::_thesis: for a, b being real number st a < b holds
ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
let a, b be real number ; ::_thesis: ( a < b implies ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) )
assume A1: a < b ; ::_thesis: ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
set f = exp_R ;
set Z = [#] REAL;
A2: n in NAT by ORDINAL1:def_12;
then A3: exp_R is_differentiable_on n, [#] REAL by TAYLOR_2:10;
(diff (exp_R,([#] REAL))) . n = exp_R | ([#] REAL) by A2, TAYLOR_2:6;
then A4: ((diff (exp_R,([#] REAL))) . n) | [.a,b.] is continuous ;
A5: exp_R is_differentiable_on n + 1,].a,b.[ by TAYLOR_2:10;
( a in REAL & b in REAL ) by XREAL_0:def_1;
then consider c being Real such that
A6: c in ].a,b.[ and
A7: exp_R . a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((((diff (exp_R,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) by A1, A3, A4, A5, A2, SIN_COS:47, TAYLOR_1:29;
take c ; ::_thesis: ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
thus ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) by A7, A6, TAYLOR_2:7; ::_thesis: verum
end;
theorem Th6: :: CARDFIN2:6
for n being positive Nat
for c being real number st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
proof
let n be positive Nat; ::_thesis: for c being real number st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
let c be real number ; ::_thesis: ( c < 0 implies |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 )
n >= 0 + 1 by NAT_1:13;
then n + 1 >= 1 + 1 by XREAL_1:6;
then A1: (exp_R c) / (n + 1) <= (exp_R c) / 2 by XREAL_1:118;
assume c < 0 ; ::_thesis: |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
then (exp_R c) / 2 < 1 / 2 by Th2, XREAL_1:74;
then A2: (exp_R c) / (n + 1) < 1 / 2 by A1, XXREAL_0:2;
A3: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2
proof
percases ( n is even or n is odd ) ;
supposeA4: n is even ; ::_thesis: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2
A5: (- 1) |^ n = (- 1) to_power n
.= 1 to_power n by A4, POWER:47
.= 1 by NEWTON:10 ;
- (1 / 2) < (exp_R c) / (n + 1) ;
hence |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A5, A2, SEQ_2:1; ::_thesis: verum
end;
supposeA6: n is odd ; ::_thesis: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2
A7: (- 1) |^ n = (- 1) to_power n
.= - 1 by A6, FIB_NUM2:2 ;
- (1 / 2) < - ((exp_R c) / (n + 1)) by A2, XREAL_1:24;
hence |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A7, SEQ_2:1; ::_thesis: verum
end;
end;
end;
((exp_R c) * ((- 1) |^ n)) / (n + 1) = ((exp_R c) * ((- 1) * (((- 1) |^ n) * (- 1)))) / (n + 1)
.= ((exp_R c) * ((- 1) * ((- 1) |^ (n + 1)))) / (n + 1) by NEWTON:6
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * (1 / (n + 1)))
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * (((n !) / (n !)) / (n + 1))) by XCMPLX_1:60
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * ((n !) / ((n !) * (n + 1)))) by XCMPLX_1:78
.= - ((((exp_R c) * ((- 1) |^ (n + 1))) * (n !)) / ((n + 1) * (n !)))
.= - ((((n !) * (exp_R c)) * ((- 1) |^ (n + 1))) / ((n + 1) !)) by NEWTON:15 ;
hence |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 by A3; ::_thesis: verum
end;
definition
let s be set ;
func derangements s -> set equals :: CARDFIN2:def 2
{ f where f is Permutation of s : f is without_fixpoints } ;
coherence
{ f where f is Permutation of s : f is without_fixpoints } is set ;
end;
:: deftheorem defines derangements CARDFIN2:def_2_:_
for s being set holds derangements s = { f where f is Permutation of s : f is without_fixpoints } ;
registration
let s be finite set ;
cluster derangements s -> finite ;
coherence
derangements s is finite
proof
A1: card { F where F is Function of s,s : F is Permutation of s } = (card s) ! by CARD_FIN:8;
derangements s c= { F where F is Function of s,s : F is Permutation of s }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in derangements s or x in { F where F is Function of s,s : F is Permutation of s } )
assume x in derangements s ; ::_thesis: x in { F where F is Function of s,s : F is Permutation of s }
then ex f being Permutation of s st
( x = f & f is without_fixpoints ) ;
hence x in { F where F is Function of s,s : F is Permutation of s } ; ::_thesis: verum
end;
then card (derangements s) c= (card s) ! by A1, CARD_1:11;
hence derangements s is finite ; ::_thesis: verum
end;
end;
theorem Th7: :: CARDFIN2:7
for s being finite set holds derangements s = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) }
proof
let s be finite set ; ::_thesis: derangements s = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) }
set xx = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } ;
hereby :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis: { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } c= derangements s
let x be set ; ::_thesis: ( x in derangements s implies x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } )
assume x in derangements s ; ::_thesis: x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) }
then consider f being Permutation of s such that
A1: ( x = f & f is without_fixpoints ) ;
now__::_thesis:_for_y_being_set_st_y_in_s_holds_
f_._y_<>_y
let y be set ; ::_thesis: ( y in s implies f . y <> y )
not y is_a_fixpoint_of f by A1, ABIAN:def_5;
hence ( y in s implies f . y <> y ) by ABIAN:def_4; ::_thesis: verum
end;
hence x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } or x in derangements s )
assume x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } ; ::_thesis: x in derangements s
then consider h being Function of s,s such that
A2: ( x = h & h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) ;
card s = card s ;
then A3: h is onto by A2, STIRL2_1:60;
now__::_thesis:_for_y_being_set_holds_not_y_is_a_fixpoint_of_h
let y be set ; ::_thesis: not y is_a_fixpoint_of h
assume y is_a_fixpoint_of h ; ::_thesis: contradiction
then ( y in dom h & h . y = y ) by ABIAN:def_3;
hence contradiction by A2; ::_thesis: verum
end;
then h is without_fixpoints by ABIAN:def_5;
hence x in derangements s by A3, A2; ::_thesis: verum
end;
theorem Th8: :: CARDFIN2:8
for s being non empty finite set ex c being real number st
( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
proof
let s be non empty finite set ; ::_thesis: ex c being real number st
( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
set n = card s;
consider XF being XFinSequence of such that
A1: Sum XF = card { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } and
A2: dom XF = (card s) + 1 and
A3: for m being Nat st m in dom XF holds
XF . m = (((- 1) |^ m) * ((card s) !)) / (m !) by CARD_FIN:63;
A4: Sum XF = card (derangements s) by A1, Th7;
set T = Taylor (exp_R,([#] REAL),0,(- 1));
consider c being real number such that
A5: ( c in ].(- 1),0.[ & exp_R (- 1) = ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card s)) + (((exp_R c) * (((- 1) - 0) |^ ((card s) + 1))) / (((card s) + 1) !)) ) by Th5;
Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) = ((card s) !) (#) (Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) by SERIES_1:9;
then A6: (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = ((card s) !) * ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card s)) by SEQ_1:9;
(Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = Sum XF
proof
consider f being Function of NAT,INT such that
A7: f . 0 = XF . 0 and
A8: for n being Nat st n + 1 < len XF holds
f . (n + 1) = addint . ((f . n),(XF . (n + 1))) and
A9: addint "**" XF = f . ((len XF) - 1) by A2, AFINSQ_2:def_8;
A10: Sum XF = f . ((len XF) - 1) by A9, AFINSQ_2:50;
defpred S1[ Element of NAT ] means ( $1 in (card s) + 1 implies (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . $1 = f . $1 );
A11: S1[ 0 ]
proof
A12: 0 in dom XF by A2, NAT_1:44;
(Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . 0 = (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . 0 by SERIES_1:def_1
.= ((card s) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . 0) by SEQ_1:9
.= ((card s) !) * (((((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0)) / (0 !)) by TAYLOR_1:def_7
.= ((card s) !) * ((1 * ((- 1) |^ 0)) / (0 !)) by SIN_COS2:13, TAYLOR_2:7
.= (((card s) !) * ((- 1) |^ 0)) / (0 !)
.= f . 0 by A3, A12, A7 ;
hence S1[ 0 ] ; ::_thesis: verum
end;
A13: for j being Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A14: S1[j] ; ::_thesis: S1[j + 1]
set j1 = j + 1;
assume A15: j + 1 in (card s) + 1 ; ::_thesis: (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (j + 1) = f . (j + 1)
then A16: j + 1 < (card s) + 1 by NAT_1:44;
then A17: j < (card s) + 1 by NAT_1:13;
(((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . (j + 1) = ((card s) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . (j + 1)) by SEQ_1:9
.= ((card s) !) * (((((diff (exp_R,([#] REAL))) . (j + 1)) . 0) * (((- 1) - 0) |^ (j + 1))) / ((j + 1) !)) by TAYLOR_1:def_7
.= ((card s) !) * ((1 * ((- 1) |^ (j + 1))) / ((j + 1) !)) by SIN_COS2:13, TAYLOR_2:7
.= (((card s) !) * ((- 1) |^ (j + 1))) / ((j + 1) !)
.= XF . (j + 1) by A3, A15, A2 ;
hence (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (j + 1) = (f . j) + (XF . (j + 1)) by A14, A17, NAT_1:44, SERIES_1:def_1
.= addint . ((f . j),(XF . (j + 1))) by BINOP_2:def_20
.= f . (j + 1) by A8, A16, A2 ;
::_thesis: verum
end;
for j being Element of NAT holds S1[j] from NAT_1:sch_1(A11, A13);
hence (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = Sum XF by A10, A2, NAT_1:45; ::_thesis: verum
end;
then A18: (card (derangements s)) + (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) = ((card s) !) * (exp_R (- 1)) by A4, A5, A6
.= ((card s) !) * (1 / (exp_R 1)) by TAYLOR_1:4
.= ((card s) !) / number_e by IRRAT_1:def_7 ;
take c ; ::_thesis: ( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
thus c in ].(- 1),0.[ by A5; ::_thesis: (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !)))
thus (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) by A18; ::_thesis: verum
end;
theorem Th9: :: CARDFIN2:9
for s being non empty finite set holds |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2
proof
let s be non empty finite set ; ::_thesis: |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2
set n = card s;
consider c being real number such that
A1: c in ].(- 1),0.[ and
A2: (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) by Th8;
c < 0 by A1, XXREAL_1:4;
hence |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by A2, Th6; ::_thesis: verum
end;
theorem Th10: :: CARDFIN2:10
for s being non empty finite set holds card (derangements s) = round (((card s) !) / number_e)
proof
let s be non empty finite set ; ::_thesis: card (derangements s) = round (((card s) !) / number_e)
|.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by Th9;
hence card (derangements s) = round (((card s) !) / number_e) by Th4; ::_thesis: verum
end;
theorem Th11: :: CARDFIN2:11
derangements {} = {{}}
proof
hereby :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis: {{}} c= derangements {}
let x be set ; ::_thesis: ( x in derangements {} implies x in {{}} )
assume x in derangements {} ; ::_thesis: x in {{}}
then ex f being Permutation of {} st
( x = f & f is without_fixpoints ) ;
hence x in {{}} by ALTCAT_1:2, FUNCT_2:9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in derangements {} )
assume x in {{}} ; ::_thesis: x in derangements {}
then A1: x = {} by TARSKI:def_1;
rng (id {}) = {} ;
then id {} is Permutation of {} by FUNCT_2:57;
hence x in derangements {} by A1, Th1; ::_thesis: verum
end;
theorem Th12: :: CARDFIN2:12
for x being set holds derangements {x} = {}
proof
let x be set ; ::_thesis: derangements {x} = {}
A1: card {x} = 1 by CARD_1:30;
1 / number_e < 1 / 2 by TAYLOR_1:11, XREAL_1:76;
then - (1 / 2) < - (1 / number_e) by XREAL_1:24;
then |.(0 - (1 / number_e)).| < 1 / 2 by SEQ_2:1;
then round (1 / number_e) = 0 by Th4;
then card (derangements {x}) = 0 by Th10, A1, NEWTON:13;
hence derangements {x} = {} ; ::_thesis: verum
end;
reconsider j = 1, z = 0 as Element of INT by INT_1:def_2;
deffunc H1( Element of NAT , Integer, Integer) -> Element of INT = ($1 + 1) * ($2 + $3);
definition
func der_seq -> sequence of INT means :Def3: :: CARDFIN2:def 3
( it . 0 = 1 & it . 1 = 0 & ( for n being Nat holds it . (n + 2) = (n + 1) * ((it . n) + (it . (n + 1))) ) );
existence
ex b1 being sequence of INT st
( b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) )
proof
consider f being Function of NAT,INT such that
A1: ( f . 0 = j & f . 1 = z & ( for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) ) ) from RECDEF_2:sch_5();
take f ; ::_thesis: ( f . 0 = 1 & f . 1 = 0 & ( for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) )
thus ( f . 0 = 1 & f . 1 = 0 ) by A1; ::_thesis: for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
let n be Nat; ::_thesis: f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
n is Element of NAT by ORDINAL1:def_12;
hence f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of INT st b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) & b2 . 0 = 1 & b2 . 1 = 0 & ( for n being Nat holds b2 . (n + 2) = (n + 1) * ((b2 . n) + (b2 . (n + 1))) ) holds
b1 = b2
proof
let f, g be sequence of INT; ::_thesis: ( f . 0 = 1 & f . 1 = 0 & ( for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) & g . 0 = 1 & g . 1 = 0 & ( for n being Nat holds g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) ) implies f = g )
assume ( f . 0 = 1 & f . 1 = 0 ) ; ::_thesis: ( ex n being Nat st not f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) or not g . 0 = 1 or not g . 1 = 0 or ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A2: ( f . 0 = j & f . 1 = z ) ;
assume for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ; ::_thesis: ( not g . 0 = 1 or not g . 1 = 0 or ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A3: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) ;
assume ( g . 0 = 1 & g . 1 = 0 ) ; ::_thesis: ( ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A4: ( g . 0 = j & g . 1 = z ) ;
assume for n being Nat holds g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) ; ::_thesis: f = g
then A5: for n being Element of NAT holds g . (n + 2) = H1(n,g . n,g . (n + 1)) ;
thus f = g from RECDEF_2:sch_7(A2, A3, A4, A5); ::_thesis: verum
end;
end;
:: deftheorem Def3 defines der_seq CARDFIN2:def_3_:_
for b1 being sequence of INT holds
( b1 = der_seq iff ( b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) ) );
registration
let c be Integer;
let F be XFinSequence of ;
clusterc (#) F -> T-Sequence-like INT -valued finite ;
coherence
( c (#) F is finite & c (#) F is INT -valued & c (#) F is T-Sequence-like ) ;
end;
registration
let c be complex number ;
let F be empty Function;
clusterc (#) F -> empty ;
coherence
c (#) F is empty ;
end;
theorem :: CARDFIN2:13
for F being XFinSequence of
for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
proof
let F be XFinSequence of ; ::_thesis: for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
let c be Integer; ::_thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
percases ( len F = 0 or len F > 0 ) ;
suppose len F = 0 ; ::_thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
then A1: ( F is empty & F . ((len F) -' 1) = 0 ) by FUNCT_1:def_2;
then Sum F = 0 ;
hence c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A1; ::_thesis: verum
end;
suppose len F > 0 ; ::_thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
then A2: ((len F) -' 1) + 1 = len F by NAT_1:14, XREAL_1:235;
A3: dom F = dom (c (#) F) by VALUED_1:def_5;
A4: c * (Sum F) = Sum (c (#) F) by AFINSQ_2:64;
A5: Sum (c (#) F) = Sum ((c (#) F) | (len F)) by A3, RELAT_1:69;
Sum ((c (#) F) | (((len F) -' 1) + 1)) = (Sum ((c (#) F) | ((len F) -' 1))) + ((c (#) F) . ((len F) -' 1)) by A3, A2, AFINSQ_2:65, NAT_1:45;
hence c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A4, A5, A2, VALUED_1:6; ::_thesis: verum
end;
end;
end;
theorem Th14: :: CARDFIN2:14
for X, N being XFinSequence of st len N = (len X) + 1 holds
for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X))
proof
let X, N be XFinSequence of ; ::_thesis: ( len N = (len X) + 1 implies for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X)) )
assume A1: len N = (len X) + 1 ; ::_thesis: for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X))
let c be Integer; ::_thesis: ( N | (len X) = c (#) X implies Sum N = (c * (Sum X)) + (N . (len X)) )
assume A2: N | (len X) = c (#) X ; ::_thesis: Sum N = (c * (Sum X)) + (N . (len X))
thus Sum N = Sum (N | (len N)) by RELAT_1:69
.= (Sum (N | (len X))) + (N . (len X)) by A1, AFINSQ_2:65, NAT_1:45
.= (c * (Sum X)) + (N . (len X)) by A2, AFINSQ_2:64 ; ::_thesis: verum
end;
theorem :: CARDFIN2:15
for s being finite set holds der_seq . (card s) = card (derangements s)
proof
let s be finite set ; ::_thesis: der_seq . (card s) = card (derangements s)
defpred S1[ finite set ] means for s being finite set st card s = $1 holds
der_seq . $1 = card (derangements s);
A1: S1[ 0 ]
proof
let s be finite set ; ::_thesis: ( card s = 0 implies der_seq . 0 = card (derangements s) )
assume card s = 0 ; ::_thesis: der_seq . 0 = card (derangements s)
then A2: s = {} ;
thus der_seq . 0 = 1 by Def3
.= card (derangements s) by Th11, A2, CARD_1:30 ; ::_thesis: verum
end;
A3: S1[1]
proof
let s be finite set ; ::_thesis: ( card s = 1 implies der_seq . 1 = card (derangements s) )
assume card s = 1 ; ::_thesis: der_seq . 1 = card (derangements s)
then consider x being set such that
A4: s = {x} by CARD_2:42;
thus der_seq . 1 = card {} by Def3
.= card (derangements s) by Th12, A4 ; ::_thesis: verum
end;
A5: for n being Nat st S1[n] & S1[n + 1] holds
S1[n + 2]
proof
let n be Nat; ::_thesis: ( S1[n] & S1[n + 1] implies S1[n + 2] )
assume A6: S1[n] ; ::_thesis: ( not S1[n + 1] or S1[n + 2] )
assume A7: S1[n + 1] ; ::_thesis: S1[n + 2]
set n1 = n + 1;
A8: ( card n = n & card (n + 1) = n + 1 ) by CARD_1:def_2;
then consider XFn being XFinSequence of such that
A9: Sum XFn = card { h where h is Function of n,n : ( h is one-to-one & ( for x being set st x in n holds
h . x <> x ) ) } and
A10: dom XFn = n + 1 and
A11: for m being Nat st m in dom XFn holds
XFn . m = (((- 1) |^ m) * (n !)) / (m !) by CARD_FIN:63;
consider XFn1 being XFinSequence of such that
A12: Sum XFn1 = card { h where h is Function of (n + 1),(n + 1) : ( h is one-to-one & ( for x being set st x in n + 1 holds
h . x <> x ) ) } and
A13: dom XFn1 = (n + 1) + 1 and
A14: for m being Nat st m in dom XFn1 holds
XFn1 . m = (((- 1) |^ m) * ((n + 1) !)) / (m !) by A8, CARD_FIN:63;
Sum XFn = card (derangements n) by A9, Th7;
then A15: der_seq . n = Sum XFn by A6, A8;
Sum XFn1 = card (derangements (n + 1)) by A12, Th7;
then A16: der_seq . (n + 1) = Sum XFn1 by A7, A8;
let sn2 be finite set ; ::_thesis: ( card sn2 = n + 2 implies der_seq . (n + 2) = card (derangements sn2) )
assume card sn2 = n + 2 ; ::_thesis: der_seq . (n + 2) = card (derangements sn2)
then consider XFn2 being XFinSequence of such that
A17: Sum XFn2 = card { h where h is Function of sn2,sn2 : ( h is one-to-one & ( for x being set st x in sn2 holds
h . x <> x ) ) } and
A18: dom XFn2 = (n + 2) + 1 and
A19: for m being Nat st m in dom XFn2 holds
XFn2 . m = (((- 1) |^ m) * ((n + 2) !)) / (m !) by CARD_FIN:63;
A20: Sum XFn2 = card (derangements sn2) by A17, Th7;
A21: len XFn1 = (len XFn) + 1 by A10, A13;
A22: len XFn2 = (len XFn1) + 1 by A13, A18;
n + 1 < n + 2 by XREAL_1:8;
then A23: len XFn c= dom XFn1 by A10, A13, NAT_1:39;
A24: dom ((n + 1) (#) XFn) = len XFn by VALUED_1:def_5;
A25: now__::_thesis:_for_x_being_set_st_x_in_dom_(XFn1_|_(len_XFn))_holds_
(XFn1_|_(len_XFn))_._x_=_((n_+_1)_(#)_XFn)_._x
let x be set ; ::_thesis: ( x in dom (XFn1 | (len XFn)) implies (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x )
assume A26: x in dom (XFn1 | (len XFn)) ; ::_thesis: (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x
then A27: x in dom XFn1 by RELAT_1:57;
reconsider m = x as Element of NAT by A26;
A28: m in dom XFn by A26, RELAT_1:57;
thus (XFn1 | (len XFn)) . x = XFn1 . x by A26, FUNCT_1:47
.= (((- 1) |^ m) * ((n + 1) !)) / (m !) by A27, A14
.= (((- 1) |^ m) * ((n !) * (n + 1))) / (m !) by NEWTON:15
.= (n + 1) * ((((- 1) |^ m) * (n !)) / (m !))
.= (n + 1) * (XFn . m) by A11, A28
.= ((n + 1) (#) XFn) . x by VALUED_1:6 ; ::_thesis: verum
end;
set a = (- 1) |^ (n + 1);
A29: (- 1) * ((- 1) |^ (n + 1)) = (- 1) |^ ((n + 1) + 1) by NEWTON:6;
(n + 1) + 0 < (n + 1) + 1 by XREAL_1:8;
then A30: n + 1 in dom XFn1 by A13, NAT_1:44;
(n + 2) + 0 < (n + 2) + 1 by XREAL_1:8;
then A31: n + 2 in dom XFn2 by A18, NAT_1:44;
XFn1 | (len XFn) = (n + 1) (#) XFn by A23, A24, A25, FUNCT_1:2, RELAT_1:62;
then A32: Sum XFn1 = ((n + 1) * (Sum XFn)) + (XFn1 . (len XFn)) by Th14, A21
.= ((n + 1) * (Sum XFn)) + ((((- 1) |^ (n + 1)) * ((n + 1) !)) / ((n + 1) !)) by A10, A14, A30
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * (((n + 1) !) / ((n + 1) !)))
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * 1) by XCMPLX_1:60 ;
A33: now__::_thesis:_for_x_being_set_st_x_in_dom_(XFn2_|_(len_XFn1))_holds_
(XFn2_|_(len_XFn1))_._x_=_((n_+_2)_(#)_XFn1)_._x
let x be set ; ::_thesis: ( x in dom (XFn2 | (len XFn1)) implies (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x )
assume A34: x in dom (XFn2 | (len XFn1)) ; ::_thesis: (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x
then A35: x in dom XFn2 by RELAT_1:57;
reconsider m = x as Element of NAT by A34;
A36: m in dom XFn1 by A34, RELAT_1:57;
thus (XFn2 | (len XFn1)) . x = XFn2 . x by A34, FUNCT_1:47
.= (((- 1) |^ m) * (((n + 1) + 1) !)) / (m !) by A35, A19
.= (((- 1) |^ m) * (((n + 1) !) * ((n + 1) + 1))) / (m !) by NEWTON:15
.= ((n + 1) + 1) * ((((- 1) |^ m) * ((n + 1) !)) / (m !))
.= (n + 2) * (XFn1 . m) by A14, A36
.= ((n + 2) (#) XFn1) . x by VALUED_1:6 ; ::_thesis: verum
end;
n + 2 < n + 3 by XREAL_1:8;
then len XFn1 c= dom XFn2 by A13, A18, NAT_1:39;
then A37: dom (XFn2 | (len XFn1)) = len XFn1 by RELAT_1:62;
dom ((n + 2) (#) XFn1) = len XFn1 by VALUED_1:def_5;
then Sum XFn2 = ((n + 2) * (Sum XFn1)) + (XFn2 . (len XFn1)) by Th14, A22, A37, A33, FUNCT_1:2
.= ((n + 2) * (Sum XFn1)) + ((((- 1) |^ (n + 2)) * ((n + 2) !)) / ((n + 2) !)) by A19, A31, A13
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * (((n + 2) !) / ((n + 2) !))) by A29
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * 1) by XCMPLX_1:60
.= (n + 1) * ((Sum XFn) + (Sum XFn1)) by A32 ;
hence der_seq . (n + 2) = card (derangements sn2) by A20, Def3, A15, A16; ::_thesis: verum
end;
for n being Nat holds S1[n] from FIB_NUM:sch_1(A1, A3, A5);
hence der_seq . (card s) = card (derangements s) ; ::_thesis: verum
end;
begin
definition
let s, t be set ;
func not-one-to-one (s,t) -> Subset of (Funcs (s,t)) equals :: CARDFIN2:def 4
{ f where f is Function of s,t : not f is one-to-one } ;
coherence
{ f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t))
proof
percases ( not t is empty or t is empty ) ;
supposeA1: not t is empty ; ::_thesis: { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t))
{ f where f is Function of s,t : not f is one-to-one } c= Funcs (s,t)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Function of s,t : not f is one-to-one } or x in Funcs (s,t) )
assume x in { f where f is Function of s,t : not f is one-to-one } ; ::_thesis: x in Funcs (s,t)
then ex f being Function of s,t st
( x = f & not f is one-to-one ) ;
hence x in Funcs (s,t) by A1, FUNCT_2:8; ::_thesis: verum
end;
hence { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t)) ; ::_thesis: verum
end;
supposeA2: t is empty ; ::_thesis: { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t))
{ f where f is Function of s,t : not f is one-to-one } = {}
proof
assume { f where f is Function of s,t : not f is one-to-one } <> {} ; ::_thesis: contradiction
then consider x being set such that
A3: x in { f where f is Function of s,t : not f is one-to-one } by XBOOLE_0:def_1;
ex f being Function of s,t st
( x = f & not f is one-to-one ) by A3;
hence contradiction by A2; ::_thesis: verum
end;
hence { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t)) by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem defines not-one-to-one CARDFIN2:def_4_:_
for s, t being set holds not-one-to-one (s,t) = { f where f is Function of s,t : not f is one-to-one } ;
registration
let s, t be finite set ;
cluster not-one-to-one (s,t) -> finite ;
coherence
not-one-to-one (s,t) is finite ;
end;
scheme :: CARDFIN2:sch 1
FraenkelDiff{ F1() -> set , F2() -> set , P1[ set ] } :
{ f where f is Function of F1(),F2() : P1[f] } = (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
provided
A1: ( F2() = {} implies F1() = {} )
proof
set z1 = { f where f is Function of F1(),F2() : P1[f] } ;
set z2 = { f where f is Function of F1(),F2() : P1[f] } ;
set zc = Funcs (F1(),F2());
thus { f where f is Function of F1(),F2() : P1[f] } c= (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } :: according to XBOOLE_0:def_10 ::_thesis: (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } c= { f where f is Function of F1(),F2() : P1[f] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Function of F1(),F2() : P1[f] } or x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } )
assume x in { f where f is Function of F1(),F2() : P1[f] } ; ::_thesis: x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
then consider f being Function of F1(),F2() such that
A2: ( x = f & P1[f] ) ;
A3: f in Funcs (F1(),F2()) by A1, FUNCT_2:8;
not f in { f where f is Function of F1(),F2() : P1[f] }
proof
assume f in { f where f is Function of F1(),F2() : P1[f] } ; ::_thesis: contradiction
then ex g being Function of F1(),F2() st
( f = g & P1[g] ) ;
hence contradiction by A2; ::_thesis: verum
end;
hence x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } by A3, A2, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } or x in { f where f is Function of F1(),F2() : P1[f] } )
assume A4: x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } ; ::_thesis: x in { f where f is Function of F1(),F2() : P1[f] }
then A5: x is Function of F1(),F2() by FUNCT_2:66;
not x in { f where f is Function of F1(),F2() : P1[f] } by A4, XBOOLE_0:def_5;
then P1[x] by A5;
hence x in { f where f is Function of F1(),F2() : P1[f] } by A5; ::_thesis: verum
end;
theorem Th16: :: CARDFIN2:16
for s, t being finite set st card s <= card t holds
card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))
proof
let s, t be finite set ; ::_thesis: ( card s <= card t implies card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) )
assume A1: card s <= card t ; ::_thesis: card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))
defpred S1[ Function] means $1 is one-to-one ;
set onetoone = { f where f is Function of s,t : f is one-to-one } ;
A2: ( t = {} implies s = {} )
proof
assume t = {} ; ::_thesis: s = {}
then card t = 0 ;
hence s = {} by A1; ::_thesis: verum
end;
{ f where f is Function of s,t : f is one-to-one } c= Funcs (s,t)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is Function of s,t : f is one-to-one } or x in Funcs (s,t) )
assume x in { f where f is Function of s,t : f is one-to-one } ; ::_thesis: x in Funcs (s,t)
then ex f being Function of s,t st
( x = f & f is one-to-one ) ;
hence x in Funcs (s,t) by A2, FUNCT_2:8; ::_thesis: verum
end;
then reconsider onetoone = { f where f is Function of s,t : f is one-to-one } as Subset of (Funcs (s,t)) ;
{ f where f is Function of s,t : not S1[f] } = (Funcs (s,t)) \ { f where f is Function of s,t : S1[f] } from CARDFIN2:sch_1(A2);
then card (not-one-to-one (s,t)) = (card (Funcs (s,t))) - (card onetoone) by CARD_2:44
.= (card (Funcs (s,t))) - (((card t) !) / (((card t) -' (card s)) !)) by A1, CARD_FIN:7
.= ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) by A2, CARD_FIN:4 ;
hence card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) ; ::_thesis: verum
end;
Lm1: 2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
proof
A1: (364 + 1) ! = (364 !) * (364 + 1) by NEWTON:15;
A2: (363 + 1) ! = (363 !) * (363 + 1) by NEWTON:15;
A3: (362 + 1) ! = (362 !) * (362 + 1) by NEWTON:15;
A4: (361 + 1) ! = (361 !) * (361 + 1) by NEWTON:15;
A5: (360 + 1) ! = (360 !) * (360 + 1) by NEWTON:15;
A6: (359 + 1) ! = (359 !) * (359 + 1) by NEWTON:15;
A7: (358 + 1) ! = (358 !) * (358 + 1) by NEWTON:15;
A8: (357 + 1) ! = (357 !) * (357 + 1) by NEWTON:15;
A9: (356 + 1) ! = (356 !) * (356 + 1) by NEWTON:15;
A10: (355 + 1) ! = (355 !) * (355 + 1) by NEWTON:15;
A11: (354 + 1) ! = (354 !) * (354 + 1) by NEWTON:15;
A12: (353 + 1) ! = (353 !) * (353 + 1) by NEWTON:15;
A13: (352 + 1) ! = (352 !) * (352 + 1) by NEWTON:15;
A14: (351 + 1) ! = (351 !) * (351 + 1) by NEWTON:15;
A15: (350 + 1) ! = (350 !) * (350 + 1) by NEWTON:15;
A16: (349 + 1) ! = (349 !) * (349 + 1) by NEWTON:15;
A17: (348 + 1) ! = (348 !) * (348 + 1) by NEWTON:15;
A18: (347 + 1) ! = (347 !) * (347 + 1) by NEWTON:15;
A19: (346 + 1) ! = (346 !) * (346 + 1) by NEWTON:15;
A20: (345 + 1) ! = (345 !) * (345 + 1) by NEWTON:15;
A21: (344 + 1) ! = (344 !) * (344 + 1) by NEWTON:15;
A22: (343 + 1) ! = (343 !) * (343 + 1) by NEWTON:15;
(342 + 1) ! = (342 !) * (342 + 1) by NEWTON:15;
then 365 ! = (((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343)) * (342 !) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22;
then A23: (365 !) / (342 !) = ((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343) by XCMPLX_1:89;
365 |^ 1 = 365 by NEWTON:5;
then A24: 365 |^ (1 + 1) = 365 * 365 by NEWTON:6;
then A25: 365 |^ (2 + 1) = (365 * 365) * 365 by NEWTON:6;
A26: 365 |^ (3 + 2) = (365 |^ 3) * (365 |^ 2) by NEWTON:8;
A27: 365 |^ (3 + 3) = (365 |^ 3) * (365 |^ 3) by NEWTON:8;
A28: 365 |^ (6 + 5) = (365 |^ 6) * (365 |^ 5) by NEWTON:8;
A29: 365 |^ (6 + 6) = (365 |^ 6) * (365 |^ 6) by NEWTON:8;
365 |^ (12 + 11) = (365 |^ 12) * (365 |^ 11) by NEWTON:8;
then A30: 2 * ((365 |^ 23) - ((365 !) / (342 !))) > 365 |^ 23 by A28, A23, A29, A26, A24, A25, A27;
365 - 23 >= 0 ;
hence 2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23 by A30, XREAL_0:def_2; ::_thesis: verum
end;
theorem Th17: :: CARDFIN2:17
for s being finite set
for t being non empty finite set st card s = 23 & card t = 365 holds
2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
proof
let s be finite set ; ::_thesis: for t being non empty finite set st card s = 23 & card t = 365 holds
2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
let t be non empty finite set ; ::_thesis: ( card s = 23 & card t = 365 implies 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume A1: card s = 23 ; ::_thesis: ( not card t = 365 or 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume A2: card t = 365 ; ::_thesis: 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
then card (not-one-to-one (s,t)) = (365 |^ 23) - ((365 !) / ((365 -' 23) !)) by Th16, A1;
hence 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) by Lm1, A1, A2, CARD_FIN:4; ::_thesis: verum
end;
theorem :: CARDFIN2:18
for s, t being non empty finite set st card s = 23 & card t = 365 holds
prob (not-one-to-one (s,t)) > 1 / 2
proof
let s, t be non empty finite set ; ::_thesis: ( card s = 23 & card t = 365 implies prob (not-one-to-one (s,t)) > 1 / 2 )
assume A1: card s = 23 ; ::_thesis: ( not card t = 365 or prob (not-one-to-one (s,t)) > 1 / 2 )
assume A2: card t = 365 ; ::_thesis: prob (not-one-to-one (s,t)) > 1 / 2
set E = not-one-to-one (s,t);
set comega = card (Funcs (s,t));
(2 * (card (not-one-to-one (s,t)))) / 2 > (card (Funcs (s,t))) / 2 by Th17, A1, A2, XREAL_1:74;
then (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / 2) / (card (Funcs (s,t))) by XREAL_1:74;
then (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / (card (Funcs (s,t)))) / 2 ;
then (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > 1 / 2 by XCMPLX_0:def_7;
hence prob (not-one-to-one (s,t)) > 1 / 2 by RPR_1:def_1; ::_thesis: verum
end;