Step | Hyp | Ref
| Expression |
1 | | etransclem23.k |
. . . . . 6
β’ πΎ = (πΏ / (!β(π β 1))) |
2 | | etransclem23.l |
. . . . . . 7
β’ πΏ = Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) |
3 | 2 | oveq1i 7372 |
. . . . . 6
β’ (πΏ / (!β(π β 1))) = (Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) / (!β(π β 1))) |
4 | 1, 3 | eqtri 2765 |
. . . . 5
β’ πΎ = (Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) / (!β(π β 1))) |
5 | 4 | fveq2i 6850 |
. . . 4
β’
(absβπΎ) =
(absβ(Ξ£π β
(0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) / (!β(π β 1)))) |
6 | 5 | a1i 11 |
. . 3
β’ (π β (absβπΎ) = (absβ(Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) / (!β(π β 1))))) |
7 | | fzfid 13885 |
. . . . 5
β’ (π β (0...π) β Fin) |
8 | | etransclem23.a |
. . . . . . . . . 10
β’ (π β π΄:β0βΆβ€) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β π΄:β0βΆβ€) |
10 | | elfznn0 13541 |
. . . . . . . . . 10
β’ (π β (0...π) β π β β0) |
11 | 10 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β π β β0) |
12 | 9, 11 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β (π΄βπ) β β€) |
13 | 12 | zcnd 12615 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (π΄βπ) β β) |
14 | | ere 15978 |
. . . . . . . . . 10
β’ e β
β |
15 | 14 | recni 11176 |
. . . . . . . . 9
β’ e β
β |
16 | 15 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β e β β) |
17 | | elfzelz 13448 |
. . . . . . . . . 10
β’ (π β (0...π) β π β β€) |
18 | 17 | zcnd 12615 |
. . . . . . . . 9
β’ (π β (0...π) β π β β) |
19 | 18 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β β) |
20 | 16, 19 | cxpcld 26079 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (eβππ) β
β) |
21 | 13, 20 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π β (0...π)) β ((π΄βπ) Β· (eβππ)) β
β) |
22 | 15 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β e β β) |
23 | | elioore 13301 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)π) β π₯ β β) |
24 | 23 | recnd 11190 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)π) β π₯ β β) |
25 | 24 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β π₯ β β) |
26 | 25 | negcld 11506 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β -π₯ β β) |
27 | 22, 26 | cxpcld 26079 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (eβπ-π₯) β
β) |
28 | | ax-resscn 11115 |
. . . . . . . . . . . . 13
β’ β
β β |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
30 | | etransclem23.p |
. . . . . . . . . . . 12
β’ (π β π β β) |
31 | | etransclem23.f |
. . . . . . . . . . . 12
β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
32 | 29, 30, 31 | etransclem8 44557 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (0(,)π)) β πΉ:ββΆβ) |
34 | 23 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (0(,)π)) β π₯ β β) |
35 | 33, 34 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π₯ β (0(,)π)) β (πΉβπ₯) β β) |
36 | 35 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (πΉβπ₯) β β) |
37 | 27, 36 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β ((eβπ-π₯) Β· (πΉβπ₯)) β β) |
38 | | reelprrecn 11150 |
. . . . . . . . 9
β’ β
β {β, β} |
39 | 38 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β β β {β,
β}) |
40 | | reopn 43597 |
. . . . . . . . . 10
β’ β
β (topGenβran (,)) |
41 | | eqid 2737 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
42 | 41 | tgioo2 24182 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
43 | 40, 42 | eleqtri 2836 |
. . . . . . . . 9
β’ β
β ((TopOpenββfld) βΎt
β) |
44 | 43 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β β β
((TopOpenββfld) βΎt
β)) |
45 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β β) |
46 | | etransclem23.m |
. . . . . . . . . 10
β’ (π β π β β) |
47 | 46 | nnnn0d 12480 |
. . . . . . . . 9
β’ (π β π β
β0) |
48 | 47 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β
β0) |
49 | | etransclem6 44555 |
. . . . . . . . 9
β’ (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) = (π¦ β β β¦ ((π¦β(π β 1)) Β· ββ β (1...π)((π¦ β β)βπ))) |
50 | | etransclem6 44555 |
. . . . . . . . 9
β’ (π¦ β β β¦ ((π¦β(π β 1)) Β· ββ β (1...π)((π¦ β β)βπ))) = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
51 | 31, 49, 50 | 3eqtri 2769 |
. . . . . . . 8
β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
52 | | 0red 11165 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β 0 β β) |
53 | 17 | zred 12614 |
. . . . . . . . 9
β’ (π β (0...π) β π β β) |
54 | 53 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β β) |
55 | 39, 44, 45, 48, 51, 52, 54 | etransclem18 44567 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (π₯ β (0(,)π) β¦ ((eβπ-π₯) Β· (πΉβπ₯))) β
πΏ1) |
56 | 37, 55 | itgcl 25164 |
. . . . . 6
β’ ((π β§ π β (0...π)) β β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯ β β) |
57 | 21, 56 | mulcld 11182 |
. . . . 5
β’ ((π β§ π β (0...π)) β (((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) β β) |
58 | 7, 57 | fsumcl 15625 |
. . . 4
β’ (π β Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) β β) |
59 | | nnm1nn0 12461 |
. . . . . . 7
β’ (π β β β (π β 1) β
β0) |
60 | 30, 59 | syl 17 |
. . . . . 6
β’ (π β (π β 1) β
β0) |
61 | 60 | faccld 14191 |
. . . . 5
β’ (π β (!β(π β 1)) β
β) |
62 | 61 | nncnd 12176 |
. . . 4
β’ (π β (!β(π β 1)) β
β) |
63 | 61 | nnne0d 12210 |
. . . 4
β’ (π β (!β(π β 1)) β
0) |
64 | 58, 62, 63 | absdivd 15347 |
. . 3
β’ (π β (absβ(Ξ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) / (!β(π β 1)))) = ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (absβ(!β(π β 1))))) |
65 | 61 | nnred 12175 |
. . . . 5
β’ (π β (!β(π β 1)) β
β) |
66 | 61 | nnnn0d 12480 |
. . . . . 6
β’ (π β (!β(π β 1)) β
β0) |
67 | 66 | nn0ge0d 12483 |
. . . . 5
β’ (π β 0 β€ (!β(π β 1))) |
68 | 65, 67 | absidd 15314 |
. . . 4
β’ (π β (absβ(!β(π β 1))) = (!β(π β 1))) |
69 | 68 | oveq2d 7378 |
. . 3
β’ (π β ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (absβ(!β(π β 1)))) = ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (!β(π β 1)))) |
70 | 6, 64, 69 | 3eqtrd 2781 |
. 2
β’ (π β (absβπΎ) = ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (!β(π β 1)))) |
71 | 2, 58 | eqeltrid 2842 |
. . . . . . 7
β’ (π β πΏ β β) |
72 | 71, 62, 63 | divcld 11938 |
. . . . . 6
β’ (π β (πΏ / (!β(π β 1))) β
β) |
73 | 1, 72 | eqeltrid 2842 |
. . . . 5
β’ (π β πΎ β β) |
74 | 73 | abscld 15328 |
. . . 4
β’ (π β (absβπΎ) β
β) |
75 | 70, 74 | eqeltrrd 2839 |
. . 3
β’ (π β ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (!β(π β 1))) β
β) |
76 | 46 | nnred 12175 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
77 | 30 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
78 | 76, 77 | reexpcld 14075 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ) β β) |
79 | | peano2nn0 12460 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β0) |
80 | 47, 79 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π + 1) β
β0) |
81 | 78, 80 | reexpcld 14075 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ)β(π + 1)) β β) |
82 | 81 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ)β(π + 1)) β β) |
83 | 46 | nncnd 12176 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
84 | 82, 83 | mulcomd 11183 |
. . . . . . . . . . . 12
β’ (π β (((πβπ)β(π + 1)) Β· π) = (π Β· ((πβπ)β(π + 1)))) |
85 | 30 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
86 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β) |
87 | 85, 86 | npcand 11523 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π β 1) + 1) = π) |
88 | 87 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ (π β π = ((π β 1) + 1)) |
89 | 88 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π β ((πβ(π + 1))βπ) = ((πβ(π + 1))β((π β 1) + 1))) |
90 | 80 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + 1) β β) |
91 | 90, 85 | mulcomd 11183 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π + 1) Β· π) = (π Β· (π + 1))) |
92 | 91 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ((π + 1) Β· π)) = (πβ(π Β· (π + 1)))) |
93 | 83, 77, 80 | expmuld 14061 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ((π + 1) Β· π)) = ((πβ(π + 1))βπ)) |
94 | 83, 80, 77 | expmuld 14061 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(π Β· (π + 1))) = ((πβπ)β(π + 1))) |
95 | 92, 93, 94 | 3eqtr3d 2785 |
. . . . . . . . . . . . . 14
β’ (π β ((πβ(π + 1))βπ) = ((πβπ)β(π + 1))) |
96 | 76, 80 | reexpcld 14075 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ(π + 1)) β β) |
97 | 96 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(π + 1)) β β) |
98 | 97, 60 | expp1d 14059 |
. . . . . . . . . . . . . 14
β’ (π β ((πβ(π + 1))β((π β 1) + 1)) = (((πβ(π + 1))β(π β 1)) Β· (πβ(π + 1)))) |
99 | 89, 95, 98 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ)β(π + 1)) = (((πβ(π + 1))β(π β 1)) Β· (πβ(π + 1)))) |
100 | 99 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π β (π Β· ((πβπ)β(π + 1))) = (π Β· (((πβ(π + 1))β(π β 1)) Β· (πβ(π + 1))))) |
101 | 97, 60 | expcld 14058 |
. . . . . . . . . . . . . 14
β’ (π β ((πβ(π + 1))β(π β 1)) β
β) |
102 | 83, 101, 97 | mul12d 11371 |
. . . . . . . . . . . . 13
β’ (π β (π Β· (((πβ(π + 1))β(π β 1)) Β· (πβ(π + 1)))) = (((πβ(π + 1))β(π β 1)) Β· (π Β· (πβ(π + 1))))) |
103 | 83, 97 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ (π β (π Β· (πβ(π + 1))) β β) |
104 | 101, 103 | mulcomd 11183 |
. . . . . . . . . . . . 13
β’ (π β (((πβ(π + 1))β(π β 1)) Β· (π Β· (πβ(π + 1)))) = ((π Β· (πβ(π + 1))) Β· ((πβ(π + 1))β(π β 1)))) |
105 | 102, 104 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (π Β· (((πβ(π + 1))β(π β 1)) Β· (πβ(π + 1)))) = ((π Β· (πβ(π + 1))) Β· ((πβ(π + 1))β(π β 1)))) |
106 | 84, 100, 105 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ (π β (((πβπ)β(π + 1)) Β· π) = ((π Β· (πβ(π + 1))) Β· ((πβ(π + 1))β(π β 1)))) |
107 | 106 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (((πβπ)β(π + 1)) Β· π) = ((π Β· (πβ(π + 1))) Β· ((πβ(π + 1))β(π β 1)))) |
108 | 107 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) = ((absβ((π΄βπ) Β· (eβππ))) Β· ((π Β· (πβ(π + 1))) Β· ((πβ(π + 1))β(π β 1))))) |
109 | 21 | abscld 15328 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (absβ((π΄βπ) Β· (eβππ))) β
β) |
110 | 109 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (absβ((π΄βπ) Β· (eβππ))) β
β) |
111 | 103 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (π Β· (πβ(π + 1))) β β) |
112 | 101 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β ((πβ(π + 1))β(π β 1)) β
β) |
113 | 110, 111,
112 | mulassd 11185 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β (((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1))) = ((absβ((π΄βπ) Β· (eβππ))) Β· ((π Β· (πβ(π + 1))) Β· ((πβ(π + 1))β(π β 1))))) |
114 | 108, 113 | eqtr4d 2780 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) = (((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1)))) |
115 | 114 | sumeq2dv 15595 |
. . . . . . 7
β’ (π β Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) = Ξ£π β (0...π)(((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1)))) |
116 | 110, 111 | mulcld 11182 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) β β) |
117 | 7, 101, 116 | fsummulc1 15677 |
. . . . . . 7
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1))) = Ξ£π β (0...π)(((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1)))) |
118 | 115, 117 | eqtr4d 2780 |
. . . . . 6
β’ (π β Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) = (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1)))) |
119 | 118 | oveq1d 7377 |
. . . . 5
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) / (!β(π β 1))) = ((Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1))) / (!β(π β 1)))) |
120 | 7, 116 | fsumcl 15625 |
. . . . . 6
β’ (π β Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) β β) |
121 | 120, 101,
62, 63 | divassd 11973 |
. . . . 5
β’ (π β ((Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· ((πβ(π + 1))β(π β 1))) / (!β(π β 1))) = (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1))))) |
122 | 119, 121 | eqtrd 2777 |
. . . 4
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) / (!β(π β 1))) = (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1))))) |
123 | 81 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((πβπ)β(π + 1)) β β) |
124 | 76 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β β) |
125 | 123, 124 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (((πβπ)β(π + 1)) Β· π) β β) |
126 | 109, 125 | remulcld 11192 |
. . . . . 6
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) β β) |
127 | 7, 126 | fsumrecl 15626 |
. . . . 5
β’ (π β Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) β β) |
128 | 127, 61 | nndivred 12214 |
. . . 4
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) / (!β(π β 1))) β
β) |
129 | 122, 128 | eqeltrrd 2839 |
. . 3
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1)))) β
β) |
130 | | 1red 11163 |
. . 3
β’ (π β 1 β
β) |
131 | 58 | abscld 15328 |
. . . . 5
β’ (π β (absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β β) |
132 | 61 | nnrpd 12962 |
. . . . 5
β’ (π β (!β(π β 1)) β
β+) |
133 | 57 | abscld 15328 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β β) |
134 | 7, 133 | fsumrecl 15626 |
. . . . . 6
β’ (π β Ξ£π β (0...π)(absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β β) |
135 | 7, 57 | fsumabs 15693 |
. . . . . 6
β’ (π β (absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β€ Ξ£π β (0...π)(absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯))) |
136 | 81 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β ((πβπ)β(π + 1)) β β) |
137 | | ioombl 24945 |
. . . . . . . . . . . 12
β’
(0(,)π) β dom
vol |
138 | 137 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (0(,)π) β dom vol) |
139 | | 0red 11165 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β 0 β β) |
140 | | elfzle1 13451 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β 0 β€ π) |
141 | | volioo 24949 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ π
β β β§ 0 β€ π) β (volβ(0(,)π)) = (π β 0)) |
142 | 139, 53, 140, 141 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β (volβ(0(,)π)) = (π β 0)) |
143 | 53, 139 | resubcld 11590 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β (π β 0) β β) |
144 | 142, 143 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ (π β (0...π) β (volβ(0(,)π)) β β) |
145 | 144 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (volβ(0(,)π)) β β) |
146 | 82 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β ((πβπ)β(π + 1)) β β) |
147 | | iblconstmpt 44271 |
. . . . . . . . . . 11
β’
(((0(,)π) β dom
vol β§ (volβ(0(,)π)) β β β§ ((πβπ)β(π + 1)) β β) β (π₯ β (0(,)π) β¦ ((πβπ)β(π + 1))) β
πΏ1) |
148 | 138, 145,
146, 147 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (π₯ β (0(,)π) β¦ ((πβπ)β(π + 1))) β
πΏ1) |
149 | 136, 148 | itgrecl 25178 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β β«(0(,)π)((πβπ)β(π + 1)) dπ₯ β β) |
150 | 109, 149 | remulcld 11192 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯) β β) |
151 | 7, 150 | fsumrecl 15626 |
. . . . . . 7
β’ (π β Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯) β β) |
152 | 21, 56 | absmuld 15346 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β (absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) = ((absβ((π΄βπ) Β· (eβππ))) Β·
(absββ«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯))) |
153 | 56 | abscld 15328 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (absββ«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) β β) |
154 | 21 | absge0d 15336 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β 0 β€ (absβ((π΄βπ) Β· (eβππ)))) |
155 | 37 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
(absβ((eβπ-π₯) Β· (πΉβπ₯))) β β) |
156 | 37, 55 | iblabs 25209 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β (π₯ β (0(,)π) β¦
(absβ((eβπ-π₯) Β· (πΉβπ₯)))) β
πΏ1) |
157 | 155, 156 | itgrecl 25178 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β β«(0(,)π)(absβ((eβπ-π₯) Β· (πΉβπ₯))) dπ₯ β β) |
158 | 37, 55 | itgabs 25215 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (absββ«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) β€ β«(0(,)π)(absβ((eβπ-π₯) Β· (πΉβπ₯))) dπ₯) |
159 | 27, 36 | absmuld 15346 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
(absβ((eβπ-π₯) Β· (πΉβπ₯))) =
((absβ(eβπ-π₯)) Β· (absβ(πΉβπ₯)))) |
160 | 27 | abscld 15328 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
(absβ(eβπ-π₯)) β β) |
161 | | 1red 11163 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β 1 β β) |
162 | 36 | abscld 15328 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (absβ(πΉβπ₯)) β β) |
163 | 27 | absge0d 15336 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β 0 β€
(absβ(eβπ-π₯))) |
164 | 36 | absge0d 15336 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β 0 β€ (absβ(πΉβπ₯))) |
165 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (0(,)π) β e β β) |
166 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β |
167 | | epos 16096 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 <
e |
168 | 166, 14, 167 | ltleii 11285 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β€
e |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (0(,)π) β 0 β€ e) |
170 | 23 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (0(,)π) β -π₯ β β) |
171 | 165, 169,
170 | recxpcld 26094 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (0(,)π) β (eβπ-π₯) β
β) |
172 | 165, 169,
170 | cxpge0d 26095 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (0(,)π) β 0 β€
(eβπ-π₯)) |
173 | 171, 172 | absidd 15314 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (0(,)π) β
(absβ(eβπ-π₯)) = (eβπ-π₯)) |
174 | 173 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β
(absβ(eβπ-π₯)) = (eβπ-π₯)) |
175 | 171 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (eβπ-π₯) β
β) |
176 | | 1red 11163 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β 1 β β) |
177 | | 0xr 11209 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
β* |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β 0 β
β*) |
179 | 53 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β π β β*) |
180 | 179 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π β β*) |
181 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π₯ β (0(,)π)) |
182 | | ioogtlb 43807 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((0
β β* β§ π β β* β§ π₯ β (0(,)π)) β 0 < π₯) |
183 | 178, 180,
181, 182 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β 0 < π₯) |
184 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π₯ β β) |
185 | 184 | lt0neg2d 11732 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (0 < π₯ β -π₯ < 0)) |
186 | 183, 185 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β -π₯ < 0) |
187 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β e β β) |
188 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 <
2 |
189 | | egt2lt3 16095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (2 < e
β§ e < 3) |
190 | 189 | simpli 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 2 <
e |
191 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
β |
192 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 β
β |
193 | 191, 192,
14 | lttri 11288 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1 <
2 β§ 2 < e) β 1 < e) |
194 | 188, 190,
193 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 <
e |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β 1 < e) |
196 | 170 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β -π₯ β β) |
197 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β 0 β β) |
198 | 187, 195,
196, 197 | cxpltd 26090 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (-π₯ < 0 β
(eβπ-π₯) <
(eβπ0))) |
199 | 186, 198 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (eβπ-π₯) <
(eβπ0)) |
200 | | cxp0 26041 |
. . . . . . . . . . . . . . . . . . . 20
β’ (e β
β β (eβπ0) = 1) |
201 | 15, 200 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (eβπ0) =
1) |
202 | 199, 201 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (eβπ-π₯) < 1) |
203 | 175, 176,
202 | ltled 11310 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β (eβπ-π₯) β€ 1) |
204 | 174, 203 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β
(absβ(eβπ-π₯)) β€ 1) |
205 | 204 | adantll 713 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
(absβ(eβπ-π₯)) β€ 1) |
206 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β β β
β) |
207 | 30 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β π β β) |
208 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β π β
β0) |
209 | 31, 49 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ = (π¦ β β β¦ ((π¦β(π β 1)) Β· ββ β (1...π)((π¦ β β)βπ))) |
210 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β π₯ β β) |
211 | 206, 207,
208, 209, 210 | etransclem13 44562 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (πΉβπ₯) = ββ β (0...π)((π₯ β β)βif(β = 0, (π β 1), π))) |
212 | 211 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (absβ(πΉβπ₯)) = (absβββ β (0...π)((π₯ β β)βif(β = 0, (π β 1), π)))) |
213 | | nn0uz 12812 |
. . . . . . . . . . . . . . . . . 18
β’
β0 = (β€β₯β0) |
214 | 23 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β (0(,)π) β§ β β β0) β π₯ β
β) |
215 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β β β0
β β β
β) |
216 | 215 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β (0(,)π) β§ β β β0) β β β β) |
217 | 214, 216 | resubcld 11590 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (0(,)π) β§ β β β0) β (π₯ β β) β β) |
218 | 217 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β β0) β (π₯ β β) β β) |
219 | 60, 77 | ifcld 4537 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β if(β = 0, (π β 1), π) β
β0) |
220 | 219 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β β0) β if(β = 0, (π β 1), π) β
β0) |
221 | 218, 220 | reexpcld 14075 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β β0) β ((π₯ β β)βif(β = 0, (π β 1), π)) β β) |
222 | 221 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β β0) β ((π₯ β β)βif(β = 0, (π β 1), π)) β β) |
223 | 213, 208,
222 | fprodabs 15864 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (absβββ β (0...π)((π₯ β β)βif(β = 0, (π β 1), π))) = ββ β (0...π)(absβ((π₯ β β)βif(β = 0, (π β 1), π)))) |
224 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β β (0...π) β β β β0) |
225 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β (0(,)π) β§ β β β0) β π₯ β
β) |
226 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β β β0
β β β
β) |
227 | 226 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β (0(,)π) β§ β β β0) β β β β) |
228 | 225, 227 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (0(,)π) β§ β β β0) β (π₯ β β) β β) |
229 | 228 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β β0) β (π₯ β β) β β) |
230 | 224, 229 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (π₯ β β) β β) |
231 | 219 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β if(β = 0, (π β 1), π) β
β0) |
232 | 230, 231 | absexpd 15344 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (absβ((π₯ β β)βif(β = 0, (π β 1), π))) = ((absβ(π₯ β β))βif(β = 0, (π β 1), π))) |
233 | 232 | prodeq2dv 15813 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β ββ β (0...π)(absβ((π₯ β β)βif(β = 0, (π β 1), π))) = ββ β (0...π)((absβ(π₯ β β))βif(β = 0, (π β 1), π))) |
234 | 212, 223,
233 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (absβ(πΉβπ₯)) = ββ β (0...π)((absβ(π₯ β β))βif(β = 0, (π β 1), π))) |
235 | | nfv 1918 |
. . . . . . . . . . . . . . . . . 18
β’
β²β((π β§ π β (0...π)) β§ π₯ β (0(,)π)) |
236 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (0...π) β Fin) |
237 | 224, 228 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (0(,)π) β§ β β (0...π)) β (π₯ β β) β β) |
238 | 237 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (0(,)π) β§ β β (0...π)) β (absβ(π₯ β β)) β β) |
239 | 238 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (absβ(π₯ β β)) β β) |
240 | 239, 231 | reexpcld 14075 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β ((absβ(π₯ β β))βif(β = 0, (π β 1), π)) β β) |
241 | 237 | absge0d 15336 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (0(,)π) β§ β β (0...π)) β 0 β€ (absβ(π₯ β β))) |
242 | 241 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β 0 β€ (absβ(π₯ β β))) |
243 | 239, 231,
242 | expge0d 14076 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β 0 β€ ((absβ(π₯ β β))βif(β = 0, (π β 1), π))) |
244 | 78 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (πβπ) β β) |
245 | 76 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β π β β) |
246 | 245, 231 | reexpcld 14075 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (πβif(β = 0, (π β 1), π)) β β) |
247 | 224, 218 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (π₯ β β) β β) |
248 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ β (0(,)π) β§ β β (0...π)) β π₯ β β) |
249 | 224, 227 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ β (0(,)π) β§ β β (0...π)) β β β β) |
250 | 248, 249 | negsubdi2d 11535 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π₯ β (0(,)π) β§ β β (0...π)) β -(π₯ β β) = (β β π₯)) |
251 | 250 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β -(π₯ β β) = (β β π₯)) |
252 | 224 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β β β β0) |
253 | 252 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β β β β) |
254 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β 0 β β) |
255 | 210 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β π₯ β β) |
256 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (β β (0...π) β β β€ π) |
257 | 256 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β β β€ π) |
258 | 197, 184,
183 | ltled 11310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β 0 β€ π₯) |
259 | 258 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β 0 β€ π₯) |
260 | 259 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β 0 β€ π₯) |
261 | 253, 254,
245, 255, 257, 260 | le2subd 11782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (β β π₯) β€ (π β 0)) |
262 | 83 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π β 0) = π) |
263 | 262 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (π β 0) = π) |
264 | 261, 263 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (β β π₯) β€ π) |
265 | 251, 264 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β -(π₯ β β) β€ π) |
266 | 247, 245,
265 | lenegcon1d 11744 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β -π β€ (π₯ β β)) |
267 | | elfzel2 13446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0...π) β π β β€) |
268 | 267 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0...π) β π β β) |
269 | 268 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π β β) |
270 | 53 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π β β) |
271 | | iooltub 43822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((0
β β* β§ π β β* β§ π₯ β (0(,)π)) β π₯ < π) |
272 | 178, 180,
181, 271 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π₯ < π) |
273 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0...π) β π β€ π) |
274 | 273 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π β€ π) |
275 | 184, 270,
269, 272, 274 | ltletrd 11322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π₯ < π) |
276 | 184, 269,
275 | ltled 11310 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0...π) β§ π₯ β (0(,)π)) β π₯ β€ π) |
277 | 276 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β π₯ β€ π) |
278 | 277 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β π₯ β€ π) |
279 | 252 | nn0ge0d 12483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β 0 β€ β) |
280 | 255, 254,
245, 253, 278, 279 | le2subd 11782 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (π₯ β β) β€ (π β 0)) |
281 | 280, 263 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (π₯ β β) β€ π) |
282 | 247, 245 | absled 15322 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β ((absβ(π₯ β β)) β€ π β (-π β€ (π₯ β β) β§ (π₯ β β) β€ π))) |
283 | 266, 281,
282 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (absβ(π₯ β β)) β€ π) |
284 | | leexp1a 14087 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((absβ(π₯
β β)) β β
β§ π β β
β§ if(β = 0, (π β 1), π) β β0) β§ (0 β€
(absβ(π₯ β β)) β§ (absβ(π₯ β β)) β€ π)) β ((absβ(π₯ β β))βif(β = 0, (π β 1), π)) β€ (πβif(β = 0, (π β 1), π))) |
285 | 239, 245,
231, 242, 283, 284 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β ((absβ(π₯ β β))βif(β = 0, (π β 1), π)) β€ (πβif(β = 0, (π β 1), π))) |
286 | 46 | nnge1d 12208 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1 β€ π) |
287 | 286 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β 1 β€ π) |
288 | 219 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β if(β = 0, (π β 1), π) β β€) |
289 | 77 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β€) |
290 | | iftrue 4497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (β = 0 β if(β = 0, (π β 1), π) = (π β 1)) |
291 | 290 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ β = 0) β if(β = 0, (π β 1), π) = (π β 1)) |
292 | 30 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β β) |
293 | 292 | lem1d 12095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π β 1) β€ π) |
294 | 293 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ β = 0) β (π β 1) β€ π) |
295 | 291, 294 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ β = 0) β if(β = 0, (π β 1), π) β€ π) |
296 | | iffalse 4500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
β = 0 β if(β = 0, (π β 1), π) = π) |
297 | 296 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ Β¬ β = 0) β if(β = 0, (π β 1), π) = π) |
298 | 292 | leidd 11728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β€ π) |
299 | 298 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ Β¬ β = 0) β π β€ π) |
300 | 297, 299 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ Β¬ β = 0) β if(β = 0, (π β 1), π) β€ π) |
301 | 295, 300 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β if(β = 0, (π β 1), π) β€ π) |
302 | | eluz2 12776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(β€β₯βif(β = 0, (π β 1), π)) β (if(β = 0, (π β 1), π) β β€ β§ π β β€ β§ if(β = 0, (π β 1), π) β€ π)) |
303 | 288, 289,
301, 302 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β
(β€β₯βif(β = 0, (π β 1), π))) |
304 | 303 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β π β
(β€β₯βif(β = 0, (π β 1), π))) |
305 | 245, 287,
304 | leexp2ad 14164 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β (πβif(β = 0, (π β 1), π)) β€ (πβπ)) |
306 | 240, 246,
244, 285, 305 | letrd 11319 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β§ β β (0...π)) β ((absβ(π₯ β β))βif(β = 0, (π β 1), π)) β€ (πβπ)) |
307 | 235, 236,
240, 243, 244, 306 | fprodle 15886 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β ββ β (0...π)((absβ(π₯ β β))βif(β = 0, (π β 1), π)) β€ ββ β (0...π)(πβπ)) |
308 | 78 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πβπ) β β) |
309 | | fprodconst 15868 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((0...π) β Fin
β§ (πβπ) β β) β
ββ β (0...π)(πβπ) = ((πβπ)β(β―β(0...π)))) |
310 | 7, 308, 309 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ββ β (0...π)(πβπ) = ((πβπ)β(β―β(0...π)))) |
311 | | hashfz0 14339 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β (β―β(0...π)) = (π + 1)) |
312 | 47, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β―β(0...π)) = (π + 1)) |
313 | 312 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((πβπ)β(β―β(0...π))) = ((πβπ)β(π + 1))) |
314 | 310, 313 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ββ β (0...π)(πβπ) = ((πβπ)β(π + 1))) |
315 | 314 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β ββ β (0...π)(πβπ) = ((πβπ)β(π + 1))) |
316 | 307, 315 | breqtrd 5136 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β ββ β (0...π)((absβ(π₯ β β))βif(β = 0, (π β 1), π)) β€ ((πβπ)β(π + 1))) |
317 | 234, 316 | eqbrtrd 5132 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (absβ(πΉβπ₯)) β€ ((πβπ)β(π + 1))) |
318 | 160, 161,
162, 136, 163, 164, 205, 317 | lemul12ad 12104 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
((absβ(eβπ-π₯)) Β· (absβ(πΉβπ₯))) β€ (1 Β· ((πβπ)β(π + 1)))) |
319 | 82 | mulid2d 11180 |
. . . . . . . . . . . . . . 15
β’ (π β (1 Β· ((πβπ)β(π + 1))) = ((πβπ)β(π + 1))) |
320 | 319 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β (1 Β· ((πβπ)β(π + 1))) = ((πβπ)β(π + 1))) |
321 | 318, 320 | breqtrd 5136 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
((absβ(eβπ-π₯)) Β· (absβ(πΉβπ₯))) β€ ((πβπ)β(π + 1))) |
322 | 159, 321 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π₯ β (0(,)π)) β
(absβ((eβπ-π₯) Β· (πΉβπ₯))) β€ ((πβπ)β(π + 1))) |
323 | 156, 148,
155, 136, 322 | itgle 25190 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β β«(0(,)π)(absβ((eβπ-π₯) Β· (πΉβπ₯))) dπ₯ β€ β«(0(,)π)((πβπ)β(π + 1)) dπ₯) |
324 | 153, 157,
149, 158, 323 | letrd 11319 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (absββ«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯) β€ β«(0(,)π)((πβπ)β(π + 1)) dπ₯) |
325 | 153, 149,
109, 154, 324 | lemul2ad 12102 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β·
(absββ«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β€ ((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯)) |
326 | 152, 325 | eqbrtrd 5132 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β (absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β€ ((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯)) |
327 | 7, 133, 150, 326 | fsumle 15691 |
. . . . . . 7
β’ (π β Ξ£π β (0...π)(absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β€ Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯)) |
328 | | itgconst 25199 |
. . . . . . . . . . 11
β’
(((0(,)π) β dom
vol β§ (volβ(0(,)π)) β β β§ ((πβπ)β(π + 1)) β β) β
β«(0(,)π)((πβπ)β(π + 1)) dπ₯ = (((πβπ)β(π + 1)) Β· (volβ(0(,)π)))) |
329 | 138, 145,
146, 328 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β β«(0(,)π)((πβπ)β(π + 1)) dπ₯ = (((πβπ)β(π + 1)) Β· (volβ(0(,)π)))) |
330 | 47 | nn0ge0d 12483 |
. . . . . . . . . . . . . 14
β’ (π β 0 β€ π) |
331 | 76, 77, 330 | expge0d 14076 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ (πβπ)) |
332 | 78, 80, 331 | expge0d 14076 |
. . . . . . . . . . . 12
β’ (π β 0 β€ ((πβπ)β(π + 1))) |
333 | 332 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β 0 β€ ((πβπ)β(π + 1))) |
334 | 18 | subid1d 11508 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β (π β 0) = π) |
335 | 142, 334 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β (volβ(0(,)π)) = π) |
336 | 335, 273 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (π β (0...π) β (volβ(0(,)π)) β€ π) |
337 | 336 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (volβ(0(,)π)) β€ π) |
338 | 145, 124,
123, 333, 337 | lemul2ad 12102 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (((πβπ)β(π + 1)) Β· (volβ(0(,)π))) β€ (((πβπ)β(π + 1)) Β· π)) |
339 | 329, 338 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β β«(0(,)π)((πβπ)β(π + 1)) dπ₯ β€ (((πβπ)β(π + 1)) Β· π)) |
340 | 149, 125,
109, 154, 339 | lemul2ad 12102 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯) β€ ((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π))) |
341 | 7, 150, 126, 340 | fsumle 15691 |
. . . . . . 7
β’ (π β Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· β«(0(,)π)((πβπ)β(π + 1)) dπ₯) β€ Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π))) |
342 | 134, 151,
127, 327, 341 | letrd 11319 |
. . . . . 6
β’ (π β Ξ£π β (0...π)(absβ(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β€ Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π))) |
343 | 131, 134,
127, 135, 342 | letrd 11319 |
. . . . 5
β’ (π β (absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) β€ Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π))) |
344 | 131, 127,
132, 343 | lediv1dd 13022 |
. . . 4
β’ (π β ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (!β(π β 1))) β€ (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (((πβπ)β(π + 1)) Β· π)) / (!β(π β 1)))) |
345 | 344, 122 | breqtrd 5136 |
. . 3
β’ (π β ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (!β(π β 1))) β€ (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1))))) |
346 | | etransclem23.lt1 |
. . 3
β’ (π β (Ξ£π β (0...π)((absβ((π΄βπ) Β· (eβππ))) Β· (π Β· (πβ(π + 1)))) Β· (((πβ(π + 1))β(π β 1)) / (!β(π β 1)))) < 1) |
347 | 75, 129, 130, 345, 346 | lelttrd 11320 |
. 2
β’ (π β ((absβΞ£π β (0...π)(((π΄βπ) Β· (eβππ)) Β· β«(0(,)π)((eβπ-π₯) Β· (πΉβπ₯)) dπ₯)) / (!β(π β 1))) < 1) |
348 | 70, 347 | eqbrtrd 5132 |
1
β’ (π β (absβπΎ) < 1) |