Proof of Theorem birthday
| Step | Hyp | Ref
| Expression |
| 1 | | birthday.k |
. . . 4
⊢ 𝐾 = ;23 |
| 2 | | 2nn0 12543 |
. . . . 5
⊢ 2 ∈
ℕ0 |
| 3 | | 3nn0 12544 |
. . . . 5
⊢ 3 ∈
ℕ0 |
| 4 | 2, 3 | deccl 12748 |
. . . 4
⊢ ;23 ∈
ℕ0 |
| 5 | 1, 4 | eqeltri 2837 |
. . 3
⊢ 𝐾 ∈
ℕ0 |
| 6 | | birthday.n |
. . . 4
⊢ 𝑁 = ;;365 |
| 7 | | 6nn0 12547 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
| 8 | 3, 7 | deccl 12748 |
. . . . 5
⊢ ;36 ∈
ℕ0 |
| 9 | | 5nn 12352 |
. . . . 5
⊢ 5 ∈
ℕ |
| 10 | 8, 9 | decnncl 12753 |
. . . 4
⊢ ;;365 ∈ ℕ |
| 11 | 6, 10 | eqeltri 2837 |
. . 3
⊢ 𝑁 ∈ ℕ |
| 12 | | birthday.s |
. . . 4
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} |
| 13 | | birthday.t |
. . . 4
⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} |
| 14 | 12, 13 | birthdaylem3 26996 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ ((♯‘𝑇) /
(♯‘𝑆)) ≤
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁))) |
| 15 | 5, 11, 14 | mp2an 692 |
. 2
⊢
((♯‘𝑇) /
(♯‘𝑆)) ≤
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) |
| 16 | | log2ub 26992 |
. . . . . 6
⊢
(log‘2) < (;;253 / ;;365) |
| 17 | 5 | nn0cni 12538 |
. . . . . . . . . . . 12
⊢ 𝐾 ∈ ℂ |
| 18 | 17 | sqvali 14219 |
. . . . . . . . . . 11
⊢ (𝐾↑2) = (𝐾 · 𝐾) |
| 19 | 17 | mulridi 11265 |
. . . . . . . . . . . 12
⊢ (𝐾 · 1) = 𝐾 |
| 20 | 19 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ 𝐾 = (𝐾 · 1) |
| 21 | 18, 20 | oveq12i 7443 |
. . . . . . . . . 10
⊢ ((𝐾↑2) − 𝐾) = ((𝐾 · 𝐾) − (𝐾 · 1)) |
| 22 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 23 | 17, 17, 22 | subdii 11712 |
. . . . . . . . . 10
⊢ (𝐾 · (𝐾 − 1)) = ((𝐾 · 𝐾) − (𝐾 · 1)) |
| 24 | 21, 23 | eqtr4i 2768 |
. . . . . . . . 9
⊢ ((𝐾↑2) − 𝐾) = (𝐾 · (𝐾 − 1)) |
| 25 | 24 | oveq1i 7441 |
. . . . . . . 8
⊢ (((𝐾↑2) − 𝐾) / 2) = ((𝐾 · (𝐾 − 1)) / 2) |
| 26 | 17, 22 | subcli 11585 |
. . . . . . . . 9
⊢ (𝐾 − 1) ∈
ℂ |
| 27 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 28 | | 2ne0 12370 |
. . . . . . . . 9
⊢ 2 ≠
0 |
| 29 | 17, 26, 27, 28 | divassi 12023 |
. . . . . . . 8
⊢ ((𝐾 · (𝐾 − 1)) / 2) = (𝐾 · ((𝐾 − 1) / 2)) |
| 30 | | 1nn0 12542 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
| 31 | 2, 2 | deccl 12748 |
. . . . . . . . . . . . 13
⊢ ;22 ∈
ℕ0 |
| 32 | 31 | nn0cni 12538 |
. . . . . . . . . . . 12
⊢ ;22 ∈ ℂ |
| 33 | | 2p1e3 12408 |
. . . . . . . . . . . . . 14
⊢ (2 + 1) =
3 |
| 34 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ ;22 = ;22 |
| 35 | 2, 2, 33, 34 | decsuc 12764 |
. . . . . . . . . . . . 13
⊢ (;22 + 1) = ;23 |
| 36 | 1, 35 | eqtr4i 2768 |
. . . . . . . . . . . 12
⊢ 𝐾 = (;22 + 1) |
| 37 | 32, 22, 36 | mvrraddi 11525 |
. . . . . . . . . . 11
⊢ (𝐾 − 1) = ;22 |
| 38 | 37 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((𝐾 − 1) / 2) = (;22 / 2) |
| 39 | 2 | 11multnc 12801 |
. . . . . . . . . . 11
⊢ (2
· ;11) = ;22 |
| 40 | 30, 30 | deccl 12748 |
. . . . . . . . . . . . 13
⊢ ;11 ∈
ℕ0 |
| 41 | 40 | nn0cni 12538 |
. . . . . . . . . . . 12
⊢ ;11 ∈ ℂ |
| 42 | 32, 27, 41, 28 | divmuli 12021 |
. . . . . . . . . . 11
⊢ ((;22 / 2) = ;11 ↔ (2 · ;11) = ;22) |
| 43 | 39, 42 | mpbir 231 |
. . . . . . . . . 10
⊢ (;22 / 2) = ;11 |
| 44 | 38, 43 | eqtri 2765 |
. . . . . . . . 9
⊢ ((𝐾 − 1) / 2) = ;11 |
| 45 | 19, 1 | eqtri 2765 |
. . . . . . . . . 10
⊢ (𝐾 · 1) = ;23 |
| 46 | | 3p2e5 12417 |
. . . . . . . . . 10
⊢ (3 + 2) =
5 |
| 47 | 2, 3, 2, 45, 46 | decaddi 12793 |
. . . . . . . . 9
⊢ ((𝐾 · 1) + 2) = ;25 |
| 48 | 5, 30, 30, 44, 3, 2, 47, 45 | decmul2c 12799 |
. . . . . . . 8
⊢ (𝐾 · ((𝐾 − 1) / 2)) = ;;253 |
| 49 | 25, 29, 48 | 3eqtri 2769 |
. . . . . . 7
⊢ (((𝐾↑2) − 𝐾) / 2) = ;;253 |
| 50 | 49, 6 | oveq12i 7443 |
. . . . . 6
⊢ ((((𝐾↑2) − 𝐾) / 2) / 𝑁) = (;;253 /
;;365) |
| 51 | 16, 50 | breqtrri 5170 |
. . . . 5
⊢
(log‘2) < ((((𝐾↑2) − 𝐾) / 2) / 𝑁) |
| 52 | | 2rp 13039 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
| 53 | | relogcl 26617 |
. . . . . . 7
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
| 54 | 52, 53 | ax-mp 5 |
. . . . . 6
⊢
(log‘2) ∈ ℝ |
| 55 | | 5nn0 12546 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ0 |
| 56 | 2, 55 | deccl 12748 |
. . . . . . . . . 10
⊢ ;25 ∈
ℕ0 |
| 57 | 56, 3 | deccl 12748 |
. . . . . . . . 9
⊢ ;;253 ∈ ℕ0 |
| 58 | 49, 57 | eqeltri 2837 |
. . . . . . . 8
⊢ (((𝐾↑2) − 𝐾) / 2) ∈
ℕ0 |
| 59 | 58 | nn0rei 12537 |
. . . . . . 7
⊢ (((𝐾↑2) − 𝐾) / 2) ∈
ℝ |
| 60 | | nndivre 12307 |
. . . . . . 7
⊢
(((((𝐾↑2)
− 𝐾) / 2) ∈
ℝ ∧ 𝑁 ∈
ℕ) → ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ) |
| 61 | 59, 11, 60 | mp2an 692 |
. . . . . 6
⊢ ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ∈ ℝ |
| 62 | 54, 61 | ltnegi 11807 |
. . . . 5
⊢
((log‘2) < ((((𝐾↑2) − 𝐾) / 2) / 𝑁) ↔ -((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2)) |
| 63 | 51, 62 | mpbi 230 |
. . . 4
⊢
-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) <
-(log‘2) |
| 64 | 61 | renegcli 11570 |
. . . . 5
⊢
-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) ∈
ℝ |
| 65 | 54 | renegcli 11570 |
. . . . 5
⊢
-(log‘2) ∈ ℝ |
| 66 | | eflt 16153 |
. . . . 5
⊢
((-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) ∈ ℝ ∧
-(log‘2) ∈ ℝ) → (-((((𝐾↑2) − 𝐾) / 2) / 𝑁) < -(log‘2) ↔
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) <
(exp‘-(log‘2)))) |
| 67 | 64, 65, 66 | mp2an 692 |
. . . 4
⊢
(-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) < -(log‘2) ↔
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) <
(exp‘-(log‘2))) |
| 68 | 63, 67 | mpbi 230 |
. . 3
⊢
(exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) <
(exp‘-(log‘2)) |
| 69 | 54 | recni 11275 |
. . . . 5
⊢
(log‘2) ∈ ℂ |
| 70 | | efneg 16134 |
. . . . 5
⊢
((log‘2) ∈ ℂ → (exp‘-(log‘2)) = (1 /
(exp‘(log‘2)))) |
| 71 | 69, 70 | ax-mp 5 |
. . . 4
⊢
(exp‘-(log‘2)) = (1 /
(exp‘(log‘2))) |
| 72 | | reeflog 26622 |
. . . . . 6
⊢ (2 ∈
ℝ+ → (exp‘(log‘2)) = 2) |
| 73 | 52, 72 | ax-mp 5 |
. . . . 5
⊢
(exp‘(log‘2)) = 2 |
| 74 | 73 | oveq2i 7442 |
. . . 4
⊢ (1 /
(exp‘(log‘2))) = (1 / 2) |
| 75 | 71, 74 | eqtri 2765 |
. . 3
⊢
(exp‘-(log‘2)) = (1 / 2) |
| 76 | 68, 75 | breqtri 5168 |
. 2
⊢
(exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (1 / 2) |
| 77 | 12, 13 | birthdaylem1 26994 |
. . . . . . . 8
⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅)) |
| 78 | 77 | simp2i 1141 |
. . . . . . 7
⊢ 𝑆 ∈ Fin |
| 79 | 77 | simp1i 1140 |
. . . . . . 7
⊢ 𝑇 ⊆ 𝑆 |
| 80 | | ssfi 9213 |
. . . . . . 7
⊢ ((𝑆 ∈ Fin ∧ 𝑇 ⊆ 𝑆) → 𝑇 ∈ Fin) |
| 81 | 78, 79, 80 | mp2an 692 |
. . . . . 6
⊢ 𝑇 ∈ Fin |
| 82 | | hashcl 14395 |
. . . . . 6
⊢ (𝑇 ∈ Fin →
(♯‘𝑇) ∈
ℕ0) |
| 83 | 81, 82 | ax-mp 5 |
. . . . 5
⊢
(♯‘𝑇)
∈ ℕ0 |
| 84 | 83 | nn0rei 12537 |
. . . 4
⊢
(♯‘𝑇)
∈ ℝ |
| 85 | 77 | simp3i 1142 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑆 ≠ ∅) |
| 86 | 11, 85 | ax-mp 5 |
. . . . 5
⊢ 𝑆 ≠ ∅ |
| 87 | | hashnncl 14405 |
. . . . . 6
⊢ (𝑆 ∈ Fin →
((♯‘𝑆) ∈
ℕ ↔ 𝑆 ≠
∅)) |
| 88 | 78, 87 | ax-mp 5 |
. . . . 5
⊢
((♯‘𝑆)
∈ ℕ ↔ 𝑆
≠ ∅) |
| 89 | 86, 88 | mpbir 231 |
. . . 4
⊢
(♯‘𝑆)
∈ ℕ |
| 90 | | nndivre 12307 |
. . . 4
⊢
(((♯‘𝑇)
∈ ℝ ∧ (♯‘𝑆) ∈ ℕ) →
((♯‘𝑇) /
(♯‘𝑆)) ∈
ℝ) |
| 91 | 84, 89, 90 | mp2an 692 |
. . 3
⊢
((♯‘𝑇) /
(♯‘𝑆)) ∈
ℝ |
| 92 | | reefcl 16123 |
. . . 4
⊢
(-((((𝐾↑2)
− 𝐾) / 2) / 𝑁) ∈ ℝ →
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) ∈
ℝ) |
| 93 | 64, 92 | ax-mp 5 |
. . 3
⊢
(exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) ∈ ℝ |
| 94 | | halfre 12480 |
. . 3
⊢ (1 / 2)
∈ ℝ |
| 95 | 91, 93, 94 | lelttri 11388 |
. 2
⊢
((((♯‘𝑇)
/ (♯‘𝑆)) ≤
(exp‘-((((𝐾↑2)
− 𝐾) / 2) / 𝑁)) ∧ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)) < (1 / 2)) →
((♯‘𝑇) /
(♯‘𝑆)) < (1
/ 2)) |
| 96 | 15, 76, 95 | mp2an 692 |
1
⊢
((♯‘𝑇) /
(♯‘𝑆)) < (1
/ 2) |