Metamath Proof Explorer

Theorem birthday

Description: The Birthday Problem. There is a more than even chance that out of 23 people in a room, at least two of them have the same birthday. Mathematically, this is asserting that for K = 2 3 and N = 3 6 5 , fewer than half of the set of all functions from 1 ... K to 1 ... N are injective. This is Metamath 100 proof #93. (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypotheses birthday.s 
|- S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }
birthday.t 
|- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }
birthday.k 
|- K = ; 2 3
birthday.n 
|- N = ; ; 3 6 5
Assertion birthday 
|- ( ( # ` T ) / ( # ` S ) ) < ( 1 / 2 )

Proof

Step Hyp Ref Expression
1 birthday.s 
 |-  S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }
2 birthday.t 
 |-  T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }
3 birthday.k 
 |-  K = ; 2 3
4 birthday.n 
 |-  N = ; ; 3 6 5
5 2nn0 
 |-  2 e. NN0
6 3nn0 
 |-  3 e. NN0
7 5 6 deccl 
 |-  ; 2 3 e. NN0
8 3 7 eqeltri 
 |-  K e. NN0
9 6nn0 
 |-  6 e. NN0
10 6 9 deccl 
 |-  ; 3 6 e. NN0
11 5nn 
 |-  5 e. NN
12 10 11 decnncl 
 |-  ; ; 3 6 5 e. NN
13 4 12 eqeltri 
 |-  N e. NN
14 1 2 birthdaylem3 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )
15 8 13 14 mp2an 
 |-  ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) )
16 log2ub 
 |-  ( log ` 2 ) < ( ; ; 2 5 3 / ; ; 3 6 5 )
17 8 nn0cni 
 |-  K e. CC
18 17 sqvali 
 |-  ( K ^ 2 ) = ( K x. K )
19 17 mulid1i 
 |-  ( K x. 1 ) = K
20 19 eqcomi 
 |-  K = ( K x. 1 )
21 18 20 oveq12i 
 |-  ( ( K ^ 2 ) - K ) = ( ( K x. K ) - ( K x. 1 ) )
22 ax-1cn 
 |-  1 e. CC
23 17 17 22 subdii 
 |-  ( K x. ( K - 1 ) ) = ( ( K x. K ) - ( K x. 1 ) )
24 21 23 eqtr4i 
 |-  ( ( K ^ 2 ) - K ) = ( K x. ( K - 1 ) )
25 24 oveq1i 
 |-  ( ( ( K ^ 2 ) - K ) / 2 ) = ( ( K x. ( K - 1 ) ) / 2 )
26 17 22 subcli 
 |-  ( K - 1 ) e. CC
27 2cn 
 |-  2 e. CC
28 2ne0 
 |-  2 =/= 0
29 17 26 27 28 divassi 
 |-  ( ( K x. ( K - 1 ) ) / 2 ) = ( K x. ( ( K - 1 ) / 2 ) )
30 1nn0 
 |-  1 e. NN0
31 5 5 deccl 
 |-  ; 2 2 e. NN0
32 31 nn0cni 
 |-  ; 2 2 e. CC
33 2p1e3 
 |-  ( 2 + 1 ) = 3
34 eqid 
 |-  ; 2 2 = ; 2 2
35 5 5 33 34 decsuc 
 |-  ( ; 2 2 + 1 ) = ; 2 3
36 3 35 eqtr4i 
 |-  K = ( ; 2 2 + 1 )
37 32 22 36 mvrraddi 
 |-  ( K - 1 ) = ; 2 2
38 37 oveq1i 
 |-  ( ( K - 1 ) / 2 ) = ( ; 2 2 / 2 )
39 5 11multnc 
 |-  ( 2 x. ; 1 1 ) = ; 2 2
40 30 30 deccl 
 |-  ; 1 1 e. NN0
41 40 nn0cni 
 |-  ; 1 1 e. CC
42 32 27 41 28 divmuli 
 |-  ( ( ; 2 2 / 2 ) = ; 1 1 <-> ( 2 x. ; 1 1 ) = ; 2 2 )
43 39 42 mpbir 
 |-  ( ; 2 2 / 2 ) = ; 1 1
44 38 43 eqtri 
 |-  ( ( K - 1 ) / 2 ) = ; 1 1
45 19 3 eqtri 
 |-  ( K x. 1 ) = ; 2 3
46 3p2e5 
 |-  ( 3 + 2 ) = 5
47 5 6 5 45 46 decaddi 
 |-  ( ( K x. 1 ) + 2 ) = ; 2 5
48 8 30 30 44 6 5 47 45 decmul2c 
 |-  ( K x. ( ( K - 1 ) / 2 ) ) = ; ; 2 5 3
49 25 29 48 3eqtri 
 |-  ( ( ( K ^ 2 ) - K ) / 2 ) = ; ; 2 5 3
50 49 4 oveq12i 
 |-  ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) = ( ; ; 2 5 3 / ; ; 3 6 5 )
51 16 50 breqtrri 
 |-  ( log ` 2 ) < ( ( ( ( K ^ 2 ) - K ) / 2 ) / N )
