Step | Hyp | Ref
| Expression |
1 | | birthday.k |
. . . 4
โข ๐พ = ;23 |
2 | | 2nn0 12437 |
. . . . 5
โข 2 โ
โ0 |
3 | | 3nn0 12438 |
. . . . 5
โข 3 โ
โ0 |
4 | 2, 3 | deccl 12640 |
. . . 4
โข ;23 โ
โ0 |
5 | 1, 4 | eqeltri 2834 |
. . 3
โข ๐พ โ
โ0 |
6 | | birthday.n |
. . . 4
โข ๐ = ;;365 |
7 | | 6nn0 12441 |
. . . . . 6
โข 6 โ
โ0 |
8 | 3, 7 | deccl 12640 |
. . . . 5
โข ;36 โ
โ0 |
9 | | 5nn 12246 |
. . . . 5
โข 5 โ
โ |
10 | 8, 9 | decnncl 12645 |
. . . 4
โข ;;365 โ โ |
11 | 6, 10 | eqeltri 2834 |
. . 3
โข ๐ โ โ |
12 | | birthday.s |
. . . 4
โข ๐ = {๐ โฃ ๐:(1...๐พ)โถ(1...๐)} |
13 | | birthday.t |
. . . 4
โข ๐ = {๐ โฃ ๐:(1...๐พ)โ1-1โ(1...๐)} |
14 | 12, 13 | birthdaylem3 26319 |
. . 3
โข ((๐พ โ โ0
โง ๐ โ โ)
โ ((โฏโ๐) /
(โฏโ๐)) โค
(expโ-((((๐พโ2)
โ ๐พ) / 2) / ๐))) |
15 | 5, 11, 14 | mp2an 691 |
. 2
โข
((โฏโ๐) /
(โฏโ๐)) โค
(expโ-((((๐พโ2)
โ ๐พ) / 2) / ๐)) |
16 | | log2ub 26315 |
. . . . . 6
โข
(logโ2) < (;;253 / ;;365) |
17 | 5 | nn0cni 12432 |
. . . . . . . . . . . 12
โข ๐พ โ โ |
18 | 17 | sqvali 14091 |
. . . . . . . . . . 11
โข (๐พโ2) = (๐พ ยท ๐พ) |
19 | 17 | mulid1i 11166 |
. . . . . . . . . . . 12
โข (๐พ ยท 1) = ๐พ |
20 | 19 | eqcomi 2746 |
. . . . . . . . . . 11
โข ๐พ = (๐พ ยท 1) |
21 | 18, 20 | oveq12i 7374 |
. . . . . . . . . 10
โข ((๐พโ2) โ ๐พ) = ((๐พ ยท ๐พ) โ (๐พ ยท 1)) |
22 | | ax-1cn 11116 |
. . . . . . . . . . 11
โข 1 โ
โ |
23 | 17, 17, 22 | subdii 11611 |
. . . . . . . . . 10
โข (๐พ ยท (๐พ โ 1)) = ((๐พ ยท ๐พ) โ (๐พ ยท 1)) |
24 | 21, 23 | eqtr4i 2768 |
. . . . . . . . 9
โข ((๐พโ2) โ ๐พ) = (๐พ ยท (๐พ โ 1)) |
25 | 24 | oveq1i 7372 |
. . . . . . . 8
โข (((๐พโ2) โ ๐พ) / 2) = ((๐พ ยท (๐พ โ 1)) / 2) |
26 | 17, 22 | subcli 11484 |
. . . . . . . . 9
โข (๐พ โ 1) โ
โ |
27 | | 2cn 12235 |
. . . . . . . . 9
โข 2 โ
โ |
28 | | 2ne0 12264 |
. . . . . . . . 9
โข 2 โ
0 |
29 | 17, 26, 27, 28 | divassi 11918 |
. . . . . . . 8
โข ((๐พ ยท (๐พ โ 1)) / 2) = (๐พ ยท ((๐พ โ 1) / 2)) |
30 | | 1nn0 12436 |
. . . . . . . . 9
โข 1 โ
โ0 |
31 | 2, 2 | deccl 12640 |
. . . . . . . . . . . . 13
โข ;22 โ
โ0 |
32 | 31 | nn0cni 12432 |
. . . . . . . . . . . 12
โข ;22 โ โ |
33 | | 2p1e3 12302 |
. . . . . . . . . . . . . 14
โข (2 + 1) =
3 |
34 | | eqid 2737 |
. . . . . . . . . . . . . 14
โข ;22 = ;22 |
35 | 2, 2, 33, 34 | decsuc 12656 |
. . . . . . . . . . . . 13
โข (;22 + 1) = ;23 |
36 | 1, 35 | eqtr4i 2768 |
. . . . . . . . . . . 12
โข ๐พ = (;22 + 1) |
37 | 32, 22, 36 | mvrraddi 11425 |
. . . . . . . . . . 11
โข (๐พ โ 1) = ;22 |
38 | 37 | oveq1i 7372 |
. . . . . . . . . 10
โข ((๐พ โ 1) / 2) = (;22 / 2) |
39 | 2 | 11multnc 12693 |
. . . . . . . . . . 11
โข (2
ยท ;11) = ;22 |
40 | 30, 30 | deccl 12640 |
. . . . . . . . . . . . 13
โข ;11 โ
โ0 |
41 | 40 | nn0cni 12432 |
. . . . . . . . . . . 12
โข ;11 โ โ |
42 | 32, 27, 41, 28 | divmuli 11916 |
. . . . . . . . . . 11
โข ((;22 / 2) = ;11 โ (2 ยท ;11) = ;22) |
43 | 39, 42 | mpbir 230 |
. . . . . . . . . 10
โข (;22 / 2) = ;11 |
44 | 38, 43 | eqtri 2765 |
. . . . . . . . 9
โข ((๐พ โ 1) / 2) = ;11 |
45 | 19, 1 | eqtri 2765 |
. . . . . . . . . 10
โข (๐พ ยท 1) = ;23 |
46 | | 3p2e5 12311 |
. . . . . . . . . 10
โข (3 + 2) =
5 |
47 | 2, 3, 2, 45, 46 | decaddi 12685 |
. . . . . . . . 9
โข ((๐พ ยท 1) + 2) = ;25 |
48 | 5, 30, 30, 44, 3, 2, 47, 45 | decmul2c 12691 |
. . . . . . . 8
โข (๐พ ยท ((๐พ โ 1) / 2)) = ;;253 |
49 | 25, 29, 48 | 3eqtri 2769 |
. . . . . . 7
โข (((๐พโ2) โ ๐พ) / 2) = ;;253 |
50 | 49, 6 | oveq12i 7374 |
. . . . . 6
โข ((((๐พโ2) โ ๐พ) / 2) / ๐) = (;;253 /
;;365) |
51 | 16, 50 | breqtrri 5137 |
. . . . 5
โข
(logโ2) < ((((๐พโ2) โ ๐พ) / 2) / ๐) |
52 | | 2rp 12927 |
. . . . . . 7
โข 2 โ
โ+ |
53 | | relogcl 25947 |
. . . . . . 7
โข (2 โ
โ+ โ (logโ2) โ โ) |
54 | 52, 53 | ax-mp 5 |
. . . . . 6
โข
(logโ2) โ โ |
55 | | 5nn0 12440 |
. . . . . . . . . . 11
โข 5 โ
โ0 |
56 | 2, 55 | deccl 12640 |
. . . . . . . . . 10
โข ;25 โ
โ0 |
57 | 56, 3 | deccl 12640 |
. . . . . . . . 9
โข ;;253 โ โ0 |
58 | 49, 57 | eqeltri 2834 |
. . . . . . . 8
โข (((๐พโ2) โ ๐พ) / 2) โ
โ0 |
59 | 58 | nn0rei 12431 |
. . . . . . 7
โข (((๐พโ2) โ ๐พ) / 2) โ
โ |
60 | | nndivre 12201 |
. . . . . . 7
โข
(((((๐พโ2)
โ ๐พ) / 2) โ
โ โง ๐ โ
โ) โ ((((๐พโ2) โ ๐พ) / 2) / ๐) โ โ) |
61 | 59, 11, 60 | mp2an 691 |
. . . . . 6
โข ((((๐พโ2) โ ๐พ) / 2) / ๐) โ โ |
62 | 54, 61 | ltnegi 11706 |
. . . . 5
โข
((logโ2) < ((((๐พโ2) โ ๐พ) / 2) / ๐) โ -((((๐พโ2) โ ๐พ) / 2) / ๐) < -(logโ2)) |
63 | 51, 62 | mpbi 229 |
. . . 4
โข
-((((๐พโ2)
โ ๐พ) / 2) / ๐) <
-(logโ2) |
64 | 61 | renegcli 11469 |
. . . . 5
โข
-((((๐พโ2)
โ ๐พ) / 2) / ๐) โ
โ |
65 | 54 | renegcli 11469 |
. . . . 5
โข
-(logโ2) โ โ |
66 | | eflt 16006 |
. . . . 5
โข
((-((((๐พโ2)
โ ๐พ) / 2) / ๐) โ โ โง
-(logโ2) โ โ) โ (-((((๐พโ2) โ ๐พ) / 2) / ๐) < -(logโ2) โ
(expโ-((((๐พโ2)
โ ๐พ) / 2) / ๐)) <
(expโ-(logโ2)))) |
67 | 64, 65, 66 | mp2an 691 |
. . . 4
โข
(-((((๐พโ2)
โ ๐พ) / 2) / ๐) < -(logโ2) โ
(expโ-((((๐พโ2)
โ ๐พ) / 2) / ๐)) <
(expโ-(logโ2))) |
68 | 63, 67 | mpbi 229 |
. . 3
โข
(expโ-((((๐พโ2) โ ๐พ) / 2) / ๐)) <
(expโ-(logโ2)) |
69 | 54 | recni 11176 |
. . . . 5
โข
(logโ2) โ โ |
70 | | efneg 15987 |
. . . . 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 25952 |
. . . . . 6
โข (2 โ
โ+ โ (expโ(logโ2)) = 2) |
73 | 52, 72 | ax-mp 5 |
. . . . 5
โข
(expโ(logโ2)) = 2 |
74 | 73 | oveq2i 7373 |
. . . 4
โข (1 /
(expโ(logโ2))) = (1 / 2) |
75 | 71, 74 | eqtri 2765 |
. . 3
โข
(expโ-(logโ2)) = (1 / 2) |
76 | 68, 75 | breqtri 5135 |
. 2
โข
(expโ-((((๐พโ2) โ ๐พ) / 2) / ๐)) < (1 / 2) |
77 | 12, 13 | birthdaylem1 26317 |
. . . . . . . 8
โข (๐ โ ๐ โง ๐ โ Fin โง (๐ โ โ โ ๐ โ โ
)) |
78 | 77 | simp2i 1141 |
. . . . . . 7
โข ๐ โ Fin |
79 | 77 | simp1i 1140 |
. . . . . . 7
โข ๐ โ ๐ |
80 | | ssfi 9124 |
. . . . . . 7
โข ((๐ โ Fin โง ๐ โ ๐) โ ๐ โ Fin) |
81 | 78, 79, 80 | mp2an 691 |
. . . . . 6
โข ๐ โ Fin |
82 | | hashcl 14263 |
. . . . . 6
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
83 | 81, 82 | ax-mp 5 |
. . . . 5
โข
(โฏโ๐)
โ โ0 |
84 | 83 | nn0rei 12431 |
. . . 4
โข
(โฏโ๐)
โ โ |
85 | 77 | simp3i 1142 |
. . . . . 6
โข (๐ โ โ โ ๐ โ โ
) |
86 | 11, 85 | ax-mp 5 |
. . . . 5
โข ๐ โ โ
|
87 | | hashnncl 14273 |
. . . . . 6
โข (๐ โ Fin โ
((โฏโ๐) โ
โ โ ๐ โ
โ
)) |
88 | 78, 87 | ax-mp 5 |
. . . . 5
โข
((โฏโ๐)
โ โ โ ๐
โ โ
) |
89 | 86, 88 | mpbir 230 |
. . . 4
โข
(โฏโ๐)
โ โ |
90 | | nndivre 12201 |
. . . 4
โข
(((โฏโ๐)
โ โ โง (โฏโ๐) โ โ) โ
((โฏโ๐) /
(โฏโ๐)) โ
โ) |
91 | 84, 89, 90 | mp2an 691 |
. . 3
โข
((โฏโ๐) /
(โฏโ๐)) โ
โ |
92 | | reefcl 15976 |
. . . 4
โข
(-((((๐พโ2)
โ ๐พ) / 2) / ๐) โ โ โ
(expโ-((((๐พโ2)
โ ๐พ) / 2) / ๐)) โ
โ) |
93 | 64, 92 | ax-mp 5 |
. . 3
โข
(expโ-((((๐พโ2) โ ๐พ) / 2) / ๐)) โ โ |
94 | | halfre 12374 |
. . 3
โข (1 / 2)
โ โ |
95 | 91, 93, 94 | lelttri 11289 |
. 2
โข
((((โฏโ๐)
/ (โฏโ๐)) โค
(expโ-((((๐พโ2)
โ ๐พ) / 2) / ๐)) โง (expโ-((((๐พโ2) โ ๐พ) / 2) / ๐)) < (1 / 2)) โ
((โฏโ๐) /
(โฏโ๐)) < (1
/ 2)) |
96 | 15, 76, 95 | mp2an 691 |
1
โข
((โฏโ๐) /
(โฏโ๐)) < (1
/ 2) |