Step | Hyp | Ref
| Expression |
1 | | nnnn0 12481 |
. . . . . . 7
β’ (π β β β π β
β0) |
2 | | derang.d |
. . . . . . . . 9
β’ π· = (π₯ β Fin β¦ (β―β{π β£ (π:π₯β1-1-ontoβπ₯ β§ βπ¦ β π₯ (πβπ¦) β π¦)})) |
3 | | subfac.n |
. . . . . . . . 9
β’ π = (π β β0 β¦ (π·β(1...π))) |
4 | 2, 3 | subfacf 34235 |
. . . . . . . 8
β’ π:β0βΆβ0 |
5 | 4 | ffvelcdmi 7085 |
. . . . . . 7
β’ (π β β0
β (πβπ) β
β0) |
6 | 1, 5 | syl 17 |
. . . . . 6
β’ (π β β β (πβπ) β
β0) |
7 | 6 | nn0zd 12586 |
. . . . 5
β’ (π β β β (πβπ) β β€) |
8 | 7 | zred 12668 |
. . . 4
β’ (π β β β (πβπ) β β) |
9 | | faccl 14245 |
. . . . . . . 8
β’ (π β β0
β (!βπ) β
β) |
10 | 1, 9 | syl 17 |
. . . . . . 7
β’ (π β β β
(!βπ) β
β) |
11 | 10 | nnred 12229 |
. . . . . 6
β’ (π β β β
(!βπ) β
β) |
12 | | epr 16153 |
. . . . . 6
β’ e β
β+ |
13 | | rerpdivcl 13006 |
. . . . . 6
β’
(((!βπ) β
β β§ e β β+) β ((!βπ) / e) β β) |
14 | 11, 12, 13 | sylancl 586 |
. . . . 5
β’ (π β β β
((!βπ) / e) β
β) |
15 | | halfre 12428 |
. . . . 5
β’ (1 / 2)
β β |
16 | | readdcl 11195 |
. . . . 5
β’
((((!βπ) / e)
β β β§ (1 / 2) β β) β (((!βπ) / e) + (1 / 2)) β
β) |
17 | 14, 15, 16 | sylancl 586 |
. . . 4
β’ (π β β β
(((!βπ) / e) + (1 /
2)) β β) |
18 | | elnn1uz2 12911 |
. . . . . . . 8
β’ (π β β β (π = 1 β¨ π β
(β€β₯β2))) |
19 | | fveq2 6891 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β (!βπ) =
(!β1)) |
20 | | fac1 14239 |
. . . . . . . . . . . . . . . 16
β’
(!β1) = 1 |
21 | 19, 20 | eqtrdi 2788 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (!βπ) = 1) |
22 | 21 | oveq1d 7426 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ((!βπ) / e) = (1 /
e)) |
23 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (πβπ) = (πβ1)) |
24 | 2, 3 | subfac1 34238 |
. . . . . . . . . . . . . . 15
β’ (πβ1) = 0 |
25 | 23, 24 | eqtrdi 2788 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (πβπ) = 0) |
26 | 22, 25 | oveq12d 7429 |
. . . . . . . . . . . . 13
β’ (π = 1 β (((!βπ) / e) β (πβπ)) = ((1 / e) β 0)) |
27 | | rpreccl 13002 |
. . . . . . . . . . . . . . . . 17
β’ (e β
β+ β (1 / e) β β+) |
28 | 12, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (1 / e)
β β+ |
29 | | rpre 12984 |
. . . . . . . . . . . . . . . 16
β’ ((1 / e)
β β+ β (1 / e) β β) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (1 / e)
β β |
31 | 30 | recni 11230 |
. . . . . . . . . . . . . 14
β’ (1 / e)
β β |
32 | 31 | subid1i 11534 |
. . . . . . . . . . . . 13
β’ ((1 / e)
β 0) = (1 / e) |
33 | 26, 32 | eqtrdi 2788 |
. . . . . . . . . . . 12
β’ (π = 1 β (((!βπ) / e) β (πβπ)) = (1 / e)) |
34 | 33 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (π = 1 β
(absβ(((!βπ) /
e) β (πβπ))) = (absβ(1 /
e))) |
35 | | rpge0 12989 |
. . . . . . . . . . . . 13
β’ ((1 / e)
β β+ β 0 β€ (1 / e)) |
36 | 28, 35 | ax-mp 5 |
. . . . . . . . . . . 12
β’ 0 β€ (1
/ e) |
37 | | absid 15245 |
. . . . . . . . . . . 12
β’ (((1 / e)
β β β§ 0 β€ (1 / e)) β (absβ(1 / e)) = (1 /
e)) |
38 | 30, 36, 37 | mp2an 690 |
. . . . . . . . . . 11
β’
(absβ(1 / e)) = (1 / e) |
39 | 34, 38 | eqtrdi 2788 |
. . . . . . . . . 10
β’ (π = 1 β
(absβ(((!βπ) /
e) β (πβπ))) = (1 / e)) |
40 | | egt2lt3 16151 |
. . . . . . . . . . . 12
β’ (2 < e
β§ e < 3) |
41 | 40 | simpli 484 |
. . . . . . . . . . 11
β’ 2 <
e |
42 | | 2re 12288 |
. . . . . . . . . . . 12
β’ 2 β
β |
43 | | ere 16034 |
. . . . . . . . . . . 12
β’ e β
β |
44 | | 2pos 12317 |
. . . . . . . . . . . 12
β’ 0 <
2 |
45 | | epos 16152 |
. . . . . . . . . . . 12
β’ 0 <
e |
46 | 42, 43, 44, 45 | ltrecii 12132 |
. . . . . . . . . . 11
β’ (2 < e
β (1 / e) < (1 / 2)) |
47 | 41, 46 | mpbi 229 |
. . . . . . . . . 10
β’ (1 / e)
< (1 / 2) |
48 | 39, 47 | eqbrtrdi 5187 |
. . . . . . . . 9
β’ (π = 1 β
(absβ(((!βπ) /
e) β (πβπ))) < (1 /
2)) |
49 | | eluz2nn 12870 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β π β β) |
50 | 14, 8 | resubcld 11644 |
. . . . . . . . . . . . 13
β’ (π β β β
(((!βπ) / e) β
(πβπ)) β β) |
51 | 50 | recnd 11244 |
. . . . . . . . . . . 12
β’ (π β β β
(((!βπ) / e) β
(πβπ)) β β) |
52 | 49, 51 | syl 17 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (((!βπ) / e) β (πβπ)) β β) |
53 | 52 | abscld 15385 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (absβ(((!βπ) / e) β (πβπ))) β β) |
54 | 49 | nnrecred 12265 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (1 / π) β β) |
55 | 15 | a1i 11 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (1 / 2) β
β) |
56 | 2, 3 | subfaclim 34248 |
. . . . . . . . . . 11
β’ (π β β β
(absβ(((!βπ) /
e) β (πβπ))) < (1 / π)) |
57 | 49, 56 | syl 17 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (absβ(((!βπ) / e) β (πβπ))) < (1 / π)) |
58 | | eluzle 12837 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β 2 β€ π) |
59 | | nnre 12221 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
60 | | nngt0 12245 |
. . . . . . . . . . . . 13
β’ (π β β β 0 <
π) |
61 | | lerec 12099 |
. . . . . . . . . . . . . 14
β’ (((2
β β β§ 0 < 2) β§ (π β β β§ 0 < π)) β (2 β€ π β (1 / π) β€ (1 / 2))) |
62 | 42, 44, 61 | mpanl12 700 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 <
π) β (2 β€ π β (1 / π) β€ (1 / 2))) |
63 | 59, 60, 62 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β β β (2 β€
π β (1 / π) β€ (1 /
2))) |
64 | 49, 63 | syl 17 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (2 β€ π β (1 / π) β€ (1 / 2))) |
65 | 58, 64 | mpbid 231 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (1 / π) β€ (1 / 2)) |
66 | 53, 54, 55, 57, 65 | ltletrd 11376 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β (absβ(((!βπ) / e) β (πβπ))) < (1 / 2)) |
67 | 48, 66 | jaoi 855 |
. . . . . . . 8
β’ ((π = 1 β¨ π β (β€β₯β2))
β (absβ(((!βπ) / e) β (πβπ))) < (1 / 2)) |
68 | 18, 67 | sylbi 216 |
. . . . . . 7
β’ (π β β β
(absβ(((!βπ) /
e) β (πβπ))) < (1 /
2)) |
69 | 15 | a1i 11 |
. . . . . . . 8
β’ (π β β β (1 / 2)
β β) |
70 | 14, 8, 69 | absdifltd 15382 |
. . . . . . 7
β’ (π β β β
((absβ(((!βπ) /
e) β (πβπ))) < (1 / 2) β (((πβπ) β (1 / 2)) < ((!βπ) / e) β§ ((!βπ) / e) < ((πβπ) + (1 / 2))))) |
71 | 68, 70 | mpbid 231 |
. . . . . 6
β’ (π β β β (((πβπ) β (1 / 2)) < ((!βπ) / e) β§ ((!βπ) / e) < ((πβπ) + (1 / 2)))) |
72 | 71 | simpld 495 |
. . . . 5
β’ (π β β β ((πβπ) β (1 / 2)) < ((!βπ) / e)) |
73 | 8, 69, 14 | ltsubaddd 11812 |
. . . . 5
β’ (π β β β (((πβπ) β (1 / 2)) < ((!βπ) / e) β (πβπ) < (((!βπ) / e) + (1 / 2)))) |
74 | 72, 73 | mpbid 231 |
. . . 4
β’ (π β β β (πβπ) < (((!βπ) / e) + (1 / 2))) |
75 | 8, 17, 74 | ltled 11364 |
. . 3
β’ (π β β β (πβπ) β€ (((!βπ) / e) + (1 / 2))) |
76 | | readdcl 11195 |
. . . . . 6
β’ (((πβπ) β β β§ (1 / 2) β
β) β ((πβπ) + (1 / 2)) β
β) |
77 | 8, 15, 76 | sylancl 586 |
. . . . 5
β’ (π β β β ((πβπ) + (1 / 2)) β
β) |
78 | 71 | simprd 496 |
. . . . 5
β’ (π β β β
((!βπ) / e) <
((πβπ) + (1 / 2))) |
79 | 14, 77, 69, 78 | ltadd1dd 11827 |
. . . 4
β’ (π β β β
(((!βπ) / e) + (1 /
2)) < (((πβπ) + (1 / 2)) + (1 /
2))) |
80 | 8 | recnd 11244 |
. . . . . 6
β’ (π β β β (πβπ) β β) |
81 | 69 | recnd 11244 |
. . . . . 6
β’ (π β β β (1 / 2)
β β) |
82 | 80, 81, 81 | addassd 11238 |
. . . . 5
β’ (π β β β (((πβπ) + (1 / 2)) + (1 / 2)) = ((πβπ) + ((1 / 2) + (1 / 2)))) |
83 | | ax-1cn 11170 |
. . . . . . 7
β’ 1 β
β |
84 | | 2halves 12442 |
. . . . . . 7
β’ (1 β
β β ((1 / 2) + (1 / 2)) = 1) |
85 | 83, 84 | ax-mp 5 |
. . . . . 6
β’ ((1 / 2)
+ (1 / 2)) = 1 |
86 | 85 | oveq2i 7422 |
. . . . 5
β’ ((πβπ) + ((1 / 2) + (1 / 2))) = ((πβπ) + 1) |
87 | 82, 86 | eqtrdi 2788 |
. . . 4
β’ (π β β β (((πβπ) + (1 / 2)) + (1 / 2)) = ((πβπ) + 1)) |
88 | 79, 87 | breqtrd 5174 |
. . 3
β’ (π β β β
(((!βπ) / e) + (1 /
2)) < ((πβπ) + 1)) |
89 | | flbi 13783 |
. . . 4
β’
(((((!βπ) / e)
+ (1 / 2)) β β β§ (πβπ) β β€) β
((ββ(((!βπ) / e) + (1 / 2))) = (πβπ) β ((πβπ) β€ (((!βπ) / e) + (1 / 2)) β§ (((!βπ) / e) + (1 / 2)) < ((πβπ) + 1)))) |
90 | 17, 7, 89 | syl2anc 584 |
. . 3
β’ (π β β β
((ββ(((!βπ) / e) + (1 / 2))) = (πβπ) β ((πβπ) β€ (((!βπ) / e) + (1 / 2)) β§ (((!βπ) / e) + (1 / 2)) < ((πβπ) + 1)))) |
91 | 75, 88, 90 | mpbir2and 711 |
. 2
β’ (π β β β
(ββ(((!βπ) / e) + (1 / 2))) = (πβπ)) |
92 | 91 | eqcomd 2738 |
1
β’ (π β β β (πβπ) = (ββ(((!βπ) / e) + (1 /
2)))) |