Theorem birthday 25137

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 𝐾 = 23 and 𝑁 = 365, fewer than half of the set of all functions from 1...𝐾 to 1...𝑁 are injective. This is Metamath 100 proof #93. (Contributed by Mario Carneiro, 17-Apr-2015.)

Hypotheses

Ref	Expression
birthday.s	⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}
birthday.t	⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}
birthday.k	⊢ 𝐾 = ;23
birthday.n	⊢ 𝑁 = ;;365

Assertion

Ref	Expression
birthday	⊢ ((♯‘𝑇) / (♯‘𝑆)) < (1 / 2)

Distinct variable groups:   𝑓,𝐾   𝑓,𝑁

Allowed substitution hints:   𝑆(𝑓)   𝑇(𝑓)

Proof of Theorem birthday

Step	Hyp	Ref	Expression
1		birthday.k	. . . 4 ⊢ 𝐾 = ;23
2		2nn0 11665	. . . . 5 ⊢ 2 ∈ ℕ0
3		3nn0 11666	. . . . 5 ⊢ 3 ∈ ℕ0
4	2, 3	deccl 11864	. . . 4 ⊢ ;23 ∈ ℕ0
5	1, 4	eqeltri 2855	. . 3 ⊢ 𝐾 ∈ ℕ0
6		birthday.n	. . . 4 ⊢ 𝑁 = ;;365
7		6nn0 11669	. . . . . 6 ⊢ 6 ∈ ℕ0
8	3, 7	deccl 11864	. . . . 5 ⊢ ;36 ∈ ℕ0
9		5nn 11467	. . . . 5 ⊢ 5 ∈ ℕ
10	8, 9	decnncl 11870	. . . 4 ⊢ ;;365 ∈ ℕ
11	6, 10	eqeltri 2855	. . 3 ⊢ 𝑁 ∈ ℕ
12		birthday.s	. . . 4 ⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}
13		birthday.t	. . . 4 ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}
14	12, 13	birthdaylem3 25136	. . 3 ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((♯‘𝑇) / (♯‘𝑆)) ≤ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)))
15	5, 11, 14	mp2an 682	. 2 ⊢ ((♯‘𝑇) / (♯‘𝑆)) ≤ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁))
16		log2ub 25132	. . . . . 6 ⊢ (log‘2) < (;;253 / ;;365)
17	5	nn0cni 11659	. . . . . . . . . . . 12 ⊢ 𝐾 ∈ ℂ
18	17	sqvali 13266	. . . . . . . . . . 11 ⊢ (𝐾↑2) = (𝐾 · 𝐾)
19	17	mulid1i 10383	. . . . . . . . . . . 12 ⊢ (𝐾 · 1) = 𝐾
20	19	eqcomi 2787	. . . . . . . . . . 11 ⊢ 𝐾 = (𝐾 · 1)
21	18, 20	oveq12i 6936	. . . . . . . . . 10 ⊢ ((𝐾↑2) − 𝐾) = ((𝐾 · 𝐾) − (𝐾 · 1))
22		ax-1cn 10332	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
23	17, 17, 22	subdii 10826	. . . . . . . . . 10 ⊢ (𝐾 · (𝐾 − 1)) = ((𝐾 · 𝐾) − (𝐾 · 1))
24	21, 23	eqtr4i 2805	. . . . . . . . 9 ⊢ ((𝐾↑2) − 𝐾) = (𝐾 · (𝐾 − 1))
25	24	oveq1i 6934	. . . . . . . 8 ⊢ (((𝐾↑2) − 𝐾) / 2) = ((𝐾 · (𝐾 − 1)) / 2)
26	17, 22	subcli 10701	. . . . . . . . . 10 ⊢ (𝐾 − 1) ∈ ℂ
27		2cn 11454	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
28		2ne0 11490	. . . . . . . . . 10 ⊢ 2 ≠ 0
29	17, 26, 27, 28	divassi 11133	. . . . . . . . 9 ⊢ ((𝐾 · (𝐾 − 1)) / 2) = (𝐾 · ((𝐾 − 1) / 2))
30		1nn0 11664	. . . . . . . . . 10 ⊢ 1 ∈ ℕ0
31		2p1e3 11528	. . . . . . . . . . . . . . . 16 ⊢ (2 + 1) = 3
32		eqid 2778	. . . . . . . . . . . . . . . 16 ⊢ ;22 = ;22
33	2, 2, 31, 32	decsuc 11881	. . . . . . . . . . . . . . 15 ⊢ (;22 + 1) = ;23
34	1, 33	eqtr4i 2805	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (;22 + 1)
35	34	oveq1i 6934	. . . . . . . . . . . . 13 ⊢ (𝐾 − 1) = ((;22 + 1) − 1)
36	2, 2	deccl 11864	. . . . . . . . . . . . . . 15 ⊢ ;22 ∈ ℕ0
37	36	nn0cni 11659	. . . . . . . . . . . . . 14 ⊢ ;22 ∈ ℂ
38	37, 22	pncan3oi 10641	. . . . . . . . . . . . 13 ⊢ ((;22 + 1) − 1) = ;22
39	35, 38	eqtri 2802	. . . . . . . . . . . 12 ⊢ (𝐾 − 1) = ;22
40	39	oveq1i 6934	. . . . . . . . . . 11 ⊢ ((𝐾 − 1) / 2) = (;22 / 2)
41		eqid 2778	. . . . . . . . . . . . 13 ⊢ ;11 = ;11
42		0nn0 11663	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
43	27	mulid1i 10383	. . . . . . . . . . . . . . 15 ⊢ (2 · 1) = 2
44	43	oveq1i 6934	. . . . . . . . . . . . . 14 ⊢ ((2 · 1) + 0) = (2 + 0)
45	27	addid1i 10565	. . . . . . . . . . . . . 14 ⊢ (2 + 0) = 2
46	44, 45	eqtri 2802	. . . . . . . . . . . . 13 ⊢ ((2 · 1) + 0) = 2
47	2	dec0h 11872	. . . . . . . . . . . . . 14 ⊢ 2 = ;02
48	43, 47	eqtri 2802	. . . . . . . . . . . . 13 ⊢ (2 · 1) = ;02
49	2, 30, 30, 41, 2, 42, 46, 48	decmul2c 11917	. . . . . . . . . . . 12 ⊢ (2 · ;11) = ;22
50	30, 30	deccl 11864	. . . . . . . . . . . . . 14 ⊢ ;11 ∈ ℕ0
51	50	nn0cni 11659	. . . . . . . . . . . . 13 ⊢ ;11 ∈ ℂ
52	37, 27, 51, 28	divmuli 11131	. . . . . . . . . . . 12 ⊢ ((;22 / 2) = ;11 ↔ (2 · ;11) = ;22)
53	49, 52	mpbir 223	. . . . . . . . . . 11 ⊢ (;22 / 2) = ;11
54	40, 53	eqtri 2802	. . . . . . . . . 10 ⊢ ((𝐾 − 1) / 2) = ;11
55	19, 1	eqtri 2802	. . . . . . . . . . 11 ⊢ (𝐾 · 1) = ;23
56		3p2e5 11537	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
57	2, 3, 2, 55, 56	decaddi 11910	. . . . . . . . . 10 ⊢ ((𝐾 · 1) + 2) = ;25
58	5, 30, 30, 54, 3, 2, 57, 55	decmul2c 11917	. . . . . . . . 9 ⊢ (𝐾 · ((𝐾 − 1) / 2)) = ;;253
59	29, 58	eqtri 2802	. . . . . . . 8 ⊢ ((𝐾 · (𝐾 − 1)) / 2) = ;;253
60	25, 59	eqtri 2802	. . . . . . 7 ⊢ (((𝐾↑2) − 𝐾) / 2) = ;;253
61	60, 6	oveq12i 6936	. . . . . 6 ⊢ ((((𝐾↑2) − 𝐾) / 2) / 𝑁) = (;;253 / ;;365)
62	16, 61	breqtrri 4915	. . . . 5 ⊢ (log‘2) < ((((𝐾↑2) − 𝐾) / 2) / 𝑁)
63		2rp 12146	. . . . . . 7 ⊢ 2 ∈ ℝ+
64		relogcl 24763	. . . . . . 7 ⊢ (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
65	63, 64	ax-mp 5	. . . . . 6 ⊢ (log‘2) ∈ ℝ
66		5nn0 11668	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
67	2, 66	deccl 11864	. . . . . . . . . 10 ⊢ ;25 ∈ ℕ0
68	67, 3	deccl 11864	. . . . . . . . 9 ⊢ ;;253 ∈ ℕ0
69	60, 68	eqeltri 2855	. . . . . . . 8 ⊢ (((𝐾↑2) − 𝐾) / 2) ∈ ℕ0
70	69	nn0rei 11658	. . . . . . 7 ⊢ (((𝐾↑2) − 𝐾) / 2) ∈ ℝ
71		nndivre 11420	. . . . . . 7 ⊢ (((((𝐾↑2) − 𝐾) / 2) ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ)
72	70, 11, 71	mp2an 682	. . . . . 6 ⊢ ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ
73	65, 72	ltnegi 10921	. . . . 5 ⊢ ((log‘2) < ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ↔ -((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2))
74	62, 73	mpbi 222	. . . 4 ⊢ -((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2)
75	72	renegcli 10686	. . . . 5 ⊢ -((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ
76	65	renegcli 10686	. . . . 5 ⊢ -(log‘2) ∈ ℝ
77		eflt 15253	. . . . 5 ⊢ ((-((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ ∧ -(log‘2) ∈ ℝ) → (-((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2) ↔ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (exp‘-(log‘2))))
78	75, 76, 77	mp2an 682	. . . 4 ⊢ (-((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2) ↔ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (exp‘-(log‘2)))
79	74, 78	mpbi 222	. . 3 ⊢ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (exp‘-(log‘2))
80	65	recni 10393	. . . . 5 ⊢ (log‘2) ∈ ℂ
81		efneg 15234	. . . . 5 ⊢ ((log‘2) ∈ ℂ → (exp‘-(log‘2)) = (1 / (exp‘(log‘2))))
82	80, 81	ax-mp 5	. . . 4 ⊢ (exp‘-(log‘2)) = (1 / (exp‘(log‘2)))
83		reeflog 24768	. . . . . 6 ⊢ (2 ∈ ℝ+ → (exp‘(log‘2)) = 2)
84	63, 83	ax-mp 5	. . . . 5 ⊢ (exp‘(log‘2)) = 2
85	84	oveq2i 6935	. . . 4 ⊢ (1 / (exp‘(log‘2))) = (1 / 2)
86	82, 85	eqtri 2802	. . 3 ⊢ (exp‘-(log‘2)) = (1 / 2)
87	79, 86	breqtri 4913	. 2 ⊢ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (1 / 2)
88	12, 13	birthdaylem1 25134	. . . . . . . 8 ⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅))
89	88	simp2i 1131	. . . . . . 7 ⊢ 𝑆 ∈ Fin
90	88	simp1i 1130	. . . . . . 7 ⊢ 𝑇 ⊆ 𝑆
91		ssfi 8470	. . . . . . 7 ⊢ ((𝑆 ∈ Fin ∧ 𝑇 ⊆ 𝑆) → 𝑇 ∈ Fin)
92	89, 90, 91	mp2an 682	. . . . . 6 ⊢ 𝑇 ∈ Fin
93		hashcl 13466	. . . . . 6 ⊢ (𝑇 ∈ Fin → (♯‘𝑇) ∈ ℕ0)
94	92, 93	ax-mp 5	. . . . 5 ⊢ (♯‘𝑇) ∈ ℕ0
95	94	nn0rei 11658	. . . 4 ⊢ (♯‘𝑇) ∈ ℝ
96	88	simp3i 1132	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑆 ≠ ∅)
97	11, 96	ax-mp 5	. . . . 5 ⊢ 𝑆 ≠ ∅
98		hashnncl 13476	. . . . . 6 ⊢ (𝑆 ∈ Fin → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
99	89, 98	ax-mp 5	. . . . 5 ⊢ ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅)
100	97, 99	mpbir 223	. . . 4 ⊢ (♯‘𝑆) ∈ ℕ
101		nndivre 11420	. . . 4 ⊢ (((♯‘𝑇) ∈ ℝ ∧ (♯‘𝑆) ∈ ℕ) → ((♯‘𝑇) / (♯‘𝑆)) ∈ ℝ)
102	95, 100, 101	mp2an 682	. . 3 ⊢ ((♯‘𝑇) / (♯‘𝑆)) ∈ ℝ
103		reefcl 15223	. . . 4 ⊢ (-((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ → (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) ∈ ℝ)
104	75, 103	ax-mp 5	. . 3 ⊢ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) ∈ ℝ
105		halfre 11600	. . 3 ⊢ (1 / 2) ∈ ℝ
106	102, 104, 105	lelttri 10505	. 2 ⊢ ((((♯‘𝑇) / (♯‘𝑆)) ≤ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) ∧ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (1 / 2)) → ((♯‘𝑇) / (♯‘𝑆)) < (1 / 2))
107	15, 87, 106	mp2an 682	1 ⊢ ((♯‘𝑇) / (♯‘𝑆)) < (1 / 2)

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  {cab 2763   ≠ wne 2969   ⊆ wss 3792  ∅c0 4141   class class class wbr 4888  ⟶wf 6133  –1-1→wf1 6134  ‘cfv 6137  (class class class)co 6924  Fincfn 8243  ℂcc 10272  ℝcr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279   < clt 10413   ≤ cle 10414   − cmin 10608  -cneg 10609   / cdiv 11034  ℕcn 11378  2c2 11434  3c3 11435  5c5 11437  6c6 11438  ℕ₀cn0 11646  ;cdc 11849  ℝ⁺crp 12141  ...cfz 12647  ↑cexp 13182  ♯chash 13439  expce 15198  logclog 24742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-4 11444  df-5 11445  df-6 11446  df-7 11447  df-8 11448  df-9 11449  df-n0 11647  df-xnn0 11719  df-z 11733  df-dec 11850  df-uz 11997  df-q 12100  df-rp 12142  df-xneg 12261  df-xadd 12262  df-xmul 12263  df-ioo 12495  df-ioc 12496  df-ico 12497  df-icc 12498  df-fz 12648  df-fzo 12789  df-fl 12916  df-mod 12992  df-seq 13124  df-exp 13183  df-fac 13383  df-bc 13412  df-hash 13440  df-shft 14218  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-limsup 14614  df-clim 14631  df-rlim 14632  df-sum 14829  df-ef 15204  df-sin 15206  df-cos 15207  df-tan 15208  df-pi 15209  df-dvds 15392  df-struct 16261  df-ndx 16262  df-slot 16263  df-base 16265  df-sets 16266  df-ress 16267  df-plusg 16355  df-mulr 16356  df-starv 16357  df-sca 16358  df-vsca 16359  df-ip 16360  df-tset 16361  df-ple 16362  df-ds 16364  df-unif 16365  df-hom 16366  df-cco 16367  df-rest 16473  df-topn 16474  df-0g 16492  df-gsum 16493  df-topgen 16494  df-pt 16495  df-prds 16498  df-xrs 16552  df-qtop 16557  df-imas 16558  df-xps 16560  df-mre 16636  df-mrc 16637  df-acs 16639  df-mgm 17632  df-sgrp 17674  df-mnd 17685  df-submnd 17726  df-mulg 17932  df-cntz 18137  df-cmn 18585  df-psmet 20138  df-xmet 20139  df-met 20140  df-bl 20141  df-mopn 20142  df-fbas 20143  df-fg 20144  df-cnfld 20147  df-top 21110  df-topon 21127  df-topsp 21149  df-bases 21162  df-cld 21235  df-ntr 21236  df-cls 21237  df-nei 21314  df-lp 21352  df-perf 21353  df-cn 21443  df-cnp 21444  df-haus 21531  df-cmp 21603  df-tx 21778  df-hmeo 21971  df-fil 22062  df-fm 22154  df-flim 22155  df-flf 22156  df-xms 22537  df-ms 22538  df-tms 22539  df-cncf 23093  df-limc 24071  df-dv 24072  df-ulm 24572  df-log 24744  df-atan 25049

This theorem is referenced by: (None)