Proof of Theorem birthday
Step | Hyp | Ref
| Expression |
1 | | birthday.k |
. . . 4
⊢ 𝐾 = ;23 |
2 | | 2nn0 11309 |
. . . . 5
⊢ 2 ∈
ℕ0 |
3 | | 3nn0 11310 |
. . . . 5
⊢ 3 ∈
ℕ0 |
4 | 2, 3 | deccl 11512 |
. . . 4
⊢ ;23 ∈
ℕ0 |
5 | 1, 4 | eqeltri 2697 |
. . 3
⊢ 𝐾 ∈
ℕ0 |
6 | | birthday.n |
. . . 4
⊢ 𝑁 = ;;365 |
7 | | 6nn0 11313 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
8 | 3, 7 | deccl 11512 |
. . . . 5
⊢ ;36 ∈
ℕ0 |
9 | | 5nn 11188 |
. . . . 5
⊢ 5 ∈
ℕ |
10 | 8, 9 | decnncl 11518 |
. . . 4
⊢ ;;365 ∈ ℕ |
11 | 6, 10 | eqeltri 2697 |
. . 3
⊢ 𝑁 ∈ ℕ |
12 | | birthday.s |
. . . 4
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} |
13 | | birthday.t |
. . . 4
⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} |
14 | 12, 13 | birthdaylem3 24680 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((#‘𝑇) /
(#‘𝑆)) ≤
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁))) |
15 | 5, 11, 14 | mp2an 708 |
. 2
⊢
((#‘𝑇) /
(#‘𝑆)) ≤
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) |
16 | | log2ub 24676 |
. . . . . 6
⊢
(log‘2) < (;;253 / ;;365) |
17 | 5 | nn0cni 11304 |
. . . . . . . . . . . 12
⊢ 𝐾 ∈ ℂ |
18 | 17 | sqvali 12943 |
. . . . . . . . . . 11
⊢ (𝐾↑2) = (𝐾 · 𝐾) |
19 | 17 | mulid1i 10042 |
. . . . . . . . . . . 12
⊢ (𝐾 · 1) = 𝐾 |
20 | 19 | eqcomi 2631 |
. . . . . . . . . . 11
⊢ 𝐾 = (𝐾 · 1) |
21 | 18, 20 | oveq12i 6662 |
. . . . . . . . . 10
⊢ ((𝐾↑2) − 𝐾) = ((𝐾 · 𝐾) − (𝐾 · 1)) |
22 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
23 | 17, 17, 22 | subdii 10479 |
. . . . . . . . . 10
⊢ (𝐾 · (𝐾 − 1)) = ((𝐾 · 𝐾) − (𝐾 · 1)) |
24 | 21, 23 | eqtr4i 2647 |
. . . . . . . . 9
⊢ ((𝐾↑2) − 𝐾) = (𝐾 · (𝐾 − 1)) |
25 | 24 | oveq1i 6660 |
. . . . . . . 8
⊢ (((𝐾↑2) − 𝐾) / 2) = ((𝐾 · (𝐾 − 1)) / 2) |
26 | 17, 22 | subcli 10357 |
. . . . . . . . . 10
⊢ (𝐾 − 1) ∈
ℂ |
27 | | 2cn 11091 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
28 | | 2ne0 11113 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
29 | 17, 26, 27, 28 | divassi 10781 |
. . . . . . . . 9
⊢ ((𝐾 · (𝐾 − 1)) / 2) = (𝐾 · ((𝐾 − 1) / 2)) |
30 | | 1nn0 11308 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
31 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
3 |
32 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ ;22 = ;22 |
33 | 2, 2, 31, 32 | decsuc 11535 |
. . . . . . . . . . . . . . 15
⊢ (;22 + 1) = ;23 |
34 | 1, 33 | eqtr4i 2647 |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (;22 + 1) |
35 | 34 | oveq1i 6660 |
. . . . . . . . . . . . 13
⊢ (𝐾 − 1) = ((;22 + 1) − 1) |
36 | 2, 2 | deccl 11512 |
. . . . . . . . . . . . . . 15
⊢ ;22 ∈
ℕ0 |
37 | 36 | nn0cni 11304 |
. . . . . . . . . . . . . 14
⊢ ;22 ∈ ℂ |
38 | 37, 22 | pncan3oi 10297 |
. . . . . . . . . . . . 13
⊢ ((;22 + 1) − 1) = ;22 |
39 | 35, 38 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ (𝐾 − 1) = ;22 |
40 | 39 | oveq1i 6660 |
. . . . . . . . . . 11
⊢ ((𝐾 − 1) / 2) = (;22 / 2) |
41 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ;11 = ;11 |
42 | | 0nn0 11307 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
43 | 27 | mulid1i 10042 |
. . . . . . . . . . . . . . 15
⊢ (2
· 1) = 2 |
44 | 43 | oveq1i 6660 |
. . . . . . . . . . . . . 14
⊢ ((2
· 1) + 0) = (2 + 0) |
45 | 27 | addid1i 10223 |
. . . . . . . . . . . . . 14
⊢ (2 + 0) =
2 |
46 | 44, 45 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ ((2
· 1) + 0) = 2 |
47 | 2 | dec0h 11522 |
. . . . . . . . . . . . . 14
⊢ 2 = ;02 |
48 | 43, 47 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = ;02 |
49 | 2, 30, 30, 41, 2, 42, 46, 48 | decmul2c 11589 |
. . . . . . . . . . . 12
⊢ (2
· ;11) = ;22 |
50 | 30, 30 | deccl 11512 |
. . . . . . . . . . . . . 14
⊢ ;11 ∈
ℕ0 |
51 | 50 | nn0cni 11304 |
. . . . . . . . . . . . 13
⊢ ;11 ∈ ℂ |
52 | 37, 27, 51, 28 | divmuli 10779 |
. . . . . . . . . . . 12
⊢ ((;22 / 2) = ;11 ↔ (2 · ;11) = ;22) |
53 | 49, 52 | mpbir 221 |
. . . . . . . . . . 11
⊢ (;22 / 2) = ;11 |
54 | 40, 53 | eqtri 2644 |
. . . . . . . . . 10
⊢ ((𝐾 − 1) / 2) = ;11 |
55 | 19, 1 | eqtri 2644 |
. . . . . . . . . . 11
⊢ (𝐾 · 1) = ;23 |
56 | | 3p2e5 11160 |
. . . . . . . . . . 11
⊢ (3 + 2) =
5 |
57 | 2, 3, 2, 55, 56 | decaddi 11579 |
. . . . . . . . . 10
⊢ ((𝐾 · 1) + 2) = ;25 |
58 | 5, 30, 30, 54, 3, 2, 57, 55 | decmul2c 11589 |
. . . . . . . . 9
⊢ (𝐾 · ((𝐾 − 1) / 2)) = ;;253 |
59 | 29, 58 | eqtri 2644 |
. . . . . . . 8
⊢ ((𝐾 · (𝐾 − 1)) / 2) = ;;253 |
60 | 25, 59 | eqtri 2644 |
. . . . . . 7
⊢ (((𝐾↑2) − 𝐾) / 2) = ;;253 |
61 | 60, 6 | oveq12i 6662 |
. . . . . 6
⊢ ((((𝐾↑2) − 𝐾) / 2) / 𝑁) = (;;253 /
;;365) |
62 | 16, 61 | breqtrri 4680 |
. . . . 5
⊢
(log‘2) < ((((𝐾↑2) − 𝐾) / 2) / 𝑁) |
63 | | 2rp 11837 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
64 | | relogcl 24322 |
. . . . . . 7
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
65 | 63, 64 | ax-mp 5 |
. . . . . 6
⊢
(log‘2) ∈ ℝ |
66 | | 5nn0 11312 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ0 |
67 | 2, 66 | deccl 11512 |
. . . . . . . . . 10
⊢ ;25 ∈
ℕ0 |
68 | 67, 3 | deccl 11512 |
. . . . . . . . 9
⊢ ;;253 ∈ ℕ0 |
69 | 60, 68 | eqeltri 2697 |
. . . . . . . 8
⊢ (((𝐾↑2) − 𝐾) / 2) ∈
ℕ0 |
70 | 69 | nn0rei 11303 |
. . . . . . 7
⊢ (((𝐾↑2) − 𝐾) / 2) ∈
ℝ |
71 | | nndivre 11056 |
. . . . . . 7
⊢
(((((𝐾↑2)
− 𝐾) / 2) ∈
ℝ ∧ 𝑁 ∈
ℕ) → ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ) |
72 | 70, 11, 71 | mp2an 708 |
. . . . . 6
⊢ ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ |
73 | 65, 72 | ltnegi 10572 |
. . . . 5
⊢
((log‘2) < ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ↔ -((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2)) |
74 | 62, 73 | mpbi 220 |
. . . 4
⊢
-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) <
-(log‘2) |
75 | 72 | renegcli 10342 |
. . . . 5
⊢
-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) ∈
ℝ |
76 | 65 | renegcli 10342 |
. . . . 5
⊢
-(log‘2) ∈ ℝ |
77 | | eflt 14847 |
. . . . 5
⊢
((-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) ∈ ℝ ∧
-(log‘2) ∈ ℝ) → (-((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2) ↔
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) <
(exp‘-(log‘2)))) |
78 | 75, 76, 77 | mp2an 708 |
. . . 4
⊢
(-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) < -(log‘2) ↔
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) <
(exp‘-(log‘2))) |
79 | 74, 78 | mpbi 220 |
. . 3
⊢
(exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) <
(exp‘-(log‘2)) |
80 | 65 | recni 10052 |
. . . . 5
⊢
(log‘2) ∈ ℂ |
81 | | efneg 14828 |
. . . . 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 24327 |
. . . . . 6
⊢ (2 ∈
ℝ+ → (exp‘(log‘2)) = 2) |
84 | 63, 83 | ax-mp 5 |
. . . . 5
⊢
(exp‘(log‘2)) = 2 |
85 | 84 | oveq2i 6661 |
. . . 4
⊢ (1 /
(exp‘(log‘2))) = (1 / 2) |
86 | 82, 85 | eqtri 2644 |
. . 3
⊢
(exp‘-(log‘2)) = (1 / 2) |
87 | 79, 86 | breqtri 4678 |
. 2
⊢
(exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (1 / 2) |
88 | 12, 13 | birthdaylem1 24678 |
. . . . . . . 8
⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅)) |
89 | 88 | simp2i 1071 |
. . . . . . 7
⊢ 𝑆 ∈ Fin |
90 | 88 | simp1i 1070 |
. . . . . . 7
⊢ 𝑇 ⊆ 𝑆 |
91 | | ssfi 8180 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ 𝑇 ⊆ 𝑆) → 𝑇 ∈ Fin) |
92 | 89, 90, 91 | mp2an 708 |
. . . . . 6
⊢ 𝑇 ∈ Fin |
93 | | hashcl 13147 |
. . . . . 6
⊢ (𝑇 ∈ Fin →
(#‘𝑇) ∈
ℕ0) |
94 | 92, 93 | ax-mp 5 |
. . . . 5
⊢
(#‘𝑇) ∈
ℕ0 |
95 | 94 | nn0rei 11303 |
. . . 4
⊢
(#‘𝑇) ∈
ℝ |
96 | 88 | simp3i 1072 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑆 ≠ ∅) |
97 | 11, 96 | ax-mp 5 |
. . . . 5
⊢ 𝑆 ≠ ∅ |
98 | | hashnncl 13157 |
. . . . . 6
⊢ (𝑆 ∈ Fin →
((#‘𝑆) ∈ ℕ
↔ 𝑆 ≠
∅)) |
99 | 89, 98 | ax-mp 5 |
. . . . 5
⊢
((#‘𝑆) ∈
ℕ ↔ 𝑆 ≠
∅) |
100 | 97, 99 | mpbir 221 |
. . . 4
⊢
(#‘𝑆) ∈
ℕ |
101 | | nndivre 11056 |
. . . 4
⊢
(((#‘𝑇) ∈
ℝ ∧ (#‘𝑆)
∈ ℕ) → ((#‘𝑇) / (#‘𝑆)) ∈ ℝ) |
102 | 95, 100, 101 | mp2an 708 |
. . 3
⊢
((#‘𝑇) /
(#‘𝑆)) ∈
ℝ |
103 | | reefcl 14817 |
. . . 4
⊢
(-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) ∈ ℝ →
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) ∈
ℝ) |
104 | 75, 103 | ax-mp 5 |
. . 3
⊢
(exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) ∈ ℝ |
105 | | halfre 11246 |
. . 3
⊢ (1 / 2)
∈ ℝ |
106 | 102, 104,
105 | lelttri 10164 |
. 2
⊢
((((#‘𝑇) /
(#‘𝑆)) ≤
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) ∧ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (1 / 2)) → ((#‘𝑇) / (#‘𝑆)) < (1 / 2)) |
107 | 15, 87, 106 | mp2an 708 |
1
⊢
((#‘𝑇) /
(#‘𝑆)) < (1 /
2) |