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

Theorem lgamcvg2 25559
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 2818 . . . 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 25531 . . . 4 (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
83, 7lgamcvg 25558 . . 3 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9 seqex 13359 . . . 4 seq1( + , 𝐺) ∈ V
109a1i 11 . . 3 (𝜑 → seq1( + , 𝐺) ∈ V)
114eldifad 3945 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1211abscld 14784 . . . . . . 7 (𝜑 → (abs‘𝐴) ∈ ℝ)
13 arch 11882 . . . . . . 7 ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
1412, 13syl 17 . . . . . 6 (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15 eqid 2818 . . . . . . . . 9 (ℤ𝑟) = (ℤ𝑟)
16 simprl 767 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
1716nnzd 12074 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18 eqid 2818 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
1918logcn 25157 . . . . . . . . . 10 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
2019a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21 eqid 2818 . . . . . . . . . . . 12 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
2221dvlog2lem 25162 . . . . . . . . . . 11 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
2311ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝐴 ∈ ℂ)
24 eluznn 12306 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2524ex 413 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2625ad2antrl 724 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2726imp 407 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2827nncnd 11642 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℂ)
29 1cnd 10624 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℂ)
3028, 29addcld 10648 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℂ)
3127peano2nnd 11643 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℕ)
3231nnne0d 11675 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ≠ 0)
3323, 30, 32divcld 11404 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
3433, 29addcld 10648 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35 ax-1cn 10583 . . . . . . . . . . . . . . 15 1 ∈ ℂ
36 eqid 2818 . . . . . . . . . . . . . . . 16 (abs ∘ − ) = (abs ∘ − )
3736cnmetdval 23306 . . . . . . . . . . . . . . 15 ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3834, 35, 37sylancl 586 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3933, 29pncand 10986 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
4039fveq2d 6667 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
4123, 30, 32absdivd 14803 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
4231nnred 11641 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ)
4331nnrpd 12417 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ+)
4443rpge0d 12423 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 0 ≤ (𝑚 + 1))
4542, 44absidd 14770 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
4645oveq2d 7161 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4741, 46eqtrd 2853 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4838, 40, 473eqtrd 2857 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
4912ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) ∈ ℝ)
5016adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℕ)
5150nnred 11641 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℝ)
52 simplrr 774 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < 𝑟)
53 eluzle 12244 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ𝑟) → 𝑟𝑚)
5453adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟𝑚)
55 nnleltp1 12025 . . . . . . . . . . . . . . . . . 18 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5650, 27, 55syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5754, 56mpbid 233 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 < (𝑚 + 1))
5849, 51, 42, 52, 57lttrd 10789 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < (𝑚 + 1))
5930mulid1d 10646 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
6058, 59breqtrrd 5085 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61 1red 10630 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ)
6249, 61, 43ltdivmuld 12470 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
6360, 62mpbird 258 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
6448, 63eqbrtrd 5079 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65 cnxmet 23308 . . . . . . . . . . . . . 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 22929 . . . . . . . . . . . . 13 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7166, 69, 29, 34, 70syl22anc 834 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7264, 71mpbird 258 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1))
7322, 72sseldi 3962 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
7473fmpttd 6871 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)))
7526ssrdv 3970 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ𝑟) ⊆ ℕ)
7675resmptd 5901 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
77 nnex 11632 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
7877mptex 6977 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
7978a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
80 oveq1 7152 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
8180oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
82 eqid 2818 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
83 ovex 7178 . . . . . . . . . . . . . . . . 17 (𝐴 / (𝑛 + 1)) ∈ V
8481, 82, 83fvmpt 6761 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
8584adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
861, 2, 11, 2, 79, 85divcnvshft 15198 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
87 1cnd 10624 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
8877mptex 6977 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
8988a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
9011adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
91 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9291nncnd 11642 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
93 1cnd 10624 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℂ)
9492, 93addcld 10648 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
9591peano2nnd 11643 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
9695nnne0d 11675 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
9790, 94, 96divcld 11404 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
9885, 97eqeltrd 2910 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
9981oveq1d 7160 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100 eqid 2818 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
101 ovex 7178 . . . . . . . . . . . . . . . . 17 ((𝐴 / (𝑛 + 1)) + 1) ∈ V
10299, 100, 101fvmpt 6761 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
103102adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
10485oveq1d 7160 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105103, 104eqtr4d 2856 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
1061, 2, 86, 87, 89, 98, 105climaddc1 14979 . . . . . . . . . . . . 13 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
107 0p1e1 11747 . . . . . . . . . . . . 13 (0 + 1) = 1
108106, 107breqtrdi 5098 . . . . . . . . . . . 12 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
109108adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
110 climres 14920 . . . . . . . . . . . 12 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
11117, 88, 110sylancl 586 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
112109, 111mpbird 258 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1)
11376, 112eqbrtrrd 5081 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
11467a1i 11 . . . . . . . . . . 11 (1 ∈ ℝ → 1 ∈ ℝ+)
11518ellogdm 25149 . . . . . . . . . . 11 (1 ∈ (ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈ ℝ → 1 ∈ ℝ+)))
11635, 114, 115mpbir2an 707 . . . . . . . . . 10 1 ∈ (ℂ ∖ (-∞(,]0))
117116a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖ (-∞(,]0)))
11815, 17, 20, 74, 113, 117climcncf 23435 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
119 logf1o 25075 . . . . . . . . . . 11 log:(ℂ ∖ {0})–1-1-onto→ran log
120 f1of 6608 . . . . . . . . . . 11 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
121119, 120mp1i 13 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖ {0})⟶ran log)
12218logdmss 25152 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
123122, 73sseldi 3962 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
124121, 123cofmpt 6886 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
125 frn 6513 . . . . . . . . . 10 ((𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
126 cores 6095 . . . . . . . . . 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 5901 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
129124, 127, 1283eqtr4d 2863 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)))
130 fvres 6682 . . . . . . . . . 10 (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
131116, 130mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
132 log1 25096 . . . . . . . . 9 (log‘1) = 0
133131, 132syl6eq 2869 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
134118, 129, 1333brtr3d 5088 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0)
13577mptex 6977 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
136 climres 14920 . . . . . . . 8 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
13717, 135, 136sylancl 586 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
138134, 137mpbid 233 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
13914, 138rexlimddv 3288 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
14011, 87addcld 10648 . . . . . 6 (𝜑 → (𝐴 + 1) ∈ ℂ)
1417dmgmn0 25530 . . . . . 6 (𝜑 → (𝐴 + 1) ≠ 0)
142140, 141logcld 25081 . . . . 5 (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
14377mptex 6977 . . . . . 6 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
144143a1i 11 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
14581fvoveq1d 7167 . . . . . . . 8 (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
146 eqid 2818 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
147 fvex 6676 . . . . . . . 8 (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148145, 146, 147fvmpt 6761 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
149148adantl 482 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
15097, 93addcld 10648 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
1514adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
152151, 95dmgmdivn0 25532 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
153150, 152logcld 25081 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
154149, 153eqeltrd 2910 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
155145oveq2d 7161 . . . . . . . 8 (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
156 eqid 2818 . . . . . . . 8 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
157 ovex 7178 . . . . . . . 8 ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158155, 156, 157fvmpt 6761 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
159158adantl 482 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
160149oveq2d 7161 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
161159, 160eqtr4d 2856 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
1621, 2, 139, 142, 144, 154, 161climsubc2 14983 . . . 4 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
163142subid1d 10974 . . . 4 (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
164162, 163breqtrd 5083 . . 3 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
165 elfznn 12924 . . . . . . 7 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
166165adantl 482 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
167 oveq1 7152 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
168 id 22 . . . . . . . . . . 11 (𝑚 = 𝑘𝑚 = 𝑘)
169167, 168oveq12d 7163 . . . . . . . . . 10 (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
170169fveq2d 6667 . . . . . . . . 9 (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
171170oveq2d 7161 . . . . . . . 8 (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
172 oveq2 7153 . . . . . . . . 9 (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
173172fvoveq1d 7167 . . . . . . . 8 (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
174171, 173oveq12d 7163 . . . . . . 7 (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
175 ovex 7178 . . . . . . 7 (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
176174, 3, 175fvmpt 6761 . . . . . 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 2920 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
17911ad2antrr 722 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
180 1cnd 10624 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
181179, 180addcld 10648 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
182166peano2nnd 11643 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
183182nnrpd 12417 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ+)
184166nnrpd 12417 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+)
185183, 184rpdivcld 12436 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ+)
186185relogcld 25133 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
187186recnd 10657 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
188181, 187mulcld 10649 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
189166nncnd 11642 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
190166nnne0d 11675 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
191181, 189, 190divcld 11404 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
192191, 180addcld 10648 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
1937ad2antrr 722 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
194193, 166dmgmdivn0 25532 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
195192, 194logcld 25081 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
196188, 195subcld 10985 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
197177, 178, 196fsumser 15075 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
198 fzfid 13329 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
199198, 196fsumcl 15078 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
200197, 199eqeltrrd 2911 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
201142adantr 481 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
202201, 153subcld 10985 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
203159, 202eqeltrd 2910 . . 3 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
204179, 187mulcld 10649 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
205179, 189, 190divcld 11404 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
206205, 180addcld 10648 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
2074ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
208207, 166dmgmdivn0 25532 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
209206, 208logcld 25081 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
210204, 209subcld 10985 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
211198, 210fsumcl 15078 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
212199, 211nncand 10990 . . . . 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 11034 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
214179, 180pncan2d 10987 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
215214oveq1d 7160 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
216181, 179, 187subdird 11085 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
217187mulid2d 10647 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
218215, 216, 2173eqtr3d 2861 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
219218oveq1d 7160 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
220187, 195, 209subsubd 11013 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
221187, 195subcld 10985 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
222221, 209addcomd 10830 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
223209, 195, 187subsub2d 11014 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
224182nncnd 11642 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
225179, 224addcld 10648 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
226182nnnn0d 11943 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ0)
227 dmgmaddn0 25527 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴 + (𝑘 + 1)) ≠ 0)
228207, 226, 227syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
229225, 228logcld 25081 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
230183relogcld 25133 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
231230recnd 10657 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
232184relogcld 25133 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
233232recnd 10657 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
234229, 231, 233nnncan2d 11020 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
235181, 189, 189, 190divdird 11442 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
236179, 189, 180add32d 10855 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
237179, 189, 180addassd 10651 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
238236, 237eqtr3d 2855 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
239238oveq1d 7160 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
240189, 190dividd 11402 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
241240oveq2d 7161 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
242235, 239, 2413eqtr3rd 2862 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
243242fveq2d 6667 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
244 logdiv2 25127 . . . . . . . . . . . . . . . 16 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
245225, 228, 184, 244syl3anc 1363 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
246243, 245eqtrd 2853 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
247183, 184relogdivd 25136 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
248246, 247oveq12d 7163 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
249182nnne0d 11675 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
250179, 224, 224, 249divdird 11442 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
251224, 249dividd 11402 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
252251oveq2d 7161 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
253250, 252eqtr2d 2854 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
254253fveq2d 6667 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
255 logdiv2 25127 . . . . . . . . . . . . . . 15 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
256225, 228, 183, 255syl3anc 1363 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
257254, 256eqtrd 2853 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
258234, 248, 2573eqtr4d 2863 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
259258oveq2d 7161 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
260223, 259eqtr3d 2855 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
261220, 222, 2603eqtrd 2857 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
262213, 219, 2613eqtrd 2857 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
263262sumeq2dv 15048 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
264198, 196, 210fsumsub 15131 . . . . . . 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 7153 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
266265fvoveq1d 7167 . . . . . . . . 9 (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
267 oveq2 7153 . . . . . . . . . 10 (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
268267fvoveq1d 7167 . . . . . . . . 9 (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
269 oveq2 7153 . . . . . . . . . 10 (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
270269fvoveq1d 7167 . . . . . . . . 9 (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
271 oveq2 7153 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
272271fvoveq1d 7167 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
27391nnzd 12074 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
27495, 1eleqtrdi 2920 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ‘1))
27511ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
276 elfznn 12924 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
277276adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
278277nncnd 11642 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
279277nnne0d 11675 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
280275, 278, 279divcld 11404 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
281 1cnd 10624 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
282280, 281addcld 10648 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
2834ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
284283, 277dmgmdivn0 25532 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
285282, 284logcld 25081 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
286266, 268, 270, 272, 273, 274, 285telfsum 15147 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
28790div1d 11396 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
288287fvoveq1d 7167 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
289288oveq1d 7160 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
290286, 289eqtrd 2853 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
291263, 264, 2903eqtr3d 2861 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
292291oveq2d 7161 . . . . 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 2855 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
294170oveq2d 7161 . . . . . . . 8 (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
295 oveq2 7153 . . . . . . . . 9 (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
296295fvoveq1d 7167 . . . . . . . 8 (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
297294, 296oveq12d 7163 . . . . . . 7 (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
298 lgamcvg.g . . . . . . 7 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
299 ovex 7178 . . . . . . 7 ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
300297, 298, 299fvmpt 6761 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
301166, 300syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
302301, 178, 210fsumser 15075 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
303159eqcomd 2824 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
304197, 303oveq12d 7163 . . . 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 2861 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
3061, 2, 8, 10, 164, 200, 203, 305climsub 14978 . 2 (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
307 lgamcl 25545 . . . 4 ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
3087, 307syl 17 . . 3 (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
309308, 142pncand 10986 . 2 (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
310306, 309breqtrd 5083 1 (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wne 3013  wrex 3136  Vcvv 3492  cdif 3930  wss 3933  {csn 4557   class class class wbr 5057  cmpt 5137  ran crn 5549  cres 5550  ccom 5552  wf 6344  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  -∞cmnf 10661  *cxr 10662   < clt 10663  cle 10664  cmin 10858   / cdiv 11285  cn 11626  0cn0 11885  cz 11969  cuz 12231  +crp 12377  (,]cioc 12727  ...cfz 12880  seqcseq 13357  abscabs 14581  cli 14829  Σcsu 15030  ∞Metcxmet 20458  ballcbl 20460  cnccncf 23411  logclog 25065  log Γclgam 25520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  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 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-shft 14414  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-ef 15409  df-sin 15411  df-cos 15412  df-tan 15413  df-pi 15414  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-cmp 21923  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-limc 24391  df-dv 24392  df-ulm 24892  df-log 25067  df-cxp 25068  df-lgam 25523
This theorem is referenced by:  lgamp1  25561
  Copyright terms: Public domain W3C validator