Step | Hyp | Ref
| Expression |
1 | | addcl 11191 |
. . . . 5
β’ ((π β β β§ π₯ β β) β (π + π₯) β β) |
2 | 1 | adantl 482 |
. . . 4
β’ (((π β§ π β β) β§ (π β β β§ π₯ β β)) β (π + π₯) β β) |
3 | | simpll 765 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...π)) β π) |
4 | | elfznn 13529 |
. . . . . 6
β’ (π β (1...π) β π β β) |
5 | 4 | adantl 482 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
6 | | oveq1 7415 |
. . . . . . . . . . . 12
β’ (π = π β (π + 1) = (π + 1)) |
7 | | id 22 |
. . . . . . . . . . . 12
β’ (π = π β π = π) |
8 | 6, 7 | oveq12d 7426 |
. . . . . . . . . . 11
β’ (π = π β ((π + 1) / π) = ((π + 1) / π)) |
9 | 8 | fveq2d 6895 |
. . . . . . . . . 10
β’ (π = π β (logβ((π + 1) / π)) = (logβ((π + 1) / π))) |
10 | 9 | oveq2d 7424 |
. . . . . . . . 9
β’ (π = π β (π΄ Β· (logβ((π + 1) / π))) = (π΄ Β· (logβ((π + 1) / π)))) |
11 | | oveq2 7416 |
. . . . . . . . . . 11
β’ (π = π β (π΄ / π) = (π΄ / π)) |
12 | 11 | oveq1d 7423 |
. . . . . . . . . 10
β’ (π = π β ((π΄ / π) + 1) = ((π΄ / π) + 1)) |
13 | 12 | fveq2d 6895 |
. . . . . . . . 9
β’ (π = π β (logβ((π΄ / π) + 1)) = (logβ((π΄ / π) + 1))) |
14 | 10, 13 | oveq12d 7426 |
. . . . . . . 8
β’ (π = π β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) = ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
15 | | gamcvg2.g |
. . . . . . . 8
β’ πΊ = (π β β β¦ ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
16 | | ovex 7441 |
. . . . . . . 8
β’ ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) β V |
17 | 14, 15, 16 | fvmpt 6998 |
. . . . . . 7
β’ (π β β β (πΊβπ) = ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
18 | 17 | adantl 482 |
. . . . . 6
β’ ((π β§ π β β) β (πΊβπ) = ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) |
19 | | gamcvg2.a |
. . . . . . . . . 10
β’ (π β π΄ β (β β (β€ β
β))) |
20 | 19 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β π΄ β (β β (β€ β
β))) |
21 | 20 | eldifad 3960 |
. . . . . . . 8
β’ ((π β§ π β β) β π΄ β β) |
22 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
23 | 22 | peano2nnd 12228 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π + 1) β β) |
24 | 23 | nnrpd 13013 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π + 1) β
β+) |
25 | 22 | nnrpd 13013 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β+) |
26 | 24, 25 | rpdivcld 13032 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π + 1) / π) β
β+) |
27 | 26 | relogcld 26130 |
. . . . . . . . 9
β’ ((π β§ π β β) β (logβ((π + 1) / π)) β β) |
28 | 27 | recnd 11241 |
. . . . . . . 8
β’ ((π β§ π β β) β (logβ((π + 1) / π)) β β) |
29 | 21, 28 | mulcld 11233 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄ Β· (logβ((π + 1) / π))) β β) |
30 | 22 | nncnd 12227 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
31 | 22 | nnne0d 12261 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β 0) |
32 | 21, 30, 31 | divcld 11989 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π΄ / π) β β) |
33 | | 1cnd 11208 |
. . . . . . . . 9
β’ ((π β§ π β β) β 1 β
β) |
34 | 32, 33 | addcld 11232 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π΄ / π) + 1) β β) |
35 | 20, 22 | dmgmdivn0 26529 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π΄ / π) + 1) β 0) |
36 | 34, 35 | logcld 26078 |
. . . . . . 7
β’ ((π β§ π β β) β (logβ((π΄ / π) + 1)) β β) |
37 | 29, 36 | subcld 11570 |
. . . . . 6
β’ ((π β§ π β β) β ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))) β β) |
38 | 18, 37 | eqeltrd 2833 |
. . . . 5
β’ ((π β§ π β β) β (πΊβπ) β β) |
39 | 3, 5, 38 | syl2anc 584 |
. . . 4
β’ (((π β§ π β β) β§ π β (1...π)) β (πΊβπ) β β) |
40 | | simpr 485 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
41 | | nnuz 12864 |
. . . . 5
β’ β =
(β€β₯β1) |
42 | 40, 41 | eleqtrdi 2843 |
. . . 4
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
43 | | efadd 16036 |
. . . . 5
β’ ((π β β β§ π₯ β β) β
(expβ(π + π₯)) = ((expβπ) Β· (expβπ₯))) |
44 | 43 | adantl 482 |
. . . 4
β’ (((π β§ π β β) β§ (π β β β§ π₯ β β)) β (expβ(π + π₯)) = ((expβπ) Β· (expβπ₯))) |
45 | | efsub 16042 |
. . . . . . . 8
β’ (((π΄ Β· (logβ((π + 1) / π))) β β β§ (logβ((π΄ / π) + 1)) β β) β
(expβ((π΄ Β·
(logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = ((expβ(π΄ Β· (logβ((π + 1) / π)))) / (expβ(logβ((π΄ / π) + 1))))) |
46 | 29, 36, 45 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β β) β (expβ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = ((expβ(π΄ Β· (logβ((π + 1) / π)))) / (expβ(logβ((π΄ / π) + 1))))) |
47 | 30, 33 | addcld 11232 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π + 1) β β) |
48 | 47, 30, 31 | divcld 11989 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π + 1) / π) β β) |
49 | 23 | nnne0d 12261 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π + 1) β 0) |
50 | 47, 30, 49, 31 | divne0d 12005 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π + 1) / π) β 0) |
51 | 48, 50, 21 | cxpefd 26219 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((π + 1) / π)βππ΄) = (expβ(π΄ Β· (logβ((π + 1) / π))))) |
52 | 51 | eqcomd 2738 |
. . . . . . . 8
β’ ((π β§ π β β) β (expβ(π΄ Β· (logβ((π + 1) / π)))) = (((π + 1) / π)βππ΄)) |
53 | | eflog 26084 |
. . . . . . . . 9
β’ ((((π΄ / π) + 1) β β β§ ((π΄ / π) + 1) β 0) β
(expβ(logβ((π΄ /
π) + 1))) = ((π΄ / π) + 1)) |
54 | 34, 35, 53 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ π β β) β
(expβ(logβ((π΄ /
π) + 1))) = ((π΄ / π) + 1)) |
55 | 52, 54 | oveq12d 7426 |
. . . . . . 7
β’ ((π β§ π β β) β ((expβ(π΄ Β· (logβ((π + 1) / π)))) / (expβ(logβ((π΄ / π) + 1)))) = ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1))) |
56 | 46, 55 | eqtrd 2772 |
. . . . . 6
β’ ((π β§ π β β) β (expβ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1)))) = ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1))) |
57 | 18 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π β β) β (expβ(πΊβπ)) = (expβ((π΄ Β· (logβ((π + 1) / π))) β (logβ((π΄ / π) + 1))))) |
58 | 8 | oveq1d 7423 |
. . . . . . . . 9
β’ (π = π β (((π + 1) / π)βππ΄) = (((π + 1) / π)βππ΄)) |
59 | 58, 12 | oveq12d 7426 |
. . . . . . . 8
β’ (π = π β ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1)) = ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1))) |
60 | | gamcvg2.f |
. . . . . . . 8
β’ πΉ = (π β β β¦ ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1))) |
61 | | ovex 7441 |
. . . . . . . 8
β’ ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1)) β V |
62 | 59, 60, 61 | fvmpt 6998 |
. . . . . . 7
β’ (π β β β (πΉβπ) = ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1))) |
63 | 62 | adantl 482 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ) = ((((π + 1) / π)βππ΄) / ((π΄ / π) + 1))) |
64 | 56, 57, 63 | 3eqtr4d 2782 |
. . . . 5
β’ ((π β§ π β β) β (expβ(πΊβπ)) = (πΉβπ)) |
65 | 3, 5, 64 | syl2anc 584 |
. . . 4
β’ (((π β§ π β β) β§ π β (1...π)) β (expβ(πΊβπ)) = (πΉβπ)) |
66 | 2, 39, 42, 44, 65 | seqhomo 14014 |
. . 3
β’ ((π β§ π β β) β (expβ(seq1( + ,
πΊ)βπ)) = (seq1( Β· , πΉ)βπ)) |
67 | 66 | mpteq2dva 5248 |
. 2
β’ (π β (π β β β¦ (expβ(seq1( + ,
πΊ)βπ))) = (π β β β¦ (seq1( Β· ,
πΉ)βπ))) |
68 | | eff 16024 |
. . . 4
β’
exp:ββΆβ |
69 | 68 | a1i 11 |
. . 3
β’ (π β
exp:ββΆβ) |
70 | | 1z 12591 |
. . . . 5
β’ 1 β
β€ |
71 | 70 | a1i 11 |
. . . 4
β’ (π β 1 β
β€) |
72 | 41, 71, 38 | serf 13995 |
. . 3
β’ (π β seq1( + , πΊ):ββΆβ) |
73 | | fcompt 7130 |
. . 3
β’
((exp:ββΆβ β§ seq1( + , πΊ):ββΆβ) β (exp
β seq1( + , πΊ)) =
(π β β β¦
(expβ(seq1( + , πΊ)βπ)))) |
74 | 69, 72, 73 | syl2anc 584 |
. 2
β’ (π β (exp β seq1( + ,
πΊ)) = (π β β β¦ (expβ(seq1( + ,
πΊ)βπ)))) |
75 | | seqfn 13977 |
. . . . 5
β’ (1 β
β€ β seq1( Β· , πΉ) Fn
(β€β₯β1)) |
76 | 70, 75 | mp1i 13 |
. . . 4
β’ (π β seq1( Β· , πΉ) Fn
(β€β₯β1)) |
77 | 41 | fneq2i 6647 |
. . . 4
β’ (seq1(
Β· , πΉ) Fn β
β seq1( Β· , πΉ)
Fn (β€β₯β1)) |
78 | 76, 77 | sylibr 233 |
. . 3
β’ (π β seq1( Β· , πΉ) Fn β) |
79 | | dffn5 6950 |
. . 3
β’ (seq1(
Β· , πΉ) Fn β
β seq1( Β· , πΉ)
= (π β β β¦
(seq1( Β· , πΉ)βπ))) |
80 | 78, 79 | sylib 217 |
. 2
β’ (π β seq1( Β· , πΉ) = (π β β β¦ (seq1( Β· ,
πΉ)βπ))) |
81 | 67, 74, 80 | 3eqtr4d 2782 |
1
β’ (π β (exp β seq1( + ,
πΊ)) = seq1( Β· ,
πΉ)) |