Step | Hyp | Ref
| Expression |
1 | | nn0uz 12810 |
. . . . 5
β’
β0 = (β€β₯β0) |
2 | | 0zd 12516 |
. . . . 5
β’ (π β 0 β
β€) |
3 | | effsumlt.1 |
. . . . . . . 8
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) |
4 | 3 | eftval 15964 |
. . . . . . 7
β’ (π β β0
β (πΉβπ) = ((π΄βπ) / (!βπ))) |
5 | 4 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β0) β (πΉβπ) = ((π΄βπ) / (!βπ))) |
6 | | effsumlt.2 |
. . . . . . . 8
β’ (π β π΄ β
β+) |
7 | 6 | rpred 12962 |
. . . . . . 7
β’ (π β π΄ β β) |
8 | | reeftcl 15962 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β ((π΄βπ) / (!βπ)) β β) |
9 | 7, 8 | sylan 581 |
. . . . . 6
β’ ((π β§ π β β0) β ((π΄βπ) / (!βπ)) β β) |
10 | 5, 9 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β β0) β (πΉβπ) β β) |
11 | 1, 2, 10 | serfre 13943 |
. . . 4
β’ (π β seq0( + , πΉ):β0βΆβ) |
12 | | effsumlt.3 |
. . . 4
β’ (π β π β
β0) |
13 | 11, 12 | ffvelcdmd 7037 |
. . 3
β’ (π β (seq0( + , πΉ)βπ) β β) |
14 | | eqid 2733 |
. . . 4
β’
(β€β₯β(π + 1)) =
(β€β₯β(π + 1)) |
15 | | peano2nn0 12458 |
. . . . 5
β’ (π β β0
β (π + 1) β
β0) |
16 | 12, 15 | syl 17 |
. . . 4
β’ (π β (π + 1) β
β0) |
17 | | eqidd 2734 |
. . . 4
β’ ((π β§ π β β0) β (πΉβπ) = (πΉβπ)) |
18 | | nn0z 12529 |
. . . . . . 7
β’ (π β β0
β π β
β€) |
19 | | rpexpcl 13992 |
. . . . . . 7
β’ ((π΄ β β+
β§ π β β€)
β (π΄βπ) β
β+) |
20 | 6, 18, 19 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β β0) β (π΄βπ) β
β+) |
21 | | faccl 14189 |
. . . . . . . 8
β’ (π β β0
β (!βπ) β
β) |
22 | 21 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β0) β
(!βπ) β
β) |
23 | 22 | nnrpd 12960 |
. . . . . 6
β’ ((π β§ π β β0) β
(!βπ) β
β+) |
24 | 20, 23 | rpdivcld 12979 |
. . . . 5
β’ ((π β§ π β β0) β ((π΄βπ) / (!βπ)) β
β+) |
25 | 5, 24 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β β0) β (πΉβπ) β
β+) |
26 | 7 | recnd 11188 |
. . . . 5
β’ (π β π΄ β β) |
27 | 3 | efcllem 15965 |
. . . . 5
β’ (π΄ β β β seq0( + ,
πΉ) β dom β
) |
28 | 26, 27 | syl 17 |
. . . 4
β’ (π β seq0( + , πΉ) β dom β
) |
29 | 1, 14, 16, 17, 25, 28 | isumrpcl 15733 |
. . 3
β’ (π β Ξ£π β (β€β₯β(π + 1))(πΉβπ) β
β+) |
30 | 13, 29 | ltaddrpd 12995 |
. 2
β’ (π β (seq0( + , πΉ)βπ) < ((seq0( + , πΉ)βπ) + Ξ£π β (β€β₯β(π + 1))(πΉβπ))) |
31 | 3 | efval2 15971 |
. . . 4
β’ (π΄ β β β
(expβπ΄) =
Ξ£π β
β0 (πΉβπ)) |
32 | 26, 31 | syl 17 |
. . 3
β’ (π β (expβπ΄) = Ξ£π β β0 (πΉβπ)) |
33 | 10 | recnd 11188 |
. . . 4
β’ ((π β§ π β β0) β (πΉβπ) β β) |
34 | 1, 14, 16, 17, 33, 28 | isumsplit 15730 |
. . 3
β’ (π β Ξ£π β β0 (πΉβπ) = (Ξ£π β (0...((π + 1) β 1))(πΉβπ) + Ξ£π β (β€β₯β(π + 1))(πΉβπ))) |
35 | 12 | nn0cnd 12480 |
. . . . . . . 8
β’ (π β π β β) |
36 | | ax-1cn 11114 |
. . . . . . . 8
β’ 1 β
β |
37 | | pncan 11412 |
. . . . . . . 8
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
38 | 35, 36, 37 | sylancl 587 |
. . . . . . 7
β’ (π β ((π + 1) β 1) = π) |
39 | 38 | oveq2d 7374 |
. . . . . 6
β’ (π β (0...((π + 1) β 1)) = (0...π)) |
40 | 39 | sumeq1d 15591 |
. . . . 5
β’ (π β Ξ£π β (0...((π + 1) β 1))(πΉβπ) = Ξ£π β (0...π)(πΉβπ)) |
41 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πΉβπ) = (πΉβπ)) |
42 | 12, 1 | eleqtrdi 2844 |
. . . . . 6
β’ (π β π β
(β€β₯β0)) |
43 | | elfznn0 13540 |
. . . . . . 7
β’ (π β (0...π) β π β β0) |
44 | 43, 33 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πΉβπ) β β) |
45 | 41, 42, 44 | fsumser 15620 |
. . . . 5
β’ (π β Ξ£π β (0...π)(πΉβπ) = (seq0( + , πΉ)βπ)) |
46 | 40, 45 | eqtrd 2773 |
. . . 4
β’ (π β Ξ£π β (0...((π + 1) β 1))(πΉβπ) = (seq0( + , πΉ)βπ)) |
47 | 46 | oveq1d 7373 |
. . 3
β’ (π β (Ξ£π β (0...((π + 1) β 1))(πΉβπ) + Ξ£π β (β€β₯β(π + 1))(πΉβπ)) = ((seq0( + , πΉ)βπ) + Ξ£π β (β€β₯β(π + 1))(πΉβπ))) |
48 | 32, 34, 47 | 3eqtrd 2777 |
. 2
β’ (π β (expβπ΄) = ((seq0( + , πΉ)βπ) + Ξ£π β (β€β₯β(π + 1))(πΉβπ))) |
49 | 30, 48 | breqtrrd 5134 |
1
β’ (π β (seq0( + , πΉ)βπ) < (expβπ΄)) |