Step | Hyp | Ref
| Expression |
1 | | nn0uz 12810 |
. 2
β’
β0 = (β€β₯β0) |
2 | | 1nn0 12434 |
. . 3
β’ 1 β
β0 |
3 | 2 | a1i 11 |
. 2
β’ (π β 1 β
β0) |
4 | | ax-1cn 11114 |
. . . . 5
β’ 1 β
β |
5 | | nn0cn 12428 |
. . . . . 6
β’ (π β β0
β π β
β) |
6 | 5 | adantl 483 |
. . . . 5
β’ ((π β§ π β β0) β π β
β) |
7 | | nn0ex 12424 |
. . . . . . 7
β’
β0 β V |
8 | 7 | mptex 7174 |
. . . . . 6
β’ (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) β V |
9 | 8 | shftval4 14968 |
. . . . 5
β’ ((1
β β β§ π
β β) β (((π
β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)βπ) = ((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(1 + π))) |
10 | 4, 6, 9 | sylancr 588 |
. . . 4
β’ ((π β§ π β β0) β (((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)βπ) = ((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(1 + π))) |
11 | | addcom 11346 |
. . . . . 6
β’ ((1
β β β§ π
β β) β (1 + π) = (π + 1)) |
12 | 4, 6, 11 | sylancr 588 |
. . . . 5
β’ ((π β§ π β β0) β (1 +
π) = (π + 1)) |
13 | 12 | fveq2d 6847 |
. . . 4
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))β(1 + π)) = ((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(π + 1))) |
14 | | peano2nn0 12458 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β0) |
15 | 14 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β0) β (π + 1) β
β0) |
16 | | id 22 |
. . . . . . . 8
β’ (π = (π + 1) β π = (π + 1)) |
17 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π = (π + 1) β (absβ((πΊβπ)βπ)) = (absβ((πΊβπ)β(π + 1)))) |
18 | 16, 17 | oveq12d 7376 |
. . . . . . 7
β’ (π = (π + 1) β (π Β· (absβ((πΊβπ)βπ))) = ((π + 1) Β· (absβ((πΊβπ)β(π + 1))))) |
19 | | eqid 2733 |
. . . . . . 7
β’ (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
20 | | ovex 7391 |
. . . . . . 7
β’ ((π + 1) Β·
(absβ((πΊβπ)β(π + 1)))) β V |
21 | 18, 19, 20 | fvmpt 6949 |
. . . . . 6
β’ ((π + 1) β β0
β ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(π + 1)) = ((π + 1) Β· (absβ((πΊβπ)β(π + 1))))) |
22 | 15, 21 | syl 17 |
. . . . 5
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))β(π + 1)) = ((π + 1) Β· (absβ((πΊβπ)β(π + 1))))) |
23 | | dvradcnv.x |
. . . . . . . 8
β’ (π β π β β) |
24 | | dvradcnv.g |
. . . . . . . . 9
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
25 | 24 | pserval2 25786 |
. . . . . . . 8
β’ ((π β β β§ (π + 1) β
β0) β ((πΊβπ)β(π + 1)) = ((π΄β(π + 1)) Β· (πβ(π + 1)))) |
26 | 23, 14, 25 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β β0) β ((πΊβπ)β(π + 1)) = ((π΄β(π + 1)) Β· (πβ(π + 1)))) |
27 | 26 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π β β0) β
(absβ((πΊβπ)β(π + 1))) = (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))) |
28 | 27 | oveq2d 7374 |
. . . . 5
β’ ((π β§ π β β0) β ((π + 1) Β·
(absβ((πΊβπ)β(π + 1)))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
29 | 22, 28 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))β(π + 1)) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
30 | 10, 13, 29 | 3eqtrd 2777 |
. . 3
β’ ((π β§ π β β0) β (((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)βπ) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
31 | 15 | nn0red 12479 |
. . . 4
β’ ((π β§ π β β0) β (π + 1) β
β) |
32 | | dvradcnv.a |
. . . . . . 7
β’ (π β π΄:β0βΆβ) |
33 | | ffvelcdm 7033 |
. . . . . . 7
β’ ((π΄:β0βΆβ β§
(π + 1) β
β0) β (π΄β(π + 1)) β β) |
34 | 32, 14, 33 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β β0) β (π΄β(π + 1)) β β) |
35 | | expcl 13991 |
. . . . . . 7
β’ ((π β β β§ (π + 1) β
β0) β (πβ(π + 1)) β β) |
36 | 23, 14, 35 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β β0) β (πβ(π + 1)) β β) |
37 | 34, 36 | mulcld 11180 |
. . . . 5
β’ ((π β§ π β β0) β ((π΄β(π + 1)) Β· (πβ(π + 1))) β β) |
38 | 37 | abscld 15327 |
. . . 4
β’ ((π β§ π β β0) β
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))) β β) |
39 | 31, 38 | remulcld 11190 |
. . 3
β’ ((π β§ π β β0) β ((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1))))) β β) |
40 | 30, 39 | eqeltrd 2834 |
. 2
β’ ((π β§ π β β0) β (((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)βπ) β β) |
41 | | oveq1 7365 |
. . . . . . 7
β’ (π = π β (π + 1) = (π + 1)) |
42 | 41 | fveq2d 6847 |
. . . . . . 7
β’ (π = π β (π΄β(π + 1)) = (π΄β(π + 1))) |
43 | 41, 42 | oveq12d 7376 |
. . . . . 6
β’ (π = π β ((π + 1) Β· (π΄β(π + 1))) = ((π + 1) Β· (π΄β(π + 1)))) |
44 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
45 | 43, 44 | oveq12d 7376 |
. . . . 5
β’ (π = π β (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) = (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
46 | | dvradcnv.h |
. . . . 5
β’ π» = (π β β0 β¦ (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
47 | | ovex 7391 |
. . . . 5
β’ (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) β V |
48 | 45, 46, 47 | fvmpt 6949 |
. . . 4
β’ (π β β0
β (π»βπ) = (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
49 | 48 | adantl 483 |
. . 3
β’ ((π β§ π β β0) β (π»βπ) = (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
50 | 15 | nn0cnd 12480 |
. . . . 5
β’ ((π β§ π β β0) β (π + 1) β
β) |
51 | 50, 34 | mulcld 11180 |
. . . 4
β’ ((π β§ π β β0) β ((π + 1) Β· (π΄β(π + 1))) β β) |
52 | | expcl 13991 |
. . . . 5
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
53 | 23, 52 | sylan 581 |
. . . 4
β’ ((π β§ π β β0) β (πβπ) β β) |
54 | 51, 53 | mulcld 11180 |
. . 3
β’ ((π β§ π β β0) β (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) β β) |
55 | 49, 54 | eqeltrd 2834 |
. 2
β’ ((π β§ π β β0) β (π»βπ) β β) |
56 | | dvradcnv.r |
. . . . . . . 8
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
57 | | dvradcnv.l |
. . . . . . . 8
β’ (π β (absβπ) < π
) |
58 | | id 22 |
. . . . . . . . . 10
β’ (π = π β π = π) |
59 | | 2fveq3 6848 |
. . . . . . . . . 10
β’ (π = π β (absβ((πΊβπ)βπ)) = (absβ((πΊβπ)βπ))) |
60 | 58, 59 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β (π Β· (absβ((πΊβπ)βπ))) = (π Β· (absβ((πΊβπ)βπ)))) |
61 | 60 | cbvmptv 5219 |
. . . . . . . 8
β’ (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
62 | 24, 32, 56, 23, 57, 61 | radcnvlt1 25793 |
. . . . . . 7
β’ (π β (seq0( + , (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))) β dom β β§ seq0( + , (abs
β (πΊβπ))) β dom β
)) |
63 | 62 | simpld 496 |
. . . . . 6
β’ (π β seq0( + , (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))) β dom β ) |
64 | | climdm 15442 |
. . . . . 6
β’ (seq0( +
, (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))) β dom β β seq0( + ,
(π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))) β ( β βseq0( + ,
(π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))))) |
65 | 63, 64 | sylib 217 |
. . . . 5
β’ (π β seq0( + , (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))) β ( β βseq0( + ,
(π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))))) |
66 | | 0z 12515 |
. . . . . 6
β’ 0 β
β€ |
67 | | neg1z 12544 |
. . . . . 6
β’ -1 β
β€ |
68 | 8 | isershft 15554 |
. . . . . 6
β’ ((0
β β€ β§ -1 β β€) β (seq0( + , (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))) β ( β βseq0( + ,
(π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))))) β seq(0 + -1)( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β ( β
βseq0( + , (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))))))) |
69 | 66, 67, 68 | mp2an 691 |
. . . . 5
β’ (seq0( +
, (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))) β ( β βseq0( + ,
(π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))))) β seq(0 + -1)( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β ( β
βseq0( + , (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))))) |
70 | 65, 69 | sylib 217 |
. . . 4
β’ (π β seq(0 + -1)( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β ( β
βseq0( + , (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))))) |
71 | | seqex 13914 |
. . . . 5
β’ seq(0 +
-1)( + , ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)) β V |
72 | | fvex 6856 |
. . . . 5
β’ ( β
βseq0( + , (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))))) β V |
73 | 71, 72 | breldm 5865 |
. . . 4
β’ (seq(0 +
-1)( + , ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)) β ( β
βseq0( + , (π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))))) β seq(0 + -1)( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β dom β
) |
74 | 70, 73 | syl 17 |
. . 3
β’ (π β seq(0 + -1)( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β dom β
) |
75 | | eqid 2733 |
. . . 4
β’
(β€β₯β(0 + -1)) =
(β€β₯β(0 + -1)) |
76 | | neg1cn 12272 |
. . . . . . . 8
β’ -1 β
β |
77 | 76 | addid2i 11348 |
. . . . . . 7
β’ (0 + -1)
= -1 |
78 | | 0le1 11683 |
. . . . . . . 8
β’ 0 β€
1 |
79 | | 1re 11160 |
. . . . . . . . 9
β’ 1 β
β |
80 | | le0neg2 11669 |
. . . . . . . . 9
β’ (1 β
β β (0 β€ 1 β -1 β€ 0)) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . 8
β’ (0 β€ 1
β -1 β€ 0) |
82 | 78, 81 | mpbi 229 |
. . . . . . 7
β’ -1 β€
0 |
83 | 77, 82 | eqbrtri 5127 |
. . . . . 6
β’ (0 + -1)
β€ 0 |
84 | 77, 67 | eqeltri 2830 |
. . . . . . 7
β’ (0 + -1)
β β€ |
85 | 84 | eluz1i 12776 |
. . . . . 6
β’ (0 β
(β€β₯β(0 + -1)) β (0 β β€ β§ (0 + -1)
β€ 0)) |
86 | 66, 83, 85 | mpbir2an 710 |
. . . . 5
β’ 0 β
(β€β₯β(0 + -1)) |
87 | 86 | a1i 11 |
. . . 4
β’ (π β 0 β
(β€β₯β(0 + -1))) |
88 | | eluzelcn 12780 |
. . . . . . 7
β’ (π β
(β€β₯β(0 + -1)) β π β β) |
89 | 88 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(0 +
-1))) β π β
β) |
90 | 4, 89, 9 | sylancr 588 |
. . . . 5
β’ ((π β§ π β (β€β₯β(0 +
-1))) β (((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)βπ) = ((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(1 + π))) |
91 | | nn0re 12427 |
. . . . . . . . . 10
β’ (π β β0
β π β
β) |
92 | 91 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β0) β π β
β) |
93 | 24, 32, 23 | psergf 25787 |
. . . . . . . . . . 11
β’ (π β (πΊβπ):β0βΆβ) |
94 | 93 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((πΊβπ)βπ) β β) |
95 | 94 | abscld 15327 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
(absβ((πΊβπ)βπ)) β β) |
96 | 92, 95 | remulcld 11190 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π Β· (absβ((πΊβπ)βπ))) β β) |
97 | 96 | recnd 11188 |
. . . . . . 7
β’ ((π β§ π β β0) β (π Β· (absβ((πΊβπ)βπ))) β β) |
98 | 97 | fmpttd 7064 |
. . . . . 6
β’ (π β (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))):β0βΆβ) |
99 | 4, 88, 11 | sylancr 588 |
. . . . . . 7
β’ (π β
(β€β₯β(0 + -1)) β (1 + π) = (π + 1)) |
100 | | eluzp1p1 12796 |
. . . . . . . 8
β’ (π β
(β€β₯β(0 + -1)) β (π + 1) β
(β€β₯β((0 + -1) + 1))) |
101 | 77 | oveq1i 7368 |
. . . . . . . . . . 11
β’ ((0 + -1)
+ 1) = (-1 + 1) |
102 | | 1pneg1e0 12277 |
. . . . . . . . . . . 12
β’ (1 + -1)
= 0 |
103 | 4, 76, 102 | addcomli 11352 |
. . . . . . . . . . 11
β’ (-1 + 1)
= 0 |
104 | 101, 103 | eqtri 2761 |
. . . . . . . . . 10
β’ ((0 + -1)
+ 1) = 0 |
105 | 104 | fveq2i 6846 |
. . . . . . . . 9
β’
(β€β₯β((0 + -1) + 1)) =
(β€β₯β0) |
106 | 1, 105 | eqtr4i 2764 |
. . . . . . . 8
β’
β0 = (β€β₯β((0 + -1) +
1)) |
107 | 100, 106 | eleqtrrdi 2845 |
. . . . . . 7
β’ (π β
(β€β₯β(0 + -1)) β (π + 1) β
β0) |
108 | 99, 107 | eqeltrd 2834 |
. . . . . 6
β’ (π β
(β€β₯β(0 + -1)) β (1 + π) β
β0) |
109 | | ffvelcdm 7033 |
. . . . . 6
β’ (((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))):β0βΆβ β§
(1 + π) β
β0) β ((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(1 + π)) β β) |
110 | 98, 108, 109 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (β€β₯β(0 +
-1))) β ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))β(1 + π)) β β) |
111 | 90, 110 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β (β€β₯β(0 +
-1))) β (((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)βπ) β β) |
112 | 75, 87, 111 | iserex 15547 |
. . 3
β’ (π β (seq(0 + -1)( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β dom β β
seq0( + , ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)) β dom β
)) |
113 | 74, 112 | mpbid 231 |
. 2
β’ (π β seq0( + , ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)) β dom β
) |
114 | | 1red 11161 |
. . 3
β’ ((π β§ π = 0) β 1 β
β) |
115 | | neqne 2948 |
. . . . 5
β’ (Β¬
π = 0 β π β 0) |
116 | | absrpcl 15179 |
. . . . 5
β’ ((π β β β§ π β 0) β (absβπ) β
β+) |
117 | 23, 115, 116 | syl2an 597 |
. . . 4
β’ ((π β§ Β¬ π = 0) β (absβπ) β
β+) |
118 | 117 | rprecred 12973 |
. . 3
β’ ((π β§ Β¬ π = 0) β (1 / (absβπ)) β
β) |
119 | 114, 118 | ifclda 4522 |
. 2
β’ (π β if(π = 0, 1, (1 / (absβπ))) β β) |
120 | | oveq1 7365 |
. . . . 5
β’ (1 =
if(π = 0, 1, (1 /
(absβπ))) β (1
Β· ((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
121 | 120 | breq2d 5118 |
. . . 4
β’ (1 =
if(π = 0, 1, (1 /
(absβπ))) β
((absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ (1 Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) β (absβ(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) β€ (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))))) |
122 | | oveq1 7365 |
. . . . 5
β’ ((1 /
(absβπ)) = if(π = 0, 1, (1 / (absβπ))) β ((1 /
(absβπ)) Β·
((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
123 | 122 | breq2d 5118 |
. . . 4
β’ ((1 /
(absβπ)) = if(π = 0, 1, (1 / (absβπ))) β ((absβ(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) β€ ((1 / (absβπ)) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) β (absβ(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) β€ (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))))) |
124 | | elnnuz 12812 |
. . . . . . . 8
β’ (π β β β π β
(β€β₯β1)) |
125 | | nnnn0 12425 |
. . . . . . . 8
β’ (π β β β π β
β0) |
126 | 124, 125 | sylbir 234 |
. . . . . . 7
β’ (π β
(β€β₯β1) β π β β0) |
127 | 15 | nn0ge0d 12481 |
. . . . . . . 8
β’ ((π β§ π β β0) β 0 β€
(π + 1)) |
128 | 37 | absge0d 15335 |
. . . . . . . 8
β’ ((π β§ π β β0) β 0 β€
(absβ((π΄β(π + 1)) Β· (πβ(π + 1))))) |
129 | 31, 38, 127, 128 | mulge0d 11737 |
. . . . . . 7
β’ ((π β§ π β β0) β 0 β€
((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
130 | 126, 129 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (β€β₯β1))
β 0 β€ ((π + 1)
Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
131 | 130 | adantr 482 |
. . . . 5
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β 0 β€
((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
132 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = 0 β (πβπ) = (0βπ)) |
133 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯β1))
β π β
(β€β₯β1)) |
134 | 133, 124 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯β1))
β π β
β) |
135 | 134 | 0expd 14050 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯β1))
β (0βπ) =
0) |
136 | 132, 135 | sylan9eqr 2795 |
. . . . . . . 8
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β (πβπ) = 0) |
137 | 136 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β
(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) = (((π + 1) Β· (π΄β(π + 1))) Β· 0)) |
138 | 51 | mul01d 11359 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (((π + 1) Β· (π΄β(π + 1))) Β· 0) = 0) |
139 | 126, 138 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β1))
β (((π + 1) Β·
(π΄β(π + 1))) Β· 0) =
0) |
140 | 139 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β
(((π + 1) Β· (π΄β(π + 1))) Β· 0) = 0) |
141 | 137, 140 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β
(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) = 0) |
142 | 141 | abs00bd 15182 |
. . . . 5
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) = 0) |
143 | 39 | recnd 11188 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1))))) β β) |
144 | 143 | mulid2d 11178 |
. . . . . . 7
β’ ((π β§ π β β0) β (1
Β· ((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
145 | 126, 144 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (β€β₯β1))
β (1 Β· ((π + 1)
Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
146 | 145 | adantr 482 |
. . . . 5
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β (1
Β· ((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
147 | 131, 142,
146 | 3brtr4d 5138 |
. . . 4
β’ (((π β§ π β (β€β₯β1))
β§ π = 0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ (1 Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
148 | | df-ne 2941 |
. . . . 5
β’ (π β 0 β Β¬ π = 0) |
149 | 54 | abscld 15327 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β β) |
150 | 50, 34, 53 | mulassd 11183 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) = ((π + 1) Β· ((π΄β(π + 1)) Β· (πβπ)))) |
151 | 150 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) = (absβ((π + 1) Β· ((π΄β(π + 1)) Β· (πβπ))))) |
152 | 34, 53 | mulcld 11180 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((π΄β(π + 1)) Β· (πβπ)) β β) |
153 | 50, 152 | absmuld 15345 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
(absβ((π + 1)
Β· ((π΄β(π + 1)) Β· (πβπ)))) = ((absβ(π + 1)) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
154 | 31, 127 | absidd 15313 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β
(absβ(π + 1)) =
(π + 1)) |
155 | 154 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
((absβ(π + 1))
Β· (absβ((π΄β(π + 1)) Β· (πβπ)))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
156 | 151, 153,
155 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
157 | 149, 156 | eqled 11263 |
. . . . . . . 8
β’ ((π β§ π β β0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
158 | 157 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β 0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
159 | 23 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π β
β) |
160 | 116 | rpreccld 12972 |
. . . . . . . . . . 11
β’ ((π β β β§ π β 0) β (1 /
(absβπ)) β
β+) |
161 | 159, 160 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β 0) β (1 /
(absβπ)) β
β+) |
162 | 161 | rpcnd 12964 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β 0) β (1 /
(absβπ)) β
β) |
163 | 50 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β 0) β (π + 1) β
β) |
164 | 38 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β 0) β
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))) β β) |
165 | 164 | recnd 11188 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β 0) β
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))) β β) |
166 | 162, 163,
165 | mul12d 11369 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π β 0) β ((1 /
(absβπ)) Β·
((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = ((π + 1) Β· ((1 / (absβπ)) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
167 | 37 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β 0) β ((π΄β(π + 1)) Β· (πβ(π + 1))) β β) |
168 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β 0) β π β
β) |
169 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β 0) β π β 0) |
170 | 167, 168,
169 | absdivd 15346 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β 0) β
(absβ(((π΄β(π + 1)) Β· (πβ(π + 1))) / π)) = ((absβ((π΄β(π + 1)) Β· (πβ(π + 1)))) / (absβπ))) |
171 | 34 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ π β 0) β (π΄β(π + 1)) β β) |
172 | 36 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ π β 0) β (πβ(π + 1)) β β) |
173 | 171, 172,
168, 169 | divassd 11971 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ π β 0) β (((π΄β(π + 1)) Β· (πβ(π + 1))) / π) = ((π΄β(π + 1)) Β· ((πβ(π + 1)) / π))) |
174 | 6 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ π β 0) β π β
β) |
175 | | pncan 11412 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
176 | 174, 4, 175 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β 0) β ((π + 1) β 1) = π) |
177 | 176 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β 0) β (πβ((π + 1) β 1)) = (πβπ)) |
178 | 15 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (π + 1) β
β€) |
179 | 178 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ π β 0) β (π + 1) β
β€) |
180 | 168, 169,
179 | expm1d 14067 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β 0) β (πβ((π + 1) β 1)) = ((πβ(π + 1)) / π)) |
181 | 177, 180 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ π β 0) β (πβπ) = ((πβ(π + 1)) / π)) |
182 | 181 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ π β 0) β ((π΄β(π + 1)) Β· (πβπ)) = ((π΄β(π + 1)) Β· ((πβ(π + 1)) / π))) |
183 | 173, 182 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β 0) β (((π΄β(π + 1)) Β· (πβ(π + 1))) / π) = ((π΄β(π + 1)) Β· (πβπ))) |
184 | 183 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β 0) β
(absβ(((π΄β(π + 1)) Β· (πβ(π + 1))) / π)) = (absβ((π΄β(π + 1)) Β· (πβπ)))) |
185 | 23 | abscld 15327 |
. . . . . . . . . . . . 13
β’ (π β (absβπ) β
β) |
186 | 185 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ π β 0) β (absβπ) β
β) |
187 | 186 | recnd 11188 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β 0) β (absβπ) β
β) |
188 | 159, 116 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ π β 0) β (absβπ) β
β+) |
189 | 188 | rpne0d 12967 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β 0) β (absβπ) β 0) |
190 | 165, 187,
189 | divrec2d 11940 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β 0) β
((absβ((π΄β(π + 1)) Β· (πβ(π + 1)))) / (absβπ)) = ((1 / (absβπ)) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) |
191 | 170, 184,
190 | 3eqtr3rd 2782 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β 0) β ((1 /
(absβπ)) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1))))) = (absβ((π΄β(π + 1)) Β· (πβπ)))) |
192 | 191 | oveq2d 7374 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π β 0) β ((π + 1) Β· ((1 /
(absβπ)) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
193 | 166, 192 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π β 0) β ((1 /
(absβπ)) Β·
((π + 1) Β·
(absβ((π΄β(π + 1)) Β· (πβ(π + 1)))))) = ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβπ))))) |
194 | 158, 193 | breqtrrd 5134 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β 0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ ((1 / (absβπ)) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
195 | 126, 194 | sylanl2 680 |
. . . . 5
β’ (((π β§ π β (β€β₯β1))
β§ π β 0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ ((1 / (absβπ)) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
196 | 148, 195 | sylan2br 596 |
. . . 4
β’ (((π β§ π β (β€β₯β1))
β§ Β¬ π = 0) β
(absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ ((1 / (absβπ)) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
197 | 121, 123,
147, 196 | ifbothda 4525 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (absβ(((π + 1)
Β· (π΄β(π + 1))) Β· (πβπ))) β€ (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
198 | 49 | fveq2d 6847 |
. . . 4
β’ ((π β§ π β β0) β
(absβ(π»βπ)) = (absβ(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)))) |
199 | 126, 198 | sylan2 594 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (absβ(π»βπ)) = (absβ(((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)))) |
200 | 30 | oveq2d 7374 |
. . . 4
β’ ((π β§ π β β0) β (if(π = 0, 1, (1 / (absβπ))) Β· (((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) shift -1)βπ)) = (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
201 | 126, 200 | sylan2 594 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (if(π = 0, 1, (1 /
(absβπ))) Β·
(((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)βπ)) = (if(π = 0, 1, (1 / (absβπ))) Β· ((π + 1) Β· (absβ((π΄β(π + 1)) Β· (πβ(π + 1))))))) |
202 | 197, 199,
201 | 3brtr4d 5138 |
. 2
β’ ((π β§ π β (β€β₯β1))
β (absβ(π»βπ)) β€ (if(π = 0, 1, (1 / (absβπ))) Β· (((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) shift -1)βπ))) |
203 | 1, 3, 40, 55, 113, 119, 202 | cvgcmpce 15708 |
1
β’ (π β seq0( + , π») β dom β
) |