Metamath Proof Explorer

Theorem lgamcvglem

Description: Lemma for lgamf and lgamcvg . (Contributed by Mario Carneiro, 8-Jul-2017)

Ref Expression
Hypotheses lgamucov.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑟 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑟 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamucov.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
lgamcvglem.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
Assertion lgamcvglem ( 𝜑 → ( ( log Γ ‘ 𝐴 ) ∈ ℂ ∧ seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) )

Proof

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 ‘ 𝐴 ) ) ) )