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 ⊢ 𝑆 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
birthday.t ⊢ 𝑇 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) }
birthday.k ⊢ 𝐾 = 2 3
birthday.n ⊢ 𝑁 = 3 6 5
Assertion birthday ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) < ( 1 / 2 )

Proof

Step Hyp Ref Expression
1 birthday.s ⊢ 𝑆 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
2 birthday.t ⊢ 𝑇 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) }
3 birthday.k ⊢ 𝐾 = 2 3
4 birthday.n ⊢ 𝑁 = 3 6 5
5 2nn0 ⊢ 2 ∈ ℕ0
6 3nn0 ⊢ 3 ∈ ℕ0
7 5 6 deccl ⊢ 2 3 ∈ ℕ0
8 3 7 eqeltri ⊢ 𝐾 ∈ ℕ0
9 6nn0 ⊢ 6 ∈ ℕ0
10 6 9 deccl ⊢ 3 6 ∈ ℕ0
11 5nn ⊢ 5 ∈ ℕ
12 10 11 decnncl ⊢ 3 6 5 ∈ ℕ
13 4 12 eqeltri ⊢ 𝑁 ∈ ℕ
14 1 2 birthdaylem3 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) ≤ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) )
15 8 13 14 mp2an ⊢ ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) ≤ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) )
16 log2ub ⊢ ( log ‘ 2 ) < ( 2 5 3 / 3 6 5 )
17 8 nn0cni ⊢ 𝐾 ∈ ℂ
18 17 sqvali ⊢ ( 𝐾 ↑ 2 ) = ( 𝐾 · 𝐾 )
19 17 mulridi ⊢ ( 𝐾 · 1 ) = 𝐾
20 19 eqcomi ⊢ 𝐾 = ( 𝐾 · 1 )
21 18 20 oveq12i ⊢ ( ( 𝐾 ↑ 2 ) − 𝐾 ) = ( ( 𝐾 · 𝐾 ) − ( 𝐾 · 1 ) )
22 ax-1cn ⊢ 1 ∈ ℂ
23 17 17 22 subdii ⊢ ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( 𝐾 · 𝐾 ) − ( 𝐾 · 1 ) )
24 21 23 eqtr4i ⊢ ( ( 𝐾 ↑ 2 ) − 𝐾 ) = ( 𝐾 · ( 𝐾 − 1 ) )
25 24 oveq1i ⊢ ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) / 2 )
26 17 22 subcli ⊢ ( 𝐾 − 1 ) ∈ ℂ
27 2cn ⊢ 2 ∈ ℂ
28 2ne0 ⊢ 2 ≠ 0
29 17 26 27 28 divassi ⊢ ( ( 𝐾 · ( 𝐾 − 1 ) ) / 2 ) = ( 𝐾 · ( ( 𝐾 − 1 ) / 2 ) )
30 1nn0 ⊢ 1 ∈ ℕ0
31 5 5 deccl ⊢ 2 2 ∈ ℕ0
32 31 nn0cni ⊢ 2 2 ∈ ℂ
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 ⊢ 𝐾 = ( 2 2 + 1 )
37 32 22 36 mvrraddi ⊢ ( 𝐾 − 1 ) = 2 2
38 37 oveq1i ⊢ ( ( 𝐾 − 1 ) / 2 ) = ( 2 2 / 2 )
39 5 11multnc ⊢ ( 2 · 1 1 ) = 2 2
40 30 30 deccl ⊢ 1 1 ∈ ℕ0
41 40 nn0cni ⊢ 1 1 ∈ ℂ
42 32 27 41 28 divmuli ⊢ ( ( 2 2 / 2 ) = 1 1 ↔ ( 2 · 1 1 ) = 2 2 )
43 39 42 mpbir ⊢ ( 2 2 / 2 ) = 1 1
44 38 43 eqtri ⊢ ( ( 𝐾 − 1 ) / 2 ) = 1 1
45 19 3 eqtri ⊢ ( 𝐾 · 1 ) = 2 3
46 3p2e5 ⊢ ( 3 + 2 ) = 5
47 5 6 5 45 46 decaddi ⊢ ( ( 𝐾 · 1 ) + 2 ) = 2 5
48 8 30 30 44 6 5 47 45 decmul2c ⊢ ( 𝐾 · ( ( 𝐾 − 1 ) / 2 ) ) = 2 5 3
49 25 29 48 3eqtri ⊢ ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) = 2 5 3
50 49 4 oveq12i ⊢ ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) = ( 2 5 3 / 3 6 5 )
51 16 50 breqtrri ⊢ ( log ‘ 2 ) < ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 )
52 2rp ⊢ 2 ∈ ℝ+
53 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
54 52 53 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
55 5nn0 ⊢ 5 ∈ ℕ0
56 5 55 deccl ⊢ 2 5 ∈ ℕ0
57 56 6 deccl ⊢ 2 5 3 ∈ ℕ0
58 49 57 eqeltri ⊢ ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) ∈ ℕ0
59 58 nn0rei ⊢ ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) ∈ ℝ
60 nndivre ⊢ ( ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ∈ ℝ )
61 59 13 60 mp2an ⊢ ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ∈ ℝ
62 54 61 ltnegi ⊢ ( ( log ‘ 2 ) < ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ↔ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) < - ( log ‘ 2 ) )
63 51 62 mpbi ⊢ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) < - ( log ‘ 2 )
64 61 renegcli ⊢ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ∈ ℝ
65 54 renegcli ⊢ - ( log ‘ 2 ) ∈ ℝ
66 eflt ⊢ ( ( - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ∈ ℝ ∧ - ( log ‘ 2 ) ∈ ℝ ) → ( - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) < - ( log ‘ 2 ) ↔ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) < ( exp ‘ - ( log ‘ 2 ) ) ) )
67 64 65 66 mp2an ⊢ ( - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) < - ( log ‘ 2 ) ↔ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) < ( exp ‘ - ( log ‘ 2 ) ) )
68 63 67 mpbi ⊢ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) < ( exp ‘ - ( log ‘ 2 ) )
69 54 recni ⊢ ( log ‘ 2 ) ∈ ℂ
70 efneg ⊢ ( ( log ‘ 2 ) ∈ ℂ → ( exp ‘ - ( log ‘ 2 ) ) = ( 1 / ( exp ‘ ( log ‘ 2 ) ) ) )
71 69 70 ax-mp ⊢ ( exp ‘ - ( log ‘ 2 ) ) = ( 1 / ( exp ‘ ( log ‘ 2 ) ) )
72 reeflog ⊢ ( 2 ∈ ℝ+ → ( 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 ‘ - ( log ‘ 2 ) ) = ( 1 / 2 )
76 68 75 breqtri ⊢ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) < ( 1 / 2 )
77 1 2 birthdaylem1 ⊢ ( 𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ ( 𝑁 ∈ ℕ → 𝑆 ≠ ∅ ) )
78 77 simp2i ⊢ 𝑆 ∈ Fin
79 77 simp1i ⊢ 𝑇 ⊆ 𝑆
80 ssfi ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ∈ Fin )
81 78 79 80 mp2an ⊢ 𝑇 ∈ Fin
82 hashcl ⊢ ( 𝑇 ∈ Fin → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
83 81 82 ax-mp ⊢ ( ♯ ‘ 𝑇 ) ∈ ℕ0
84 83 nn0rei ⊢ ( ♯ ‘ 𝑇 ) ∈ ℝ
85 77 simp3i ⊢ ( 𝑁 ∈ ℕ → 𝑆 ≠ ∅ )
86 13 85 ax-mp ⊢ 𝑆 ≠ ∅
87 hashnncl ⊢ ( 𝑆 ∈ Fin → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ↔ 𝑆 ≠ ∅ ) )
88 78 87 ax-mp ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ ↔ 𝑆 ≠ ∅ )
89 86 88 mpbir ⊢ ( ♯ ‘ 𝑆 ) ∈ ℕ
90 nndivre ⊢ ( ( ( ♯ ‘ 𝑇 ) ∈ ℝ ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ ) → ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) ∈ ℝ )
91 84 89 90 mp2an ⊢ ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) ∈ ℝ
92 reefcl ⊢ ( - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ∈ ℝ → ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) ∈ ℝ )
93 64 92 ax-mp ⊢ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) ∈ ℝ
94 halfre ⊢ ( 1 / 2 ) ∈ ℝ
95 91 93 94 lelttri ⊢ ( ( ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) ≤ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) ∧ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) < ( 1 / 2 ) ) → ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) < ( 1 / 2 ) )
96 15 76 95 mp2an ⊢ ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) < ( 1 / 2 )