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

Theorem lgamcvg2 24698
 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 11675 . . 3 ℕ = (ℤ‘1)
2 1zzd 11360 . . 3 (𝜑 → 1 ∈ ℤ)
3 eqid 2621 . . . 4 (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))
4 lgamcvg.a . . . . 5 (𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
5 1nn0 11260 . . . . . 6 1 ∈ ℕ0
65a1i 11 . . . . 5 (𝜑 → 1 ∈ ℕ0)
74, 6dmgmaddnn0 24670 . . . 4 (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
83, 7lgamcvg 24697 . . 3 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9 seqex 12751 . . . 4 seq1( + , 𝐺) ∈ V
109a1i 11 . . 3 (𝜑 → seq1( + , 𝐺) ∈ V)
114eldifad 3571 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1211abscld 14117 . . . . . . 7 (𝜑 → (abs‘𝐴) ∈ ℝ)
13 arch 11241 . . . . . . 7 ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
1412, 13syl 17 . . . . . 6 (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15 eqid 2621 . . . . . . . . 9 (ℤ𝑟) = (ℤ𝑟)
16 simprl 793 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
1716nnzd 11433 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18 eqid 2621 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
1918logcn 24310 . . . . . . . . . 10 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
2019a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21 eqid 2621 . . . . . . . . . . . 12 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
2221dvlog2lem 24315 . . . . . . . . . . 11 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
2311ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝐴 ∈ ℂ)
24 eluznn 11710 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2524ex 450 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2625ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2726imp 445 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2827nncnd 10988 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℂ)
29 1cnd 10008 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℂ)
3028, 29addcld 10011 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℂ)
3127peano2nnd 10989 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℕ)
3231nnne0d 11017 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ≠ 0)
3323, 30, 32divcld 10753 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
3433, 29addcld 10011 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35 ax-1cn 9946 . . . . . . . . . . . . . . 15 1 ∈ ℂ
36 eqid 2621 . . . . . . . . . . . . . . . 16 (abs ∘ − ) = (abs ∘ − )
3736cnmetdval 22497 . . . . . . . . . . . . . . 15 ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3834, 35, 37sylancl 693 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3933, 29pncand 10345 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
4039fveq2d 6157 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
4123, 30, 32absdivd 14136 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
4231nnred 10987 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ)
4331nnrpd 11822 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ+)
4443rpge0d 11828 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 0 ≤ (𝑚 + 1))
4542, 44absidd 14103 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
4645oveq2d 6626 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4741, 46eqtrd 2655 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4838, 40, 473eqtrd 2659 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
4912ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) ∈ ℝ)
5016adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℕ)
5150nnred 10987 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℝ)
52 simplrr 800 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < 𝑟)
53 eluzle 11652 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ𝑟) → 𝑟𝑚)
5453adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟𝑚)
55 nnleltp1 11384 . . . . . . . . . . . . . . . . . 18 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5650, 27, 55syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5754, 56mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 < (𝑚 + 1))
5849, 51, 42, 52, 57lttrd 10150 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < (𝑚 + 1))
5930mulid1d 10009 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
6058, 59breqtrrd 4646 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61 1red 10007 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ)
6249, 61, 43ltdivmuld 11875 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
6360, 62mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
6448, 63eqbrtrd 4640 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65 cnxmet 22499 . . . . . . . . . . . . . 14 (abs ∘ − ) ∈ (∞Met‘ℂ)
6665a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
67 1rp 11788 . . . . . . . . . . . . . 14 1 ∈ ℝ+
68 rpxr 11792 . . . . . . . . . . . . . 14 (1 ∈ ℝ+ → 1 ∈ ℝ*)
6967, 68mp1i 13 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ*)
70 elbl3 22120 . . . . . . . . . . . . 13 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7166, 69, 29, 34, 70syl22anc 1324 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7264, 71mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1))
7322, 72sseldi 3585 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
74 eqid 2621 . . . . . . . . . 10 (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))
7573, 74fmptd 6346 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)))
7626ssrdv 3593 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ𝑟) ⊆ ℕ)
7776resmptd 5416 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
7812recnd 10020 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝐴) ∈ ℂ)
79 divcnv 14521 . . . . . . . . . . . . . . . . 17 ((abs‘𝐴) ∈ ℂ → (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0)
8078, 79syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0)
81 nnex 10978 . . . . . . . . . . . . . . . . . 18 ℕ ∈ V
8281mptex 6446 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ∈ V
8382a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ∈ V)
84 oveq2 6618 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((abs‘𝐴) / 𝑚) = ((abs‘𝐴) / 𝑛))
85 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) = (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))
86 ovex 6638 . . . . . . . . . . . . . . . . . . 19 ((abs‘𝐴) / 𝑛) ∈ V
8784, 85, 86fvmpt 6244 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛))
8887adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛))
8911adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
9089abscld 14117 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (abs‘𝐴) ∈ ℝ)
91 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9290, 91nndivred 11021 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((abs‘𝐴) / 𝑛) ∈ ℝ)
9388, 92eqeltrd 2698 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) ∈ ℝ)
94 oveq1 6617 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
9594oveq2d 6626 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
9695fveq2d 6157 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (abs‘(𝐴 / (𝑚 + 1))) = (abs‘(𝐴 / (𝑛 + 1))))
97 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) = (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))
98 fvex 6163 . . . . . . . . . . . . . . . . . . 19 (abs‘(𝐴 / (𝑛 + 1))) ∈ V
9996, 97, 98fvmpt 6244 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1))))
10099adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1))))
10191nncnd 10988 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
102 1cnd 10008 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℂ)
103101, 102addcld 10011 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
10491peano2nnd 10989 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
105104nnne0d 11017 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
10689, 103, 105divcld 10753 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
107106abscld 14117 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ∈ ℝ)
108100, 107eqeltrd 2698 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ∈ ℝ)
10989, 103, 105absdivd 14136 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (abs‘(𝑛 + 1))))
110104nnred 10987 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ)
111104nnrpd 11822 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ+)
112111rpge0d 11828 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝑛 + 1))
113110, 112absidd 14103 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝑛 + 1)) = (𝑛 + 1))
114113oveq2d 6626 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((abs‘𝐴) / (abs‘(𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1)))
115109, 114eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1)))
11691nnrpd 11822 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+)
11789absge0d 14125 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (abs‘𝐴))
11891nnred 10987 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
119118lep1d 10907 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1))
120116, 111, 90, 117, 119lediv2ad 11846 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((abs‘𝐴) / (𝑛 + 1)) ≤ ((abs‘𝐴) / 𝑛))
121115, 120eqbrtrd 4640 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ≤ ((abs‘𝐴) / 𝑛))
122121, 100, 883brtr4d 4650 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ≤ ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛))
123106absge0d 14125 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (abs‘(𝐴 / (𝑛 + 1))))
124123, 100breqtrrd 4646 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛))
1251, 2, 80, 83, 93, 108, 122, 124climsqz2 14314 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0)
12681mptex 6446 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
127126a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
128 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
129 ovex 6638 . . . . . . . . . . . . . . . . . . 19 (𝐴 / (𝑛 + 1)) ∈ V
13095, 128, 129fvmpt 6244 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
131130adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
132131, 106eqeltrd 2698 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
133131fveq2d 6157 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛)) = (abs‘(𝐴 / (𝑛 + 1))))
134100, 133eqtr4d 2658 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛)))
1351, 2, 127, 83, 132, 134climabs0 14258 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0))
136125, 135mpbird 247 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
137 1cnd 10008 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
13881mptex 6446 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
139138a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
14095oveq1d 6625 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
141 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
142 ovex 6638 . . . . . . . . . . . . . . . . 17 ((𝐴 / (𝑛 + 1)) + 1) ∈ V
143140, 141, 142fvmpt 6244 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
144143adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
145131oveq1d 6625 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
146144, 145eqtr4d 2658 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
1471, 2, 136, 137, 139, 132, 146climaddc1 14307 . . . . . . . . . . . . 13 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
148 0p1e1 11084 . . . . . . . . . . . . 13 (0 + 1) = 1
149147, 148syl6breq 4659 . . . . . . . . . . . 12 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
150149adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
151 climres 14248 . . . . . . . . . . . 12 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
15217, 138, 151sylancl 693 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
153150, 152mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1)
15477, 153eqbrtrrd 4642 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
15567a1i 11 . . . . . . . . . . 11 (1 ∈ ℝ → 1 ∈ ℝ+)
15618ellogdm 24302 . . . . . . . . . . 11 (1 ∈ (ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈ ℝ → 1 ∈ ℝ+)))
15735, 155, 156mpbir2an 954 . . . . . . . . . 10 1 ∈ (ℂ ∖ (-∞(,]0))
158157a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖ (-∞(,]0)))
15915, 17, 20, 75, 154, 158climcncf 22626 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
16018logdmss 24305 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
161160, 73sseldi 3585 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
162 eqidd 2622 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
163 logf1o 24232 . . . . . . . . . . . 12 log:(ℂ ∖ {0})–1-1-onto→ran log
164 f1of 6099 . . . . . . . . . . . 12 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
165163, 164mp1i 13 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖ {0})⟶ran log)
166165feqmptd 6211 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log = (𝑥 ∈ (ℂ ∖ {0}) ↦ (log‘𝑥)))
167 fveq2 6153 . . . . . . . . . 10 (𝑥 = ((𝐴 / (𝑚 + 1)) + 1) → (log‘𝑥) = (log‘((𝐴 / (𝑚 + 1)) + 1)))
168161, 162, 166, 167fmptco 6357 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
169 frn 6015 . . . . . . . . . 10 ((𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
170 cores 5602 . . . . . . . . . 10 (ran (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
17175, 169, 1703syl 18 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
17276resmptd 5416 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
173168, 171, 1723eqtr4d 2665 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)))
174 fvres 6169 . . . . . . . . . 10 (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
175157, 174mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
176 log1 24253 . . . . . . . . 9 (log‘1) = 0
177175, 176syl6eq 2671 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
178159, 173, 1773brtr3d 4649 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0)
17981mptex 6446 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
180 climres 14248 . . . . . . . 8 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
18117, 179, 180sylancl 693 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
182178, 181mpbid 222 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
18314, 182rexlimddv 3029 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
18411, 137addcld 10011 . . . . . 6 (𝜑 → (𝐴 + 1) ∈ ℂ)
1857dmgmn0 24669 . . . . . 6 (𝜑 → (𝐴 + 1) ≠ 0)
186184, 185logcld 24238 . . . . 5 (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
18781mptex 6446 . . . . . 6 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
188187a1i 11 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
189140fveq2d 6157 . . . . . . . 8 (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
190 eqid 2621 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
191 fvex 6163 . . . . . . . 8 (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
192189, 190, 191fvmpt 6244 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
193192adantl 482 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
194106, 102addcld 10011 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
1954adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
196195, 104dmgmdivn0 24671 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
197194, 196logcld 24238 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
198193, 197eqeltrd 2698 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
199189oveq2d 6626 . . . . . . . 8 (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
200 eqid 2621 . . . . . . . 8 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
201 ovex 6638 . . . . . . . 8 ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
202199, 200, 201fvmpt 6244 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
203202adantl 482 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
204193oveq2d 6626 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
205203, 204eqtr4d 2658 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
2061, 2, 183, 186, 188, 198, 205climsubc2 14311 . . . 4 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
207186subid1d 10333 . . . 4 (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
208206, 207breqtrd 4644 . . 3 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
209 elfznn 12320 . . . . . . 7 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
210209adantl 482 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
211 oveq1 6617 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
212 id 22 . . . . . . . . . . 11 (𝑚 = 𝑘𝑚 = 𝑘)
213211, 212oveq12d 6628 . . . . . . . . . 10 (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
214213fveq2d 6157 . . . . . . . . 9 (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
215214oveq2d 6626 . . . . . . . 8 (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
216 oveq2 6618 . . . . . . . . . 10 (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
217216oveq1d 6625 . . . . . . . . 9 (𝑚 = 𝑘 → (((𝐴 + 1) / 𝑚) + 1) = (((𝐴 + 1) / 𝑘) + 1))
218217fveq2d 6157 . . . . . . . 8 (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
219215, 218oveq12d 6628 . . . . . . 7 (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
220 ovex 6638 . . . . . . 7 (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
221219, 3, 220fvmpt 6244 . . . . . 6 (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
222210, 221syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
22391, 1syl6eleq 2708 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
22411ad2antrr 761 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
225 1cnd 10008 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
226224, 225addcld 10011 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
227210peano2nnd 10989 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
228227nnrpd 11822 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ+)
229210nnrpd 11822 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+)
230228, 229rpdivcld 11841 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ+)
231230relogcld 24290 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
232231recnd 10020 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
233226, 232mulcld 10012 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
234210nncnd 10988 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
235210nnne0d 11017 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
236226, 234, 235divcld 10753 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
237236, 225addcld 10011 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
2387ad2antrr 761 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
239238, 210dmgmdivn0 24671 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
240237, 239logcld 24238 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
241233, 240subcld 10344 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
242222, 223, 241fsumser 14402 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
243 fzfid 12720 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
244243, 241fsumcl 14405 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
245242, 244eqeltrrd 2699 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
246186adantr 481 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
247246, 197subcld 10344 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
248203, 247eqeltrd 2698 . . 3 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
249224, 232mulcld 10012 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
250224, 234, 235divcld 10753 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
251250, 225addcld 10011 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
2524ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
253252, 210dmgmdivn0 24671 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
254251, 253logcld 24238 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
255249, 254subcld 10344 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
256243, 255fsumcl 14405 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
257244, 256nncand 10349 . . . . 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))))
258233, 240, 249, 254sub4d 10393 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
259224, 225pncan2d 10346 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
260259oveq1d 6625 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
261226, 224, 232subdird 10439 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
262232mulid2d 10010 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
263260, 261, 2623eqtr3d 2663 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
264263oveq1d 6625 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
265232, 240, 254subsubd 10372 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
266232, 240subcld 10344 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
267266, 254addcomd 10190 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
268254, 240, 232subsub2d 10373 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
269227nncnd 10988 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
270224, 269addcld 10011 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
271227nnnn0d 11303 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ0)
272 dmgmaddn0 24666 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴 + (𝑘 + 1)) ≠ 0)
273252, 271, 272syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
274270, 273logcld 24238 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
275228relogcld 24290 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
276275recnd 10020 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
277229relogcld 24290 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
278277recnd 10020 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
279274, 276, 278nnncan2d 10379 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
280226, 234, 234, 235divdird 10791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
281224, 234, 225add32d 10215 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
282224, 234, 225addassd 10014 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
283281, 282eqtr3d 2657 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
284283oveq1d 6625 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
285234, 235dividd 10751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
286285oveq2d 6626 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
287280, 284, 2863eqtr3rd 2664 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
288287fveq2d 6157 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
289 logdiv2 24284 . . . . . . . . . . . . . . . 16 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
290270, 273, 229, 289syl3anc 1323 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
291288, 290eqtrd 2655 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
292228, 229relogdivd 24293 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
293291, 292oveq12d 6628 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
294227nnne0d 11017 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
295224, 269, 269, 294divdird 10791 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
296269, 294dividd 10751 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
297296oveq2d 6626 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
298295, 297eqtr2d 2656 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
299298fveq2d 6157 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
300 logdiv2 24284 . . . . . . . . . . . . . . 15 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
301270, 273, 228, 300syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
302299, 301eqtrd 2655 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
303279, 293, 3023eqtr4d 2665 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
304303oveq2d 6626 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
305268, 304eqtr3d 2657 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
306265, 267, 3053eqtrd 2659 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
307258, 264, 3063eqtrd 2659 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
308307sumeq2dv 14375 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
309243, 241, 255fsumsub 14459 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))))
310 oveq2 6618 . . . . . . . . . . 11 (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
311310oveq1d 6625 . . . . . . . . . 10 (𝑥 = 𝑘 → ((𝐴 / 𝑥) + 1) = ((𝐴 / 𝑘) + 1))
312311fveq2d 6157 . . . . . . . . 9 (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
313 oveq2 6618 . . . . . . . . . . 11 (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
314313oveq1d 6625 . . . . . . . . . 10 (𝑥 = (𝑘 + 1) → ((𝐴 / 𝑥) + 1) = ((𝐴 / (𝑘 + 1)) + 1))
315314fveq2d 6157 . . . . . . . . 9 (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
316 oveq2 6618 . . . . . . . . . . 11 (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
317316oveq1d 6625 . . . . . . . . . 10 (𝑥 = 1 → ((𝐴 / 𝑥) + 1) = ((𝐴 / 1) + 1))
318317fveq2d 6157 . . . . . . . . 9 (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
319 oveq2 6618 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
320319oveq1d 6625 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝐴 / 𝑥) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
321320fveq2d 6157 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
32291nnzd 11433 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
323104, 1syl6eleq 2708 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ‘1))
32411ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
325 elfznn 12320 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
326325adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
327326nncnd 10988 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
328326nnne0d 11017 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
329324, 327, 328divcld 10753 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
330 1cnd 10008 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
331329, 330addcld 10011 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
3324ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
333332, 326dmgmdivn0 24671 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
334331, 333logcld 24238 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
335312, 315, 318, 321, 322, 323, 334telfsum 14474 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
33689div1d 10745 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
337336oveq1d 6625 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / 1) + 1) = (𝐴 + 1))
338337fveq2d 6157 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
339338oveq1d 6625 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
340335, 339eqtrd 2655 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
341308, 309, 3403eqtr3d 2663 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
342341oveq2d 6626 . . . . 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)))))
343257, 342eqtr3d 2657 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
344214oveq2d 6626 . . . . . . . 8 (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
345 oveq2 6618 . . . . . . . . . 10 (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
346345oveq1d 6625 . . . . . . . . 9 (𝑚 = 𝑘 → ((𝐴 / 𝑚) + 1) = ((𝐴 / 𝑘) + 1))
347346fveq2d 6157 . . . . . . . 8 (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
348344, 347oveq12d 6628 . . . . . . 7 (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
349 lgamcvg.g . . . . . . 7 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
350 ovex 6638 . . . . . . 7 ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
351348, 349, 350fvmpt 6244 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
352210, 351syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
353352, 223, 255fsumser 14402 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
354203eqcomd 2627 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
355242, 354oveq12d 6628 . . . 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))))‘𝑛)))
356343, 353, 3553eqtr3d 2663 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
3571, 2, 8, 10, 208, 245, 248, 356climsub 14306 . 2 (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
358 lgamcl 24684 . . . 4 ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
3597, 358syl 17 . . 3 (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
360359, 186pncand 10345 . 2 (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
361357, 360breqtrd 4644 1 (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908  Vcvv 3189   ∖ cdif 3556   ⊆ wss 3559  {csn 4153   class class class wbr 4618   ↦ cmpt 4678  ran crn 5080   ↾ cres 5081   ∘ ccom 5083  ⟶wf 5848  –1-1-onto→wf1o 5851  ‘cfv 5852  (class class class)co 6610  ℂcc 9886  ℝcr 9887  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893  -∞cmnf 10024  ℝ*cxr 10025   < clt 10026   ≤ cle 10027   − cmin 10218   / cdiv 10636  ℕcn 10972  ℕ0cn0 11244  ℤcz 11329  ℤ≥cuz 11639  ℝ+crp 11784  (,]cioc 12126  ...cfz 12276  seqcseq 12749  abscabs 13916   ⇝ cli 14157  Σcsu 14358  ∞Metcxmt 19663  ballcbl 19665  –cn→ccncf 22602  logclog 24222  log Γclgam 24659 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967  ax-mulf 9968 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7861  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fsupp 8228  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-q 11741  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-ioo 12129  df-ioc 12130  df-ico 12131  df-icc 12132  df-fz 12277  df-fzo 12415  df-fl 12541  df-mod 12617  df-seq 12750  df-exp 12809  df-fac 13009  df-bc 13038  df-hash 13066  df-shft 13749  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-limsup 14144  df-clim 14161  df-rlim 14162  df-sum 14359  df-ef 14734  df-sin 14736  df-cos 14737  df-tan 14738  df-pi 14739  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-starv 15888  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-unif 15897  df-hom 15898  df-cco 15899  df-rest 16015  df-topn 16016  df-0g 16034  df-gsum 16035  df-topgen 16036  df-pt 16037  df-prds 16040  df-xrs 16094  df-qtop 16099  df-imas 16100  df-xps 16102  df-mre 16178  df-mrc 16179  df-acs 16181  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-submnd 17268  df-mulg 17473  df-cntz 17682  df-cmn 18127  df-psmet 19670  df-xmet 19671  df-met 19672  df-bl 19673  df-mopn 19674  df-fbas 19675  df-fg 19676  df-cnfld 19679  df-top 20631  df-topon 20648  df-topsp 20661  df-bases 20674  df-cld 20746  df-ntr 20747  df-cls 20748  df-nei 20825  df-lp 20863  df-perf 20864  df-cn 20954  df-cnp 20955  df-haus 21042  df-cmp 21113  df-tx 21288  df-hmeo 21481  df-fil 21573  df-fm 21665  df-flim 21666  df-flf 21667  df-xms 22048  df-ms 22049  df-tms 22050  df-cncf 22604  df-limc 23553  df-dv 23554  df-ulm 24052  df-log 24224  df-cxp 24225  df-lgam 24662 This theorem is referenced by:  lgamp1  24700
 Copyright terms: Public domain W3C validator