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=\left\{f|f:\left(1\dots K\right)⟶\left(1\dots N\right)\right\}$$
	birthday.t	$$⊢T=\left\{f|f:\left(1\dots K\right)\underset{1-1}{⟶}\left(1\dots N\right)\right\}$$
	birthday.k	$$⊢K=23$$
	birthday.n	$$⊢N=365$$
Assertion	birthday	$$⊢\frac{\left|T\right|}{\left|S\right|}<\frac{1}{2}$$

Proof

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