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

Theorem lgamcvg2 25002
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 11925 . . 3 ℕ = (ℤ‘1)
2 1zzd 11610 . . 3 (𝜑 → 1 ∈ ℤ)
3 eqid 2771 . . . 4 (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))
4 lgamcvg.a . . . . 5 (𝜑𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
5 1nn0 11510 . . . . . 6 1 ∈ ℕ0
65a1i 11 . . . . 5 (𝜑 → 1 ∈ ℕ0)
74, 6dmgmaddnn0 24974 . . . 4 (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
83, 7lgamcvg 25001 . . 3 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9 seqex 13010 . . . 4 seq1( + , 𝐺) ∈ V
109a1i 11 . . 3 (𝜑 → seq1( + , 𝐺) ∈ V)
114eldifad 3735 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1211abscld 14383 . . . . . . 7 (𝜑 → (abs‘𝐴) ∈ ℝ)
13 arch 11491 . . . . . . 7 ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
1412, 13syl 17 . . . . . 6 (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15 eqid 2771 . . . . . . . . 9 (ℤ𝑟) = (ℤ𝑟)
16 simprl 746 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
1716nnzd 11683 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18 eqid 2771 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
1918logcn 24614 . . . . . . . . . 10 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
2019a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21 eqid 2771 . . . . . . . . . . . 12 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
2221dvlog2lem 24619 . . . . . . . . . . 11 (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
2311ad2antrr 697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝐴 ∈ ℂ)
24 eluznn 11961 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2524ex 397 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2625ad2antrl 699 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) → 𝑚 ∈ ℕ))
2726imp 393 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℕ)
2827nncnd 11238 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑚 ∈ ℂ)
29 1cnd 10258 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℂ)
3028, 29addcld 10261 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℂ)
3127peano2nnd 11239 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℕ)
3231nnne0d 11267 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ≠ 0)
3323, 30, 32divcld 11003 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
3433, 29addcld 10261 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35 ax-1cn 10196 . . . . . . . . . . . . . . 15 1 ∈ ℂ
36 eqid 2771 . . . . . . . . . . . . . . . 16 (abs ∘ − ) = (abs ∘ − )
3736cnmetdval 22794 . . . . . . . . . . . . . . 15 ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3834, 35, 37sylancl 566 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
3933, 29pncand 10595 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
4039fveq2d 6336 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
4123, 30, 32absdivd 14402 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
4231nnred 11237 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ)
4331nnrpd 12073 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑚 + 1) ∈ ℝ+)
4443rpge0d 12079 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 0 ≤ (𝑚 + 1))
4542, 44absidd 14369 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
4645oveq2d 6809 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4741, 46eqtrd 2805 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
4838, 40, 473eqtrd 2809 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
4912ad2antrr 697 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) ∈ ℝ)
5016adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℕ)
5150nnred 11237 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 ∈ ℝ)
52 simplrr 755 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < 𝑟)
53 eluzle 11901 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ𝑟) → 𝑟𝑚)
5453adantl 467 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟𝑚)
55 nnleltp1 11634 . . . . . . . . . . . . . . . . . 18 ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5650, 27, 55syl2anc 565 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (𝑟𝑚𝑟 < (𝑚 + 1)))
5754, 56mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 𝑟 < (𝑚 + 1))
5849, 51, 42, 52, 57lttrd 10400 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < (𝑚 + 1))
5930mulid1d 10259 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
6058, 59breqtrrd 4814 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61 1red 10257 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ)
6249, 61, 43ltdivmuld 12126 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
6360, 62mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
6448, 63eqbrtrd 4808 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65 cnxmet 22796 . . . . . . . . . . . . . 14 (abs ∘ − ) ∈ (∞Met‘ℂ)
6665a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
67 1rp 12039 . . . . . . . . . . . . . 14 1 ∈ ℝ+
68 rpxr 12043 . . . . . . . . . . . . . 14 (1 ∈ ℝ+ → 1 ∈ ℝ*)
6967, 68mp1i 13 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → 1 ∈ ℝ*)
70 elbl3 22417 . . . . . . . . . . . . 13 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
7166, 69, 29, 34, 70syl22anc 1477 . . . . . . . . . . . 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 3750 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
74 eqid 2771 . . . . . . . . . 10 (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))
7573, 74fmptd 6527 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)))
7626ssrdv 3758 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ𝑟) ⊆ ℕ)
7776resmptd 5593 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
7812recnd 10270 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝐴) ∈ ℂ)
79 divcnv 14792 . . . . . . . . . . . . . . . . 17 ((abs‘𝐴) ∈ ℂ → (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0)
8078, 79syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0)
81 nnex 11228 . . . . . . . . . . . . . . . . . 18 ℕ ∈ V
8281mptex 6630 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ∈ V
8382a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ∈ V)
84 oveq2 6801 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((abs‘𝐴) / 𝑚) = ((abs‘𝐴) / 𝑛))
85 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) = (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))
86 ovex 6823 . . . . . . . . . . . . . . . . . . 19 ((abs‘𝐴) / 𝑛) ∈ V
8784, 85, 86fvmpt 6424 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛))
8887adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛))
8911adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
9089abscld 14383 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (abs‘𝐴) ∈ ℝ)
91 simpr 471 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9290, 91nndivred 11271 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((abs‘𝐴) / 𝑛) ∈ ℝ)
9388, 92eqeltrd 2850 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) ∈ ℝ)
94 oveq1 6800 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
9594oveq2d 6809 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
9695fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (abs‘(𝐴 / (𝑚 + 1))) = (abs‘(𝐴 / (𝑛 + 1))))
97 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) = (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))
98 fvex 6342 . . . . . . . . . . . . . . . . . . 19 (abs‘(𝐴 / (𝑛 + 1))) ∈ V
9996, 97, 98fvmpt 6424 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1))))
10099adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1))))
10191nncnd 11238 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
102 1cnd 10258 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 1 ∈ ℂ)
103101, 102addcld 10261 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
10491peano2nnd 11239 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
105104nnne0d 11267 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
10689, 103, 105divcld 11003 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
107106abscld 14383 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ∈ ℝ)
108100, 107eqeltrd 2850 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ∈ ℝ)
10989, 103, 105absdivd 14402 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (abs‘(𝑛 + 1))))
110104nnred 11237 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ)
111104nnrpd 12073 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ+)
112111rpge0d 12079 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝑛 + 1))
113110, 112absidd 14369 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝑛 + 1)) = (𝑛 + 1))
114113oveq2d 6809 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ((abs‘𝐴) / (abs‘(𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1)))
115109, 114eqtrd 2805 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1)))
11691nnrpd 12073 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+)
11789absge0d 14391 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (abs‘𝐴))
11891nnred 11237 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
119118lep1d 11157 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1))
120116, 111, 90, 117, 119lediv2ad 12097 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ((abs‘𝐴) / (𝑛 + 1)) ≤ ((abs‘𝐴) / 𝑛))
121115, 120eqbrtrd 4808 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ≤ ((abs‘𝐴) / 𝑛))
122121, 100, 883brtr4d 4818 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ≤ ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛))
123106absge0d 14391 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (abs‘(𝐴 / (𝑛 + 1))))
124123, 100breqtrrd 4814 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛))
1251, 2, 80, 83, 93, 108, 122, 124climsqz2 14580 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0)
12681mptex 6630 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
127126a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
128 eqid 2771 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
129 ovex 6823 . . . . . . . . . . . . . . . . . . 19 (𝐴 / (𝑛 + 1)) ∈ V
13095, 128, 129fvmpt 6424 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
131130adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
132131, 106eqeltrd 2850 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
133131fveq2d 6336 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛)) = (abs‘(𝐴 / (𝑛 + 1))))
134100, 133eqtr4d 2808 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛)))
1351, 2, 127, 83, 132, 134climabs0 14524 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0))
136125, 135mpbird 247 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
137 1cnd 10258 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℂ)
13881mptex 6630 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
139138a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
14095oveq1d 6808 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
141 eqid 2771 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
142 ovex 6823 . . . . . . . . . . . . . . . . 17 ((𝐴 / (𝑛 + 1)) + 1) ∈ V
143140, 141, 142fvmpt 6424 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
144143adantl 467 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
145131oveq1d 6808 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
146144, 145eqtr4d 2808 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
1471, 2, 136, 137, 139, 132, 146climaddc1 14573 . . . . . . . . . . . . 13 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
148 0p1e1 11334 . . . . . . . . . . . . 13 (0 + 1) = 1
149147, 148syl6breq 4827 . . . . . . . . . . . 12 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
150149adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
151 climres 14514 . . . . . . . . . . . 12 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
15217, 138, 151sylancl 566 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
153150, 152mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ𝑟)) ⇝ 1)
15477, 153eqbrtrrd 4810 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
15567a1i 11 . . . . . . . . . . 11 (1 ∈ ℝ → 1 ∈ ℝ+)
15618ellogdm 24606 . . . . . . . . . . 11 (1 ∈ (ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈ ℝ → 1 ∈ ℝ+)))
15735, 155, 156mpbir2an 682 . . . . . . . . . 10 1 ∈ (ℂ ∖ (-∞(,]0))
158157a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖ (-∞(,]0)))
15915, 17, 20, 75, 154, 158climcncf 22923 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
16018logdmss 24609 . . . . . . . . . . 11 (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
161160, 73sseldi 3750 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
162 eqidd 2772 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
163 logf1o 24532 . . . . . . . . . . . 12 log:(ℂ ∖ {0})–1-1-onto→ran log
164 f1of 6278 . . . . . . . . . . . 12 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
165163, 164mp1i 13 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖ {0})⟶ran log)
166165feqmptd 6391 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log = (𝑥 ∈ (ℂ ∖ {0}) ↦ (log‘𝑥)))
167 fveq2 6332 . . . . . . . . . 10 (𝑥 = ((𝐴 / (𝑚 + 1)) + 1) → (log‘𝑥) = (log‘((𝐴 / (𝑚 + 1)) + 1)))
168161, 162, 166, 167fmptco 6539 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
169 frn 6193 . . . . . . . . . 10 ((𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
170 cores 5782 . . . . . . . . . 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 5593 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) = (𝑚 ∈ (ℤ𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
173168, 171, 1723eqtr4d 2815 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)))
174 fvres 6348 . . . . . . . . . 10 (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
175157, 174mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
176 log1 24553 . . . . . . . . 9 (log‘1) = 0
177175, 176syl6eq 2821 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
178159, 173, 1773brtr3d 4817 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0)
17981mptex 6630 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
180 climres 14514 . . . . . . . 8 ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
18117, 179, 180sylancl 566 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
182178, 181mpbid 222 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
18314, 182rexlimddv 3183 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
18411, 137addcld 10261 . . . . . 6 (𝜑 → (𝐴 + 1) ∈ ℂ)
1857dmgmn0 24973 . . . . . 6 (𝜑 → (𝐴 + 1) ≠ 0)
186184, 185logcld 24538 . . . . 5 (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
18781mptex 6630 . . . . . 6 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
188187a1i 11 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
18995fvoveq1d 6815 . . . . . . . 8 (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
190 eqid 2771 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
191 fvex 6342 . . . . . . . 8 (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
192189, 190, 191fvmpt 6424 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
193192adantl 467 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
194106, 102addcld 10261 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
1954adantr 466 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
196195, 104dmgmdivn0 24975 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
197194, 196logcld 24538 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
198193, 197eqeltrd 2850 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
199189oveq2d 6809 . . . . . . . 8 (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
200 eqid 2771 . . . . . . . 8 (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
201 ovex 6823 . . . . . . . 8 ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
202199, 200, 201fvmpt 6424 . . . . . . 7 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
203202adantl 467 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
204193oveq2d 6809 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
205203, 204eqtr4d 2808 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
2061, 2, 183, 186, 188, 198, 205climsubc2 14577 . . . 4 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
207186subid1d 10583 . . . 4 (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
208206, 207breqtrd 4812 . . 3 (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
209 elfznn 12577 . . . . . . 7 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
210209adantl 467 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
211 oveq1 6800 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
212 id 22 . . . . . . . . . . 11 (𝑚 = 𝑘𝑚 = 𝑘)
213211, 212oveq12d 6811 . . . . . . . . . 10 (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
214213fveq2d 6336 . . . . . . . . 9 (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
215214oveq2d 6809 . . . . . . . 8 (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
216 oveq2 6801 . . . . . . . . 9 (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
217216fvoveq1d 6815 . . . . . . . 8 (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
218215, 217oveq12d 6811 . . . . . . 7 (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
219 ovex 6823 . . . . . . 7 (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
220218, 3, 219fvmpt 6424 . . . . . 6 (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
221210, 220syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
22291, 1syl6eleq 2860 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
22311ad2antrr 697 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
224 1cnd 10258 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
225223, 224addcld 10261 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
226210peano2nnd 11239 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
227226nnrpd 12073 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ+)
228210nnrpd 12073 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+)
229227, 228rpdivcld 12092 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ+)
230229relogcld 24590 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
231230recnd 10270 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
232225, 231mulcld 10262 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
233210nncnd 11238 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
234210nnne0d 11267 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
235225, 233, 234divcld 11003 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
236235, 224addcld 10261 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
2377ad2antrr 697 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
238237, 210dmgmdivn0 24975 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
239236, 238logcld 24538 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
240232, 239subcld 10594 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
241221, 222, 240fsumser 14669 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
242 fzfid 12980 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
243242, 240fsumcl 14672 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
244241, 243eqeltrrd 2851 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
245186adantr 466 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
246245, 197subcld 10594 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
247203, 246eqeltrd 2850 . . 3 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
248223, 231mulcld 10262 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
249223, 233, 234divcld 11003 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
250249, 224addcld 10261 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
2514ad2antrr 697 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
252251, 210dmgmdivn0 24975 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
253250, 252logcld 24538 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
254248, 253subcld 10594 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
255242, 254fsumcl 14672 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
256243, 255nncand 10599 . . . . 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))))
257232, 239, 248, 253sub4d 10643 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
258223, 224pncan2d 10596 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
259258oveq1d 6808 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
260225, 223, 231subdird 10689 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
261231mulid2d 10260 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
262259, 260, 2613eqtr3d 2813 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
263262oveq1d 6808 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
264231, 239, 253subsubd 10622 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
265231, 239subcld 10594 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
266265, 253addcomd 10440 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
267253, 239, 231subsub2d 10623 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
268226nncnd 11238 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
269223, 268addcld 10261 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
270226nnnn0d 11553 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ0)
271 dmgmaddn0 24970 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ0) → (𝐴 + (𝑘 + 1)) ≠ 0)
272251, 270, 271syl2anc 565 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
273269, 272logcld 24538 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
274227relogcld 24590 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
275274recnd 10270 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
276228relogcld 24590 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
277276recnd 10270 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
278273, 275, 277nnncan2d 10629 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
279225, 233, 233, 234divdird 11041 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
280223, 233, 224add32d 10465 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
281223, 233, 224addassd 10264 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
282280, 281eqtr3d 2807 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
283282oveq1d 6808 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
284233, 234dividd 11001 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
285284oveq2d 6809 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
286279, 283, 2853eqtr3rd 2814 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
287286fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
288 logdiv2 24584 . . . . . . . . . . . . . . . 16 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
289269, 272, 228, 288syl3anc 1476 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
290287, 289eqtrd 2805 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
291227, 228relogdivd 24593 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
292290, 291oveq12d 6811 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
293226nnne0d 11267 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
294223, 268, 268, 293divdird 11041 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
295268, 293dividd 11001 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
296295oveq2d 6809 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
297294, 296eqtr2d 2806 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
298297fveq2d 6336 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
299 logdiv2 24584 . . . . . . . . . . . . . . 15 (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ+) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
300269, 272, 227, 299syl3anc 1476 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
301298, 300eqtrd 2805 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
302278, 292, 3013eqtr4d 2815 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
303302oveq2d 6809 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
304267, 303eqtr3d 2807 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
305264, 266, 3043eqtrd 2809 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
306257, 263, 3053eqtrd 2809 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
307306sumeq2dv 14641 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
308242, 240, 254fsumsub 14727 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))))
309 oveq2 6801 . . . . . . . . . 10 (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
310309fvoveq1d 6815 . . . . . . . . 9 (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
311 oveq2 6801 . . . . . . . . . 10 (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
312311fvoveq1d 6815 . . . . . . . . 9 (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
313 oveq2 6801 . . . . . . . . . 10 (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
314313fvoveq1d 6815 . . . . . . . . 9 (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
315 oveq2 6801 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
316315fvoveq1d 6815 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
31791nnzd 11683 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
318104, 1syl6eleq 2860 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ‘1))
31911ad2antrr 697 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
320 elfznn 12577 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
321320adantl 467 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
322321nncnd 11238 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
323321nnne0d 11267 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
324319, 322, 323divcld 11003 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
325 1cnd 10258 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
326324, 325addcld 10261 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
3274ad2antrr 697 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
328327, 321dmgmdivn0 24975 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
329326, 328logcld 24538 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
330310, 312, 314, 316, 317, 318, 329telfsum 14743 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
33189div1d 10995 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
332331fvoveq1d 6815 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
333332oveq1d 6808 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
334330, 333eqtrd 2805 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
335307, 308, 3343eqtr3d 2813 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
336335oveq2d 6809 . . . . 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)))))
337256, 336eqtr3d 2807 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
338214oveq2d 6809 . . . . . . . 8 (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
339 oveq2 6801 . . . . . . . . 9 (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
340339fvoveq1d 6815 . . . . . . . 8 (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
341338, 340oveq12d 6811 . . . . . . 7 (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
342 lgamcvg.g . . . . . . 7 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
343 ovex 6823 . . . . . . 7 ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
344341, 342, 343fvmpt 6424 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
345210, 344syl 17 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
346345, 222, 254fsumser 14669 . . . 4 ((𝜑𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
347203eqcomd 2777 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
348241, 347oveq12d 6811 . . . 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))))‘𝑛)))
349337, 346, 3483eqtr3d 2813 . . 3 ((𝜑𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
3501, 2, 8, 10, 208, 244, 247, 349climsub 14572 . 2 (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
351 lgamcl 24988 . . . 4 ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
3527, 351syl 17 . . 3 (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
353352, 186pncand 10595 . 2 (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
354350, 353breqtrd 4812 1 (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  wrex 3062  Vcvv 3351  cdif 3720  wss 3723  {csn 4316   class class class wbr 4786  cmpt 4863  ran crn 5250  cres 5251  ccom 5253  wf 6027  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  -∞cmnf 10274  *cxr 10275   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  cn 11222  0cn0 11494  cz 11579  cuz 11888  +crp 12035  (,]cioc 12381  ...cfz 12533  seqcseq 13008  abscabs 14182  cli 14423  Σcsu 14624  ∞Metcxmt 19946  ballcbl 19948  cnccncf 22899  logclog 24522  log Γclgam 24963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14015  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428  df-sum 14625  df-ef 15004  df-sin 15006  df-cos 15007  df-tan 15008  df-pi 15009  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17957  df-cmn 18402  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-cmp 21411  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-xms 22345  df-ms 22346  df-tms 22347  df-cncf 22901  df-limc 23850  df-dv 23851  df-ulm 24351  df-log 24524  df-cxp 24525  df-lgam 24966
This theorem is referenced by:  lgamp1  25004
  Copyright terms: Public domain W3C validator