Metamath Proof Explorer

Theorem lgamgulm2

Description: Rewrite the limit of the sequence G in terms of the log-Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamgulm.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
Assertion lgamgulm2 ( 𝜑 → ( ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ ∧ seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2 lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3 lgamgulm.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
4 1 2 lgamgulmlem1 ⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
5 4 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
6 ovex ⊢ ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) ∈ V
7 df-lgam ⊢ log Γ = ( 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↦ ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) )
8 7 fvmpt2 ⊢ ( ( 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) ∈ V ) → ( log Γ ‘ 𝑧 ) = ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) )
9 5 6 8 sylancl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( log Γ ‘ 𝑧 ) = ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) )
10 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
11 1zzd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 1 ∈ ℤ )
12 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
13 id ⊢ ( 𝑚 = 𝑛 → 𝑚 = 𝑛 )
14 12 13 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 + 1 ) / 𝑚 ) = ( ( 𝑛 + 1 ) / 𝑛 ) )
15 14 fveq2d ⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) = ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
16 15 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
17 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑧 / 𝑚 ) = ( 𝑧 / 𝑛 ) )
18 17 fvoveq1d ⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) = ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) )
19 16 18 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) = ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) )
20 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) )
21 ovex ⊢ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ∈ V
22 19 20 21 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ‘ 𝑛 ) = ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ‘ 𝑛 ) = ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) )
24 5 eldifad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ℂ )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ℂ )
26 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
27 26 peano2nnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
28 27 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℝ+ )
29 26 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ+ )
30 28 29 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / 𝑛 ) ∈ ℝ+ )
31 30 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℝ )
32 31 recnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℂ )
33 25 32 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ∈ ℂ )
34 26 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
35 26 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
36 25 34 35 divcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑧 / 𝑛 ) ∈ ℂ )
37 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℂ )
38 36 37 addcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 / 𝑛 ) + 1 ) ∈ ℂ )
39 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
40 39 26 dmgmdivn0 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 / 𝑛 ) + 1 ) ≠ 0 )
41 38 40 logcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ∈ ℂ )
42 33 41 subcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ∈ ℂ )
43 1z ⊢ 1 ∈ ℤ
44 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( ∘f + , 𝐺 ) Fn ( ℤ≥ ‘ 1 ) )
45 43 44 ax-mp ⊢ seq 1 ( ∘f + , 𝐺 ) Fn ( ℤ≥ ‘ 1 )
46 10 fneq2i ⊢ ( seq 1 ( ∘f + , 𝐺 ) Fn ℕ ↔ seq 1 ( ∘f + , 𝐺 ) Fn ( ℤ≥ ‘ 1 ) )
47 45 46 mpbir ⊢ seq 1 ( ∘f + , 𝐺 ) Fn ℕ
48 1 2 3 lgamgulm ⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) ∈ dom ( ⇝𝑢 ‘ 𝑈 ) )
49 ulmdm ⊢ ( seq 1 ( ∘f + , 𝐺 ) ∈ dom ( ⇝𝑢 ‘ 𝑈 ) ↔ seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) )
50 48 49 sylib ⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) )
51 ulmf2 ⊢ ( ( seq 1 ( ∘f + , 𝐺 ) Fn ℕ ∧ seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ) → seq 1 ( ∘f + , 𝐺 ) : ℕ ⟶ ( ℂ ↑m 𝑈 ) )
52 47 50 51 sylancr ⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) : ℕ ⟶ ( ℂ ↑m 𝑈 ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → seq 1 ( ∘f + , 𝐺 ) : ℕ ⟶ ( ℂ ↑m 𝑈 ) )
54 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑈 )
55 seqex ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ∈ V
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ∈ V )
57 3 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) )
58 57 seqeq3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → seq 1 ( ∘f + , 𝐺 ) = seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) )
59 58 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( ∘f + , 𝐺 ) ‘ 𝑛 ) = ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ‘ 𝑛 ) )
60 cnex ⊢ ℂ ∈ V
61 2 60 rabex2 ⊢ 𝑈 ∈ V
62 61 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑈 ∈ V )
63 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
64 63 10 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
65 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ )
67 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ∈ V )
68 62 64 66 67 seqof2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) )
69 68 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( ∘f + , ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) )
70 59 69 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( ∘f + , 𝐺 ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) )
71 70 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( seq 1 ( ∘f + , 𝐺 ) ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) ‘ 𝑧 ) )
72 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → 𝑧 ∈ 𝑈 )
73 fvex ⊢ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ∈ V
74 eqid ⊢ ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) = ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) )
75 74 fvmpt2 ⊢ ( ( 𝑧 ∈ 𝑈 ∧ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ∈ V ) → ( ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) ‘ 𝑧 ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) )
76 72 73 75 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑧 ∈ 𝑈 ↦ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ) ‘ 𝑧 ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) )
77 71 76 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑛 ∈ ℕ ) → ( ( seq 1 ( ∘f + , 𝐺 ) ‘ 𝑛 ) ‘ 𝑧 ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) )
78 50 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) )
79 10 11 53 54 56 77 78 ulmclm ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) )
80 10 11 23 42 79 isumclim ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) = ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) )
81 ulmcl ⊢ ( seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) → ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) : 𝑈 ⟶ ℂ )
82 50 81 syl ⊢ ( 𝜑 → ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) : 𝑈 ⟶ ℂ )
83 82 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) ∈ ℂ )
84 80 83 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ∈ ℂ )
85 5 dmgmn0 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ≠ 0 )
86 24 85 logcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( log ‘ 𝑧 ) ∈ ℂ )
87 84 86 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) ∈ ℂ )
88 9 87 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( log Γ ‘ 𝑧 ) ∈ ℂ )
89 88 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ )
90 ffn ⊢ ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) : 𝑈 ⟶ ℂ → ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) Fn 𝑈 )
91 50 81 90 3syl ⊢ ( 𝜑 → ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) Fn 𝑈 )
92 nfcv ⊢ Ⅎ 𝑧 ( ⇝𝑢 ‘ 𝑈 )
93 nfcv ⊢ Ⅎ 𝑧 1
94 nfcv ⊢ Ⅎ 𝑧 ∘f +
95 nfcv ⊢ Ⅎ 𝑧 ℕ
96 nfmpt1 ⊢ Ⅎ 𝑧 ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) )
97 95 96 nfmpt ⊢ Ⅎ 𝑧 ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
98 3 97 nfcxfr ⊢ Ⅎ 𝑧 𝐺
99 93 94 98 nfseq ⊢ Ⅎ 𝑧 seq 1 ( ∘f + , 𝐺 )
100 92 99 nffv ⊢ Ⅎ 𝑧 ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) )
101 100 dffn5f ⊢ ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) Fn 𝑈 ↔ ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) ) )
102 91 101 sylib ⊢ ( 𝜑 → ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) ) )
103 9 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) = ( ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) + ( log ‘ 𝑧 ) ) )
104 84 86 npcand ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) + ( log ‘ 𝑧 ) ) = Σ 𝑛 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) )
105 103 104 80 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑈 ) → ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) = ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) )
106 105 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑈 ↦ ( ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) )
107 102 106 eqtrd ⊢ ( 𝜑 → ( ( ⇝𝑢 ‘ 𝑈 ) ‘ seq 1 ( ∘f + , 𝐺 ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) )
108 50 107 breqtrd ⊢ ( 𝜑 → seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) )
109 89 108 jca ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑈 ( log Γ ‘ 𝑧 ) ∈ ℂ ∧ seq 1 ( ∘f + , 𝐺 ) ( ⇝𝑢 ‘ 𝑈 ) ( 𝑧 ∈ 𝑈 ↦ ( ( log Γ ‘ 𝑧 ) + ( log ‘ 𝑧 ) ) ) ) )