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

Theorem lgamcvg2 26420
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 12811 . . 3 β„• = (β„€β‰₯β€˜1)
2 1zzd 12539 . . 3 (πœ‘ β†’ 1 ∈ β„€)
3 eqid 2733 . . . 4 (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))) = (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1))))
4 lgamcvg.a . . . . 5 (πœ‘ β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
5 1nn0 12434 . . . . . 6 1 ∈ β„•0
65a1i 11 . . . . 5 (πœ‘ β†’ 1 ∈ β„•0)
74, 6dmgmaddnn0 26392 . . . 4 (πœ‘ β†’ (𝐴 + 1) ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
83, 7lgamcvg 26419 . . 3 (πœ‘ β†’ seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1))))) ⇝ ((log Ξ“β€˜(𝐴 + 1)) + (logβ€˜(𝐴 + 1))))
9 seqex 13914 . . . 4 seq1( + , 𝐺) ∈ V
109a1i 11 . . 3 (πœ‘ β†’ seq1( + , 𝐺) ∈ V)
114eldifad 3923 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ β„‚)
1211abscld 15327 . . . . . . 7 (πœ‘ β†’ (absβ€˜π΄) ∈ ℝ)
13 arch 12415 . . . . . . 7 ((absβ€˜π΄) ∈ ℝ β†’ βˆƒπ‘Ÿ ∈ β„• (absβ€˜π΄) < π‘Ÿ)
1412, 13syl 17 . . . . . 6 (πœ‘ β†’ βˆƒπ‘Ÿ ∈ β„• (absβ€˜π΄) < π‘Ÿ)
15 eqid 2733 . . . . . . . . 9 (β„€β‰₯β€˜π‘Ÿ) = (β„€β‰₯β€˜π‘Ÿ)
16 simprl 770 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ π‘Ÿ ∈ β„•)
1716nnzd 12531 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ π‘Ÿ ∈ β„€)
18 eqid 2733 . . . . . . . . . . 11 (β„‚ βˆ– (-∞(,]0)) = (β„‚ βˆ– (-∞(,]0))
1918logcn 26018 . . . . . . . . . 10 (log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∈ ((β„‚ βˆ– (-∞(,]0))–cnβ†’β„‚)
2019a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∈ ((β„‚ βˆ– (-∞(,]0))–cnβ†’β„‚))
21 eqid 2733 . . . . . . . . . . . 12 (1(ballβ€˜(abs ∘ βˆ’ ))1) = (1(ballβ€˜(abs ∘ βˆ’ ))1)
2221dvlog2lem 26023 . . . . . . . . . . 11 (1(ballβ€˜(abs ∘ βˆ’ ))1) βŠ† (β„‚ βˆ– (-∞(,]0))
2311ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 𝐴 ∈ β„‚)
24 eluznn 12848 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ β„• ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘š ∈ β„•)
2524ex 414 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ÿ ∈ β„• β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) β†’ π‘š ∈ β„•))
2625ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) β†’ π‘š ∈ β„•))
2726imp 408 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘š ∈ β„•)
2827nncnd 12174 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘š ∈ β„‚)
29 1cnd 11155 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 1 ∈ β„‚)
3028, 29addcld 11179 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ β„‚)
3127peano2nnd 12175 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ β„•)
3231nnne0d 12208 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) β‰  0)
3323, 30, 32divcld 11936 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (𝐴 / (π‘š + 1)) ∈ β„‚)
3433, 29addcld 11179 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ β„‚)
35 ax-1cn 11114 . . . . . . . . . . . . . . 15 1 ∈ β„‚
36 eqid 2733 . . . . . . . . . . . . . . . 16 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
3736cnmetdval 24150 . . . . . . . . . . . . . . 15 ((((𝐴 / (π‘š + 1)) + 1) ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) = (absβ€˜(((𝐴 / (π‘š + 1)) + 1) βˆ’ 1)))
3834, 35, 37sylancl 587 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) = (absβ€˜(((𝐴 / (π‘š + 1)) + 1) βˆ’ 1)))
3933, 29pncand 11518 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1) βˆ’ 1) = (𝐴 / (π‘š + 1)))
4039fveq2d 6847 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(((𝐴 / (π‘š + 1)) + 1) βˆ’ 1)) = (absβ€˜(𝐴 / (π‘š + 1))))
4123, 30, 32absdivd 15346 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(𝐴 / (π‘š + 1))) = ((absβ€˜π΄) / (absβ€˜(π‘š + 1))))
4231nnred 12173 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ ℝ)
4331nnrpd 12960 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ ℝ+)
4443rpge0d 12966 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 0 ≀ (π‘š + 1))
4542, 44absidd 15313 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(π‘š + 1)) = (π‘š + 1))
4645oveq2d 7374 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((absβ€˜π΄) / (absβ€˜(π‘š + 1))) = ((absβ€˜π΄) / (π‘š + 1)))
4741, 46eqtrd 2773 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(𝐴 / (π‘š + 1))) = ((absβ€˜π΄) / (π‘š + 1)))
4838, 40, 473eqtrd 2777 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) = ((absβ€˜π΄) / (π‘š + 1)))
4912ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) ∈ ℝ)
5016adantr 482 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ ∈ β„•)
5150nnred 12173 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ ∈ ℝ)
52 simplrr 777 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) < π‘Ÿ)
53 eluzle 12781 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) β†’ π‘Ÿ ≀ π‘š)
5453adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ ≀ π‘š)
55 nnleltp1 12563 . . . . . . . . . . . . . . . . . 18 ((π‘Ÿ ∈ β„• ∧ π‘š ∈ β„•) β†’ (π‘Ÿ ≀ π‘š ↔ π‘Ÿ < (π‘š + 1)))
5650, 27, 55syl2anc 585 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘Ÿ ≀ π‘š ↔ π‘Ÿ < (π‘š + 1)))
5754, 56mpbid 231 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ < (π‘š + 1))
5849, 51, 42, 52, 57lttrd 11321 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) < (π‘š + 1))
5930mulid1d 11177 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((π‘š + 1) Β· 1) = (π‘š + 1))
6058, 59breqtrrd 5134 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) < ((π‘š + 1) Β· 1))
61 1red 11161 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 1 ∈ ℝ)
6249, 61, 43ltdivmuld 13013 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((absβ€˜π΄) / (π‘š + 1)) < 1 ↔ (absβ€˜π΄) < ((π‘š + 1) Β· 1)))
6360, 62mpbird 257 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((absβ€˜π΄) / (π‘š + 1)) < 1)
6448, 63eqbrtrd 5128 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) < 1)
65 cnxmet 24152 . . . . . . . . . . . . . 14 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
6665a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
67 1rp 12924 . . . . . . . . . . . . . 14 1 ∈ ℝ+
68 rpxr 12929 . . . . . . . . . . . . . 14 (1 ∈ ℝ+ β†’ 1 ∈ ℝ*)
6967, 68mp1i 13 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 1 ∈ ℝ*)
70 elbl3 23761 . . . . . . . . . . . . 13 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 1 ∈ ℝ*) ∧ (1 ∈ β„‚ ∧ ((𝐴 / (π‘š + 1)) + 1) ∈ β„‚)) β†’ (((𝐴 / (π‘š + 1)) + 1) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1) ↔ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) < 1))
7166, 69, 29, 34, 70syl22anc 838 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1) ↔ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) < 1))
7264, 71mpbird 257 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1))
7322, 72sselid 3943 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ (β„‚ βˆ– (-∞(,]0)))
7473fmpttd 7064 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)):(β„€β‰₯β€˜π‘Ÿ)⟢(β„‚ βˆ– (-∞(,]0)))
7526ssrdv 3951 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (β„€β‰₯β€˜π‘Ÿ) βŠ† β„•)
7675resmptd 5995 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) = (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)))
77 nnex 12164 . . . . . . . . . . . . . . . . 17 β„• ∈ V
7877mptex 7174 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) ∈ V
7978a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) ∈ V)
80 oveq1 7365 . . . . . . . . . . . . . . . . . 18 (π‘š = 𝑛 β†’ (π‘š + 1) = (𝑛 + 1))
8180oveq2d 7374 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ (𝐴 / (π‘š + 1)) = (𝐴 / (𝑛 + 1)))
82 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) = (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))
83 ovex 7391 . . . . . . . . . . . . . . . . 17 (𝐴 / (𝑛 + 1)) ∈ V
8481, 82, 83fvmpt 6949 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) = (𝐴 / (𝑛 + 1)))
8584adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) = (𝐴 / (𝑛 + 1)))
861, 2, 11, 2, 79, 85divcnvshft 15745 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) ⇝ 0)
87 1cnd 11155 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 ∈ β„‚)
8877mptex 7174 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ∈ V
8988a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ∈ V)
9011adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ β„‚)
91 simpr 486 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
9291nncnd 12174 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„‚)
93 1cnd 11155 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 1 ∈ β„‚)
9492, 93addcld 11179 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) ∈ β„‚)
9591peano2nnd 12175 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) ∈ β„•)
9695nnne0d 12208 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) β‰  0)
9790, 94, 96divcld 11936 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐴 / (𝑛 + 1)) ∈ β„‚)
9885, 97eqeltrd 2834 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) ∈ β„‚)
9981oveq1d 7373 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ ((𝐴 / (π‘š + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100 eqid 2733 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) = (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))
101 ovex 7391 . . . . . . . . . . . . . . . . 17 ((𝐴 / (𝑛 + 1)) + 1) ∈ V
10299, 100, 101fvmpt 6949 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))β€˜π‘›) = ((𝐴 / (𝑛 + 1)) + 1))
103102adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))β€˜π‘›) = ((𝐴 / (𝑛 + 1)) + 1))
10485oveq1d 7373 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105103, 104eqtr4d 2776 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))β€˜π‘›) = (((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) + 1))
1061, 2, 86, 87, 89, 98, 105climaddc1 15523 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ (0 + 1))
107 0p1e1 12280 . . . . . . . . . . . . 13 (0 + 1) = 1
108106, 107breqtrdi 5147 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1)
109108adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1)
110 climres 15463 . . . . . . . . . . . 12 ((π‘Ÿ ∈ β„€ ∧ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ∈ V) β†’ (((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 1 ↔ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1))
11117, 88, 110sylancl 587 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 1 ↔ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1))
112109, 111mpbird 257 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 1)
11376, 112eqbrtrrd 5130 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1)
11467a1i 11 . . . . . . . . . . 11 (1 ∈ ℝ β†’ 1 ∈ ℝ+)
11518ellogdm 26010 . . . . . . . . . . 11 (1 ∈ (β„‚ βˆ– (-∞(,]0)) ↔ (1 ∈ β„‚ ∧ (1 ∈ ℝ β†’ 1 ∈ ℝ+)))
11635, 114, 115mpbir2an 710 . . . . . . . . . 10 1 ∈ (β„‚ βˆ– (-∞(,]0))
117116a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ 1 ∈ (β„‚ βˆ– (-∞(,]0)))
11815, 17, 20, 74, 113, 117climcncf 24279 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∘ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1))) ⇝ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1))
119 logf1o 25936 . . . . . . . . . . 11 log:(β„‚ βˆ– {0})–1-1-ontoβ†’ran log
120 f1of 6785 . . . . . . . . . . 11 (log:(β„‚ βˆ– {0})–1-1-ontoβ†’ran log β†’ log:(β„‚ βˆ– {0})⟢ran log)
121119, 120mp1i 13 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ log:(β„‚ βˆ– {0})⟢ran log)
12218logdmss 26013 . . . . . . . . . . 11 (β„‚ βˆ– (-∞(,]0)) βŠ† (β„‚ βˆ– {0})
123122, 73sselid 3943 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ (β„‚ βˆ– {0}))
124121, 123cofmpt 7079 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (log ∘ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1))) = (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))
125 frn 6676 . . . . . . . . . 10 ((π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)):(β„€β‰₯β€˜π‘Ÿ)⟢(β„‚ βˆ– (-∞(,]0)) β†’ ran (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)) βŠ† (β„‚ βˆ– (-∞(,]0)))
126 cores 6202 . . . . . . . . . 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 5995 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) = (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))
129124, 127, 1283eqtr4d 2783 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∘ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1))) = ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)))
130 fvres 6862 . . . . . . . . . 10 (1 ∈ (β„‚ βˆ– (-∞(,]0)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1) = (logβ€˜1))
131116, 130mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1) = (logβ€˜1))
132 log1 25957 . . . . . . . . 9 (logβ€˜1) = 0
133131, 132eqtrdi 2789 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1) = 0)
134118, 129, 1333brtr3d 5137 . . . . . . 7 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 0)
13577mptex 7174 . . . . . . . 8 (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ∈ V
136 climres 15463 . . . . . . . 8 ((π‘Ÿ ∈ β„€ ∧ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ∈ V) β†’ (((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 0 ↔ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ⇝ 0))
13717, 135, 136sylancl 587 . . . . . . 7 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 0 ↔ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ⇝ 0))
138134, 137mpbid 231 . . . . . 6 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ⇝ 0)
13914, 138rexlimddv 3155 . . . . 5 (πœ‘ β†’ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ⇝ 0)
14011, 87addcld 11179 . . . . . 6 (πœ‘ β†’ (𝐴 + 1) ∈ β„‚)
1417dmgmn0 26391 . . . . . 6 (πœ‘ β†’ (𝐴 + 1) β‰  0)
142140, 141logcld 25942 . . . . 5 (πœ‘ β†’ (logβ€˜(𝐴 + 1)) ∈ β„‚)
14377mptex 7174 . . . . . 6 (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ∈ V
144143a1i 11 . . . . 5 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ∈ V)
14581fvoveq1d 7380 . . . . . . . 8 (π‘š = 𝑛 β†’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
146 eqid 2733 . . . . . . . 8 (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) = (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))
147 fvex 6856 . . . . . . . 8 (logβ€˜((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148145, 146, 147fvmpt 6949 . . . . . . 7 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
149148adantl 483 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
15097, 93addcld 11179 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝐴 / (𝑛 + 1)) + 1) ∈ β„‚)
1514adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
152151, 95dmgmdivn0 26393 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝐴 / (𝑛 + 1)) + 1) β‰  0)
153150, 152logcld 25942 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1)) ∈ β„‚)
154149, 153eqeltrd 2834 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›) ∈ β„‚)
155145oveq2d 7374 . . . . . . . 8 (π‘š = 𝑛 β†’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
156 eqid 2733 . . . . . . . 8 (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) = (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))
157 ovex 7391 . . . . . . . 8 ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158155, 156, 157fvmpt 6949 . . . . . . 7 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
159158adantl 483 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
160149oveq2d 7374 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜(𝐴 + 1)) βˆ’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›)) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
161159, 160eqtr4d 2776 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) = ((logβ€˜(𝐴 + 1)) βˆ’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›)))
1621, 2, 139, 142, 144, 154, 161climsubc2 15527 . . . 4 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ⇝ ((logβ€˜(𝐴 + 1)) βˆ’ 0))
163142subid1d 11506 . . . 4 (πœ‘ β†’ ((logβ€˜(𝐴 + 1)) βˆ’ 0) = (logβ€˜(𝐴 + 1)))
164162, 163breqtrd 5132 . . 3 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ⇝ (logβ€˜(𝐴 + 1)))
165 elfznn 13476 . . . . . . 7 (π‘˜ ∈ (1...𝑛) β†’ π‘˜ ∈ β„•)
166165adantl 483 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ β„•)
167 oveq1 7365 . . . . . . . . . . 11 (π‘š = π‘˜ β†’ (π‘š + 1) = (π‘˜ + 1))
168 id 22 . . . . . . . . . . 11 (π‘š = π‘˜ β†’ π‘š = π‘˜)
169167, 168oveq12d 7376 . . . . . . . . . 10 (π‘š = π‘˜ β†’ ((π‘š + 1) / π‘š) = ((π‘˜ + 1) / π‘˜))
170169fveq2d 6847 . . . . . . . . 9 (π‘š = π‘˜ β†’ (logβ€˜((π‘š + 1) / π‘š)) = (logβ€˜((π‘˜ + 1) / π‘˜)))
171170oveq2d 7374 . . . . . . . 8 (π‘š = π‘˜ β†’ ((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) = ((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))))
172 oveq2 7366 . . . . . . . . 9 (π‘š = π‘˜ β†’ ((𝐴 + 1) / π‘š) = ((𝐴 + 1) / π‘˜))
173172fvoveq1d 7380 . . . . . . . 8 (π‘š = π‘˜ β†’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)) = (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))
174171, 173oveq12d 7376 . . . . . . 7 (π‘š = π‘˜ β†’ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1))) = (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))))
175 ovex 7391 . . . . . . 7 (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ V
176174, 3, 175fvmpt 6949 . . . . . 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 2844 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
17911ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 𝐴 ∈ β„‚)
180 1cnd 11155 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 1 ∈ β„‚)
181179, 180addcld 11179 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + 1) ∈ β„‚)
182166peano2nnd 12175 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ β„•)
183182nnrpd 12960 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ ℝ+)
184166nnrpd 12960 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ ℝ+)
185183, 184rpdivcld 12979 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((π‘˜ + 1) / π‘˜) ∈ ℝ+)
186185relogcld 25994 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((π‘˜ + 1) / π‘˜)) ∈ ℝ)
187186recnd 11188 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((π‘˜ + 1) / π‘˜)) ∈ β„‚)
188181, 187mulcld 11180 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) ∈ β„‚)
189166nncnd 12174 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ β„‚)
190166nnne0d 12208 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ β‰  0)
191181, 189, 190divcld 11936 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) / π‘˜) ∈ β„‚)
192191, 180addcld 11179 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + 1) ∈ β„‚)
1937ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + 1) ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
194193, 166dmgmdivn0 26393 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + 1) β‰  0)
195192, 194logcld 25942 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)) ∈ β„‚)
196188, 195subcld 11517 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ β„‚)
197177, 178, 196fsumser 15620 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) = (seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))))β€˜π‘›))
198 fzfid 13884 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1...𝑛) ∈ Fin)
199198, 196fsumcl 15623 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ β„‚)
200197, 199eqeltrrd 2835 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))))β€˜π‘›) ∈ β„‚)
201142adantr 482 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (logβ€˜(𝐴 + 1)) ∈ β„‚)
202201, 153subcld 11517 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) ∈ β„‚)
203159, 202eqeltrd 2834 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) ∈ β„‚)
204179, 187mulcld 11180 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) ∈ β„‚)
205179, 189, 190divcld 11936 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 / π‘˜) ∈ β„‚)
206205, 180addcld 11179 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / π‘˜) + 1) ∈ β„‚)
2074ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
208207, 166dmgmdivn0 26393 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / π‘˜) + 1) β‰  0)
209206, 208logcld 25942 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 / π‘˜) + 1)) ∈ β„‚)
210204, 209subcld 11517 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) ∈ β„‚)
211198, 210fsumcl 15623 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) ∈ β„‚)
212199, 211nncand 11522 . . . . 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 11566 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))))
214179, 180pncan2d 11519 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) βˆ’ 𝐴) = 1)
215214oveq1d 7373 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) βˆ’ 𝐴) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) = (1 Β· (logβ€˜((π‘˜ + 1) / π‘˜))))
216181, 179, 187subdird 11617 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) βˆ’ 𝐴) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) = (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))))
217187mulid2d 11178 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (1 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) = (logβ€˜((π‘˜ + 1) / π‘˜)))
218215, 216, 2173eqtr3d 2781 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))) = (logβ€˜((π‘˜ + 1) / π‘˜)))
219218oveq1d 7373 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))))
220187, 195, 209subsubd 11545 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = (((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) + (logβ€˜((𝐴 / π‘˜) + 1))))
221187, 195subcld 11517 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ β„‚)
222221, 209addcomd 11362 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) + (logβ€˜((𝐴 / π‘˜) + 1))) = ((logβ€˜((𝐴 / π‘˜) + 1)) + ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))))
223209, 195, 187subsub2d 11546 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) + ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))))
224182nncnd 12174 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ β„‚)
225179, 224addcld 11179 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + (π‘˜ + 1)) ∈ β„‚)
226182nnnn0d 12478 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ β„•0)
227 dmgmaddn0 26388 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)) ∧ (π‘˜ + 1) ∈ β„•0) β†’ (𝐴 + (π‘˜ + 1)) β‰  0)
228207, 226, 227syl2anc 585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + (π‘˜ + 1)) β‰  0)
229225, 228logcld 25942 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(𝐴 + (π‘˜ + 1))) ∈ β„‚)
230183relogcld 25994 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(π‘˜ + 1)) ∈ ℝ)
231230recnd 11188 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(π‘˜ + 1)) ∈ β„‚)
232184relogcld 25994 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜π‘˜) ∈ ℝ)
233232recnd 11188 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜π‘˜) ∈ β„‚)
234229, 231, 233nnncan2d 11552 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)) βˆ’ ((logβ€˜(π‘˜ + 1)) βˆ’ (logβ€˜π‘˜))) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
235181, 189, 189, 190divdird 11974 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) + π‘˜) / π‘˜) = (((𝐴 + 1) / π‘˜) + (π‘˜ / π‘˜)))
236179, 189, 180add32d 11387 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + π‘˜) + 1) = ((𝐴 + 1) + π‘˜))
237179, 189, 180addassd 11182 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + π‘˜) + 1) = (𝐴 + (π‘˜ + 1)))
238236, 237eqtr3d 2775 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) + π‘˜) = (𝐴 + (π‘˜ + 1)))
239238oveq1d 7373 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) + π‘˜) / π‘˜) = ((𝐴 + (π‘˜ + 1)) / π‘˜))
240189, 190dividd 11934 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ / π‘˜) = 1)
241240oveq2d 7374 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + (π‘˜ / π‘˜)) = (((𝐴 + 1) / π‘˜) + 1))
242235, 239, 2413eqtr3rd 2782 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + 1) = ((𝐴 + (π‘˜ + 1)) / π‘˜))
243242fveq2d 6847 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)) = (logβ€˜((𝐴 + (π‘˜ + 1)) / π‘˜)))
244 logdiv2 25988 . . . . . . . . . . . . . . . 16 (((𝐴 + (π‘˜ + 1)) ∈ β„‚ ∧ (𝐴 + (π‘˜ + 1)) β‰  0 ∧ π‘˜ ∈ ℝ+) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / π‘˜)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)))
245225, 228, 184, 244syl3anc 1372 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / π‘˜)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)))
246243, 245eqtrd 2773 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)))
247183, 184relogdivd 25997 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((π‘˜ + 1) / π‘˜)) = ((logβ€˜(π‘˜ + 1)) βˆ’ (logβ€˜π‘˜)))
248246, 247oveq12d 7376 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜))) = (((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)) βˆ’ ((logβ€˜(π‘˜ + 1)) βˆ’ (logβ€˜π‘˜))))
249182nnne0d 12208 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) β‰  0)
250179, 224, 224, 249divdird 11974 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1)) = ((𝐴 / (π‘˜ + 1)) + ((π‘˜ + 1) / (π‘˜ + 1))))
251224, 249dividd 11934 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((π‘˜ + 1) / (π‘˜ + 1)) = 1)
252251oveq2d 7374 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / (π‘˜ + 1)) + ((π‘˜ + 1) / (π‘˜ + 1))) = ((𝐴 / (π‘˜ + 1)) + 1))
253250, 252eqtr2d 2774 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / (π‘˜ + 1)) + 1) = ((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1)))
254253fveq2d 6847 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)) = (logβ€˜((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1))))
255 logdiv2 25988 . . . . . . . . . . . . . . 15 (((𝐴 + (π‘˜ + 1)) ∈ β„‚ ∧ (𝐴 + (π‘˜ + 1)) β‰  0 ∧ (π‘˜ + 1) ∈ ℝ+) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1))) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
256225, 228, 183, 255syl3anc 1372 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1))) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
257254, 256eqtrd 2773 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
258234, 248, 2573eqtr4d 2783 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜))) = (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)))
259258oveq2d 7374 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
260223, 259eqtr3d 2775 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((𝐴 / π‘˜) + 1)) + ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
261220, 222, 2603eqtrd 2777 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
262213, 219, 2613eqtrd 2777 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
263262sumeq2dv 15593 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = Ξ£π‘˜ ∈ (1...𝑛)((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
264198, 196, 210fsumsub 15678 . . . . . . 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 7366 . . . . . . . . . 10 (π‘₯ = π‘˜ β†’ (𝐴 / π‘₯) = (𝐴 / π‘˜))
266265fvoveq1d 7380 . . . . . . . . 9 (π‘₯ = π‘˜ β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / π‘˜) + 1)))
267 oveq2 7366 . . . . . . . . . 10 (π‘₯ = (π‘˜ + 1) β†’ (𝐴 / π‘₯) = (𝐴 / (π‘˜ + 1)))
268267fvoveq1d 7380 . . . . . . . . 9 (π‘₯ = (π‘˜ + 1) β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)))
269 oveq2 7366 . . . . . . . . . 10 (π‘₯ = 1 β†’ (𝐴 / π‘₯) = (𝐴 / 1))
270269fvoveq1d 7380 . . . . . . . . 9 (π‘₯ = 1 β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / 1) + 1)))
271 oveq2 7366 . . . . . . . . . 10 (π‘₯ = (𝑛 + 1) β†’ (𝐴 / π‘₯) = (𝐴 / (𝑛 + 1)))
272271fvoveq1d 7380 . . . . . . . . 9 (π‘₯ = (𝑛 + 1) β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
27391nnzd 12531 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„€)
27495, 1eleqtrdi 2844 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) ∈ (β„€β‰₯β€˜1))
27511ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ 𝐴 ∈ β„‚)
276 elfznn 13476 . . . . . . . . . . . . . 14 (π‘₯ ∈ (1...(𝑛 + 1)) β†’ π‘₯ ∈ β„•)
277276adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ π‘₯ ∈ β„•)
278277nncnd 12174 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ π‘₯ ∈ β„‚)
279277nnne0d 12208 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ π‘₯ β‰  0)
280275, 278, 279divcld 11936 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ (𝐴 / π‘₯) ∈ β„‚)
281 1cnd 11155 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ 1 ∈ β„‚)
282280, 281addcld 11179 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ ((𝐴 / π‘₯) + 1) ∈ β„‚)
2834ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
284283, 277dmgmdivn0 26393 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ ((𝐴 / π‘₯) + 1) β‰  0)
285282, 284logcld 25942 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ (logβ€˜((𝐴 / π‘₯) + 1)) ∈ β„‚)
286266, 268, 270, 272, 273, 274, 285telfsum 15694 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))) = ((logβ€˜((𝐴 / 1) + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
28790div1d 11928 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐴 / 1) = 𝐴)
288287fvoveq1d 7380 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (logβ€˜((𝐴 / 1) + 1)) = (logβ€˜(𝐴 + 1)))
289288oveq1d 7373 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜((𝐴 / 1) + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
290286, 289eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
291263, 264, 2903eqtr3d 2781 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
292291oveq2d 7374 . . . . 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 2775 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) = (Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))))
294170oveq2d 7374 . . . . . . . 8 (π‘š = π‘˜ β†’ (𝐴 Β· (logβ€˜((π‘š + 1) / π‘š))) = (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))))
295 oveq2 7366 . . . . . . . . 9 (π‘š = π‘˜ β†’ (𝐴 / π‘š) = (𝐴 / π‘˜))
296295fvoveq1d 7380 . . . . . . . 8 (π‘š = π‘˜ β†’ (logβ€˜((𝐴 / π‘š) + 1)) = (logβ€˜((𝐴 / π‘˜) + 1)))
297294, 296oveq12d 7376 . . . . . . 7 (π‘š = π‘˜ β†’ ((𝐴 Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜((𝐴 / π‘š) + 1))) = ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))))
298 lgamcvg.g . . . . . . 7 𝐺 = (π‘š ∈ β„• ↦ ((𝐴 Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜((𝐴 / π‘š) + 1))))
299 ovex 7391 . . . . . . 7 ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) ∈ V
300297, 298, 299fvmpt 6949 . . . . . 6 (π‘˜ ∈ β„• β†’ (πΊβ€˜π‘˜) = ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))))
301166, 300syl 17 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (πΊβ€˜π‘˜) = ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))))
302301, 178, 210fsumser 15620 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) = (seq1( + , 𝐺)β€˜π‘›))
303159eqcomd 2739 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) = ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›))
304197, 303oveq12d 7376 . . . 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 2781 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (seq1( + , 𝐺)β€˜π‘›) = ((seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))))β€˜π‘›) βˆ’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›)))
3061, 2, 8, 10, 164, 200, 203, 305climsub 15522 . 2 (πœ‘ β†’ seq1( + , 𝐺) ⇝ (((log Ξ“β€˜(𝐴 + 1)) + (logβ€˜(𝐴 + 1))) βˆ’ (logβ€˜(𝐴 + 1))))
307 lgamcl 26406 . . . 4 ((𝐴 + 1) ∈ (β„‚ βˆ– (β„€ βˆ– β„•)) β†’ (log Ξ“β€˜(𝐴 + 1)) ∈ β„‚)
3087, 307syl 17 . . 3 (πœ‘ β†’ (log Ξ“β€˜(𝐴 + 1)) ∈ β„‚)
309308, 142pncand 11518 . 2 (πœ‘ β†’ (((log Ξ“β€˜(𝐴 + 1)) + (logβ€˜(𝐴 + 1))) βˆ’ (logβ€˜(𝐴 + 1))) = (log Ξ“β€˜(𝐴 + 1)))
310306, 309breqtrd 5132 1 (πœ‘ β†’ seq1( + , 𝐺) ⇝ (log Ξ“β€˜(𝐴 + 1)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆƒwrex 3070  Vcvv 3444   βˆ– cdif 3908   βŠ† wss 3911  {csn 4587   class class class wbr 5106   ↦ cmpt 5189  ran crn 5635   β†Ύ cres 5636   ∘ ccom 5638  βŸΆwf 6493  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  (class class class)co 7358  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061  -∞cmnf 11192  β„*cxr 11193   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390   / cdiv 11817  β„•cn 12158  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„+crp 12920  (,]cioc 13271  ...cfz 13430  seqcseq 13912  abscabs 15125   ⇝ cli 15372  Ξ£csu 15576  βˆžMetcxmet 20797  ballcbl 20799  β€“cnβ†’ccncf 24255  logclog 25926  log Ξ“clgam 26381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-sin 15957  df-cos 15958  df-tan 15959  df-pi 15960  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-ulm 25752  df-log 25928  df-cxp 25929  df-lgam 26384
This theorem is referenced by:  lgamp1  26422
  Copyright terms: Public domain W3C validator