Step | Hyp | Ref
| Expression |
1 | | iprodgam.1 |
. . 3
โข (๐ โ ๐ด โ (โ โ (โค โ
โ))) |
2 | | eflgam 26446 |
. . 3
โข (๐ด โ (โ โ
(โค โ โ)) โ (expโ(log ฮโ๐ด)) = (ฮโ๐ด)) |
3 | 1, 2 | syl 17 |
. 2
โข (๐ โ (expโ(log
ฮโ๐ด)) =
(ฮโ๐ด)) |
4 | | oveq1 7384 |
. . . . . . . . 9
โข (๐ง = ๐ด โ (๐ง ยท (logโ((๐ + 1) / ๐))) = (๐ด ยท (logโ((๐ + 1) / ๐)))) |
5 | | oveq1 7384 |
. . . . . . . . . 10
โข (๐ง = ๐ด โ (๐ง / ๐) = (๐ด / ๐)) |
6 | 5 | fvoveq1d 7399 |
. . . . . . . . 9
โข (๐ง = ๐ด โ (logโ((๐ง / ๐) + 1)) = (logโ((๐ด / ๐) + 1))) |
7 | 4, 6 | oveq12d 7395 |
. . . . . . . 8
โข (๐ง = ๐ด โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) = ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) |
8 | 7 | sumeq2sdv 15615 |
. . . . . . 7
โข (๐ง = ๐ด โ ฮฃ๐ โ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) = ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) |
9 | | fveq2 6862 |
. . . . . . 7
โข (๐ง = ๐ด โ (logโ๐ง) = (logโ๐ด)) |
10 | 8, 9 | oveq12d 7395 |
. . . . . 6
โข (๐ง = ๐ด โ (ฮฃ๐ โ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) โ (logโ๐ง)) = (ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด))) |
11 | | df-lgam 26420 |
. . . . . 6
โข log
ฮ = (๐ง โ
(โ โ (โค โ โ)) โฆ (ฮฃ๐ โ โ ((๐ง ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ง / ๐) + 1))) โ (logโ๐ง))) |
12 | | ovex 7410 |
. . . . . 6
โข
(ฮฃ๐ โ
โ ((๐ด ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด)) โ V |
13 | 10, 11, 12 | fvmpt 6968 |
. . . . 5
โข (๐ด โ (โ โ
(โค โ โ)) โ (log ฮโ๐ด) = (ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด))) |
14 | 1, 13 | syl 17 |
. . . 4
โข (๐ โ (log ฮโ๐ด) = (ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด))) |
15 | 14 | fveq2d 6866 |
. . 3
โข (๐ โ (expโ(log
ฮโ๐ด)) =
(expโ(ฮฃ๐ โ
โ ((๐ด ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด)))) |
16 | | nnuz 12830 |
. . . . . 6
โข โ =
(โคโฅโ1) |
17 | | 1zzd 12558 |
. . . . . 6
โข (๐ โ 1 โ
โค) |
18 | | oveq1 7384 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
19 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ๐ = ๐) |
20 | 18, 19 | oveq12d 7395 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ + 1) / ๐) = ((๐ + 1) / ๐)) |
21 | 20 | fveq2d 6866 |
. . . . . . . . . 10
โข (๐ = ๐ โ (logโ((๐ + 1) / ๐)) = (logโ((๐ + 1) / ๐))) |
22 | 21 | oveq2d 7393 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ด ยท (logโ((๐ + 1) / ๐))) = (๐ด ยท (logโ((๐ + 1) / ๐)))) |
23 | | oveq2 7385 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ด / ๐) = (๐ด / ๐)) |
24 | 23 | fvoveq1d 7399 |
. . . . . . . . 9
โข (๐ = ๐ โ (logโ((๐ด / ๐) + 1)) = (logโ((๐ด / ๐) + 1))) |
25 | 22, 24 | oveq12d 7395 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) = ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) |
26 | | eqid 2731 |
. . . . . . . 8
โข (๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = (๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) |
27 | | ovex 7410 |
. . . . . . . 8
โข ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ V |
28 | 25, 26, 27 | fvmpt 6968 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))โ๐) = ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) |
29 | 28 | adantl 482 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))โ๐) = ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) |
30 | 1 | eldifad 3940 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
31 | 30 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐ด โ โ) |
32 | | peano2nn 12189 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ + 1) โ
โ) |
33 | 32 | adantl 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ โ) |
34 | 33 | nncnd 12193 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ โ) |
35 | | nncn 12185 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
36 | 35 | adantl 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
37 | | nnne0 12211 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ 0) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐ โ 0) |
39 | 34, 36, 38 | divcld 11955 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((๐ + 1) / ๐) โ โ) |
40 | 33 | nnne0d 12227 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ 0) |
41 | 34, 36, 40, 38 | divne0d 11971 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((๐ + 1) / ๐) โ 0) |
42 | 39, 41 | logcld 25978 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (logโ((๐ + 1) / ๐)) โ โ) |
43 | 31, 42 | mulcld 11199 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐ด ยท (logโ((๐ + 1) / ๐))) โ โ) |
44 | 31, 36, 38 | divcld 11955 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐ด / ๐) โ โ) |
45 | | 1cnd 11174 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ 1 โ
โ) |
46 | 44, 45 | addcld 11198 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((๐ด / ๐) + 1) โ โ) |
47 | 1 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ๐ด โ (โ โ (โค โ
โ))) |
48 | | simpr 485 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
49 | 47, 48 | dmgmdivn0 26429 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((๐ด / ๐) + 1) โ 0) |
50 | 46, 49 | logcld 25978 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (logโ((๐ด / ๐) + 1)) โ โ) |
51 | 43, 50 | subcld 11536 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ โ) |
52 | 26, 1 | lgamcvg 26455 |
. . . . . . 7
โข (๐ โ seq1( + , (๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))) โ ((log ฮโ๐ด) + (logโ๐ด))) |
53 | | seqex 13933 |
. . . . . . . 8
โข seq1( + ,
(๐ โ โ โฆ
((๐ด ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))) โ V |
54 | | ovex 7410 |
. . . . . . . 8
โข ((log
ฮโ๐ด) +
(logโ๐ด)) โ
V |
55 | 53, 54 | breldm 5884 |
. . . . . . 7
โข (seq1( +
, (๐ โ โ โฆ
((๐ด ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))) โ ((log ฮโ๐ด) + (logโ๐ด)) โ seq1( + , (๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))) โ dom โ
) |
56 | 52, 55 | syl 17 |
. . . . . 6
โข (๐ โ seq1( + , (๐ โ โ โฆ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))) โ dom โ
) |
57 | 16, 17, 29, 51, 56 | isumcl 15672 |
. . . . 5
โข (๐ โ ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ โ) |
58 | 1 | dmgmn0 26427 |
. . . . . 6
โข (๐ โ ๐ด โ 0) |
59 | 30, 58 | logcld 25978 |
. . . . 5
โข (๐ โ (logโ๐ด) โ
โ) |
60 | | efsub 16008 |
. . . . 5
โข
((ฮฃ๐ โ
โ ((๐ด ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ โ โง
(logโ๐ด) โ
โ) โ (expโ(ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด))) = ((expโฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) / (expโ(logโ๐ด)))) |
61 | 57, 59, 60 | syl2anc 584 |
. . . 4
โข (๐ โ (expโ(ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด))) = ((expโฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) / (expโ(logโ๐ด)))) |
62 | 16, 17, 29, 51, 56 | iprodefisum 34434 |
. . . . . 6
โข (๐ โ โ๐ โ โ (expโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = (expโฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))))) |
63 | | efsub 16008 |
. . . . . . . . 9
โข (((๐ด ยท (logโ((๐ + 1) / ๐))) โ โ โง (logโ((๐ด / ๐) + 1)) โ โ) โ
(expโ((๐ด ยท
(logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = ((expโ(๐ด ยท (logโ((๐ + 1) / ๐)))) / (expโ(logโ((๐ด / ๐) + 1))))) |
64 | 43, 50, 63 | syl2anc 584 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (expโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = ((expโ(๐ด ยท (logโ((๐ + 1) / ๐)))) / (expโ(logโ((๐ด / ๐) + 1))))) |
65 | 36, 45, 36, 38 | divdird 11993 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ((๐ + 1) / ๐) = ((๐ / ๐) + (1 / ๐))) |
66 | 36, 38 | dividd 11953 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ โ) โ (๐ / ๐) = 1) |
67 | 66 | oveq1d 7392 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ((๐ / ๐) + (1 / ๐)) = (1 + (1 / ๐))) |
68 | 65, 67 | eqtrd 2771 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ ((๐ + 1) / ๐) = (1 + (1 / ๐))) |
69 | 68 | fveq2d 6866 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (logโ((๐ + 1) / ๐)) = (logโ(1 + (1 / ๐)))) |
70 | 69 | oveq2d 7393 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐ด ยท (logโ((๐ + 1) / ๐))) = (๐ด ยท (logโ(1 + (1 / ๐))))) |
71 | 70 | fveq2d 6866 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (expโ(๐ด ยท (logโ((๐ + 1) / ๐)))) = (expโ(๐ด ยท (logโ(1 + (1 / ๐)))))) |
72 | | 1rp 12943 |
. . . . . . . . . . . . . 14
โข 1 โ
โ+ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ 1 โ
โ+) |
74 | 48 | nnrpd 12979 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ) โ ๐ โ โ+) |
75 | 74 | rpreccld 12991 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ) โ (1 / ๐) โ
โ+) |
76 | 73, 75 | rpaddcld 12996 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ (1 + (1 / ๐)) โ
โ+) |
77 | 76 | rpcnd 12983 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (1 + (1 / ๐)) โ
โ) |
78 | 76 | rpne0d 12986 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (1 + (1 / ๐)) โ 0) |
79 | 77, 78, 31 | cxpefd 26119 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ((1 + (1 / ๐))โ๐๐ด) = (expโ(๐ด ยท (logโ(1 + (1 / ๐)))))) |
80 | 71, 79 | eqtr4d 2774 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (expโ(๐ด ยท (logโ((๐ + 1) / ๐)))) = ((1 + (1 / ๐))โ๐๐ด)) |
81 | | eflog 25984 |
. . . . . . . . . . 11
โข ((((๐ด / ๐) + 1) โ โ โง ((๐ด / ๐) + 1) โ 0) โ
(expโ(logโ((๐ด /
๐) + 1))) = ((๐ด / ๐) + 1)) |
82 | 46, 49, 81 | syl2anc 584 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ
(expโ(logโ((๐ด /
๐) + 1))) = ((๐ด / ๐) + 1)) |
83 | 44, 45 | addcomd 11381 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ((๐ด / ๐) + 1) = (1 + (๐ด / ๐))) |
84 | 82, 83 | eqtrd 2771 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ
(expโ(logโ((๐ด /
๐) + 1))) = (1 + (๐ด / ๐))) |
85 | 80, 84 | oveq12d 7395 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((expโ(๐ด ยท (logโ((๐ + 1) / ๐)))) / (expโ(logโ((๐ด / ๐) + 1)))) = (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐)))) |
86 | 64, 85 | eqtrd 2771 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (expโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐)))) |
87 | 86 | prodeq2dv 15832 |
. . . . . 6
โข (๐ โ โ๐ โ โ (expโ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = โ๐ โ โ (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐)))) |
88 | 62, 87 | eqtr3d 2773 |
. . . . 5
โข (๐ โ (expโฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) = โ๐ โ โ (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐)))) |
89 | | eflog 25984 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ
(expโ(logโ๐ด)) =
๐ด) |
90 | 30, 58, 89 | syl2anc 584 |
. . . . 5
โข (๐ โ
(expโ(logโ๐ด)) =
๐ด) |
91 | 88, 90 | oveq12d 7395 |
. . . 4
โข (๐ โ ((expโฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1)))) / (expโ(logโ๐ด))) = (โ๐ โ โ (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐))) / ๐ด)) |
92 | 61, 91 | eqtrd 2771 |
. . 3
โข (๐ โ (expโ(ฮฃ๐ โ โ ((๐ด ยท (logโ((๐ + 1) / ๐))) โ (logโ((๐ด / ๐) + 1))) โ (logโ๐ด))) = (โ๐ โ โ (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐))) / ๐ด)) |
93 | 15, 92 | eqtrd 2771 |
. 2
โข (๐ โ (expโ(log
ฮโ๐ด)) =
(โ๐ โ โ
(((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐))) / ๐ด)) |
94 | 3, 93 | eqtr3d 2773 |
1
โข (๐ โ (ฮโ๐ด) = (โ๐ โ โ (((1 + (1 / ๐))โ๐๐ด) / (1 + (๐ด / ๐))) / ๐ด)) |