Step | Hyp | Ref
| Expression |
1 | | nnuz 12811 |
. . 3
β’ β =
(β€β₯β1) |
2 | | 1zzd 12539 |
. . 3
β’ (π β 1 β
β€) |
3 | | eqid 2733 |
. . . 4
β’ (π β β β¦ (((π΄ + 1) Β·
(logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))) = (π β β β¦ (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))) |
4 | | lgamcvg.a |
. . . . 5
β’ (π β π΄ β (β β (β€ β
β))) |
5 | | 1nn0 12434 |
. . . . . 6
β’ 1 β
β0 |
6 | 5 | a1i 11 |
. . . . 5
β’ (π β 1 β
β0) |
7 | 4, 6 | dmgmaddnn0 26392 |
. . . 4
β’ (π β (π΄ + 1) β (β β (β€
β β))) |
8 | 3, 7 | lgamcvg 26419 |
. . 3
β’ (π β seq1( + , (π β β β¦ (((π΄ + 1) Β·
(logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))))) β ((log Ξβ(π΄ + 1)) + (logβ(π΄ + 1)))) |
9 | | seqex 13914 |
. . . 4
β’ seq1( + ,
πΊ) β
V |
10 | 9 | a1i 11 |
. . 3
β’ (π β seq1( + , πΊ) β V) |
11 | 4 | eldifad 3923 |
. . . . . . . 8
β’ (π β π΄ β β) |
12 | 11 | abscld 15327 |
. . . . . . 7
β’ (π β (absβπ΄) β
β) |
13 | | arch 12415 |
. . . . . . 7
β’
((absβπ΄)
β β β βπ β β (absβπ΄) < π) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β βπ β β (absβπ΄) < π) |
15 | | eqid 2733 |
. . . . . . . . 9
β’
(β€β₯βπ) = (β€β₯βπ) |
16 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β π β β) |
17 | 16 | nnzd 12531 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β π β β€) |
18 | | eqid 2733 |
. . . . . . . . . . 11
β’ (β
β (-β(,]0)) = (β β (-β(,]0)) |
19 | 18 | logcn 26018 |
. . . . . . . . . 10
β’ (log
βΎ (β β (-β(,]0))) β ((β β
(-β(,]0))βcnββ) |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (log βΎ (β β
(-β(,]0))) β ((β β (-β(,]0))βcnββ)) |
21 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(1(ballβ(abs β β ))1) = (1(ballβ(abs β
β ))1) |
22 | 21 | dvlog2lem 26023 |
. . . . . . . . . . 11
β’
(1(ballβ(abs β β ))1) β (β β
(-β(,]0)) |
23 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π΄ β β) |
24 | | eluznn 12848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
25 | 24 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (π β
(β€β₯βπ) β π β β)) |
26 | 25 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (π β (β€β₯βπ) β π β β)) |
27 | 26 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π β β) |
28 | 27 | nncnd 12174 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π β β) |
29 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β 1 β
β) |
30 | 28, 29 | addcld 11179 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π + 1) β β) |
31 | 27 | peano2nnd 12175 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π + 1) β β) |
32 | 31 | nnne0d 12208 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π + 1) β 0) |
33 | 23, 30, 32 | divcld 11936 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π΄ / (π + 1)) β β) |
34 | 33, 29 | addcld 11179 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((π΄ / (π + 1)) + 1) β β) |
35 | | ax-1cn 11114 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
36 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (abs
β β ) = (abs β β ) |
37 | 36 | cnmetdval 24150 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ / (π + 1)) + 1) β β β§ 1 β
β) β (((π΄ /
(π + 1)) + 1)(abs β
β )1) = (absβ(((π΄ / (π + 1)) + 1) β 1))) |
38 | 34, 35, 37 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (((π΄ / (π + 1)) + 1)(abs β β )1) =
(absβ(((π΄ / (π + 1)) + 1) β
1))) |
39 | 33, 29 | pncand 11518 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (((π΄ / (π + 1)) + 1) β 1) = (π΄ / (π + 1))) |
40 | 39 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβ(((π΄ / (π + 1)) + 1) β 1)) = (absβ(π΄ / (π + 1)))) |
41 | 23, 30, 32 | absdivd 15346 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβ(π΄ / (π + 1))) = ((absβπ΄) / (absβ(π + 1)))) |
42 | 31 | nnred 12173 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π + 1) β β) |
43 | 31 | nnrpd 12960 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π + 1) β
β+) |
44 | 43 | rpge0d 12966 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β 0 β€ (π + 1)) |
45 | 42, 44 | absidd 15313 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβ(π + 1)) = (π + 1)) |
46 | 45 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((absβπ΄) / (absβ(π + 1))) = ((absβπ΄) / (π + 1))) |
47 | 41, 46 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβ(π΄ / (π + 1))) = ((absβπ΄) / (π + 1))) |
48 | 38, 40, 47 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (((π΄ / (π + 1)) + 1)(abs β β )1) =
((absβπ΄) / (π + 1))) |
49 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβπ΄) β
β) |
50 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π β β) |
51 | 50 | nnred 12173 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π β β) |
52 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβπ΄) < π) |
53 | | eluzle 12781 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯βπ) β π β€ π) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π β€ π) |
55 | | nnleltp1 12563 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β (π β€ π β π < (π + 1))) |
56 | 50, 27, 55 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (π β€ π β π < (π + 1))) |
57 | 54, 56 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β π < (π + 1)) |
58 | 49, 51, 42, 52, 57 | lttrd 11321 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβπ΄) < (π + 1)) |
59 | 30 | mulid1d 11177 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((π + 1) Β· 1) = (π + 1)) |
60 | 58, 59 | breqtrrd 5134 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (absβπ΄) < ((π + 1) Β· 1)) |
61 | | 1red 11161 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β 1 β
β) |
62 | 49, 61, 43 | ltdivmuld 13013 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (((absβπ΄) / (π + 1)) < 1 β (absβπ΄) < ((π + 1) Β· 1))) |
63 | 60, 62 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((absβπ΄) / (π + 1)) < 1) |
64 | 48, 63 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (((π΄ / (π + 1)) + 1)(abs β β )1) <
1) |
65 | | cnxmet 24152 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) β (βMetββ) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (abs β β )
β (βMetββ)) |
67 | | 1rp 12924 |
. . . . . . . . . . . . . 14
β’ 1 β
β+ |
68 | | rpxr 12929 |
. . . . . . . . . . . . . 14
β’ (1 β
β+ β 1 β β*) |
69 | 67, 68 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β 1 β
β*) |
70 | | elbl3 23761 |
. . . . . . . . . . . . 13
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (1 β β β§ ((π΄ / (π + 1)) + 1) β β)) β (((π΄ / (π + 1)) + 1) β (1(ballβ(abs β
β ))1) β (((π΄ /
(π + 1)) + 1)(abs β
β )1) < 1)) |
71 | 66, 69, 29, 34, 70 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β (((π΄ / (π + 1)) + 1) β (1(ballβ(abs β
β ))1) β (((π΄ /
(π + 1)) + 1)(abs β
β )1) < 1)) |
72 | 64, 71 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((π΄ / (π + 1)) + 1) β (1(ballβ(abs β
β ))1)) |
73 | 22, 72 | sselid 3943 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((π΄ / (π + 1)) + 1) β (β β
(-β(,]0))) |
74 | 73 | fmpttd 7064 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (π β (β€β₯βπ) β¦ ((π΄ / (π + 1)) +
1)):(β€β₯βπ)βΆ(β β
(-β(,]0))) |
75 | 26 | ssrdv 3951 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (β€β₯βπ) β
β) |
76 | 75 | resmptd 5995 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((π β β β¦ ((π΄ / (π + 1)) + 1)) βΎ
(β€β₯βπ)) = (π β (β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1))) |
77 | | nnex 12164 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
78 | 77 | mptex 7174 |
. . . . . . . . . . . . . . . 16
β’ (π β β β¦ (π΄ / (π + 1))) β V |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π β β β¦ (π΄ / (π + 1))) β V) |
80 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π + 1) = (π + 1)) |
81 | 80 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π΄ / (π + 1)) = (π΄ / (π + 1))) |
82 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β¦ (π΄ / (π + 1))) = (π β β β¦ (π΄ / (π + 1))) |
83 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ / (π + 1)) β V |
84 | 81, 82, 83 | fvmpt 6949 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π β β β¦ (π΄ / (π + 1)))βπ) = (π΄ / (π + 1))) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((π β β β¦ (π΄ / (π + 1)))βπ) = (π΄ / (π + 1))) |
86 | 1, 2, 11, 2, 79, 85 | divcnvshft 15745 |
. . . . . . . . . . . . . 14
β’ (π β (π β β β¦ (π΄ / (π + 1))) β 0) |
87 | | 1cnd 11155 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
88 | 77 | mptex 7174 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ ((π΄ / (π + 1)) + 1)) β V |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (π β β β¦ ((π΄ / (π + 1)) + 1)) β V) |
90 | 11 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π΄ β β) |
91 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β) |
92 | 91 | nncnd 12174 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β β) |
93 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β 1 β
β) |
94 | 92, 93 | addcld 11179 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (π + 1) β β) |
95 | 91 | peano2nnd 12175 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π + 1) β β) |
96 | 95 | nnne0d 12208 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (π + 1) β 0) |
97 | 90, 94, 96 | divcld 11936 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π΄ / (π + 1)) β β) |
98 | 85, 97 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π β β β¦ (π΄ / (π + 1)))βπ) β β) |
99 | 81 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((π΄ / (π + 1)) + 1) = ((π΄ / (π + 1)) + 1)) |
100 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β¦ ((π΄ / (π + 1)) + 1)) = (π β β β¦ ((π΄ / (π + 1)) + 1)) |
101 | | ovex 7391 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ / (π + 1)) + 1) β V |
102 | 99, 100, 101 | fvmpt 6949 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π β β β¦ ((π΄ / (π + 1)) + 1))βπ) = ((π΄ / (π + 1)) + 1)) |
103 | 102 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((π β β β¦ ((π΄ / (π + 1)) + 1))βπ) = ((π΄ / (π + 1)) + 1)) |
104 | 85 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (((π β β β¦ (π΄ / (π + 1)))βπ) + 1) = ((π΄ / (π + 1)) + 1)) |
105 | 103, 104 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π β β β¦ ((π΄ / (π + 1)) + 1))βπ) = (((π β β β¦ (π΄ / (π + 1)))βπ) + 1)) |
106 | 1, 2, 86, 87, 89, 98, 105 | climaddc1 15523 |
. . . . . . . . . . . . 13
β’ (π β (π β β β¦ ((π΄ / (π + 1)) + 1)) β (0 +
1)) |
107 | | 0p1e1 12280 |
. . . . . . . . . . . . 13
β’ (0 + 1) =
1 |
108 | 106, 107 | breqtrdi 5147 |
. . . . . . . . . . . 12
β’ (π β (π β β β¦ ((π΄ / (π + 1)) + 1)) β 1) |
109 | 108 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (π β β β¦ ((π΄ / (π + 1)) + 1)) β 1) |
110 | | climres 15463 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ (π β β β¦ ((π΄ / (π + 1)) + 1)) β V) β (((π β β β¦ ((π΄ / (π + 1)) + 1)) βΎ
(β€β₯βπ)) β 1 β (π β β β¦ ((π΄ / (π + 1)) + 1)) β 1)) |
111 | 17, 88, 110 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (((π β β β¦ ((π΄ / (π + 1)) + 1)) βΎ
(β€β₯βπ)) β 1 β (π β β β¦ ((π΄ / (π + 1)) + 1)) β 1)) |
112 | 109, 111 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((π β β β¦ ((π΄ / (π + 1)) + 1)) βΎ
(β€β₯βπ)) β 1) |
113 | 76, 112 | eqbrtrrd 5130 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (π β (β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1)) β 1) |
114 | 67 | a1i 11 |
. . . . . . . . . . 11
β’ (1 β
β β 1 β β+) |
115 | 18 | ellogdm 26010 |
. . . . . . . . . . 11
β’ (1 β
(β β (-β(,]0)) β (1 β β β§ (1 β
β β 1 β β+))) |
116 | 35, 114, 115 | mpbir2an 710 |
. . . . . . . . . 10
β’ 1 β
(β β (-β(,]0)) |
117 | 116 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β 1 β (β β
(-β(,]0))) |
118 | 15, 17, 20, 74, 113, 117 | climcncf 24279 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((log βΎ (β β
(-β(,]0))) β (π
β (β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1))) β ((log βΎ (β
β (-β(,]0)))β1)) |
119 | | logf1o 25936 |
. . . . . . . . . . 11
β’
log:(β β {0})β1-1-ontoβran
log |
120 | | f1of 6785 |
. . . . . . . . . . 11
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})βΆran log) |
121 | 119, 120 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β log:(β β
{0})βΆran log) |
122 | 18 | logdmss 26013 |
. . . . . . . . . . 11
β’ (β
β (-β(,]0)) β (β β {0}) |
123 | 122, 73 | sselid 3943 |
. . . . . . . . . 10
β’ (((π β§ (π β β β§ (absβπ΄) < π)) β§ π β (β€β₯βπ)) β ((π΄ / (π + 1)) + 1) β (β β
{0})) |
124 | 121, 123 | cofmpt 7079 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (log β (π β (β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1))) = (π β (β€β₯βπ) β¦ (logβ((π΄ / (π + 1)) + 1)))) |
125 | | frn 6676 |
. . . . . . . . . 10
β’ ((π β
(β€β₯βπ) β¦ ((π΄ / (π + 1)) +
1)):(β€β₯βπ)βΆ(β β (-β(,]0))
β ran (π β
(β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1)) β (β β
(-β(,]0))) |
126 | | cores 6202 |
. . . . . . . . . 10
β’ (ran
(π β
(β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1)) β (β β
(-β(,]0)) β ((log βΎ (β β (-β(,]0))) β
(π β
(β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1))) = (log β (π β
(β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1)))) |
127 | 74, 125, 126 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((log βΎ (β β
(-β(,]0))) β (π
β (β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1))) = (log β (π β
(β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1)))) |
128 | 75 | resmptd 5995 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((π β β β¦ (logβ((π΄ / (π + 1)) + 1))) βΎ
(β€β₯βπ)) = (π β (β€β₯βπ) β¦ (logβ((π΄ / (π + 1)) + 1)))) |
129 | 124, 127,
128 | 3eqtr4d 2783 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((log βΎ (β β
(-β(,]0))) β (π
β (β€β₯βπ) β¦ ((π΄ / (π + 1)) + 1))) = ((π β β β¦ (logβ((π΄ / (π + 1)) + 1))) βΎ
(β€β₯βπ))) |
130 | | fvres 6862 |
. . . . . . . . . 10
β’ (1 β
(β β (-β(,]0)) β ((log βΎ (β β
(-β(,]0)))β1) = (logβ1)) |
131 | 116, 130 | mp1i 13 |
. . . . . . . . 9
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((log βΎ (β β
(-β(,]0)))β1) = (logβ1)) |
132 | | log1 25957 |
. . . . . . . . 9
β’
(logβ1) = 0 |
133 | 131, 132 | eqtrdi 2789 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((log βΎ (β β
(-β(,]0)))β1) = 0) |
134 | 118, 129,
133 | 3brtr3d 5137 |
. . . . . . 7
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β ((π β β β¦ (logβ((π΄ / (π + 1)) + 1))) βΎ
(β€β₯βπ)) β 0) |
135 | 77 | mptex 7174 |
. . . . . . . 8
β’ (π β β β¦
(logβ((π΄ / (π + 1)) + 1))) β
V |
136 | | climres 15463 |
. . . . . . . 8
β’ ((π β β€ β§ (π β β β¦
(logβ((π΄ / (π + 1)) + 1))) β V) β
(((π β β β¦
(logβ((π΄ / (π + 1)) + 1))) βΎ
(β€β₯βπ)) β 0 β (π β β β¦ (logβ((π΄ / (π + 1)) + 1))) β 0)) |
137 | 17, 135, 136 | sylancl 587 |
. . . . . . 7
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (((π β β β¦ (logβ((π΄ / (π + 1)) + 1))) βΎ
(β€β₯βπ)) β 0 β (π β β β¦ (logβ((π΄ / (π + 1)) + 1))) β 0)) |
138 | 134, 137 | mpbid 231 |
. . . . . 6
β’ ((π β§ (π β β β§ (absβπ΄) < π)) β (π β β β¦ (logβ((π΄ / (π + 1)) + 1))) β 0) |
139 | 14, 138 | rexlimddv 3155 |
. . . . 5
β’ (π β (π β β β¦ (logβ((π΄ / (π + 1)) + 1))) β 0) |
140 | 11, 87 | addcld 11179 |
. . . . . 6
β’ (π β (π΄ + 1) β β) |
141 | 7 | dmgmn0 26391 |
. . . . . 6
β’ (π β (π΄ + 1) β 0) |
142 | 140, 141 | logcld 25942 |
. . . . 5
β’ (π β (logβ(π΄ + 1)) β
β) |
143 | 77 | mptex 7174 |
. . . . . 6
β’ (π β β β¦
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) + 1)))) β
V |
144 | 143 | a1i 11 |
. . . . 5
β’ (π β (π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) β
V) |
145 | 81 | fvoveq1d 7380 |
. . . . . . . 8
β’ (π = π β (logβ((π΄ / (π + 1)) + 1)) = (logβ((π΄ / (π + 1)) + 1))) |
146 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦
(logβ((π΄ / (π + 1)) + 1))) = (π β β β¦
(logβ((π΄ / (π + 1)) + 1))) |
147 | | fvex 6856 |
. . . . . . . 8
β’
(logβ((π΄ /
(π + 1)) + 1)) β
V |
148 | 145, 146,
147 | fvmpt 6949 |
. . . . . . 7
β’ (π β β β ((π β β β¦
(logβ((π΄ / (π + 1)) + 1)))βπ) = (logβ((π΄ / (π + 1)) + 1))) |
149 | 148 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ (logβ((π΄ / (π + 1)) + 1)))βπ) = (logβ((π΄ / (π + 1)) + 1))) |
150 | 97, 93 | addcld 11179 |
. . . . . . 7
β’ ((π β§ π β β) β ((π΄ / (π + 1)) + 1) β β) |
151 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π΄ β (β β (β€ β
β))) |
152 | 151, 95 | dmgmdivn0 26393 |
. . . . . . 7
β’ ((π β§ π β β) β ((π΄ / (π + 1)) + 1) β 0) |
153 | 150, 152 | logcld 25942 |
. . . . . 6
β’ ((π β§ π β β) β (logβ((π΄ / (π + 1)) + 1)) β β) |
154 | 149, 153 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ (logβ((π΄ / (π + 1)) + 1)))βπ) β β) |
155 | 145 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β ((logβ(π΄ + 1)) β (logβ((π΄ / (π + 1)) + 1))) = ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) |
156 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) + 1)))) = (π β β β¦
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) +
1)))) |
157 | | ovex 7391 |
. . . . . . . 8
β’
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) + 1))) β
V |
158 | 155, 156,
157 | fvmpt 6949 |
. . . . . . 7
β’ (π β β β ((π β β β¦
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) +
1))))βπ) =
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) +
1)))) |
159 | 158 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))βπ) = ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) |
160 | 149 | oveq2d 7374 |
. . . . . 6
β’ ((π β§ π β β) β ((logβ(π΄ + 1)) β ((π β β β¦
(logβ((π΄ / (π + 1)) + 1)))βπ)) = ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) |
161 | 159, 160 | eqtr4d 2776 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))βπ) = ((logβ(π΄ + 1)) β ((π β β β¦
(logβ((π΄ / (π + 1)) + 1)))βπ))) |
162 | 1, 2, 139, 142, 144, 154, 161 | climsubc2 15527 |
. . . 4
β’ (π β (π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) β
((logβ(π΄ + 1))
β 0)) |
163 | 142 | subid1d 11506 |
. . . 4
β’ (π β ((logβ(π΄ + 1)) β 0) =
(logβ(π΄ +
1))) |
164 | 162, 163 | breqtrd 5132 |
. . 3
β’ (π β (π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) β
(logβ(π΄ +
1))) |
165 | | elfznn 13476 |
. . . . . . 7
β’ (π β (1...π) β π β β) |
166 | 165 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
167 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π = π β (π + 1) = (π + 1)) |
168 | | id 22 |
. . . . . . . . . . 11
β’ (π = π β π = π) |
169 | 167, 168 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π = π β ((π + 1) / π) = ((π + 1) / π)) |
170 | 169 | fveq2d 6847 |
. . . . . . . . 9
β’ (π = π β (logβ((π + 1) / π)) = (logβ((π + 1) / π))) |
171 | 170 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β ((π΄ + 1) Β· (logβ((π + 1) / π))) = ((π΄ + 1) Β· (logβ((π + 1) / π)))) |
172 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = π β ((π΄ + 1) / π) = ((π΄ + 1) / π)) |
173 | 172 | fvoveq1d 7380 |
. . . . . . . 8
β’ (π = π β (logβ(((π΄ + 1) / π) + 1)) = (logβ(((π΄ + 1) / π) + 1))) |
174 | 171, 173 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) = (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))) |
175 | | ovex 7391 |
. . . . . . 7
β’ (((π΄ + 1) Β·
(logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β V |
176 | 174, 3, 175 | fvmpt 6949 |
. . . . . 6
β’ (π β β β ((π β β β¦ (((π΄ + 1) Β·
(logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))))βπ) = (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))) |
177 | 166, 176 | syl 17 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...π)) β ((π β β β¦ (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))))βπ) = (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))) |
178 | 91, 1 | eleqtrdi 2844 |
. . . . 5
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
179 | 11 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β π΄ β β) |
180 | | 1cnd 11155 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β 1 β β) |
181 | 179, 180 | addcld 11179 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β (π΄ + 1) β β) |
182 | 166 | peano2nnd 12175 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β (π + 1) β β) |
183 | 182 | nnrpd 12960 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (π + 1) β
β+) |
184 | 166 | nnrpd 12960 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β π β β+) |
185 | 183, 184 | rpdivcld 12979 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((π + 1) / π) β
β+) |
186 | 185 | relogcld 25994 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π + 1) / π)) β β) |
187 | 186 | recnd 11188 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π + 1) / π)) β β) |
188 | 181, 187 | mulcld 11180 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + 1) Β· (logβ((π + 1) / π))) β β) |
189 | 166 | nncnd 12174 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
190 | 166 | nnne0d 12208 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β π β 0) |
191 | 181, 189,
190 | divcld 11936 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + 1) / π) β β) |
192 | 191, 180 | addcld 11179 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) / π) + 1) β β) |
193 | 7 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β (π΄ + 1) β (β β (β€
β β))) |
194 | 193, 166 | dmgmdivn0 26393 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) / π) + 1) β 0) |
195 | 192, 194 | logcld 25942 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ(((π΄ + 1) / π) + 1)) β β) |
196 | 188, 195 | subcld 11517 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β β) |
197 | 177, 178,
196 | fsumser 15620 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) = (seq1( + , (π β β β¦ (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))))βπ)) |
198 | | fzfid 13884 |
. . . . 5
β’ ((π β§ π β β) β (1...π) β Fin) |
199 | 198, 196 | fsumcl 15623 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β β) |
200 | 197, 199 | eqeltrrd 2835 |
. . 3
β’ ((π β§ π β β) β (seq1( + , (π β β β¦ (((π΄ + 1) Β·
(logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))))βπ) β β) |
201 | 142 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β (logβ(π΄ + 1)) β
β) |
202 | 201, 153 | subcld 11517 |
. . . 4
β’ ((π β§ π β β) β ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))) β
β) |
203 | 159, 202 | eqeltrd 2834 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))βπ) β
β) |
204 | 179, 187 | mulcld 11180 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β (π΄ Β· (logβ((π + 1) / π))) β β) |
205 | 179, 189,
190 | divcld 11936 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (π΄ / π) β β) |
206 | 205, 180 | addcld 11179 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ / π) + 1) β β) |
207 | 4 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β π΄ β (β β (β€ β
β))) |
208 | 207, 166 | dmgmdivn0 26393 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ / π) + 1) β 0) |
209 | 206, 208 | logcld 25942 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π΄ / π) + 1)) β β) |
210 | 204, 209 | subcld 11517 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) β β) |
211 | 198, 210 | fsumcl 15623 |
. . . . . 6
β’ ((π β§ π β β) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) β β) |
212 | 199, 211 | nncand 11522 |
. . . . 5
β’ ((π β§ π β β) β (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))))) = Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
213 | 188, 195,
204, 209 | sub4d 11566 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = ((((π΄ + 1) Β· (logβ((π + 1) / π))) β (π΄ Β· (logβ((π + 1) / π)))) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π΄ / π) + 1))))) |
214 | 179, 180 | pncan2d 11519 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + 1) β π΄) = 1) |
215 | 214 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) β π΄) Β· (logβ((π + 1) / π))) = (1 Β· (logβ((π + 1) / π)))) |
216 | 181, 179,
187 | subdird 11617 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) β π΄) Β· (logβ((π + 1) / π))) = (((π΄ + 1) Β· (logβ((π + 1) / π))) β (π΄ Β· (logβ((π + 1) / π))))) |
217 | 187 | mulid2d 11178 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β (1 Β· (logβ((π + 1) / π))) = (logβ((π + 1) / π))) |
218 | 215, 216,
217 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) Β· (logβ((π + 1) / π))) β (π΄ Β· (logβ((π + 1) / π)))) = (logβ((π + 1) / π))) |
219 | 218 | oveq1d 7373 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((((π΄ + 1) Β· (logβ((π + 1) / π))) β (π΄ Β· (logβ((π + 1) / π)))) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π΄ / π) + 1)))) = ((logβ((π + 1) / π)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π΄ / π) + 1))))) |
220 | 187, 195,
209 | subsubd 11545 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ((π + 1) / π)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π΄ / π) + 1)))) = (((logβ((π + 1) / π)) β (logβ(((π΄ + 1) / π) + 1))) + (logβ((π΄ / π) + 1)))) |
221 | 187, 195 | subcld 11517 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ((π + 1) / π)) β (logβ(((π΄ + 1) / π) + 1))) β β) |
222 | 221, 209 | addcomd 11362 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (((logβ((π + 1) / π)) β (logβ(((π΄ + 1) / π) + 1))) + (logβ((π΄ / π) + 1))) = ((logβ((π΄ / π) + 1)) + ((logβ((π + 1) / π)) β (logβ(((π΄ + 1) / π) + 1))))) |
223 | 209, 195,
187 | subsub2d 11546 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ((π΄ / π) + 1)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π + 1) / π)))) = ((logβ((π΄ / π) + 1)) + ((logβ((π + 1) / π)) β (logβ(((π΄ + 1) / π) + 1))))) |
224 | 182 | nncnd 12174 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...π)) β (π + 1) β β) |
225 | 179, 224 | addcld 11179 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β (π΄ + (π + 1)) β β) |
226 | 182 | nnnn0d 12478 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...π)) β (π + 1) β
β0) |
227 | | dmgmaddn0 26388 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β (β β
(β€ β β)) β§ (π + 1) β β0) β
(π΄ + (π + 1)) β 0) |
228 | 207, 226,
227 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β (π΄ + (π + 1)) β 0) |
229 | 225, 228 | logcld 25942 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ(π΄ + (π + 1))) β β) |
230 | 183 | relogcld 25994 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ(π + 1)) β β) |
231 | 230 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ(π + 1)) β β) |
232 | 184 | relogcld 25994 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β (logβπ) β β) |
233 | 232 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβπ) β β) |
234 | 229, 231,
233 | nnncan2d 11552 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (1...π)) β (((logβ(π΄ + (π + 1))) β (logβπ)) β ((logβ(π + 1)) β (logβπ))) = ((logβ(π΄ + (π + 1))) β (logβ(π + 1)))) |
235 | 181, 189,
189, 190 | divdird 11974 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) + π) / π) = (((π΄ + 1) / π) + (π / π))) |
236 | 179, 189,
180 | add32d 11387 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + π) + 1) = ((π΄ + 1) + π)) |
237 | 179, 189,
180 | addassd 11182 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + π) + 1) = (π΄ + (π + 1))) |
238 | 236, 237 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + 1) + π) = (π΄ + (π + 1))) |
239 | 238 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) + π) / π) = ((π΄ + (π + 1)) / π)) |
240 | 189, 190 | dividd 11934 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...π)) β (π / π) = 1) |
241 | 240 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) / π) + (π / π)) = (((π΄ + 1) / π) + 1)) |
242 | 235, 239,
241 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄ + 1) / π) + 1) = ((π΄ + (π + 1)) / π)) |
243 | 242 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ(((π΄ + 1) / π) + 1)) = (logβ((π΄ + (π + 1)) / π))) |
244 | | logdiv2 25988 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ + (π + 1)) β β β§ (π΄ + (π + 1)) β 0 β§ π β β+) β
(logβ((π΄ + (π + 1)) / π)) = ((logβ(π΄ + (π + 1))) β (logβπ))) |
245 | 225, 228,
184, 244 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π΄ + (π + 1)) / π)) = ((logβ(π΄ + (π + 1))) β (logβπ))) |
246 | 243, 245 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ(((π΄ + 1) / π) + 1)) = ((logβ(π΄ + (π + 1))) β (logβπ))) |
247 | 183, 184 | relogdivd 25997 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π + 1) / π)) = ((logβ(π + 1)) β (logβπ))) |
248 | 246, 247 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π + 1) / π))) = (((logβ(π΄ + (π + 1))) β (logβπ)) β ((logβ(π + 1)) β (logβπ)))) |
249 | 182 | nnne0d 12208 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (1...π)) β (π + 1) β 0) |
250 | 179, 224,
224, 249 | divdird 11974 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ + (π + 1)) / (π + 1)) = ((π΄ / (π + 1)) + ((π + 1) / (π + 1)))) |
251 | 224, 249 | dividd 11934 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (1...π)) β ((π + 1) / (π + 1)) = 1) |
252 | 251 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ / (π + 1)) + ((π + 1) / (π + 1))) = ((π΄ / (π + 1)) + 1)) |
253 | 250, 252 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (1...π)) β ((π΄ / (π + 1)) + 1) = ((π΄ + (π + 1)) / (π + 1))) |
254 | 253 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π΄ / (π + 1)) + 1)) = (logβ((π΄ + (π + 1)) / (π + 1)))) |
255 | | logdiv2 25988 |
. . . . . . . . . . . . . . 15
β’ (((π΄ + (π + 1)) β β β§ (π΄ + (π + 1)) β 0 β§ (π + 1) β β+) β
(logβ((π΄ + (π + 1)) / (π + 1))) = ((logβ(π΄ + (π + 1))) β (logβ(π + 1)))) |
256 | 225, 228,
183, 255 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π΄ + (π + 1)) / (π + 1))) = ((logβ(π΄ + (π + 1))) β (logβ(π + 1)))) |
257 | 254, 256 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (1...π)) β (logβ((π΄ / (π + 1)) + 1)) = ((logβ(π΄ + (π + 1))) β (logβ(π + 1)))) |
258 | 234, 248,
257 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π + 1) / π))) = (logβ((π΄ / (π + 1)) + 1))) |
259 | 258 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ((π΄ / π) + 1)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π + 1) / π)))) = ((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1)))) |
260 | 223, 259 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ((π΄ / π) + 1)) + ((logβ((π + 1) / π)) β (logβ(((π΄ + 1) / π) + 1)))) = ((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1)))) |
261 | 220, 222,
260 | 3eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β ((logβ((π + 1) / π)) β ((logβ(((π΄ + 1) / π) + 1)) β (logβ((π΄ / π) + 1)))) = ((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1)))) |
262 | 213, 219,
261 | 3eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β ((((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = ((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1)))) |
263 | 262 | sumeq2dv 15593 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (1...π)((((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = Ξ£π β (1...π)((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1)))) |
264 | 198, 196,
210 | fsumsub 15678 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (1...π)((((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))))) |
265 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = π β (π΄ / π₯) = (π΄ / π)) |
266 | 265 | fvoveq1d 7380 |
. . . . . . . . 9
β’ (π₯ = π β (logβ((π΄ / π₯) + 1)) = (logβ((π΄ / π) + 1))) |
267 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = (π + 1) β (π΄ / π₯) = (π΄ / (π + 1))) |
268 | 267 | fvoveq1d 7380 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (logβ((π΄ / π₯) + 1)) = (logβ((π΄ / (π + 1)) + 1))) |
269 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = 1 β (π΄ / π₯) = (π΄ / 1)) |
270 | 269 | fvoveq1d 7380 |
. . . . . . . . 9
β’ (π₯ = 1 β (logβ((π΄ / π₯) + 1)) = (logβ((π΄ / 1) + 1))) |
271 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = (π + 1) β (π΄ / π₯) = (π΄ / (π + 1))) |
272 | 271 | fvoveq1d 7380 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (logβ((π΄ / π₯) + 1)) = (logβ((π΄ / (π + 1)) + 1))) |
273 | 91 | nnzd 12531 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β€) |
274 | 95, 1 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π + 1) β
(β€β₯β1)) |
275 | 11 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β π΄ β β) |
276 | | elfznn 13476 |
. . . . . . . . . . . . . 14
β’ (π₯ β (1...(π + 1)) β π₯ β β) |
277 | 276 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β π₯ β β) |
278 | 277 | nncnd 12174 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β π₯ β β) |
279 | 277 | nnne0d 12208 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β π₯ β 0) |
280 | 275, 278,
279 | divcld 11936 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β (π΄ / π₯) β β) |
281 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β 1 β
β) |
282 | 280, 281 | addcld 11179 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β ((π΄ / π₯) + 1) β β) |
283 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β π΄ β (β β (β€ β
β))) |
284 | 283, 277 | dmgmdivn0 26393 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β ((π΄ / π₯) + 1) β 0) |
285 | 282, 284 | logcld 25942 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (1...(π + 1))) β (logβ((π΄ / π₯) + 1)) β β) |
286 | 266, 268,
270, 272, 273, 274, 285 | telfsum 15694 |
. . . . . . . 8
β’ ((π β§ π β β) β Ξ£π β (1...π)((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1))) = ((logβ((π΄ / 1) + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) |
287 | 90 | div1d 11928 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π΄ / 1) = π΄) |
288 | 287 | fvoveq1d 7380 |
. . . . . . . . 9
β’ ((π β§ π β β) β (logβ((π΄ / 1) + 1)) = (logβ(π΄ + 1))) |
289 | 288 | oveq1d 7373 |
. . . . . . . 8
β’ ((π β§ π β β) β ((logβ((π΄ / 1) + 1)) β
(logβ((π΄ / (π + 1)) + 1))) =
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) +
1)))) |
290 | 286, 289 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (1...π)((logβ((π΄ / π) + 1)) β (logβ((π΄ / (π + 1)) + 1))) = ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) |
291 | 263, 264,
290 | 3eqtr3d 2781 |
. . . . . 6
β’ ((π β§ π β β) β (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = ((logβ(π΄ + 1)) β (logβ((π΄ / (π + 1)) + 1)))) |
292 | 291 | oveq2d 7374 |
. . . . 5
β’ ((π β§ π β β) β (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))))) = (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))) |
293 | 212, 292 | eqtr3d 2775 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) = (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))) |
294 | 170 | oveq2d 7374 |
. . . . . . . 8
β’ (π = π β (π΄ Β· (logβ((π + 1) / π))) = (π΄ Β· (logβ((π + 1) / π)))) |
295 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = π β (π΄ / π) = (π΄ / π)) |
296 | 295 | fvoveq1d 7380 |
. . . . . . . 8
β’ (π = π β (logβ((π΄ / π) + 1)) = (logβ((π΄ / π) + 1))) |
297 | 294, 296 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) = ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
298 | | lgamcvg.g |
. . . . . . 7
β’ πΊ = (π β β β¦ ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
299 | | ovex 7391 |
. . . . . . 7
β’ ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) β V |
300 | 297, 298,
299 | fvmpt 6949 |
. . . . . 6
β’ (π β β β (πΊβπ) = ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
301 | 166, 300 | syl 17 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...π)) β (πΊβπ) = ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
302 | 301, 178,
210 | fsumser 15620 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...π)((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) = (seq1( + , πΊ)βπ)) |
303 | 159 | eqcomd 2739 |
. . . . 5
β’ ((π β§ π β β) β ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))) = ((π β β β¦
((logβ(π΄ + 1))
β (logβ((π΄ /
(π + 1)) +
1))))βπ)) |
304 | 197, 303 | oveq12d 7376 |
. . . 4
β’ ((π β§ π β β) β (Ξ£π β (1...π)(((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1))) β ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1)))) = ((seq1( + ,
(π β β β¦
(((π΄ + 1) Β·
(logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))))βπ) β ((π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))βπ))) |
305 | 293, 302,
304 | 3eqtr3d 2781 |
. . 3
β’ ((π β§ π β β) β (seq1( + , πΊ)βπ) = ((seq1( + , (π β β β¦ (((π΄ + 1) Β· (logβ((π + 1) / π))) β (logβ(((π΄ + 1) / π) + 1)))))βπ) β ((π β β β¦ ((logβ(π΄ + 1)) β
(logβ((π΄ / (π + 1)) + 1))))βπ))) |
306 | 1, 2, 8, 10, 164, 200, 203, 305 | climsub 15522 |
. 2
β’ (π β seq1( + , πΊ) β (((log
Ξβ(π΄ + 1)) +
(logβ(π΄ + 1)))
β (logβ(π΄ +
1)))) |
307 | | lgamcl 26406 |
. . . 4
β’ ((π΄ + 1) β (β β
(β€ β β)) β (log Ξβ(π΄ + 1)) β β) |
308 | 7, 307 | syl 17 |
. . 3
β’ (π β (log Ξβ(π΄ + 1)) β
β) |
309 | 308, 142 | pncand 11518 |
. 2
β’ (π β (((log
Ξβ(π΄ + 1)) +
(logβ(π΄ + 1)))
β (logβ(π΄ +
1))) = (log Ξβ(π΄ + 1))) |
310 | 306, 309 | breqtrd 5132 |
1
β’ (π β seq1( + , πΊ) β (log
Ξβ(π΄ +
1))) |