52 2rp 
 |-  2 e. RR+
53 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
54 52 53 ax-mp 
 |-  ( log ` 2 ) e. RR
55 5nn0 
 |-  5 e. NN0
56 5 55 deccl 
 |-  ; 2 5 e. NN0
57 56 6 deccl 
 |-  ; ; 2 5 3 e. NN0
58 49 57 eqeltri 
 |-  ( ( ( K ^ 2 ) - K ) / 2 ) e. NN0
59 58 nn0rei 
 |-  ( ( ( K ^ 2 ) - K ) / 2 ) e. RR
60 nndivre 
 |-  ( ( ( ( ( K ^ 2 ) - K ) / 2 ) e. RR /\ N e. NN ) -> ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR )
61 59 13 60 mp2an 
 |-  ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR
62 54 61 ltnegi 
 |-  ( ( log ` 2 ) < ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) <-> -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) < -u ( log ` 2 ) )
63 51 62 mpbi 
 |-  -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) < -u ( log ` 2 )
64 61 renegcli 
 |-  -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR
65 54 renegcli 
 |-  -u ( log ` 2 ) e. RR
66 eflt 
 |-  ( ( -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR /\ -u ( log ` 2 ) e. RR ) -> ( -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) < -u ( log ` 2 ) <-> ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) < ( exp ` -u ( log ` 2 ) ) ) )
67 64 65 66 mp2an 
 |-  ( -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) < -u ( log ` 2 ) <-> ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) < ( exp ` -u ( log ` 2 ) ) )
68 63 67 mpbi 
 |-  ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) < ( exp ` -u ( log ` 2 ) )
69 54 recni 
 |-  ( log ` 2 ) e. CC
70 efneg 
 |-  ( ( log ` 2 ) e. CC -> ( exp ` -u ( log ` 2 ) ) = ( 1 / ( exp ` ( log ` 2 ) ) ) )
71 69 70 ax-mp 
 |-  ( exp ` -u ( log ` 2 ) ) = ( 1 / ( exp ` ( log ` 2 ) ) )
72 reeflog 
 |-  ( 2 e. RR+ -> ( exp ` ( log ` 2 ) ) = 2 )
73 52 72 ax-mp 
 |-  ( exp ` ( log ` 2 ) ) = 2
74 73 oveq2i 
 |-  ( 1 / ( exp ` ( log ` 2 ) ) ) = ( 1 / 2 )
75 71 74 eqtri 
 |-  ( exp ` -u ( log ` 2 ) ) = ( 1 / 2 )
76 68 75 breqtri 
 |-  ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) < ( 1 / 2 )
77 1 2 birthdaylem1 
 |-  ( T C_ S /\ S e. Fin /\ ( N e. NN -> S =/= (/) ) )
78 77 simp2i 
 |-  S e. Fin
79 77 simp1i 
 |-  T C_ S
80 ssfi 
 |-  ( ( S e. Fin /\ T C_ S ) -> T e. Fin )
81 78 79 80 mp2an 
 |-  T e. Fin
82 hashcl 
 |-  ( T e. Fin -> ( # ` T ) e. NN0 )
83 81 82 ax-mp 
 |-  ( # ` T ) e. NN0
84 83 nn0rei 
 |-  ( # ` T ) e. RR
85 77 simp3i 
 |-  ( N e. NN -> S =/= (/) )
86 13 85 ax-mp 
 |-  S =/= (/)
87 hashnncl 
 |-  ( S e. Fin -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
88 78 87 ax-mp 
 |-  ( ( # ` S ) e. NN <-> S =/= (/) )
89 86 88 mpbir 
 |-  ( # ` S ) e. NN
90 nndivre 
 |-  ( ( ( # ` T ) e. RR /\ ( # ` S ) e. NN ) -> ( ( # ` T ) / ( # ` S ) ) e. RR )
91 84 89 90 mp2an 
 |-  ( ( # ` T ) / ( # ` S ) ) e. RR
92 reefcl 
 |-  ( -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR -> ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) e. RR )
93 64 92 ax-mp 
 |-  ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) e. RR
94 halfre 
 |-  ( 1 / 2 ) e. RR
95 91 93 94 lelttri 
 |-  ( ( ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) /\ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) < ( 1 / 2 ) ) -> ( ( # ` T ) / ( # ` S ) ) < ( 1 / 2 ) )
96 15 76 95 mp2an 
 |-  ( ( # ` T ) / ( # ` S ) ) < ( 1 / 2 )