MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgamcvg2 Structured version   Visualization version   GIF version

Theorem lgamcvg2 25638
Description: The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.)
Hypotheses
Ref Expression
lgamcvg.g 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
lgamcvg.a (𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
Assertion
Ref Expression
lgamcvg2 (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
Distinct variable groups:   𝐴,𝑚   𝜑,𝑚
Allowed substitution hint:   𝐺(𝑚)

Proof of Theorem lgamcvg2
Dummy variables 𝑘 𝑛 𝑟 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12269 . . 3 ℕ = (ℤ‘1)
2 1zzd 12001 . . 3 (𝜑 → 1 ∈ ℤ)
3 eqid 2822 . . . 4 (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))
4 lgamcvg.a . . . . 5 (𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
5 1nn0 11901 . . . . . 6 1 ∈ ℕ0
65a1i 11 . . . . 5 (𝜑 → 1 ∈ ℕ0)
74, 6dmgmaddnn0 25610 . . . 4 (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
83, 7lgamcvg 25637 . . 3 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9 seqex 13366 . . . 4 seq1( + , 𝐺) ∈ V
109a1i 11 . . 3 (𝜑 → seq1( + , 𝐺) ∈ V)
114eldifad 3920 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1211abscld 14787 . . . . . . 7 (𝜑 → (abs‘𝐴) ∈ ℝ)
13 arch 11882 . . . . . . 7 ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
1412, 13syl 17 . . . . . 6 (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15 eqid 2822 . . . . . . . . 9 (ℤ𝑟) = (ℤ𝑟)
16 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
1716nnzd 12074 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18 eqid 2822 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
1918logcn 25236 . . . . . . . . . 10 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
2019a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21 eqid 2822 . . . . . . . . . . . 12 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
2221dvlog2lem 25241 . . . . . . . . . . 11 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
2311ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝐴 ∈ ℂ)
24 eluznn 12306 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2524ex 416 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2625ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2726imp 410 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2827nncnd 11641 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℂ)
29 1cnd 10625 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℂ)
3028, 29addcld 10649 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℂ)
3127peano2nnd 11642 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℕ)
3231nnne0d 11675 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ≠ 0)
3323, 30, 32divcld 11405 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
3433, 29addcld 10649 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35 ax-1cn 10584 . . . . . . . . . . . . . . 15 1 ∈ ℂ
36 eqid 2822 . . . . . . . . . . . . . . . 16 (abs ∘ − ) = (abs ∘ − )
3736cnmetdval 23374 . . . . . . . . . . . . . . 15 ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3834, 35, 37sylancl 589 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3933, 29pncand 10987 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
4039fveq2d 6656 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
4123, 30, 32absdivd 14806 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
4231nnred 11640 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ)
4331nnrpd 12417 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ+)
4443rpge0d 12423 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 0 ≤ (𝑚 + 1))
4542, 44absidd 14773 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
4645oveq2d 7156 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4741, 46eqtrd 2857 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4838, 40, 473eqtrd 2861 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
4912ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) ∈ ℝ)
5016adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℕ)
5150nnred 11640 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℝ)
52 simplrr 777 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < 𝑟)
53 eluzle 12244 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ𝑟) → 𝑟𝑚)
5453adantl 485 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟𝑚)
55 nnleltp1 12025 . . . . . . . . . . . . . . . . . 18 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5650, 27, 55syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5754, 56mpbid 235 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 < (𝑚 + 1))
5849, 51, 42, 52, 57lttrd 10790 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < (𝑚 + 1))
5930mulid1d 10647 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
6058, 59breqtrrd 5070 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61 1red 10631 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ)
6249, 61, 43ltdivmuld 12470 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
6360, 62mpbird 260 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
6448, 63eqbrtrd 5064 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65 cnxmet 23376 . . . . . . . . . . . . . 14 (abs ∘ − ) ∈ (∞Met‘ℂ)
6665a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
67 1rp 12381 . . . . . . . . . . . . . 14 1 ∈ ℝ+
68 rpxr 12386 . . . . . . . . . . . . . 14 (1 ∈ ℝ+ → 1 ∈ ℝ*)
6967, 68mp1i 13 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ*)
70 elbl3 22997 . . . . . . . . . . . . 13 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7166, 69, 29, 34, 70syl22anc 837 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7264, 71mpbird 260 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1))
7322, 72sseldi 3940 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
7473fmpttd 6861 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)))
7526ssrdv 3948 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ𝑟) ⊆ ℕ)
7675resmptd 5886 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
77 nnex 11631 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
7877mptex 6968 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
7978a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
80 oveq1 7147 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
8180oveq2d 7156 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
82 eqid 2822 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
83 ovex 7173 . . . . . . . . . . . . . . . . 17 (𝐴 / (𝑛 + 1)) ∈ V
8481, 82, 83fvmpt 6750 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
8584adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
861, 2, 11, 2, 79, 85divcnvshft 15201 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
87 1cnd 10625 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
8877mptex 6968 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
8988a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
9011adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
91 simpr 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9291nncnd 11641 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
93 1cnd 10625 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℂ)
9492, 93addcld 10649 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
9591peano2nnd 11642 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
9695nnne0d 11675 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
9790, 94, 96divcld 11405 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
9885, 97eqeltrd 2914 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
9981oveq1d 7155 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100 eqid 2822 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
101 ovex 7173 . . . . . . . . . . . . . . . . 17 ((𝐴 / (𝑛 + 1)) + 1) ∈ V
10299, 100, 101fvmpt 6750 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
103102adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
10485oveq1d 7155 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105103, 104eqtr4d 2860 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
1061, 2, 86, 87, 89, 98, 105climaddc1 14982 . . . . . . . . . . . . 13 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
107 0p1e1 11747 . . . . . . . . . . . . 13 (0 + 1) = 1
108106, 107breqtrdi 5083 . . . . . . . . . . . 12 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
109108adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
110 climres 14923 . . . . . . . . . . . 12 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
11117, 88, 110sylancl 589 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
112109, 111mpbird 260 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1)
11376, 112eqbrtrrd 5066 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
11467a1i 11 . . . . . . . . . . 11 (1 ∈ ℝ → 1 ∈ ℝ+)
11518ellogdm 25228 . . . . . . . . . . 11 (1 ∈ (ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈ ℝ → 1 ∈ ℝ+)))
11635, 114, 115mpbir2an 710 . . . . . . . . . 10 1 ∈ (ℂ ∖ (-∞(,]0))
117116a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖ (-∞(,]0)))
11815, 17, 20, 74, 113, 117climcncf 23503 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
119 logf1o 25154 . . . . . . . . . . 11 log:(ℂ ∖ {0})–1-1-onto→ran log
120 f1of 6597 . . . . . . . . . . 11 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
121119, 120mp1i 13 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖ {0})⟶ran log)
12218logdmss 25231 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
123122, 73sseldi 3940 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
124121, 123cofmpt 6876 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
125 frn 6500 . . . . . . . . . 10 ((𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
126 cores 6080 . . . . . . . . . 10 (ran (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
12774, 125, 1263syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
12875resmptd 5886 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
129124, 127, 1283eqtr4d 2867 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)))
130 fvres 6671 . . . . . . . . . 10 (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
131116, 130mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
132 log1 25175 . . . . . . . . 9 (log‘1) = 0
133131, 132syl6eq 2873 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
134118, 129, 1333brtr3d 5073 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0)
13577mptex 6968 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
136 climres 14923 . . . . . . . 8 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
13717, 135, 136sylancl 589 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
138134, 137mpbid 235 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
13914, 138rexlimddv 3277 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
14011, 87addcld 10649 . . . . . 6 (𝜑 → (𝐴 + 1) ∈ ℂ)
1417dmgmn0 25609 . . . . . 6 (𝜑 → (𝐴 + 1) ≠ 0)
142140, 141logcld 25160 . . . . 5 (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
14377mptex 6968 . . . . . 6 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
144143a1i 11 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
14581fvoveq1d 7162 . . . . . . . 8 (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
146 eqid 2822 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
147 fvex 6665 . . . . . . . 8 (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148145, 146, 147fvmpt 6750 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
149148adantl 485 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
15097, 93addcld 10649 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
1514adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
152151, 95dmgmdivn0 25611 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
153150, 152logcld 25160 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
154149, 153eqeltrd 2914 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
155145oveq2d 7156 . . . . . . . 8 (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
156 eqid 2822 . . . . . . . 8 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
157 ovex 7173 . . . . . . . 8 ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158155, 156, 157fvmpt 6750 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
159158adantl 485 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
160149oveq2d 7156 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
161159, 160eqtr4d 2860 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
1621, 2, 139, 142, 144, 154, 161climsubc2 14986 . . . 4 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
163142subid1d 10975 . . . 4 (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
164162, 163breqtrd 5068 . . 3 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
165 elfznn 12931 . . . . . . 7 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
166165adantl 485 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
167 oveq1 7147 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
168 id 22 . . . . . . . . . . 11 (𝑚 = 𝑘𝑚 = 𝑘)
169167, 168oveq12d 7158 . . . . . . . . . 10 (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
170169fveq2d 6656 . . . . . . . . 9 (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
171170oveq2d 7156 . . . . . . . 8 (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
172 oveq2 7148 . . . . . . . . 9 (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
173172fvoveq1d 7162 . . . . . . . 8 (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
174171, 173oveq12d 7158 . . . . . . 7 (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
175 ovex 7173 . . . . . . 7 (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
176174, 3, 175fvmpt 6750 . . . . . 6 (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
177166, 176syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
17891, 1eleqtrdi 2924 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
17911ad2antrr 725 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
180 1cnd 10625 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
181179, 180addcld 10649 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
182166peano2nnd 11642 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
183182nnrpd 12417 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ+)
184166nnrpd 12417 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+)
185183, 184rpdivcld 12436 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ+)
186185relogcld 25212 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
187186recnd 10658 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
188181, 187mulcld 10650 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
189166nncnd 11641 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
190166nnne0d 11675 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
191181, 189, 190divcld 11405 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
192191, 180addcld 10649 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
1937ad2antrr 725 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
194193, 166dmgmdivn0 25611 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
195192, 194logcld 25160 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
196188, 195subcld 10986 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
197177, 178, 196fsumser 15078 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
198 fzfid 13336 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
199198, 196fsumcl 15081 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
200197, 199eqeltrrd 2915 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
201142adantr 484 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
202201, 153subcld 10986 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
203159, 202eqeltrd 2914 . . 3 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
204179, 187mulcld 10650 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
205179, 189, 190divcld 11405 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
206205, 180addcld 10649 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
2074ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
208207, 166dmgmdivn0 25611 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
209206, 208logcld 25160 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
210204, 209subcld 10986 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
211198, 210fsumcl 15081 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
212199, 211nncand 10991 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))) = Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
213188, 195, 204, 209sub4d 11035 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
214179, 180pncan2d 10988 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
215214oveq1d 7155 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
216181, 179, 187subdird 11086 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
217187mulid2d 10648 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
218215, 216, 2173eqtr3d 2865 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
219218oveq1d 7155 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
220187, 195, 209subsubd 11014 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
221187, 195subcld 10986 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
222221, 209addcomd 10831 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
223209, 195, 187subsub2d 11015 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
224182nncnd 11641 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
225179, 224addcld 10649 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
226182nnnn0d 11943 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ0)
227 dmgmaddn0 25606 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴 + (𝑘 + 1)) ≠ 0)
228207, 226, 227syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
229225, 228logcld 25160 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
230183relogcld 25212 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
231230recnd 10658 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
232184relogcld 25212 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
233232recnd 10658 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
234229, 231, 233nnncan2d 11021 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
235181, 189, 189, 190divdird 11443 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
236179, 189, 180add32d 10856 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
237179, 189, 180addassd 10652 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
238236, 237eqtr3d 2859 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
239238oveq1d 7155 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
240189, 190dividd 11403 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
241240oveq2d 7156 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
242235, 239, 2413eqtr3rd 2866 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
243242fveq2d 6656 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
244 logdiv2 25206 . . . . . . . . . . . . . . . 16 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
245225, 228, 184, 244syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
246243, 245eqtrd 2857 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
247183, 184relogdivd 25215 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
248246, 247oveq12d 7158 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
249182nnne0d 11675 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
250179, 224, 224, 249divdird 11443 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
251224, 249dividd 11403 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
252251oveq2d 7156 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
253250, 252eqtr2d 2858 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
254253fveq2d 6656 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
255 logdiv2 25206 . . . . . . . . . . . . . . 15 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
256225, 228, 183, 255syl3anc 1368 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
257254, 256eqtrd 2857 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
258234, 248, 2573eqtr4d 2867 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
259258oveq2d 7156 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
260223, 259eqtr3d 2859 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
261220, 222, 2603eqtrd 2861 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
262213, 219, 2613eqtrd 2861 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
263262sumeq2dv 15051 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
264198, 196, 210fsumsub 15134 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))))
265 oveq2 7148 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
266265fvoveq1d 7162 . . . . . . . . 9 (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
267 oveq2 7148 . . . . . . . . . 10 (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
268267fvoveq1d 7162 . . . . . . . . 9 (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
269 oveq2 7148 . . . . . . . . . 10 (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
270269fvoveq1d 7162 . . . . . . . . 9 (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
271 oveq2 7148 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
272271fvoveq1d 7162 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
27391nnzd 12074 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
27495, 1eleqtrdi 2924 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ‘1))
27511ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
276 elfznn 12931 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
277276adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
278277nncnd 11641 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
279277nnne0d 11675 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
280275, 278, 279divcld 11405 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
281 1cnd 10625 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
282280, 281addcld 10649 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
2834ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
284283, 277dmgmdivn0 25611 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
285282, 284logcld 25160 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
286266, 268, 270, 272, 273, 274, 285telfsum 15150 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
28790div1d 11397 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
288287fvoveq1d 7162 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
289288oveq1d 7155 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
290286, 289eqtrd 2857 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
291263, 264, 2903eqtr3d 2865 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
292291oveq2d 7156 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (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)))))
293212, 292eqtr3d 2859 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
294170oveq2d 7156 . . . . . . . 8 (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
295 oveq2 7148 . . . . . . . . 9 (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
296295fvoveq1d 7162 . . . . . . . 8 (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
297294, 296oveq12d 7158 . . . . . . 7 (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
298 lgamcvg.g . . . . . . 7 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
299 ovex 7173 . . . . . . 7 ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
300297, 298, 299fvmpt 6750 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
301166, 300syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
302301, 178, 210fsumser 15078 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
303159eqcomd 2828 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
304197, 303oveq12d 7158 . . . 4 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
305293, 302, 3043eqtr3d 2865 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
3061, 2, 8, 10, 164, 200, 203, 305climsub 14981 . 2 (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
307 lgamcl 25624 . . . 4 ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
3087, 307syl 17 . . 3 (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
309308, 142pncand 10987 . 2 (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
310306, 309breqtrd 5068 1 (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2114  wne 3011  wrex 3131  Vcvv 3469  cdif 3905  wss 3908  {csn 4539   class class class wbr 5042  cmpt 5122  ran crn 5533  cres 5534  ccom 5536  wf 6330  1-1-ontowf1o 6333  cfv 6334  (class class class)co 7140  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  -∞cmnf 10662  *cxr 10663   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  cn 11625  0cn0 11885  cz 11969  cuz 12231  +crp 12377  (,]cioc 12727  ...cfz 12885  seqcseq 13364  abscabs 14584  cli 14832  Σcsu 15033  ∞Metcxmet 20074  ballcbl 20076  cnccncf 23479  logclog 25144  log Γclgam 25599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-shft 14417  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-limsup 14819  df-clim 14836  df-rlim 14837  df-sum 15034  df-ef 15412  df-sin 15414  df-cos 15415  df-tan 15416  df-pi 15417  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-mulr 16570  df-starv 16571  df-sca 16572  df-vsca 16573  df-ip 16574  df-tset 16575  df-ple 16576  df-ds 16578  df-unif 16579  df-hom 16580  df-cco 16581  df-rest 16687  df-topn 16688  df-0g 16706  df-gsum 16707  df-topgen 16708  df-pt 16709  df-prds 16712  df-xrs 16766  df-qtop 16771  df-imas 16772  df-xps 16774  df-mre 16848  df-mrc 16849  df-acs 16851  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-submnd 17948  df-mulg 18216  df-cntz 18438  df-cmn 18899  df-psmet 20081  df-xmet 20082  df-met 20083  df-bl 20084  df-mopn 20085  df-fbas 20086  df-fg 20087  df-cnfld 20090  df-top 21497  df-topon 21514  df-topsp 21536  df-bases 21549  df-cld 21622  df-ntr 21623  df-cls 21624  df-nei 21701  df-lp 21739  df-perf 21740  df-cn 21830  df-cnp 21831  df-haus 21918  df-cmp 21990  df-tx 22165  df-hmeo 22358  df-fil 22449  df-fm 22541  df-flim 22542  df-flf 22543  df-xms 22925  df-ms 22926  df-tms 22927  df-cncf 23481  df-limc 24467  df-dv 24468  df-ulm 24970  df-log 25146  df-cxp 25147  df-lgam 25602
This theorem is referenced by:  lgamp1  25640
  Copyright terms: Public domain W3C validator