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 )