Step | Hyp | Ref
| Expression |
1 | | iprodgam.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
2 | | eflgam 24571 |
. . 3
⊢ (𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (exp‘(log
Γ‘𝐴)) =
(Γ‘𝐴)) |
4 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝑧 · (log‘((𝑘 + 1) / 𝑘))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) |
5 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → (𝑧 / 𝑘) = (𝐴 / 𝑘)) |
6 | 5 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → ((𝑧 / 𝑘) + 1) = ((𝐴 / 𝑘) + 1)) |
7 | 6 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (log‘((𝑧 / 𝑘) + 1)) = (log‘((𝐴 / 𝑘) + 1))) |
8 | 4, 7 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ((𝑧 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝑧 / 𝑘) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
9 | 8 | sumeq2sdv 14282 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → Σ𝑘 ∈ ℕ ((𝑧 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝑧 / 𝑘) + 1))) = Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
10 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (log‘𝑧) = (log‘𝐴)) |
11 | 9, 10 | oveq12d 6567 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (Σ𝑘 ∈ ℕ ((𝑧 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝑧 / 𝑘) + 1))) − (log‘𝑧)) = (Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴))) |
12 | | df-lgam 24545 |
. . . . . 6
⊢ log
Γ = (𝑧 ∈
(ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑘 ∈ ℕ ((𝑧 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝑧 / 𝑘) + 1))) − (log‘𝑧))) |
13 | | ovex 6577 |
. . . . . 6
⊢
(Σ𝑘 ∈
ℕ ((𝐴 ·
(log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴)) ∈ V |
14 | 11, 12, 13 | fvmpt 6191 |
. . . . 5
⊢ (𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ)) → (log Γ‘𝐴) = (Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴))) |
15 | 1, 14 | syl 17 |
. . . 4
⊢ (𝜑 → (log Γ‘𝐴) = (Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴))) |
16 | 15 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (exp‘(log
Γ‘𝐴)) =
(exp‘(Σ𝑘 ∈
ℕ ((𝐴 ·
(log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴)))) |
17 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
18 | | 1zzd 11285 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
19 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
20 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → 𝑗 = 𝑘) |
21 | 19, 20 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑗 + 1) / 𝑗) = ((𝑘 + 1) / 𝑘)) |
22 | 21 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (log‘((𝑗 + 1) / 𝑗)) = (log‘((𝑘 + 1) / 𝑘))) |
23 | 22 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝐴 · (log‘((𝑗 + 1) / 𝑗))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) |
24 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (𝐴 / 𝑗) = (𝐴 / 𝑘)) |
25 | 24 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → ((𝐴 / 𝑗) + 1) = ((𝐴 / 𝑘) + 1)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (log‘((𝐴 / 𝑗) + 1)) = (log‘((𝐴 / 𝑘) + 1))) |
27 | 23, 26 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
28 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1)))) = (𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1)))) |
29 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V |
30 | 27, 28, 29 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
32 | 1 | eldifad 3552 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ) |
34 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
35 | 34 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
36 | 35 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ) |
37 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
38 | 37 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
39 | | nnne0 10930 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
40 | 39 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0) |
41 | 36, 38, 40 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 𝑘) ∈ ℂ) |
42 | 35 | nnne0d 10942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ≠ 0) |
43 | 36, 38, 42, 40 | divne0d 10696 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 𝑘) ≠ 0) |
44 | 41, 43 | logcld 24121 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ) |
45 | 33, 44 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ) |
46 | 33, 38, 40 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 / 𝑘) ∈ ℂ) |
47 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈
ℂ) |
48 | 46, 47 | addcld 9938 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴 / 𝑘) + 1) ∈ ℂ) |
49 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
50 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
51 | 49, 50 | dmgmdivn0 24554 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴 / 𝑘) + 1) ≠ 0) |
52 | 48, 51 | logcld 24121 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ) |
53 | 45, 52 | subcld 10271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ) |
54 | 28, 1 | lgamcvg 24580 |
. . . . . . 7
⊢ (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))) ⇝ ((log Γ‘𝐴) + (log‘𝐴))) |
55 | | seqex 12665 |
. . . . . . . 8
⊢ seq1( + ,
(𝑗 ∈ ℕ ↦
((𝐴 ·
(log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))) ∈ V |
56 | | ovex 6577 |
. . . . . . . 8
⊢ ((log
Γ‘𝐴) +
(log‘𝐴)) ∈
V |
57 | 55, 56 | breldm 5251 |
. . . . . . 7
⊢ (seq1( +
, (𝑗 ∈ ℕ ↦
((𝐴 ·
(log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))) ⇝ ((log Γ‘𝐴) + (log‘𝐴)) → seq1( + , (𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))) ∈ dom ⇝
) |
58 | 54, 57 | syl 17 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝐴 · (log‘((𝑗 + 1) / 𝑗))) − (log‘((𝐴 / 𝑗) + 1))))) ∈ dom ⇝
) |
59 | 17, 18, 31, 53, 58 | isumcl 14334 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ) |
60 | 1 | dmgmn0 24552 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 0) |
61 | 32, 60 | logcld 24121 |
. . . . 5
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
62 | | efsub 14669 |
. . . . 5
⊢
((Σ𝑘 ∈
ℕ ((𝐴 ·
(log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ ∧
(log‘𝐴) ∈
ℂ) → (exp‘(Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴))) = ((exp‘Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) / (exp‘(log‘𝐴)))) |
63 | 59, 61, 62 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (exp‘(Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴))) = ((exp‘Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) / (exp‘(log‘𝐴)))) |
64 | 17, 18, 31, 53, 58 | iprodefisum 30880 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ℕ (exp‘((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (exp‘Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))) |
65 | | efsub 14669 |
. . . . . . . . 9
⊢ (((𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ ∧ (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ) →
(exp‘((𝐴 ·
(log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((exp‘(𝐴 · (log‘((𝑘 + 1) / 𝑘)))) / (exp‘(log‘((𝐴 / 𝑘) + 1))))) |
66 | 45, 52, 65 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (exp‘((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((exp‘(𝐴 · (log‘((𝑘 + 1) / 𝑘)))) / (exp‘(log‘((𝐴 / 𝑘) + 1))))) |
67 | 38, 47, 38, 40 | divdird 10718 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 𝑘) = ((𝑘 / 𝑘) + (1 / 𝑘))) |
68 | 38, 40 | dividd 10678 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 / 𝑘) = 1) |
69 | 68 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 / 𝑘) + (1 / 𝑘)) = (1 + (1 / 𝑘))) |
70 | 67, 69 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 𝑘) = (1 + (1 / 𝑘))) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘((𝑘 + 1) / 𝑘)) = (log‘(1 + (1 / 𝑘)))) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) = (𝐴 · (log‘(1 + (1 / 𝑘))))) |
73 | 72 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (exp‘(𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (exp‘(𝐴 · (log‘(1 + (1 / 𝑘)))))) |
74 | | 1rp 11712 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
75 | 74 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈
ℝ+) |
76 | 50 | nnrpd 11746 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
77 | 76 | rpreccld 11758 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ+) |
78 | 75, 77 | rpaddcld 11763 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + (1 / 𝑘)) ∈
ℝ+) |
79 | 78 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + (1 / 𝑘)) ∈
ℂ) |
80 | 78 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + (1 / 𝑘)) ≠ 0) |
81 | 79, 80, 33 | cxpefd 24258 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 + (1 / 𝑘))↑𝑐𝐴) = (exp‘(𝐴 · (log‘(1 + (1 / 𝑘)))))) |
82 | 73, 81 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (exp‘(𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = ((1 + (1 / 𝑘))↑𝑐𝐴)) |
83 | | eflog 24127 |
. . . . . . . . . . 11
⊢ ((((𝐴 / 𝑘) + 1) ∈ ℂ ∧ ((𝐴 / 𝑘) + 1) ≠ 0) →
(exp‘(log‘((𝐴 /
𝑘) + 1))) = ((𝐴 / 𝑘) + 1)) |
84 | 48, 51, 83 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(exp‘(log‘((𝐴 /
𝑘) + 1))) = ((𝐴 / 𝑘) + 1)) |
85 | 46, 47 | addcomd 10117 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐴 / 𝑘) + 1) = (1 + (𝐴 / 𝑘))) |
86 | 84, 85 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(exp‘(log‘((𝐴 /
𝑘) + 1))) = (1 + (𝐴 / 𝑘))) |
87 | 82, 86 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((exp‘(𝐴 · (log‘((𝑘 + 1) / 𝑘)))) / (exp‘(log‘((𝐴 / 𝑘) + 1)))) = (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘)))) |
88 | 66, 87 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (exp‘((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘)))) |
89 | 88 | prodeq2dv 14492 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ℕ (exp‘((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘)))) |
90 | 64, 89 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → (exp‘Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘)))) |
91 | | eflog 24127 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(exp‘(log‘𝐴)) =
𝐴) |
92 | 32, 60, 91 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
(exp‘(log‘𝐴)) =
𝐴) |
93 | 90, 92 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → ((exp‘Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) / (exp‘(log‘𝐴))) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) |
94 | 63, 93 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (exp‘(Σ𝑘 ∈ ℕ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) − (log‘𝐴))) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) |
95 | 16, 94 | eqtrd 2644 |
. 2
⊢ (𝜑 → (exp‘(log
Γ‘𝐴)) =
(∏𝑘 ∈ ℕ
(((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) |
96 | 3, 95 | eqtr3d 2646 |
1
⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴)) |