Step | Hyp | Ref
| Expression |
1 | | 0zd 9265 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β 0 β β€) |
2 | | nn0z 9273 |
. . . . . . . 8
β’ (π β β0
β π β
β€) |
3 | 2 | adantl 277 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β π β
β€) |
4 | 1, 3 | fzfigd 10431 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β (0...π) β
Fin) |
5 | | simpll 527 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β π΄ β β) |
6 | | elfznn0 10114 |
. . . . . . . 8
β’ (π β (0...π) β π β β0) |
7 | 6 | adantl 277 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β π β β0) |
8 | | eftcl 11662 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β ((π΄βπ) / (!βπ)) β β) |
9 | 5, 7, 8 | syl2anc 411 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β ((π΄βπ) / (!βπ)) β β) |
10 | 4, 9 | fsumcl 11408 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β Ξ£π β
(0...π)((π΄βπ) / (!βπ)) β β) |
11 | 10 | ralrimiva 2550 |
. . . 4
β’ (π΄ β β β
βπ β
β0 Ξ£π β (0...π)((π΄βπ) / (!βπ)) β β) |
12 | | efcvgfsum.1 |
. . . . 5
β’ πΉ = (π β β0 β¦
Ξ£π β (0...π)((π΄βπ) / (!βπ))) |
13 | 12 | fnmpt 5343 |
. . . 4
β’
(βπ β
β0 Ξ£π β (0...π)((π΄βπ) / (!βπ)) β β β πΉ Fn β0) |
14 | 11, 13 | syl 14 |
. . 3
β’ (π΄ β β β πΉ Fn
β0) |
15 | | nn0uz 9562 |
. . . . 5
β’
β0 = (β€β₯β0) |
16 | | 0zd 9265 |
. . . . 5
β’ (π΄ β β β 0 β
β€) |
17 | | eqid 2177 |
. . . . . . 7
β’ (π β β0
β¦ ((π΄βπ) / (!βπ))) = (π β β0 β¦ ((π΄βπ) / (!βπ))) |
18 | 17 | eftvalcn 11665 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) = ((π΄βπ) / (!βπ))) |
19 | 18, 8 | eqeltrd 2254 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) β β) |
20 | 15, 16, 19 | serf 10474 |
. . . 4
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))):β0βΆβ) |
21 | 20 | ffnd 5367 |
. . 3
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))) Fn β0) |
22 | | simpr 110 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β π β
β0) |
23 | | 0zd 9265 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β 0 β β€) |
24 | 22 | nn0zd 9373 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β π β
β€) |
25 | 23, 24 | fzfigd 10431 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β (0...π) β
Fin) |
26 | | simpll 527 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β π΄ β β) |
27 | | elfznn0 10114 |
. . . . . . . 8
β’ (π β (0...π) β π β β0) |
28 | 27 | adantl 277 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β π β β0) |
29 | 26, 28, 8 | syl2anc 411 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β ((π΄βπ) / (!βπ)) β β) |
30 | 25, 29 | fsumcl 11408 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β Ξ£π β
(0...π)((π΄βπ) / (!βπ)) β β) |
31 | | oveq2 5883 |
. . . . . . 7
β’ (π = π β (0...π) = (0...π)) |
32 | 31 | sumeq1d 11374 |
. . . . . 6
β’ (π = π β Ξ£π β (0...π)((π΄βπ) / (!βπ)) = Ξ£π β (0...π)((π΄βπ) / (!βπ))) |
33 | 32, 12 | fvmptg 5593 |
. . . . 5
β’ ((π β β0
β§ Ξ£π β
(0...π)((π΄βπ) / (!βπ)) β β) β (πΉβπ) = Ξ£π β (0...π)((π΄βπ) / (!βπ))) |
34 | 22, 30, 33 | syl2anc 411 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β (πΉβπ) = Ξ£π β (0...π)((π΄βπ) / (!βπ))) |
35 | | simpll 527 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β π΄ β β) |
36 | | elnn0uz 9565 |
. . . . . . . 8
β’ (π β β0
β π β
(β€β₯β0)) |
37 | 36 | biimpri 133 |
. . . . . . 7
β’ (π β
(β€β₯β0) β π β β0) |
38 | 37 | adantl 277 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β π β β0) |
39 | 35, 38, 18 | syl2anc 411 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β ((π β β0 β¦ ((π΄βπ) / (!βπ)))βπ) = ((π΄βπ) / (!βπ))) |
40 | 22, 15 | eleqtrdi 2270 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β π β
(β€β₯β0)) |
41 | 35, 38, 8 | syl2anc 411 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β ((π΄βπ) / (!βπ)) β β) |
42 | 39, 40, 41 | fsum3ser 11405 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β Ξ£π β
(0...π)((π΄βπ) / (!βπ)) = (seq0( + , (π β β0 β¦ ((π΄βπ) / (!βπ))))βπ)) |
43 | 34, 42 | eqtrd 2210 |
. . 3
β’ ((π΄ β β β§ π β β0)
β (πΉβπ) = (seq0( + , (π β β0
β¦ ((π΄βπ) / (!βπ))))βπ)) |
44 | 14, 21, 43 | eqfnfvd 5617 |
. 2
β’ (π΄ β β β πΉ = seq0( + , (π β β0 β¦ ((π΄βπ) / (!βπ))))) |
45 | 17 | efcvg 11674 |
. 2
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))) β (expβπ΄)) |
46 | 44, 45 | eqbrtrd 4026 |
1
β’ (π΄ β β β πΉ β (expβπ΄)) |