Metamath Proof Explorer

Theorem lgamcvg2

Description: The series G converges to log_G ( A + 1 ) . (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Hypotheses lgamcvg.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
lgamcvg.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
Assertion lgamcvg2 ( 𝜑 → seq 1 ( + , 𝐺 ) ⇝ ( log Γ ‘ ( 𝐴 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 lgamcvg.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
2 lgamcvg.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
4 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
5 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) )
6 1nn0 ⊢ 1 ∈ ℕ0
7 6 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
8 2 7 dmgmaddnn0 ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
9 5 8 lgamcvg ⊢ ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( ( log Γ ‘ ( 𝐴 + 1 ) ) + ( log ‘ ( 𝐴 + 1 ) ) ) )
10 seqex ⊢ seq 1 ( + , 𝐺 ) ∈ V
11 10 a1i ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ∈ V )
12 2 eldifad ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13 12 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
14 arch ⊢ ( ( abs ‘ 𝐴 ) ∈ ℝ → ∃ 𝑟 ∈ ℕ ( abs ‘ 𝐴 ) < 𝑟 )
15 13 14 syl ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℕ ( abs ‘ 𝐴 ) < 𝑟 )
16 eqid ⊢ ( ℤ≥ ‘ 𝑟 ) = ( ℤ≥ ‘ 𝑟 )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → 𝑟 ∈ ℕ )
18 17 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → 𝑟 ∈ ℤ )
19 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
20 19 logcn ⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ )
21 20 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) )
22 eqid ⊢ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) = ( 1 ( ball ‘ ( abs ∘ − ) ) 1 )
23 22 dvlog2lem ⊢ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
24 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝐴 ∈ ℂ )
25 eluznn ⊢ ( ( 𝑟 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑚 ∈ ℕ )
26 25 ex ⊢ ( 𝑟 ∈ ℕ → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) → 𝑚 ∈ ℕ ) )
27 26 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) → 𝑚 ∈ ℕ ) )
28 27 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑚 ∈ ℕ )
29 28 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑚 ∈ ℂ )
30 1cnd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 1 ∈ ℂ )
31 29 30 addcld ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝑚 + 1 ) ∈ ℂ )
32 28 peano2nnd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝑚 + 1 ) ∈ ℕ )
33 32 nnne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝑚 + 1 ) ≠ 0 )
34 24 31 33 divcld ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝐴 / ( 𝑚 + 1 ) ) ∈ ℂ )
35 34 30 addcld ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ℂ )
36 ax-1cn ⊢ 1 ∈ ℂ
37 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
38 37 cnmetdval ⊢ ( ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ( abs ∘ − ) 1 ) = ( abs ‘ ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) − 1 ) ) )
39 35 36 38 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ( abs ∘ − ) 1 ) = ( abs ‘ ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) − 1 ) ) )
40 34 30 pncand ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) − 1 ) = ( 𝐴 / ( 𝑚 + 1 ) ) )
41 40 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) − 1 ) ) = ( abs ‘ ( 𝐴 / ( 𝑚 + 1 ) ) ) )
42 24 31 33 absdivd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ ( 𝐴 / ( 𝑚 + 1 ) ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ ( 𝑚 + 1 ) ) ) )
43 32 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝑚 + 1 ) ∈ ℝ )
44 32 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝑚 + 1 ) ∈ ℝ+ )
45 44 rpge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 0 ≤ ( 𝑚 + 1 ) )
46 43 45 absidd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ ( 𝑚 + 1 ) ) = ( 𝑚 + 1 ) )
47 46 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( abs ‘ 𝐴 ) / ( abs ‘ ( 𝑚 + 1 ) ) ) = ( ( abs ‘ 𝐴 ) / ( 𝑚 + 1 ) ) )
48 42 47 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ ( 𝐴 / ( 𝑚 + 1 ) ) ) = ( ( abs ‘ 𝐴 ) / ( 𝑚 + 1 ) ) )
49 39 41 48 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ( abs ∘ − ) 1 ) = ( ( abs ‘ 𝐴 ) / ( 𝑚 + 1 ) ) )
50 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
51 17 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑟 ∈ ℕ )
52 51 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑟 ∈ ℝ )
53 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ 𝐴 ) < 𝑟 )
54 eluzle ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) → 𝑟 ≤ 𝑚 )
55 54 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑟 ≤ 𝑚 )
56 nnleltp1 ⊢ ( ( 𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 𝑟 ≤ 𝑚 ↔ 𝑟 < ( 𝑚 + 1 ) ) )
57 51 28 56 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( 𝑟 ≤ 𝑚 ↔ 𝑟 < ( 𝑚 + 1 ) ) )
58 55 57 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 𝑟 < ( 𝑚 + 1 ) )
59 50 52 43 53 58 lttrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ 𝐴 ) < ( 𝑚 + 1 ) )
60 31 mulid1d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( 𝑚 + 1 ) · 1 ) = ( 𝑚 + 1 ) )
61 59 60 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ‘ 𝐴 ) < ( ( 𝑚 + 1 ) · 1 ) )
62 1red ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 1 ∈ ℝ )
63 50 62 44 ltdivmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( ( abs ‘ 𝐴 ) / ( 𝑚 + 1 ) ) < 1 ↔ ( abs ‘ 𝐴 ) < ( ( 𝑚 + 1 ) · 1 ) ) )
64 61 63 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( abs ‘ 𝐴 ) / ( 𝑚 + 1 ) ) < 1 )
65 49 64 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ( abs ∘ − ) 1 ) < 1 )
66 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
67 66 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
68 1rp ⊢ 1 ∈ ℝ+
69 rpxr ⊢ ( 1 ∈ ℝ+ → 1 ∈ ℝ* )
70 68 69 mp1i ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → 1 ∈ ℝ* )
71 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 1 ∈ ℂ ∧ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ℂ ) ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ( abs ∘ − ) 1 ) < 1 ) )
72 67 70 30 35 71 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ( abs ∘ − ) 1 ) < 1 ) )
73 65 72 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) )
74 23 73 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
75 74 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) : ( ℤ≥ ‘ 𝑟 ) ⟶ ( ℂ ∖ ( -∞ (,] 0 ) ) )
76 27 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ℤ≥ ‘ 𝑟 ) ⊆ ℕ )
77 76 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) )
78 nnex ⊢ ℕ ∈ V
79 78 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ∈ V
80 79 a1i ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ∈ V )
81 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
82 81 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝐴 / ( 𝑚 + 1 ) ) = ( 𝐴 / ( 𝑛 + 1 ) ) )
83 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) )
84 ovex ⊢ ( 𝐴 / ( 𝑛 + 1 ) ) ∈ V
85 82 83 84 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ‘ 𝑛 ) = ( 𝐴 / ( 𝑛 + 1 ) ) )
86 85 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ‘ 𝑛 ) = ( 𝐴 / ( 𝑛 + 1 ) ) )
87 3 4 12 4 80 86 divcnvshft ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ⇝ 0 )
88 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
89 78 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ∈ V
90 89 a1i ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ∈ V )
91 12 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℂ )
92 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
93 92 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
94 1cnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℂ )
95 93 94 addcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℂ )
96 92 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
97 96 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ≠ 0 )
98 91 95 97 divcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 / ( 𝑛 + 1 ) ) ∈ ℂ )
99 86 98 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ‘ 𝑛 ) ∈ ℂ )
100 82 oveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) = ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) )
101 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) )
102 ovex ⊢ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ∈ V
103 100 101 102 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ‘ 𝑛 ) = ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) )
104 103 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ‘ 𝑛 ) = ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) )
105 86 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ‘ 𝑛 ) + 1 ) = ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) )
106 104 105 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ‘ 𝑛 ) = ( ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / ( 𝑚 + 1 ) ) ) ‘ 𝑛 ) + 1 ) )
107 3 4 87 88 90 99 106 climaddc1 ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⇝ ( 0 + 1 ) )
108 0p1e1 ⊢ ( 0 + 1 ) = 1
109 107 108 breqtrdi ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⇝ 1 )
110 109 adantr ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⇝ 1 )
111 climres ⊢ ( ( 𝑟 ∈ ℤ ∧ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ∈ V ) → ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) ⇝ 1 ↔ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⇝ 1 ) )
112 18 89 111 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) ⇝ 1 ↔ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⇝ 1 ) )
113 110 112 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) ⇝ 1 )
114 77 113 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⇝ 1 )
115 68 a1i ⊢ ( 1 ∈ ℝ → 1 ∈ ℝ+ )
116 19 ellogdm ⊢ ( 1 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( 1 ∈ ℂ ∧ ( 1 ∈ ℝ → 1 ∈ ℝ+ ) ) )
117 36 115 116 mpbir2an ⊢ 1 ∈ ( ℂ ∖ ( -∞ (,] 0 ) )
118 117 a1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → 1 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
119 16 18 21 75 114 118 climcncf ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ⇝ ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 1 ) )
120 logf1o ⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
121 f1of ⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
122 120 121 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
123 19 logdmss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } )
124 123 74 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ) → ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ∈ ( ℂ ∖ { 0 } ) )
125 122 124 cofmpt ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( log ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) )
126 frn ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) : ( ℤ≥ ‘ 𝑟 ) ⟶ ( ℂ ∖ ( -∞ (,] 0 ) ) → ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) )
127 cores ⊢ ( ran ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) = ( log ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) )
128 75 126 127 3syl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) = ( log ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) )
129 76 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) = ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) )
130 125 128 129 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∘ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑟 ) ↦ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) = ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) )
131 fvres ⊢ ( 1 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 1 ) = ( log ‘ 1 ) )
132 117 131 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 1 ) = ( log ‘ 1 ) )
133 log1 ⊢ ( log ‘ 1 ) = 0
134 132 133 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ‘ 1 ) = 0 )
135 119 130 134 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) ⇝ 0 )
136 78 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ∈ V
137 climres ⊢ ( ( 𝑟 ∈ ℤ ∧ ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ∈ V ) → ( ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ⇝ 0 ) )
138 18 136 137 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ↾ ( ℤ≥ ‘ 𝑟 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ⇝ 0 ) )
139 135 138 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℕ ∧ ( abs ‘ 𝐴 ) < 𝑟 ) ) → ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ⇝ 0 )
140 15 139 rexlimddv ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ⇝ 0 )
141 12 88 addcld ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℂ )
142 8 dmgmn0 ⊢ ( 𝜑 → ( 𝐴 + 1 ) ≠ 0 )
143 141 142 logcld ⊢ ( 𝜑 → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℂ )
144 78 mptex ⊢ ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ∈ V
145 144 a1i ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ∈ V )
146 82 fvoveq1d ⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) = ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) )
147 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) )
148 fvex ⊢ ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ∈ V
149 146 147 148 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ‘ 𝑛 ) = ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) )
150 149 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ‘ 𝑛 ) = ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) )
151 98 94 addcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ∈ ℂ )
152 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
153 152 96 dmgmdivn0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ≠ 0 )
154 151 153 logcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ∈ ℂ )
155 150 154 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ‘ 𝑛 ) ∈ ℂ )
156 146 oveq2d ⊢ ( 𝑚 = 𝑛 → ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
157 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) )
158 ovex ⊢ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) ∈ V
159 156 157 158 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
160 159 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
161 150 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( log ‘ ( 𝐴 + 1 ) ) − ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ‘ 𝑛 ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
162 160 161 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( ( 𝑚 ∈ ℕ ↦ ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ‘ 𝑛 ) ) )
163 3 4 140 143 145 155 162 climsubc2 ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ⇝ ( ( log ‘ ( 𝐴 + 1 ) ) − 0 ) )
164 143 subid1d ⊢ ( 𝜑 → ( ( log ‘ ( 𝐴 + 1 ) ) − 0 ) = ( log ‘ ( 𝐴 + 1 ) ) )
165 163 164 breqtrd ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ⇝ ( log ‘ ( 𝐴 + 1 ) ) )
166 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ )
167 166 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
168 oveq1 ⊢ ( 𝑚 = 𝑘 → ( 𝑚 + 1 ) = ( 𝑘 + 1 ) )
169 id ⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 )
170 168 169 oveq12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 + 1 ) / 𝑚 ) = ( ( 𝑘 + 1 ) / 𝑘 ) )
171 170 fveq2d ⊢ ( 𝑚 = 𝑘 → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) = ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) )
172 171 oveq2d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) )
173 oveq2 ⊢ ( 𝑚 = 𝑘 → ( ( 𝐴 + 1 ) / 𝑚 ) = ( ( 𝐴 + 1 ) / 𝑘 ) )
174 173 fvoveq1d ⊢ ( 𝑚 = 𝑘 → ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) = ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) )
175 172 174 oveq12d ⊢ ( 𝑚 = 𝑘 → ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) = ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) )
176 ovex ⊢ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ∈ V
177 175 5 176 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ‘ 𝑘 ) = ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) )
178 167 177 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ‘ 𝑘 ) = ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) )
179 92 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
180 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ℂ )
181 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 1 ∈ ℂ )
182 180 181 addcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐴 + 1 ) ∈ ℂ )
183 167 peano2nnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 + 1 ) ∈ ℕ )
184 183 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 + 1 ) ∈ ℝ+ )
185 167 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℝ+ )
186 184 185 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑘 + 1 ) / 𝑘 ) ∈ ℝ+ )
187 186 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ∈ ℝ )
188 187 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ∈ ℂ )
189 182 188 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ∈ ℂ )
190 167 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℂ )
191 167 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ≠ 0 )
192 182 190 191 divcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + 1 ) / 𝑘 ) ∈ ℂ )
193 192 181 addcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ∈ ℂ )
194 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐴 + 1 ) ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
195 194 167 dmgmdivn0 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ≠ 0 )
196 193 195 logcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ∈ ℂ )
197 189 196 subcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ∈ ℂ )
198 178 179 197 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) )
199 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
200 199 197 fsumcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ∈ ℂ )
201 198 200 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
202 143 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℂ )
203 202 154 subcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) ∈ ℂ )
204 160 203 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
205 180 188 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ∈ ℂ )
206 180 190 191 divcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐴 / 𝑘 ) ∈ ℂ )
207 206 181 addcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 / 𝑘 ) + 1 ) ∈ ℂ )
208 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
209 208 167 dmgmdivn0 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 / 𝑘 ) + 1 ) ≠ 0 )
210 207 209 logcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ∈ ℂ )
211 205 210 subcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ∈ ℂ )
212 199 211 fsumcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ∈ ℂ )
213 200 212 nncand ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) )
214 189 196 205 210 sub4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) )
215 180 181 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
216 215 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) − 𝐴 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) = ( 1 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) )
217 182 180 188 subdird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) − 𝐴 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) = ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ) )
218 188 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 1 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) = ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) )
219 216 217 218 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ) = ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) )
220 219 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) )
221 188 196 210 subsubd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) + ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) )
222 188 196 subcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ∈ ℂ )
223 222 210 addcomd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) + ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) + ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ) )
224 210 196 188 subsub2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) + ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ) )
225 183 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 + 1 ) ∈ ℂ )
226 180 225 addcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐴 + ( 𝑘 + 1 ) ) ∈ ℂ )
227 183 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
228 dmgmaddn0 ⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐴 + ( 𝑘 + 1 ) ) ≠ 0 )
229 208 227 228 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐴 + ( 𝑘 + 1 ) ) ≠ 0 )
230 226 229 logcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) ∈ ℂ )
231 184 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
232 231 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
233 185 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ 𝑘 ) ∈ ℝ )
234 233 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ 𝑘 ) ∈ ℂ )
235 230 232 234 nnncan2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ 𝑘 ) ) − ( ( log ‘ ( 𝑘 + 1 ) ) − ( log ‘ 𝑘 ) ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ ( 𝑘 + 1 ) ) ) )
236 182 190 190 191 divdird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) + 𝑘 ) / 𝑘 ) = ( ( ( 𝐴 + 1 ) / 𝑘 ) + ( 𝑘 / 𝑘 ) ) )
237 180 190 181 add32d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + 𝑘 ) + 1 ) = ( ( 𝐴 + 1 ) + 𝑘 ) )
238 180 190 181 addassd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + 𝑘 ) + 1 ) = ( 𝐴 + ( 𝑘 + 1 ) ) )
239 237 238 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + 1 ) + 𝑘 ) = ( 𝐴 + ( 𝑘 + 1 ) ) )
240 239 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) + 𝑘 ) / 𝑘 ) = ( ( 𝐴 + ( 𝑘 + 1 ) ) / 𝑘 ) )
241 190 191 dividd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 / 𝑘 ) = 1 )
242 241 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) / 𝑘 ) + ( 𝑘 / 𝑘 ) ) = ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) )
243 236 240 242 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) = ( ( 𝐴 + ( 𝑘 + 1 ) ) / 𝑘 ) )
244 243 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) = ( log ‘ ( ( 𝐴 + ( 𝑘 + 1 ) ) / 𝑘 ) ) )
245 logdiv2 ⊢ ( ( ( 𝐴 + ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 𝐴 + ( 𝑘 + 1 ) ) ≠ 0 ∧ 𝑘 ∈ ℝ+ ) → ( log ‘ ( ( 𝐴 + ( 𝑘 + 1 ) ) / 𝑘 ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ 𝑘 ) ) )
246 226 229 185 245 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝐴 + ( 𝑘 + 1 ) ) / 𝑘 ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ 𝑘 ) ) )
247 244 246 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ 𝑘 ) ) )
248 184 185 relogdivd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) = ( ( log ‘ ( 𝑘 + 1 ) ) − ( log ‘ 𝑘 ) ) )
249 247 248 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) = ( ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ 𝑘 ) ) − ( ( log ‘ ( 𝑘 + 1 ) ) − ( log ‘ 𝑘 ) ) ) )
250 183 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑘 + 1 ) ≠ 0 )
251 180 225 225 250 divdird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 + ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) = ( ( 𝐴 / ( 𝑘 + 1 ) ) + ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) )
252 225 250 dividd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) = 1 )
253 252 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 / ( 𝑘 + 1 ) ) + ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) )
254 251 253 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) = ( ( 𝐴 + ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) )
255 254 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) = ( log ‘ ( ( 𝐴 + ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) ) )
256 logdiv2 ⊢ ( ( ( 𝐴 + ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 𝐴 + ( 𝑘 + 1 ) ) ≠ 0 ∧ ( 𝑘 + 1 ) ∈ ℝ+ ) → ( log ‘ ( ( 𝐴 + ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ ( 𝑘 + 1 ) ) ) )
257 226 229 184 256 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝐴 + ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ ( 𝑘 + 1 ) ) ) )
258 255 257 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) = ( ( log ‘ ( 𝐴 + ( 𝑘 + 1 ) ) ) − ( log ‘ ( 𝑘 + 1 ) ) ) )
259 235 249 258 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) = ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) )
260 259 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) )
261 224 260 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) + ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) )
262 221 223 261 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) − ( ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) )
263 214 220 262 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) )
264 263 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) )
265 199 197 211 fsumsub ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) )
266 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 𝑘 ) )
267 266 fvoveq1d ⊢ ( 𝑥 = 𝑘 → ( log ‘ ( ( 𝐴 / 𝑥 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) )
268 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐴 / 𝑥 ) = ( 𝐴 / ( 𝑘 + 1 ) ) )
269 268 fvoveq1d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( log ‘ ( ( 𝐴 / 𝑥 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) )
270 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 1 ) )
271 270 fvoveq1d ⊢ ( 𝑥 = 1 → ( log ‘ ( ( 𝐴 / 𝑥 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / 1 ) + 1 ) ) )
272 oveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐴 / 𝑥 ) = ( 𝐴 / ( 𝑛 + 1 ) ) )
273 272 fvoveq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( log ‘ ( ( 𝐴 / 𝑥 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) )
274 92 nnzd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
275 96 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
276 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝐴 ∈ ℂ )
277 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) → 𝑥 ∈ ℕ )
278 277 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝑥 ∈ ℕ )
279 278 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝑥 ∈ ℂ )
280 278 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝑥 ≠ 0 )
281 276 279 280 divcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → ( 𝐴 / 𝑥 ) ∈ ℂ )
282 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 1 ∈ ℂ )
283 281 282 addcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → ( ( 𝐴 / 𝑥 ) + 1 ) ∈ ℂ )
284 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
285 284 278 dmgmdivn0 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → ( ( 𝐴 / 𝑥 ) + 1 ) ≠ 0 )
286 283 285 logcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → ( log ‘ ( ( 𝐴 / 𝑥 ) + 1 ) ) ∈ ℂ )
287 267 269 271 273 274 275 286 telfsum ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) = ( ( log ‘ ( ( 𝐴 / 1 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
288 91 div1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 / 1 ) = 𝐴 )
289 288 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝐴 / 1 ) + 1 ) ) = ( log ‘ ( 𝐴 + 1 ) ) )
290 289 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( log ‘ ( ( 𝐴 / 1 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
291 287 290 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑘 + 1 ) ) + 1 ) ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
292 264 265 291 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) )
293 292 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) ) )
294 213 293 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) ) )
295 171 oveq2d ⊢ ( 𝑚 = 𝑘 → ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) )
296 oveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐴 / 𝑚 ) = ( 𝐴 / 𝑘 ) )
297 296 fvoveq1d ⊢ ( 𝑚 = 𝑘 → ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) )
298 295 297 oveq12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) )
299 ovex ⊢ ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) ∈ V
300 298 1 299 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) )
301 167 300 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) )
302 301 179 211 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝐴 · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑘 ) + 1 ) ) ) = ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) )
303 160 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) = ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) )
304 198 303 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 1 ... 𝑛 ) ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑘 + 1 ) / 𝑘 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑘 ) + 1 ) ) ) − ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑛 + 1 ) ) + 1 ) ) ) ) = ( ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) − ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) ) )
305 294 302 304 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑛 ) = ( ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( ( 𝐴 + 1 ) · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( ( 𝐴 + 1 ) / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) − ( ( 𝑚 ∈ ℕ ↦ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ ( ( 𝐴 / ( 𝑚 + 1 ) ) + 1 ) ) ) ) ‘ 𝑛 ) ) )
306 3 4 9 11 165 201 204 305 climsub ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ⇝ ( ( ( log Γ ‘ ( 𝐴 + 1 ) ) + ( log ‘ ( 𝐴 + 1 ) ) ) − ( log ‘ ( 𝐴 + 1 ) ) ) )
307 lgamcl ⊢ ( ( 𝐴 + 1 ) ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ ( 𝐴 + 1 ) ) ∈ ℂ )
308 8 307 syl ⊢ ( 𝜑 → ( log Γ ‘ ( 𝐴 + 1 ) ) ∈ ℂ )
309 308 143 pncand ⊢ ( 𝜑 → ( ( ( log Γ ‘ ( 𝐴 + 1 ) ) + ( log ‘ ( 𝐴 + 1 ) ) ) − ( log ‘ ( 𝐴 + 1 ) ) ) = ( log Γ ‘ ( 𝐴 + 1 ) ) )
310 306 309 breqtrd ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ⇝ ( log Γ ‘ ( 𝐴 + 1 ) ) )