Step |
Hyp |
Ref |
Expression |
1 |
|
lgamucov.u |
⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } |
2 |
|
lgamucov.a |
⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ) |
3 |
|
lgamcvglem.g |
⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) |
4 |
1 2
|
lgamucov2 |
⊢ ( 𝜑 → ∃ 𝑟 ∈ ℕ 𝐴 ∈ 𝑈 ) |
5 |
|
fveq2 |
⊢ ( 𝑧 = 𝐴 → ( log Γ ‘ 𝑧 ) = ( log Γ ‘ 𝐴 ) ) |
6 |
5
|
eleq1d |
⊢ ( 𝑧 = 𝐴 → ( ( log Γ ‘ 𝑧 ) ∈ ℂ ↔ ( log Γ ‘ 𝐴 ) ∈ ℂ ) ) |
7 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → 𝑟 ∈ ℕ ) |
8 |
|
fveq2 |
⊢ ( 𝑥 = 𝑡 → ( abs ‘ 𝑥 ) = ( abs ‘ 𝑡 ) ) |
9 |
8
|
breq1d |
⊢ ( 𝑥 = 𝑡 → ( ( abs ‘ 𝑥 ) ≤ 𝑟 ↔ ( abs ‘ 𝑡 ) ≤ 𝑟 ) ) |
10 |
|
fvoveq1 |
⊢ ( 𝑥 = 𝑡 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝑡 + 𝑘 ) ) ) |
11 |
10
|
breq2d |
⊢ ( 𝑥 = 𝑡 → ( ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) ) |
13 |
9 12
|
anbi12d |
⊢ ( 𝑥 = 𝑡 → ( ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ↔ ( ( abs ‘ 𝑡 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) ) ) |
14 |
13
|
cbvrabv |
⊢ { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } = { 𝑡 ∈ ℂ ∣ ( ( abs ‘ 𝑡 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) } |
15 |
1 14
|
eqtri |
⊢ 𝑈 = { 𝑡 ∈ ℂ ∣ ( ( abs ‘ 𝑡 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) } |
16 |
|
eqid |
⊢ ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) |
17 |
7 15 16
|
lgamgulm2 |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → ( ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ ∧ seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) ) |
18 |
17
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ ) |
19 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → 𝐴 ∈ 𝑈 ) |
20 |
6 18 19
|
rspcdva |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → ( log Γ ‘ 𝐴 ) ∈ ℂ ) |
21 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
22 |
|
1zzd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → 1 ∈ ℤ ) |
23 |
|
1z |
⊢ 1 ∈ ℤ |
24 |
|
seqfn |
⊢ ( 1 ∈ ℤ → seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) ) |
25 |
23 24
|
ax-mp |
⊢ seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) |
26 |
21
|
fneq2i |
⊢ ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) Fn ℕ ↔ seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) Fn ( ℤ≥ ‘ 1 ) ) |
27 |
25 26
|
mpbir |
⊢ seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) Fn ℕ |
28 |
17
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) |
29 |
|
ulmf2 |
⊢ ( ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) Fn ℕ ∧ seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) → seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) : ℕ ⟶ ( ℂ ↑m 𝑈 ) ) |
30 |
27 28 29
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) : ℕ ⟶ ( ℂ ↑m 𝑈 ) ) |
31 |
|
seqex |
⊢ seq 1 ( + , 𝐺 ) ∈ V |
32 |
31
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → seq 1 ( + , 𝐺 ) ∈ V ) |
33 |
|
cnex |
⊢ ℂ ∈ V |
34 |
1 33
|
rabex2 |
⊢ 𝑈 ∈ V |
35 |
34
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑈 ∈ V ) |
36 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ) |
37 |
36 21
|
eleqtrdi |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) ) |
38 |
|
fz1ssnn |
⊢ ( 1 ... 𝑛 ) ⊆ ℕ |
39 |
38
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ ) |
40 |
|
ovexd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ∈ V ) |
41 |
35 37 39 40
|
seqof2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) ) |
42 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) ∧ 𝑚 ∈ ℕ ) → 𝑧 = 𝐴 ) |
43 |
42
|
oveq1d |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) ) |
44 |
42
|
oveq1d |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑧 / 𝑚 ) = ( 𝐴 / 𝑚 ) ) |
45 |
44
|
fvoveq1d |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) |
46 |
43 45
|
oveq12d |
⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) |
47 |
46
|
mpteq2dva |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) |
48 |
47 3
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) = 𝐺 ) |
49 |
48
|
seqeq3d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) = seq 1 ( + , 𝐺 ) ) |
50 |
49
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = 𝐴 ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) |
51 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ 𝑈 ) |
52 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ∈ V ) |
53 |
41 50 51 52
|
fvmptd |
⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ‘ 𝑛 ) ‘ 𝐴 ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) ) |
54 |
21 22 30 19 32 53 28
|
ulmclm |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → seq 1 ( + , 𝐺 ) ⇝ ( ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ‘ 𝐴 ) ) |
55 |
|
fveq2 |
⊢ ( 𝑧 = 𝐴 → ( log ‘ 𝑧 ) = ( log ‘ 𝐴 ) ) |
56 |
5 55
|
oveq12d |
⊢ ( 𝑧 = 𝐴 → ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) = ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) |
57 |
|
eqid |
⊢ ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) |
58 |
|
ovex |
⊢ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ∈ V |
59 |
56 57 58
|
fvmpt |
⊢ ( 𝐴 ∈ 𝑈 → ( ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ‘ 𝐴 ) = ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) |
60 |
19 59
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → ( ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ‘ 𝐴 ) = ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) |
61 |
54 60
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) |
62 |
20 61
|
jca |
⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈 ) ) → ( ( log Γ ‘ 𝐴 ) ∈ ℂ ∧ seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) ) |
63 |
4 62
|
rexlimddv |
⊢ ( 𝜑 → ( ( log Γ ‘ 𝐴 ) ∈ ℂ ∧ seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) ) |