Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . 6
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β (((ββπ) + 1)...(ββ(πΎ Β· π))) β Fin) |
2 | | ioossre 13332 |
. . . . . . . . . . . . . 14
β’ (π(,)+β) β
β |
3 | | pntpbnd1.y |
. . . . . . . . . . . . . 14
β’ (π β π β (π(,)+β)) |
4 | 2, 3 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
5 | | 0red 11165 |
. . . . . . . . . . . . . 14
β’ (π β 0 β
β) |
6 | | pntpbnd1.x |
. . . . . . . . . . . . . . . 16
β’ π = (expβ(2 / πΈ)) |
7 | | 2re 12234 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
8 | | ioossre 13332 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0(,)1)
β β |
9 | | pntpbnd1.e |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΈ β (0(,)1)) |
10 | 8, 9 | sselid 3947 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΈ β β) |
11 | | eliooord 13330 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΈ β (0(,)1) β (0 <
πΈ β§ πΈ < 1)) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0 < πΈ β§ πΈ < 1)) |
13 | 12 | simpld 496 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 < πΈ) |
14 | 10, 13 | elrpd 12961 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΈ β
β+) |
15 | | rerpdivcl 12952 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β β§ πΈ
β β+) β (2 / πΈ) β β) |
16 | 7, 14, 15 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2 / πΈ) β β) |
17 | 16 | reefcld 15977 |
. . . . . . . . . . . . . . . 16
β’ (π β (expβ(2 / πΈ)) β
β) |
18 | 6, 17 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
19 | | efgt0 15992 |
. . . . . . . . . . . . . . . . 17
β’ ((2 /
πΈ) β β β 0
< (expβ(2 / πΈ))) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 < (expβ(2 /
πΈ))) |
21 | 20, 6 | breqtrrdi 5152 |
. . . . . . . . . . . . . . 15
β’ (π β 0 < π) |
22 | | eliooord 13330 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π(,)+β) β (π < π β§ π < +β)) |
23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π < π β§ π < +β)) |
24 | 23 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β π < π) |
25 | 5, 18, 4, 21, 24 | lttrd 11323 |
. . . . . . . . . . . . . 14
β’ (π β 0 < π) |
26 | 5, 4, 25 | ltled 11310 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ π) |
27 | | flge0nn0 13732 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 β€
π) β
(ββπ) β
β0) |
28 | 4, 26, 27 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (ββπ) β
β0) |
29 | | nn0p1nn 12459 |
. . . . . . . . . . . 12
β’
((ββπ)
β β0 β ((ββπ) + 1) β β) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((ββπ) + 1) β
β) |
31 | | elfzuz 13444 |
. . . . . . . . . . 11
β’ (π β (((ββπ) + 1)...(ββ(πΎ Β· π))) β π β
(β€β₯β((ββπ) + 1))) |
32 | | eluznn 12850 |
. . . . . . . . . . 11
β’
((((ββπ)
+ 1) β β β§ π
β (β€β₯β((ββπ) + 1))) β π β β) |
33 | 30, 31, 32 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β β) |
34 | 33 | nnrpd 12962 |
. . . . . . . . 9
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β β+) |
35 | | pntpbnd.r |
. . . . . . . . . . 11
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
36 | 35 | pntrf 26927 |
. . . . . . . . . 10
β’ π
:β+βΆβ |
37 | 36 | ffvelcdmi 7039 |
. . . . . . . . 9
β’ (π β β+
β (π
βπ) β
β) |
38 | 34, 37 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β β) |
39 | 33 | peano2nnd 12177 |
. . . . . . . . 9
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π + 1) β β) |
40 | 33, 39 | nnmulcld 12213 |
. . . . . . . 8
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β β) |
41 | 38, 40 | nndivred 12214 |
. . . . . . 7
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) / (π Β· (π + 1))) β β) |
42 | 41 | adantlr 714 |
. . . . . 6
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) / (π Β· (π + 1))) β β) |
43 | 1, 42 | fsumrecl 15626 |
. . . . 5
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1))) β β) |
44 | 38 | adantlr 714 |
. . . . . . 7
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β β) |
45 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (π
βπ) = (π
βπ)) |
46 | 45 | breq2d 5122 |
. . . . . . . . 9
β’ (π = π β (0 β€ (π
βπ) β 0 β€ (π
βπ))) |
47 | 46 | rspccva 3583 |
. . . . . . . 8
β’
((βπ β
(((ββπ) +
1)...(ββ(πΎ
Β· π)))0 β€ (π
βπ) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 β€ (π
βπ)) |
48 | 47 | adantll 713 |
. . . . . . 7
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 β€ (π
βπ)) |
49 | 40 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β β) |
50 | 49 | nnred 12175 |
. . . . . . 7
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β β) |
51 | 49 | nngt0d 12209 |
. . . . . . 7
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 < (π Β· (π + 1))) |
52 | | divge0 12031 |
. . . . . . 7
β’ ((((π
βπ) β β β§ 0 β€ (π
βπ)) β§ ((π Β· (π + 1)) β β β§ 0 < (π Β· (π + 1)))) β 0 β€ ((π
βπ) / (π Β· (π + 1)))) |
53 | 44, 48, 50, 51, 52 | syl22anc 838 |
. . . . . 6
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 β€ ((π
βπ) / (π Β· (π + 1)))) |
54 | 1, 42, 53 | fsumge0 15687 |
. . . . 5
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β 0 β€ Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
55 | 43, 54 | absidd 15314 |
. . . 4
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
56 | 42, 53 | absidd 15314 |
. . . . 5
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (absβ((π
βπ) / (π Β· (π + 1)))) = ((π
βπ) / (π Β· (π + 1)))) |
57 | 56 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))(absβ((π
βπ) / (π Β· (π + 1)))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
58 | 55, 57 | eqtr4d 2780 |
. . 3
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ)) β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))(absβ((π
βπ) / (π Β· (π + 1))))) |
59 | | fzfid 13885 |
. . . . 5
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β (((ββπ) + 1)...(ββ(πΎ Β· π))) β Fin) |
60 | 41 | adantlr 714 |
. . . . . 6
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) / (π Β· (π + 1))) β β) |
61 | 60 | recnd 11190 |
. . . . 5
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) / (π Β· (π + 1))) β β) |
62 | 59, 61 | fsumneg 15679 |
. . . 4
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))-((π
βπ) / (π Β· (π + 1))) = -Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
63 | 38 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β β) |
64 | 63 | renegcld 11589 |
. . . . . . . . 9
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β -(π
βπ) β β) |
65 | 45 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π = π β ((π
βπ) β€ 0 β (π
βπ) β€ 0)) |
66 | 65 | rspccva 3583 |
. . . . . . . . . . 11
β’
((βπ β
(((ββπ) +
1)...(ββ(πΎ
Β· π)))(π
βπ) β€ 0 β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β€ 0) |
67 | 66 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β€ 0) |
68 | 63 | le0neg1d 11733 |
. . . . . . . . . 10
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) β€ 0 β 0 β€ -(π
βπ))) |
69 | 67, 68 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 β€ -(π
βπ)) |
70 | 40 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β β) |
71 | 70 | nnred 12175 |
. . . . . . . . 9
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β β) |
72 | 70 | nngt0d 12209 |
. . . . . . . . 9
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 < (π Β· (π + 1))) |
73 | | divge0 12031 |
. . . . . . . . 9
β’
(((-(π
βπ) β β β§ 0 β€
-(π
βπ)) β§ ((π Β· (π + 1)) β β β§ 0 < (π Β· (π + 1)))) β 0 β€ (-(π
βπ) / (π Β· (π + 1)))) |
74 | 64, 69, 71, 72, 73 | syl22anc 838 |
. . . . . . . 8
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 β€ (-(π
βπ) / (π Β· (π + 1)))) |
75 | 38 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β β) |
76 | 40 | nncnd 12176 |
. . . . . . . . . 10
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β β) |
77 | 40 | nnne0d 12210 |
. . . . . . . . . 10
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π Β· (π + 1)) β 0) |
78 | 75, 76, 77 | divnegd 11951 |
. . . . . . . . 9
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β -((π
βπ) / (π Β· (π + 1))) = (-(π
βπ) / (π Β· (π + 1)))) |
79 | 78 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β -((π
βπ) / (π Β· (π + 1))) = (-(π
βπ) / (π Β· (π + 1)))) |
80 | 74, 79 | breqtrrd 5138 |
. . . . . . 7
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β 0 β€ -((π
βπ) / (π Β· (π + 1)))) |
81 | 60 | le0neg1d 11733 |
. . . . . . 7
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (((π
βπ) / (π Β· (π + 1))) β€ 0 β 0 β€ -((π
βπ) / (π Β· (π + 1))))) |
82 | 80, 81 | mpbird 257 |
. . . . . 6
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) / (π Β· (π + 1))) β€ 0) |
83 | 60, 82 | absnidd 15305 |
. . . . 5
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (absβ((π
βπ) / (π Β· (π + 1)))) = -((π
βπ) / (π Β· (π + 1)))) |
84 | 83 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))(absβ((π
βπ) / (π Β· (π + 1)))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))-((π
βπ) / (π Β· (π + 1)))) |
85 | 59, 60 | fsumrecl 15626 |
. . . . 5
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1))) β β) |
86 | 60 | renegcld 11589 |
. . . . . . . 8
β’ (((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β -((π
βπ) / (π Β· (π + 1))) β β) |
87 | 59, 86, 80 | fsumge0 15687 |
. . . . . . 7
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β 0 β€ Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))-((π
βπ) / (π Β· (π + 1)))) |
88 | 87, 62 | breqtrd 5136 |
. . . . . 6
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β 0 β€ -Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
89 | 85 | le0neg1d 11733 |
. . . . . 6
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β (Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1))) β€ 0 β 0 β€ -Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1))))) |
90 | 88, 89 | mpbird 257 |
. . . . 5
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1))) β€ 0) |
91 | 85, 90 | absnidd 15305 |
. . . 4
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) = -Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
92 | 62, 84, 91 | 3eqtr4rd 2788 |
. . 3
β’ ((π β§ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0) β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))(absβ((π
βπ) / (π Β· (π + 1))))) |
93 | | pntpbnd1.c |
. . . . . . . . . . . . 13
β’ πΆ = (π΄ + 2) |
94 | | pntpbnd1.1 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β
β+) |
95 | | 2rp 12927 |
. . . . . . . . . . . . . 14
β’ 2 β
β+ |
96 | | rpaddcl 12944 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β+
β§ 2 β β+) β (π΄ + 2) β
β+) |
97 | 94, 95, 96 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β (π΄ + 2) β
β+) |
98 | 93, 97 | eqeltrid 2842 |
. . . . . . . . . . . 12
β’ (π β πΆ β
β+) |
99 | 98, 14 | rpdivcld 12981 |
. . . . . . . . . . 11
β’ (π β (πΆ / πΈ) β
β+) |
100 | 99 | rpred 12964 |
. . . . . . . . . 10
β’ (π β (πΆ / πΈ) β β) |
101 | 100 | reefcld 15977 |
. . . . . . . . 9
β’ (π β (expβ(πΆ / πΈ)) β β) |
102 | | pnfxr 11216 |
. . . . . . . . 9
β’ +β
β β* |
103 | | icossre 13352 |
. . . . . . . . 9
β’
(((expβ(πΆ /
πΈ)) β β β§
+β β β*) β ((expβ(πΆ / πΈ))[,)+β) β
β) |
104 | 101, 102,
103 | sylancl 587 |
. . . . . . . 8
β’ (π β ((expβ(πΆ / πΈ))[,)+β) β
β) |
105 | | pntpbnd1.k |
. . . . . . . 8
β’ (π β πΎ β ((expβ(πΆ / πΈ))[,)+β)) |
106 | 104, 105 | sseldd 3950 |
. . . . . . 7
β’ (π β πΎ β β) |
107 | 106, 4 | remulcld 11192 |
. . . . . 6
β’ (π β (πΎ Β· π) β β) |
108 | 4 | recnd 11190 |
. . . . . . . . 9
β’ (π β π β β) |
109 | 108 | mulid2d 11180 |
. . . . . . . 8
β’ (π β (1 Β· π) = π) |
110 | | 1red 11163 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
111 | | efgt1 16005 |
. . . . . . . . . . 11
β’ ((πΆ / πΈ) β β+ β 1 <
(expβ(πΆ / πΈ))) |
112 | 99, 111 | syl 17 |
. . . . . . . . . 10
β’ (π β 1 < (expβ(πΆ / πΈ))) |
113 | | elicopnf 13369 |
. . . . . . . . . . . . 13
β’
((expβ(πΆ /
πΈ)) β β β
(πΎ β
((expβ(πΆ / πΈ))[,)+β) β (πΎ β β β§
(expβ(πΆ / πΈ)) β€ πΎ))) |
114 | 101, 113 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (πΎ β ((expβ(πΆ / πΈ))[,)+β) β (πΎ β β β§ (expβ(πΆ / πΈ)) β€ πΎ))) |
115 | 114 | simplbda 501 |
. . . . . . . . . . 11
β’ ((π β§ πΎ β ((expβ(πΆ / πΈ))[,)+β)) β (expβ(πΆ / πΈ)) β€ πΎ) |
116 | 105, 115 | mpdan 686 |
. . . . . . . . . 10
β’ (π β (expβ(πΆ / πΈ)) β€ πΎ) |
117 | 110, 101,
106, 112, 116 | ltletrd 11322 |
. . . . . . . . 9
β’ (π β 1 < πΎ) |
118 | | ltmul1 12012 |
. . . . . . . . . 10
β’ ((1
β β β§ πΎ
β β β§ (π
β β β§ 0 < π)) β (1 < πΎ β (1 Β· π) < (πΎ Β· π))) |
119 | 110, 106,
4, 25, 118 | syl112anc 1375 |
. . . . . . . . 9
β’ (π β (1 < πΎ β (1 Β· π) < (πΎ Β· π))) |
120 | 117, 119 | mpbid 231 |
. . . . . . . 8
β’ (π β (1 Β· π) < (πΎ Β· π)) |
121 | 109, 120 | eqbrtrrd 5134 |
. . . . . . 7
β’ (π β π < (πΎ Β· π)) |
122 | 4, 107, 121 | ltled 11310 |
. . . . . 6
β’ (π β π β€ (πΎ Β· π)) |
123 | | flword2 13725 |
. . . . . 6
β’ ((π β β β§ (πΎ Β· π) β β β§ π β€ (πΎ Β· π)) β (ββ(πΎ Β· π)) β
(β€β₯β(ββπ))) |
124 | 4, 107, 122, 123 | syl3anc 1372 |
. . . . 5
β’ (π β (ββ(πΎ Β· π)) β
(β€β₯β(ββπ))) |
125 | 107 | flcld 13710 |
. . . . . 6
β’ (π β (ββ(πΎ Β· π)) β β€) |
126 | | uzid 12785 |
. . . . . 6
β’
((ββ(πΎ
Β· π)) β β€
β (ββ(πΎ
Β· π)) β
(β€β₯β(ββ(πΎ Β· π)))) |
127 | 125, 126 | syl 17 |
. . . . 5
β’ (π β (ββ(πΎ Β· π)) β
(β€β₯β(ββ(πΎ Β· π)))) |
128 | | elfzuzb 13442 |
. . . . 5
β’
((ββ(πΎ
Β· π)) β
((ββπ)...(ββ(πΎ Β· π))) β ((ββ(πΎ Β· π)) β
(β€β₯β(ββπ)) β§ (ββ(πΎ Β· π)) β
(β€β₯β(ββ(πΎ Β· π))))) |
129 | 124, 127,
128 | sylanbrc 584 |
. . . 4
β’ (π β (ββ(πΎ Β· π)) β ((ββπ)...(ββ(πΎ Β· π)))) |
130 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = (ββπ) β (((ββπ) + 1)...π₯) = (((ββπ) + 1)...(ββπ))) |
131 | 130 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = (ββπ) β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β βπ β (((ββπ) + 1)...(ββπ))0 β€ (π
βπ))) |
132 | 130 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = (ββπ) β (βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0 β βπ β (((ββπ) + 1)...(ββπ))(π
βπ) β€ 0)) |
133 | 131, 132 | orbi12d 918 |
. . . . . 6
β’ (π₯ = (ββπ) β ((βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(ββπ))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββπ))(π
βπ) β€ 0))) |
134 | 133 | imbi2d 341 |
. . . . 5
β’ (π₯ = (ββπ) β ((π β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0)) β (π β (βπ β (((ββπ) + 1)...(ββπ))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββπ))(π
βπ) β€ 0)))) |
135 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = π β (((ββπ) + 1)...π₯) = (((ββπ) + 1)...π)) |
136 | 135 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = π β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β βπ β (((ββπ) + 1)...π)0 β€ (π
βπ))) |
137 | 135 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = π β (βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0 β βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0)) |
138 | 136, 137 | orbi12d 918 |
. . . . . 6
β’ (π₯ = π β ((βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0))) |
139 | 138 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β ((π β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0)) β (π β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0)))) |
140 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (((ββπ) + 1)...π₯) = (((ββπ) + 1)...(π + 1))) |
141 | 140 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = (π + 1) β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ))) |
142 | 140 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = (π + 1) β (βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0 β βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0)) |
143 | 141, 142 | orbi12d 918 |
. . . . . 6
β’ (π₯ = (π + 1) β ((βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0))) |
144 | 143 | imbi2d 341 |
. . . . 5
β’ (π₯ = (π + 1) β ((π β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0)) β (π β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0)))) |
145 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = (ββ(πΎ Β· π)) β (((ββπ) + 1)...π₯) = (((ββπ) + 1)...(ββ(πΎ Β· π)))) |
146 | 145 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = (ββ(πΎ Β· π)) β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ))) |
147 | 145 | raleqdv 3316 |
. . . . . . 7
β’ (π₯ = (ββ(πΎ Β· π)) β (βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0 β βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0)) |
148 | 146, 147 | orbi12d 918 |
. . . . . 6
β’ (π₯ = (ββ(πΎ Β· π)) β ((βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0))) |
149 | 148 | imbi2d 341 |
. . . . 5
β’ (π₯ = (ββ(πΎ Β· π)) β ((π β (βπ β (((ββπ) + 1)...π₯)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π₯)(π
βπ) β€ 0)) β (π β (βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0)))) |
150 | | elfzle3 13454 |
. . . . . . . . 9
β’ (π β (((ββπ) + 1)...(ββπ)) β ((ββπ) + 1) β€ (ββπ)) |
151 | | elfzel2 13446 |
. . . . . . . . . . . 12
β’ (π β (((ββπ) + 1)...(ββπ)) β (ββπ) β
β€) |
152 | 151 | zred 12614 |
. . . . . . . . . . 11
β’ (π β (((ββπ) + 1)...(ββπ)) β (ββπ) β
β) |
153 | 152 | ltp1d 12092 |
. . . . . . . . . 10
β’ (π β (((ββπ) + 1)...(ββπ)) β (ββπ) < ((ββπ) + 1)) |
154 | | peano2re 11335 |
. . . . . . . . . . . 12
β’
((ββπ)
β β β ((ββπ) + 1) β β) |
155 | 152, 154 | syl 17 |
. . . . . . . . . . 11
β’ (π β (((ββπ) + 1)...(ββπ)) β ((ββπ) + 1) β
β) |
156 | 152, 155 | ltnled 11309 |
. . . . . . . . . 10
β’ (π β (((ββπ) + 1)...(ββπ)) β ((ββπ) < ((ββπ) + 1) β Β¬
((ββπ) + 1)
β€ (ββπ))) |
157 | 153, 156 | mpbid 231 |
. . . . . . . . 9
β’ (π β (((ββπ) + 1)...(ββπ)) β Β¬
((ββπ) + 1)
β€ (ββπ)) |
158 | 150, 157 | pm2.21dd 194 |
. . . . . . . 8
β’ (π β (((ββπ) + 1)...(ββπ)) β (π
βπ) β€ 0) |
159 | 158 | rgen 3067 |
. . . . . . 7
β’
βπ β
(((ββπ) +
1)...(ββπ))(π
βπ) β€ 0 |
160 | 159 | olci 865 |
. . . . . 6
β’
(βπ β
(((ββπ) +
1)...(ββπ))0
β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββπ))(π
βπ) β€ 0) |
161 | 160 | 2a1i 12 |
. . . . 5
β’
((ββ(πΎ
Β· π)) β
(β€β₯β(ββπ)) β (π β (βπ β (((ββπ) + 1)...(ββπ))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββπ))(π
βπ) β€ 0))) |
162 | | elfzofz 13595 |
. . . . . . . . . 10
β’ (π β ((ββπ)..^(ββ(πΎ Β· π))) β π β ((ββπ)...(ββ(πΎ Β· π)))) |
163 | | elfzp12 13527 |
. . . . . . . . . . 11
β’
((ββ(πΎ
Β· π)) β
(β€β₯β(ββπ)) β (π β ((ββπ)...(ββ(πΎ Β· π))) β (π = (ββπ) β¨ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))))) |
164 | 124, 163 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β ((ββπ)...(ββ(πΎ Β· π))) β (π = (ββπ) β¨ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))))) |
165 | 162, 164 | imbitrid 243 |
. . . . . . . . 9
β’ (π β (π β ((ββπ)..^(ββ(πΎ Β· π))) β (π = (ββπ) β¨ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))))) |
166 | 165 | imp 408 |
. . . . . . . 8
β’ ((π β§ π β ((ββπ)..^(ββ(πΎ Β· π)))) β (π = (ββπ) β¨ π β (((ββπ) + 1)...(ββ(πΎ Β· π))))) |
167 | 30 | nnrpd 12962 |
. . . . . . . . . . . . . 14
β’ (π β ((ββπ) + 1) β
β+) |
168 | 36 | ffvelcdmi 7039 |
. . . . . . . . . . . . . 14
β’
(((ββπ)
+ 1) β β+ β (π
β((ββπ) + 1)) β β) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π
β((ββπ) + 1)) β β) |
170 | 5, 169 | letrid 11314 |
. . . . . . . . . . . 12
β’ (π β (0 β€ (π
β((ββπ) + 1)) β¨ (π
β((ββπ) + 1)) β€ 0)) |
171 | 170 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π = (ββπ)) β (0 β€ (π
β((ββπ) + 1)) β¨ (π
β((ββπ) + 1)) β€ 0)) |
172 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = (ββπ) β (π + 1) = ((ββπ) + 1)) |
173 | 172 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = (ββπ) β (((ββπ) + 1)...(π + 1)) = (((ββπ) + 1)...((ββπ) + 1))) |
174 | 4 | flcld 13710 |
. . . . . . . . . . . . . . . . 17
β’ (π β (ββπ) β
β€) |
175 | 174 | peano2zd 12617 |
. . . . . . . . . . . . . . . 16
β’ (π β ((ββπ) + 1) β
β€) |
176 | | fzsn 13490 |
. . . . . . . . . . . . . . . 16
β’
(((ββπ)
+ 1) β β€ β (((ββπ) + 1)...((ββπ) + 1)) = {((ββπ) + 1)}) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (((ββπ) + 1)...((ββπ) + 1)) = {((ββπ) + 1)}) |
178 | 173, 177 | sylan9eqr 2799 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = (ββπ)) β (((ββπ) + 1)...(π + 1)) = {((ββπ) + 1)}) |
179 | 178 | raleqdv 3316 |
. . . . . . . . . . . . 13
β’ ((π β§ π = (ββπ)) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β βπ β {((ββπ) + 1)}0 β€ (π
βπ))) |
180 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’
((ββπ) +
1) β V |
181 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = ((ββπ) + 1) β (π
βπ) = (π
β((ββπ) + 1))) |
182 | 181 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = ((ββπ) + 1) β (0 β€ (π
βπ) β 0 β€ (π
β((ββπ) + 1)))) |
183 | 180, 182 | ralsn 4647 |
. . . . . . . . . . . . 13
β’
(βπ β
{((ββπ) + 1)}0
β€ (π
βπ) β 0 β€ (π
β((ββπ) + 1))) |
184 | 179, 183 | bitrdi 287 |
. . . . . . . . . . . 12
β’ ((π β§ π = (ββπ)) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β 0 β€ (π
β((ββπ) + 1)))) |
185 | 178 | raleqdv 3316 |
. . . . . . . . . . . . 13
β’ ((π β§ π = (ββπ)) β (βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0 β βπ β {((ββπ) + 1)} (π
βπ) β€ 0)) |
186 | 181 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π = ((ββπ) + 1) β ((π
βπ) β€ 0 β (π
β((ββπ) + 1)) β€ 0)) |
187 | 180, 186 | ralsn 4647 |
. . . . . . . . . . . . 13
β’
(βπ β
{((ββπ) + 1)}
(π
βπ) β€ 0 β (π
β((ββπ) + 1)) β€ 0) |
188 | 185, 187 | bitrdi 287 |
. . . . . . . . . . . 12
β’ ((π β§ π = (ββπ)) β (βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0 β (π
β((ββπ) + 1)) β€ 0)) |
189 | 184, 188 | orbi12d 918 |
. . . . . . . . . . 11
β’ ((π β§ π = (ββπ)) β ((βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0) β (0 β€ (π
β((ββπ) + 1)) β¨ (π
β((ββπ) + 1)) β€ 0))) |
190 | 171, 189 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π = (ββπ)) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0)) |
191 | 190 | a1d 25 |
. . . . . . . . 9
β’ ((π β§ π = (ββπ)) β ((βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0))) |
192 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((ββπ) + 1)...(ββ(πΎ Β· π))) β π β
(β€β₯β((ββπ) + 1))) |
193 | 192 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β
(β€β₯β((ββπ) + 1))) |
194 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β((ββπ) + 1)) β π β (((ββπ) + 1)...π)) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β (((ββπ) + 1)...π)) |
196 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π
βπ) = (π
βπ)) |
197 | 196 | breq2d 5122 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (0 β€ (π
βπ) β 0 β€ (π
βπ))) |
198 | 197 | rspcv 3580 |
. . . . . . . . . . . . . . 15
β’ (π β (((ββπ) + 1)...π) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β 0 β€ (π
βπ))) |
199 | 195, 198 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β 0 β€ (π
βπ))) |
200 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ βπ¦ β β ((π < π¦ β§ π¦ β€ (πΎ Β· π)) β§ (absβ((π
βπ¦) / π¦)) β€ πΈ)) |
201 | 200 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β Β¬ βπ¦ β β ((π < π¦ β§ π¦ β€ (πΎ Β· π)) β§ (absβ((π
βπ¦) / π¦)) β€ πΈ)) |
202 | | eluznn 12850 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((ββπ)
+ 1) β β β§ π
β (β€β₯β((ββπ) + 1))) β π β β) |
203 | 30, 192, 202 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β β) |
204 | 203 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β π β β) |
205 | | elfzle1 13451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (((ββπ) + 1)...(ββ(πΎ Β· π))) β ((ββπ) + 1) β€ π) |
206 | 205 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((ββπ) + 1) β€ π) |
207 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (((ββπ) + 1)...(ββ(πΎ Β· π))) β π β β€) |
208 | | zltp1le 12560 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((ββπ)
β β€ β§ π
β β€) β ((ββπ) < π β ((ββπ) + 1) β€ π)) |
209 | 174, 207,
208 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((ββπ) < π β ((ββπ) + 1) β€ π)) |
210 | 206, 209 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (ββπ) < π) |
211 | | fllt 13718 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π β β€) β (π < π β (ββπ) < π)) |
212 | 4, 207, 211 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π < π β (ββπ) < π)) |
213 | 210, 212 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π < π) |
214 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (((ββπ) + 1)...(ββ(πΎ Β· π))) β π β€ (ββ(πΎ Β· π))) |
215 | 214 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β€ (ββ(πΎ Β· π))) |
216 | | flge 13717 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΎ Β· π) β β β§ π β β€) β (π β€ (πΎ Β· π) β π β€ (ββ(πΎ Β· π)))) |
217 | 107, 207,
216 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π β€ (πΎ Β· π) β π β€ (ββ(πΎ Β· π)))) |
218 | 215, 217 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β€ (πΎ Β· π)) |
219 | 213, 218 | jca 513 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π < π β§ π β€ (πΎ Β· π))) |
220 | 219 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β (π < π β§ π β€ (πΎ Β· π))) |
221 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β πΈ β (0(,)1)) |
222 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β π β (π(,)+β)) |
223 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
224 | 35, 221, 6, 222, 204, 220, 223 | pntpbnd1a 26949 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β (absβ((π
βπ) / π)) β€ πΈ) |
225 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π β (π < π¦ β π < π)) |
226 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π β (π¦ β€ (πΎ Β· π) β π β€ (πΎ Β· π))) |
227 | 225, 226 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π β ((π < π¦ β§ π¦ β€ (πΎ Β· π)) β (π < π β§ π β€ (πΎ Β· π)))) |
228 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π β (π
βπ¦) = (π
βπ)) |
229 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π β π¦ = π) |
230 | 228, 229 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ = π β ((π
βπ¦) / π¦) = ((π
βπ) / π)) |
231 | 230 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π β (absβ((π
βπ¦) / π¦)) = (absβ((π
βπ) / π))) |
232 | 231 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π β ((absβ((π
βπ¦) / π¦)) β€ πΈ β (absβ((π
βπ) / π)) β€ πΈ)) |
233 | 227, 232 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β (((π < π¦ β§ π¦ β€ (πΎ Β· π)) β§ (absβ((π
βπ¦) / π¦)) β€ πΈ) β ((π < π β§ π β€ (πΎ Β· π)) β§ (absβ((π
βπ) / π)) β€ πΈ))) |
234 | 233 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ ((π < π β§ π β€ (πΎ Β· π)) β§ (absβ((π
βπ) / π)) β€ πΈ)) β βπ¦ β β ((π < π¦ β§ π¦ β€ (πΎ Β· π)) β§ (absβ((π
βπ¦) / π¦)) β€ πΈ)) |
235 | 204, 220,
224, 234 | syl12anc 836 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) β βπ¦ β β ((π < π¦ β§ π¦ β€ (πΎ Β· π)) β§ (absβ((π
βπ¦) / π¦)) β€ πΈ)) |
236 | 201, 235 | mtand 815 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β Β¬ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
237 | 236 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ 0 β€ (π
βπ)) β Β¬ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
238 | 203 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β π β β+) |
239 | 36 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β+
β (π
βπ) β
β) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
βπ) β β) |
241 | 240 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (π
βπ) β β) |
242 | 241 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (π
βπ) β β) |
243 | 242 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β ((π
βπ) β 0) = (π
βπ)) |
244 | 203 | peano2nnd 12177 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π + 1) β β) |
245 | 244 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π + 1) β
β+) |
246 | 36 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π + 1) β β+
β (π
β(π + 1)) β
β) |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (π
β(π + 1)) β β) |
248 | 247 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (π
β(π + 1)) β β) |
249 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β 0 β
β) |
250 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
β |
251 | | letric 11262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((0
β β β§ (π
β(π + 1)) β β) β (0 β€ (π
β(π + 1)) β¨ (π
β(π + 1)) β€ 0)) |
252 | 250, 247,
251 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (0 β€ (π
β(π + 1)) β¨ (π
β(π + 1)) β€ 0)) |
253 | 252 | ord 863 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (Β¬ 0 β€ (π
β(π + 1)) β (π
β(π + 1)) β€ 0)) |
254 | 253 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ Β¬ 0 β€ (π
β(π + 1))) β (π
β(π + 1)) β€ 0) |
255 | 254 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (π
β(π + 1)) β€ 0) |
256 | 248, 249,
241, 255 | lesub2dd 11779 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β ((π
βπ) β 0) β€ ((π
βπ) β (π
β(π + 1)))) |
257 | 243, 256 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (π
βπ) β€ ((π
βπ) β (π
β(π + 1)))) |
258 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β 0 β€ (π
βπ)) |
259 | 241, 258 | absidd 15314 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (absβ(π
βπ)) = (π
βπ)) |
260 | 248, 249,
241, 255, 258 | letrd 11319 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (π
β(π + 1)) β€ (π
βπ)) |
261 | 248, 241,
260 | abssuble0d 15324 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (absβ((π
β(π + 1)) β (π
βπ))) = ((π
βπ) β (π
β(π + 1)))) |
262 | 257, 259,
261 | 3brtr4d 5142 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (0 β€ (π
βπ) β§ Β¬ 0 β€ (π
β(π + 1)))) β (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
263 | 262 | expr 458 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ 0 β€ (π
βπ)) β (Β¬ 0 β€ (π
β(π + 1)) β (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ))))) |
264 | 237, 263 | mt3d 148 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ 0 β€ (π
βπ)) β 0 β€ (π
β(π + 1))) |
265 | 264 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (0 β€ (π
βπ) β 0 β€ (π
β(π + 1)))) |
266 | 199, 265 | syld 47 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β 0 β€ (π
β(π + 1)))) |
267 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (π + 1) β V |
268 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (π
βπ) = (π
β(π + 1))) |
269 | 268 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (0 β€ (π
βπ) β 0 β€ (π
β(π + 1)))) |
270 | 267, 269 | ralsn 4647 |
. . . . . . . . . . . . 13
β’
(βπ β
{(π + 1)}0 β€ (π
βπ) β 0 β€ (π
β(π + 1))) |
271 | 266, 270 | syl6ibr 252 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β βπ β {(π + 1)}0 β€ (π
βπ))) |
272 | 271 | ancld 552 |
. . . . . . . . . . 11
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β§ βπ β {(π + 1)}0 β€ (π
βπ)))) |
273 | | fzsuc 13495 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β((ββπ) + 1)) β (((ββπ) + 1)...(π + 1)) = ((((ββπ) + 1)...π) βͺ {(π + 1)})) |
274 | 193, 273 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (((ββπ) + 1)...(π + 1)) = ((((ββπ) + 1)...π) βͺ {(π + 1)})) |
275 | 274 | raleqdv 3316 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β βπ β ((((ββπ) + 1)...π) βͺ {(π + 1)})0 β€ (π
βπ))) |
276 | | ralunb 4156 |
. . . . . . . . . . . 12
β’
(βπ β
((((ββπ) +
1)...π) βͺ {(π + 1)})0 β€ (π
βπ) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β§ βπ β {(π + 1)}0 β€ (π
βπ))) |
277 | 275, 276 | bitrdi 287 |
. . . . . . . . . . 11
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β§ βπ β {(π + 1)}0 β€ (π
βπ)))) |
278 | 272, 277 | sylibrd 259 |
. . . . . . . . . 10
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ))) |
279 | 196 | breq1d 5120 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π
βπ) β€ 0 β (π
βπ) β€ 0)) |
280 | 279 | rspcv 3580 |
. . . . . . . . . . . . . . 15
β’ (π β (((ββπ) + 1)...π) β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β (π
βπ) β€ 0)) |
281 | 195, 280 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β (π
βπ) β€ 0)) |
282 | 236 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (π
βπ) β€ 0) β Β¬ (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
283 | 253 | con1d 145 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (Β¬ (π
β(π + 1)) β€ 0 β 0 β€ (π
β(π + 1)))) |
284 | 283 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ Β¬ (π
β(π + 1)) β€ 0) β 0 β€ (π
β(π + 1))) |
285 | 284 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β 0 β€ (π
β(π + 1))) |
286 | 240 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (π
βπ) β β) |
287 | 286 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β -(π
βπ) β β) |
288 | 247 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (π
β(π + 1)) β β) |
289 | 287, 288 | addge02d 11751 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (0 β€ (π
β(π + 1)) β -(π
βπ) β€ ((π
β(π + 1)) + -(π
βπ)))) |
290 | 285, 289 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β -(π
βπ) β€ ((π
β(π + 1)) + -(π
βπ))) |
291 | 288 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (π
β(π + 1)) β β) |
292 | 286 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (π
βπ) β β) |
293 | 291, 292 | negsubd 11525 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β ((π
β(π + 1)) + -(π
βπ)) = ((π
β(π + 1)) β (π
βπ))) |
294 | 290, 293 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β -(π
βπ) β€ ((π
β(π + 1)) β (π
βπ))) |
295 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (π
βπ) β€ 0) |
296 | 286, 295 | absnidd 15305 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (absβ(π
βπ)) = -(π
βπ)) |
297 | | 0red 11165 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β 0 β
β) |
298 | 286, 297,
288, 295, 285 | letrd 11319 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (π
βπ) β€ (π
β(π + 1))) |
299 | 286, 288,
298 | abssubge0d 15323 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (absβ((π
β(π + 1)) β (π
βπ))) = ((π
β(π + 1)) β (π
βπ))) |
300 | 294, 296,
299 | 3brtr4d 5142 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ ((π
βπ) β€ 0 β§ Β¬ (π
β(π + 1)) β€ 0)) β (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ)))) |
301 | 300 | expr 458 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (π
βπ) β€ 0) β (Β¬ (π
β(π + 1)) β€ 0 β (absβ(π
βπ)) β€ (absβ((π
β(π + 1)) β (π
βπ))))) |
302 | 282, 301 | mt3d 148 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β§ (π
βπ) β€ 0) β (π
β(π + 1)) β€ 0) |
303 | 302 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((π
βπ) β€ 0 β (π
β(π + 1)) β€ 0)) |
304 | 281, 303 | syld 47 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β (π
β(π + 1)) β€ 0)) |
305 | 268 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((π
βπ) β€ 0 β (π
β(π + 1)) β€ 0)) |
306 | 267, 305 | ralsn 4647 |
. . . . . . . . . . . . 13
β’
(βπ β
{(π + 1)} (π
βπ) β€ 0 β (π
β(π + 1)) β€ 0) |
307 | 304, 306 | syl6ibr 252 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β βπ β {(π + 1)} (π
βπ) β€ 0)) |
308 | 307 | ancld 552 |
. . . . . . . . . . 11
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β§ βπ β {(π + 1)} (π
βπ) β€ 0))) |
309 | 274 | raleqdv 3316 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0 β βπ β ((((ββπ) + 1)...π) βͺ {(π + 1)})(π
βπ) β€ 0)) |
310 | | ralunb 4156 |
. . . . . . . . . . . 12
β’
(βπ β
((((ββπ) +
1)...π) βͺ {(π + 1)})(π
βπ) β€ 0 β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β§ βπ β {(π + 1)} (π
βπ) β€ 0)) |
311 | 309, 310 | bitrdi 287 |
. . . . . . . . . . 11
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0 β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β§ βπ β {(π + 1)} (π
βπ) β€ 0))) |
312 | 308, 311 | sylibrd 259 |
. . . . . . . . . 10
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β (βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0 β βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0)) |
313 | 278, 312 | orim12d 964 |
. . . . . . . . 9
β’ ((π β§ π β (((ββπ) + 1)...(ββ(πΎ Β· π)))) β ((βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0))) |
314 | 191, 313 | jaodan 957 |
. . . . . . . 8
β’ ((π β§ (π = (ββπ) β¨ π β (((ββπ) + 1)...(ββ(πΎ Β· π))))) β ((βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0))) |
315 | 166, 314 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β ((ββπ)..^(ββ(πΎ Β· π)))) β ((βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0))) |
316 | 315 | expcom 415 |
. . . . . 6
β’ (π β ((ββπ)..^(ββ(πΎ Β· π))) β (π β ((βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0) β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0)))) |
317 | 316 | a2d 29 |
. . . . 5
β’ (π β ((ββπ)..^(ββ(πΎ Β· π))) β ((π β (βπ β (((ββπ) + 1)...π)0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...π)(π
βπ) β€ 0)) β (π β (βπ β (((ββπ) + 1)...(π + 1))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(π + 1))(π
βπ) β€ 0)))) |
318 | 134, 139,
144, 149, 161, 317 | fzind2 13697 |
. . . 4
β’
((ββ(πΎ
Β· π)) β
((ββπ)...(ββ(πΎ Β· π))) β (π β (βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0))) |
319 | 129, 318 | mpcom 38 |
. . 3
β’ (π β (βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))0 β€ (π
βπ) β¨ βπ β (((ββπ) + 1)...(ββ(πΎ Β· π)))(π
βπ) β€ 0)) |
320 | 58, 92, 319 | mpjaodan 958 |
. 2
β’ (π β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))(absβ((π
βπ) / (π Β· (π + 1))))) |
321 | | pntpbnd1.2 |
. . 3
β’ (π β βπ β β βπ β β€ (absβΞ£π¦ β (π...π)((π
βπ¦) / (π¦ Β· (π¦ + 1)))) β€ π΄) |
322 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = π β (π
βπ¦) = (π
βπ)) |
323 | | id 22 |
. . . . . . . . . 10
β’ (π¦ = π β π¦ = π) |
324 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π¦ = π β (π¦ + 1) = (π + 1)) |
325 | 323, 324 | oveq12d 7380 |
. . . . . . . . 9
β’ (π¦ = π β (π¦ Β· (π¦ + 1)) = (π Β· (π + 1))) |
326 | 322, 325 | oveq12d 7380 |
. . . . . . . 8
β’ (π¦ = π β ((π
βπ¦) / (π¦ Β· (π¦ + 1))) = ((π
βπ) / (π Β· (π + 1)))) |
327 | 326 | cbvsumv 15588 |
. . . . . . 7
β’
Ξ£π¦ β
(π...π)((π
βπ¦) / (π¦ Β· (π¦ + 1))) = Ξ£π β (π...π)((π
βπ) / (π Β· (π + 1))) |
328 | | oveq1 7369 |
. . . . . . . 8
β’ (π = ((ββπ) + 1) β (π...π) = (((ββπ) + 1)...π)) |
329 | 328 | sumeq1d 15593 |
. . . . . . 7
β’ (π = ((ββπ) + 1) β Ξ£π β (π...π)((π
βπ) / (π Β· (π + 1))) = Ξ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1)))) |
330 | 327, 329 | eqtrid 2789 |
. . . . . 6
β’ (π = ((ββπ) + 1) β Ξ£π¦ β (π...π)((π
βπ¦) / (π¦ Β· (π¦ + 1))) = Ξ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1)))) |
331 | 330 | fveq2d 6851 |
. . . . 5
β’ (π = ((ββπ) + 1) β
(absβΞ£π¦ β
(π...π)((π
βπ¦) / (π¦ Β· (π¦ + 1)))) = (absβΞ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1))))) |
332 | 331 | breq1d 5120 |
. . . 4
β’ (π = ((ββπ) + 1) β
((absβΞ£π¦ β
(π...π)((π
βπ¦) / (π¦ Β· (π¦ + 1)))) β€ π΄ β (absβΞ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1)))) β€ π΄)) |
333 | | oveq2 7370 |
. . . . . . 7
β’ (π = (ββ(πΎ Β· π)) β (((ββπ) + 1)...π) = (((ββπ) + 1)...(ββ(πΎ Β· π)))) |
334 | 333 | sumeq1d 15593 |
. . . . . 6
β’ (π = (ββ(πΎ Β· π)) β Ξ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1))) = Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) |
335 | 334 | fveq2d 6851 |
. . . . 5
β’ (π = (ββ(πΎ Β· π)) β (absβΞ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1)))) = (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1))))) |
336 | 335 | breq1d 5120 |
. . . 4
β’ (π = (ββ(πΎ Β· π)) β ((absβΞ£π β (((ββπ) + 1)...π)((π
βπ) / (π Β· (π + 1)))) β€ π΄ β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) β€ π΄)) |
337 | 332, 336 | rspc2va 3594 |
. . 3
β’
(((((ββπ) + 1) β β β§
(ββ(πΎ Β·
π)) β β€) β§
βπ β β
βπ β β€
(absβΞ£π¦ β
(π...π)((π
βπ¦) / (π¦ Β· (π¦ + 1)))) β€ π΄) β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) β€ π΄) |
338 | 30, 125, 321, 337 | syl21anc 837 |
. 2
β’ (π β (absβΞ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))((π
βπ) / (π Β· (π + 1)))) β€ π΄) |
339 | 320, 338 | eqbrtrrd 5134 |
1
β’ (π β Ξ£π β (((ββπ) + 1)...(ββ(πΎ Β· π)))(absβ((π
βπ) / (π Β· (π + 1)))) β€ π΄) |