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

Theorem lgamcvg2 26942
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 12869 . . 3 β„• = (β„€β‰₯β€˜1)
2 1zzd 12597 . . 3 (πœ‘ β†’ 1 ∈ β„€)
3 eqid 2726 . . . 4 (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))) = (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1))))
4 lgamcvg.a . . . . 5 (πœ‘ β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
5 1nn0 12492 . . . . . 6 1 ∈ β„•0
65a1i 11 . . . . 5 (πœ‘ β†’ 1 ∈ β„•0)
74, 6dmgmaddnn0 26914 . . . 4 (πœ‘ β†’ (𝐴 + 1) ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
83, 7lgamcvg 26941 . . 3 (πœ‘ β†’ seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1))))) ⇝ ((log Ξ“β€˜(𝐴 + 1)) + (logβ€˜(𝐴 + 1))))
9 seqex 13974 . . . 4 seq1( + , 𝐺) ∈ V
109a1i 11 . . 3 (πœ‘ β†’ seq1( + , 𝐺) ∈ V)
114eldifad 3955 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ β„‚)
1211abscld 15389 . . . . . . 7 (πœ‘ β†’ (absβ€˜π΄) ∈ ℝ)
13 arch 12473 . . . . . . 7 ((absβ€˜π΄) ∈ ℝ β†’ βˆƒπ‘Ÿ ∈ β„• (absβ€˜π΄) < π‘Ÿ)
1412, 13syl 17 . . . . . 6 (πœ‘ β†’ βˆƒπ‘Ÿ ∈ β„• (absβ€˜π΄) < π‘Ÿ)
15 eqid 2726 . . . . . . . . 9 (β„€β‰₯β€˜π‘Ÿ) = (β„€β‰₯β€˜π‘Ÿ)
16 simprl 768 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ π‘Ÿ ∈ β„•)
1716nnzd 12589 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ π‘Ÿ ∈ β„€)
18 eqid 2726 . . . . . . . . . . 11 (β„‚ βˆ– (-∞(,]0)) = (β„‚ βˆ– (-∞(,]0))
1918logcn 26536 . . . . . . . . . 10 (log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∈ ((β„‚ βˆ– (-∞(,]0))–cnβ†’β„‚)
2019a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∈ ((β„‚ βˆ– (-∞(,]0))–cnβ†’β„‚))
21 eqid 2726 . . . . . . . . . . . 12 (1(ballβ€˜(abs ∘ βˆ’ ))1) = (1(ballβ€˜(abs ∘ βˆ’ ))1)
2221dvlog2lem 26541 . . . . . . . . . . 11 (1(ballβ€˜(abs ∘ βˆ’ ))1) βŠ† (β„‚ βˆ– (-∞(,]0))
2311ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 𝐴 ∈ β„‚)
24 eluznn 12906 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ β„• ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘š ∈ β„•)
2524ex 412 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ÿ ∈ β„• β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) β†’ π‘š ∈ β„•))
2625ad2antrl 725 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) β†’ π‘š ∈ β„•))
2726imp 406 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘š ∈ β„•)
2827nncnd 12232 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘š ∈ β„‚)
29 1cnd 11213 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 1 ∈ β„‚)
3028, 29addcld 11237 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ β„‚)
3127peano2nnd 12233 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ β„•)
3231nnne0d 12266 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) β‰  0)
3323, 30, 32divcld 11994 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (𝐴 / (π‘š + 1)) ∈ β„‚)
3433, 29addcld 11237 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ β„‚)
35 ax-1cn 11170 . . . . . . . . . . . . . . 15 1 ∈ β„‚
36 eqid 2726 . . . . . . . . . . . . . . . 16 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
3736cnmetdval 24642 . . . . . . . . . . . . . . 15 ((((𝐴 / (π‘š + 1)) + 1) ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) = (absβ€˜(((𝐴 / (π‘š + 1)) + 1) βˆ’ 1)))
3834, 35, 37sylancl 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) = (absβ€˜(((𝐴 / (π‘š + 1)) + 1) βˆ’ 1)))
3933, 29pncand 11576 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1) βˆ’ 1) = (𝐴 / (π‘š + 1)))
4039fveq2d 6889 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(((𝐴 / (π‘š + 1)) + 1) βˆ’ 1)) = (absβ€˜(𝐴 / (π‘š + 1))))
4123, 30, 32absdivd 15408 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(𝐴 / (π‘š + 1))) = ((absβ€˜π΄) / (absβ€˜(π‘š + 1))))
4231nnred 12231 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ ℝ)
4331nnrpd 13020 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘š + 1) ∈ ℝ+)
4443rpge0d 13026 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 0 ≀ (π‘š + 1))
4542, 44absidd 15375 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(π‘š + 1)) = (π‘š + 1))
4645oveq2d 7421 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((absβ€˜π΄) / (absβ€˜(π‘š + 1))) = ((absβ€˜π΄) / (π‘š + 1)))
4741, 46eqtrd 2766 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜(𝐴 / (π‘š + 1))) = ((absβ€˜π΄) / (π‘š + 1)))
4838, 40, 473eqtrd 2770 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) = ((absβ€˜π΄) / (π‘š + 1)))
4912ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) ∈ ℝ)
5016adantr 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ ∈ β„•)
5150nnred 12231 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ ∈ ℝ)
52 simplrr 775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) < π‘Ÿ)
53 eluzle 12839 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) β†’ π‘Ÿ ≀ π‘š)
5453adantl 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ ≀ π‘š)
55 nnleltp1 12621 . . . . . . . . . . . . . . . . . 18 ((π‘Ÿ ∈ β„• ∧ π‘š ∈ β„•) β†’ (π‘Ÿ ≀ π‘š ↔ π‘Ÿ < (π‘š + 1)))
5650, 27, 55syl2anc 583 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (π‘Ÿ ≀ π‘š ↔ π‘Ÿ < (π‘š + 1)))
5754, 56mpbid 231 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ π‘Ÿ < (π‘š + 1))
5849, 51, 42, 52, 57lttrd 11379 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) < (π‘š + 1))
5930mulridd 11235 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((π‘š + 1) Β· 1) = (π‘š + 1))
6058, 59breqtrrd 5169 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (absβ€˜π΄) < ((π‘š + 1) Β· 1))
61 1red 11219 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 1 ∈ ℝ)
6249, 61, 43ltdivmuld 13073 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((absβ€˜π΄) / (π‘š + 1)) < 1 ↔ (absβ€˜π΄) < ((π‘š + 1) Β· 1)))
6360, 62mpbird 257 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((absβ€˜π΄) / (π‘š + 1)) < 1)
6448, 63eqbrtrd 5163 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) < 1)
65 cnxmet 24644 . . . . . . . . . . . . . 14 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
6665a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
67 1rp 12984 . . . . . . . . . . . . . 14 1 ∈ ℝ+
68 rpxr 12989 . . . . . . . . . . . . . 14 (1 ∈ ℝ+ β†’ 1 ∈ ℝ*)
6967, 68mp1i 13 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ 1 ∈ ℝ*)
70 elbl3 24253 . . . . . . . . . . . . 13 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 1 ∈ ℝ*) ∧ (1 ∈ β„‚ ∧ ((𝐴 / (π‘š + 1)) + 1) ∈ β„‚)) β†’ (((𝐴 / (π‘š + 1)) + 1) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1) ↔ (((𝐴 / (π‘š + 1)) + 1)(abs ∘ βˆ’ )1) < 1))
7166, 69, 29, 34, 70syl22anc 836 . . . . . . . . . . . 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 3975 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ (β„‚ βˆ– (-∞(,]0)))
7473fmpttd 7110 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)):(β„€β‰₯β€˜π‘Ÿ)⟢(β„‚ βˆ– (-∞(,]0)))
7526ssrdv 3983 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (β„€β‰₯β€˜π‘Ÿ) βŠ† β„•)
7675resmptd 6034 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) = (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)))
77 nnex 12222 . . . . . . . . . . . . . . . . 17 β„• ∈ V
7877mptex 7220 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) ∈ V
7978a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) ∈ V)
80 oveq1 7412 . . . . . . . . . . . . . . . . . 18 (π‘š = 𝑛 β†’ (π‘š + 1) = (𝑛 + 1))
8180oveq2d 7421 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ (𝐴 / (π‘š + 1)) = (𝐴 / (𝑛 + 1)))
82 eqid 2726 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) = (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))
83 ovex 7438 . . . . . . . . . . . . . . . . 17 (𝐴 / (𝑛 + 1)) ∈ V
8481, 82, 83fvmpt 6992 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) = (𝐴 / (𝑛 + 1)))
8584adantl 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) = (𝐴 / (𝑛 + 1)))
861, 2, 11, 2, 79, 85divcnvshft 15807 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1))) ⇝ 0)
87 1cnd 11213 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 ∈ β„‚)
8877mptex 7220 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ∈ V
8988a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ∈ V)
9011adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ β„‚)
91 simpr 484 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
9291nncnd 12232 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„‚)
93 1cnd 11213 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 1 ∈ β„‚)
9492, 93addcld 11237 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) ∈ β„‚)
9591peano2nnd 12233 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) ∈ β„•)
9695nnne0d 12266 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) β‰  0)
9790, 94, 96divcld 11994 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐴 / (𝑛 + 1)) ∈ β„‚)
9885, 97eqeltrd 2827 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) ∈ β„‚)
9981oveq1d 7420 . . . . . . . . . . . . . . . . 17 (π‘š = 𝑛 β†’ ((𝐴 / (π‘š + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100 eqid 2726 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) = (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))
101 ovex 7438 . . . . . . . . . . . . . . . . 17 ((𝐴 / (𝑛 + 1)) + 1) ∈ V
10299, 100, 101fvmpt 6992 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))β€˜π‘›) = ((𝐴 / (𝑛 + 1)) + 1))
103102adantl 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))β€˜π‘›) = ((𝐴 / (𝑛 + 1)) + 1))
10485oveq1d 7420 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105103, 104eqtr4d 2769 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1))β€˜π‘›) = (((π‘š ∈ β„• ↦ (𝐴 / (π‘š + 1)))β€˜π‘›) + 1))
1061, 2, 86, 87, 89, 98, 105climaddc1 15585 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ (0 + 1))
107 0p1e1 12338 . . . . . . . . . . . . 13 (0 + 1) = 1
108106, 107breqtrdi 5182 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1)
109108adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1)
110 climres 15525 . . . . . . . . . . . 12 ((π‘Ÿ ∈ β„€ ∧ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ∈ V) β†’ (((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 1 ↔ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1))
11117, 88, 110sylancl 585 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 1 ↔ (π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1))
112109, 111mpbird 257 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ ((𝐴 / (π‘š + 1)) + 1)) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 1)
11376, 112eqbrtrrd 5165 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)) ⇝ 1)
11467a1i 11 . . . . . . . . . . 11 (1 ∈ ℝ β†’ 1 ∈ ℝ+)
11518ellogdm 26528 . . . . . . . . . . 11 (1 ∈ (β„‚ βˆ– (-∞(,]0)) ↔ (1 ∈ β„‚ ∧ (1 ∈ ℝ β†’ 1 ∈ ℝ+)))
11635, 114, 115mpbir2an 708 . . . . . . . . . 10 1 ∈ (β„‚ βˆ– (-∞(,]0))
117116a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ 1 ∈ (β„‚ βˆ– (-∞(,]0)))
11815, 17, 20, 74, 113, 117climcncf 24775 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∘ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1))) ⇝ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1))
119 logf1o 26453 . . . . . . . . . . 11 log:(β„‚ βˆ– {0})–1-1-ontoβ†’ran log
120 f1of 6827 . . . . . . . . . . 11 (log:(β„‚ βˆ– {0})–1-1-ontoβ†’ran log β†’ log:(β„‚ βˆ– {0})⟢ran log)
121119, 120mp1i 13 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ log:(β„‚ βˆ– {0})⟢ran log)
12218logdmss 26531 . . . . . . . . . . 11 (β„‚ βˆ– (-∞(,]0)) βŠ† (β„‚ βˆ– {0})
123122, 73sselid 3975 . . . . . . . . . 10 (((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) ∧ π‘š ∈ (β„€β‰₯β€˜π‘Ÿ)) β†’ ((𝐴 / (π‘š + 1)) + 1) ∈ (β„‚ βˆ– {0}))
124121, 123cofmpt 7126 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ (log ∘ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1))) = (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))
125 frn 6718 . . . . . . . . . 10 ((π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)):(β„€β‰₯β€˜π‘Ÿ)⟢(β„‚ βˆ– (-∞(,]0)) β†’ ran (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1)) βŠ† (β„‚ βˆ– (-∞(,]0)))
126 cores 6242 . . . . . . . . . 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 6034 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) = (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))
129124, 127, 1283eqtr4d 2776 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0))) ∘ (π‘š ∈ (β„€β‰₯β€˜π‘Ÿ) ↦ ((𝐴 / (π‘š + 1)) + 1))) = ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)))
130 fvres 6904 . . . . . . . . . 10 (1 ∈ (β„‚ βˆ– (-∞(,]0)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1) = (logβ€˜1))
131116, 130mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1) = (logβ€˜1))
132 log1 26474 . . . . . . . . 9 (logβ€˜1) = 0
133131, 132eqtrdi 2782 . . . . . . . 8 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((log β†Ύ (β„‚ βˆ– (-∞(,]0)))β€˜1) = 0)
134118, 129, 1333brtr3d 5172 . . . . . . 7 ((πœ‘ ∧ (π‘Ÿ ∈ β„• ∧ (absβ€˜π΄) < π‘Ÿ)) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 0)
13577mptex 7220 . . . . . . . 8 (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ∈ V
136 climres 15525 . . . . . . . 8 ((π‘Ÿ ∈ β„€ ∧ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ∈ V) β†’ (((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) β†Ύ (β„€β‰₯β€˜π‘Ÿ)) ⇝ 0 ↔ (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) ⇝ 0))
13717, 135, 136sylancl 585 . . . . . . 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 11237 . . . . . 6 (πœ‘ β†’ (𝐴 + 1) ∈ β„‚)
1417dmgmn0 26913 . . . . . 6 (πœ‘ β†’ (𝐴 + 1) β‰  0)
142140, 141logcld 26459 . . . . 5 (πœ‘ β†’ (logβ€˜(𝐴 + 1)) ∈ β„‚)
14377mptex 7220 . . . . . 6 (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ∈ V
144143a1i 11 . . . . 5 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ∈ V)
14581fvoveq1d 7427 . . . . . . . 8 (π‘š = 𝑛 β†’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
146 eqid 2726 . . . . . . . 8 (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) = (π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))
147 fvex 6898 . . . . . . . 8 (logβ€˜((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148145, 146, 147fvmpt 6992 . . . . . . 7 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
149148adantl 481 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
15097, 93addcld 11237 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝐴 / (𝑛 + 1)) + 1) ∈ β„‚)
1514adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
152151, 95dmgmdivn0 26915 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝐴 / (𝑛 + 1)) + 1) β‰  0)
153150, 152logcld 26459 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1)) ∈ β„‚)
154149, 153eqeltrd 2827 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›) ∈ β„‚)
155145oveq2d 7421 . . . . . . . 8 (π‘š = 𝑛 β†’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
156 eqid 2726 . . . . . . . 8 (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) = (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))
157 ovex 7438 . . . . . . . 8 ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158155, 156, 157fvmpt 6992 . . . . . . 7 (𝑛 ∈ β„• β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
159158adantl 481 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
160149oveq2d 7421 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜(𝐴 + 1)) βˆ’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›)) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
161159, 160eqtr4d 2769 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) = ((logβ€˜(𝐴 + 1)) βˆ’ ((π‘š ∈ β„• ↦ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))β€˜π‘›)))
1621, 2, 139, 142, 144, 154, 161climsubc2 15589 . . . 4 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ⇝ ((logβ€˜(𝐴 + 1)) βˆ’ 0))
163142subid1d 11564 . . . 4 (πœ‘ β†’ ((logβ€˜(𝐴 + 1)) βˆ’ 0) = (logβ€˜(𝐴 + 1)))
164162, 163breqtrd 5167 . . 3 (πœ‘ β†’ (π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1)))) ⇝ (logβ€˜(𝐴 + 1)))
165 elfznn 13536 . . . . . . 7 (π‘˜ ∈ (1...𝑛) β†’ π‘˜ ∈ β„•)
166165adantl 481 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ β„•)
167 oveq1 7412 . . . . . . . . . . 11 (π‘š = π‘˜ β†’ (π‘š + 1) = (π‘˜ + 1))
168 id 22 . . . . . . . . . . 11 (π‘š = π‘˜ β†’ π‘š = π‘˜)
169167, 168oveq12d 7423 . . . . . . . . . 10 (π‘š = π‘˜ β†’ ((π‘š + 1) / π‘š) = ((π‘˜ + 1) / π‘˜))
170169fveq2d 6889 . . . . . . . . 9 (π‘š = π‘˜ β†’ (logβ€˜((π‘š + 1) / π‘š)) = (logβ€˜((π‘˜ + 1) / π‘˜)))
171170oveq2d 7421 . . . . . . . 8 (π‘š = π‘˜ β†’ ((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) = ((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))))
172 oveq2 7413 . . . . . . . . 9 (π‘š = π‘˜ β†’ ((𝐴 + 1) / π‘š) = ((𝐴 + 1) / π‘˜))
173172fvoveq1d 7427 . . . . . . . 8 (π‘š = π‘˜ β†’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)) = (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))
174171, 173oveq12d 7423 . . . . . . 7 (π‘š = π‘˜ β†’ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1))) = (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))))
175 ovex 7438 . . . . . . 7 (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ V
176174, 3, 175fvmpt 6992 . . . . . 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 2837 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
17911ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 𝐴 ∈ β„‚)
180 1cnd 11213 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 1 ∈ β„‚)
181179, 180addcld 11237 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + 1) ∈ β„‚)
182166peano2nnd 12233 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ β„•)
183182nnrpd 13020 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ ℝ+)
184166nnrpd 13020 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ ℝ+)
185183, 184rpdivcld 13039 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((π‘˜ + 1) / π‘˜) ∈ ℝ+)
186185relogcld 26512 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((π‘˜ + 1) / π‘˜)) ∈ ℝ)
187186recnd 11246 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((π‘˜ + 1) / π‘˜)) ∈ β„‚)
188181, 187mulcld 11238 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) ∈ β„‚)
189166nncnd 12232 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ ∈ β„‚)
190166nnne0d 12266 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ π‘˜ β‰  0)
191181, 189, 190divcld 11994 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) / π‘˜) ∈ β„‚)
192191, 180addcld 11237 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + 1) ∈ β„‚)
1937ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + 1) ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
194193, 166dmgmdivn0 26915 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + 1) β‰  0)
195192, 194logcld 26459 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)) ∈ β„‚)
196188, 195subcld 11575 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ β„‚)
197177, 178, 196fsumser 15682 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) = (seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))))β€˜π‘›))
198 fzfid 13944 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1...𝑛) ∈ Fin)
199198, 196fsumcl 15685 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ β„‚)
200197, 199eqeltrrd 2828 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))))β€˜π‘›) ∈ β„‚)
201142adantr 480 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (logβ€˜(𝐴 + 1)) ∈ β„‚)
202201, 153subcld 11575 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) ∈ β„‚)
203159, 202eqeltrd 2827 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›) ∈ β„‚)
204179, 187mulcld 11238 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) ∈ β„‚)
205179, 189, 190divcld 11994 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 / π‘˜) ∈ β„‚)
206205, 180addcld 11237 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / π‘˜) + 1) ∈ β„‚)
2074ad2antrr 723 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
208207, 166dmgmdivn0 26915 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / π‘˜) + 1) β‰  0)
209206, 208logcld 26459 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 / π‘˜) + 1)) ∈ β„‚)
210204, 209subcld 11575 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) ∈ β„‚)
211198, 210fsumcl 15685 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) ∈ β„‚)
212199, 211nncand 11580 . . . . 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 11624 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))))
214179, 180pncan2d 11577 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) βˆ’ 𝐴) = 1)
215214oveq1d 7420 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) βˆ’ 𝐴) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) = (1 Β· (logβ€˜((π‘˜ + 1) / π‘˜))))
216181, 179, 187subdird 11675 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) βˆ’ 𝐴) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) = (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))))
217187mullidd 11236 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (1 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) = (logβ€˜((π‘˜ + 1) / π‘˜)))
218215, 216, 2173eqtr3d 2774 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))) = (logβ€˜((π‘˜ + 1) / π‘˜)))
219218oveq1d 7420 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜)))) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))))
220187, 195, 209subsubd 11603 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = (((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) + (logβ€˜((𝐴 / π‘˜) + 1))))
221187, 195subcld 11575 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) ∈ β„‚)
222221, 209addcomd 11420 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) + (logβ€˜((𝐴 / π‘˜) + 1))) = ((logβ€˜((𝐴 / π‘˜) + 1)) + ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))))
223209, 195, 187subsub2d 11604 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) + ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))))
224182nncnd 12232 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ β„‚)
225179, 224addcld 11237 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + (π‘˜ + 1)) ∈ β„‚)
226182nnnn0d 12536 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) ∈ β„•0)
227 dmgmaddn0 26910 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)) ∧ (π‘˜ + 1) ∈ β„•0) β†’ (𝐴 + (π‘˜ + 1)) β‰  0)
228207, 226, 227syl2anc 583 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (𝐴 + (π‘˜ + 1)) β‰  0)
229225, 228logcld 26459 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(𝐴 + (π‘˜ + 1))) ∈ β„‚)
230183relogcld 26512 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(π‘˜ + 1)) ∈ ℝ)
231230recnd 11246 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(π‘˜ + 1)) ∈ β„‚)
232184relogcld 26512 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜π‘˜) ∈ ℝ)
233232recnd 11246 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜π‘˜) ∈ β„‚)
234229, 231, 233nnncan2d 11610 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)) βˆ’ ((logβ€˜(π‘˜ + 1)) βˆ’ (logβ€˜π‘˜))) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
235181, 189, 189, 190divdird 12032 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) + π‘˜) / π‘˜) = (((𝐴 + 1) / π‘˜) + (π‘˜ / π‘˜)))
236179, 189, 180add32d 11445 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + π‘˜) + 1) = ((𝐴 + 1) + π‘˜))
237179, 189, 180addassd 11240 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + π‘˜) + 1) = (𝐴 + (π‘˜ + 1)))
238236, 237eqtr3d 2768 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + 1) + π‘˜) = (𝐴 + (π‘˜ + 1)))
239238oveq1d 7420 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) + π‘˜) / π‘˜) = ((𝐴 + (π‘˜ + 1)) / π‘˜))
240189, 190dividd 11992 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ / π‘˜) = 1)
241240oveq2d 7421 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + (π‘˜ / π‘˜)) = (((𝐴 + 1) / π‘˜) + 1))
242235, 239, 2413eqtr3rd 2775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (((𝐴 + 1) / π‘˜) + 1) = ((𝐴 + (π‘˜ + 1)) / π‘˜))
243242fveq2d 6889 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)) = (logβ€˜((𝐴 + (π‘˜ + 1)) / π‘˜)))
244 logdiv2 26506 . . . . . . . . . . . . . . . 16 (((𝐴 + (π‘˜ + 1)) ∈ β„‚ ∧ (𝐴 + (π‘˜ + 1)) β‰  0 ∧ π‘˜ ∈ ℝ+) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / π‘˜)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)))
245225, 228, 184, 244syl3anc 1368 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / π‘˜)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)))
246243, 245eqtrd 2766 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)))
247183, 184relogdivd 26515 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((π‘˜ + 1) / π‘˜)) = ((logβ€˜(π‘˜ + 1)) βˆ’ (logβ€˜π‘˜)))
248246, 247oveq12d 7423 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜))) = (((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜π‘˜)) βˆ’ ((logβ€˜(π‘˜ + 1)) βˆ’ (logβ€˜π‘˜))))
249182nnne0d 12266 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (π‘˜ + 1) β‰  0)
250179, 224, 224, 249divdird 12032 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1)) = ((𝐴 / (π‘˜ + 1)) + ((π‘˜ + 1) / (π‘˜ + 1))))
251224, 249dividd 11992 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((π‘˜ + 1) / (π‘˜ + 1)) = 1)
252251oveq2d 7421 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / (π‘˜ + 1)) + ((π‘˜ + 1) / (π‘˜ + 1))) = ((𝐴 / (π‘˜ + 1)) + 1))
253250, 252eqtr2d 2767 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((𝐴 / (π‘˜ + 1)) + 1) = ((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1)))
254253fveq2d 6889 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)) = (logβ€˜((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1))))
255 logdiv2 26506 . . . . . . . . . . . . . . 15 (((𝐴 + (π‘˜ + 1)) ∈ β„‚ ∧ (𝐴 + (π‘˜ + 1)) β‰  0 ∧ (π‘˜ + 1) ∈ ℝ+) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1))) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
256225, 228, 183, 255syl3anc 1368 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 + (π‘˜ + 1)) / (π‘˜ + 1))) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
257254, 256eqtrd 2766 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)) = ((logβ€˜(𝐴 + (π‘˜ + 1))) βˆ’ (logβ€˜(π‘˜ + 1))))
258234, 248, 2573eqtr4d 2776 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜))) = (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)))
259258oveq2d 7421 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((π‘˜ + 1) / π‘˜)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
260223, 259eqtr3d 2768 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((𝐴 / π‘˜) + 1)) + ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
261220, 222, 2603eqtrd 2770 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((logβ€˜((π‘˜ + 1) / π‘˜)) βˆ’ ((logβ€˜(((𝐴 + 1) / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
262213, 219, 2613eqtrd 2770 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ ((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
263262sumeq2dv 15655 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = Ξ£π‘˜ ∈ (1...𝑛)((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))))
264198, 196, 210fsumsub 15740 . . . . . . 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 7413 . . . . . . . . . 10 (π‘₯ = π‘˜ β†’ (𝐴 / π‘₯) = (𝐴 / π‘˜))
266265fvoveq1d 7427 . . . . . . . . 9 (π‘₯ = π‘˜ β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / π‘˜) + 1)))
267 oveq2 7413 . . . . . . . . . 10 (π‘₯ = (π‘˜ + 1) β†’ (𝐴 / π‘₯) = (𝐴 / (π‘˜ + 1)))
268267fvoveq1d 7427 . . . . . . . . 9 (π‘₯ = (π‘˜ + 1) β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / (π‘˜ + 1)) + 1)))
269 oveq2 7413 . . . . . . . . . 10 (π‘₯ = 1 β†’ (𝐴 / π‘₯) = (𝐴 / 1))
270269fvoveq1d 7427 . . . . . . . . 9 (π‘₯ = 1 β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / 1) + 1)))
271 oveq2 7413 . . . . . . . . . 10 (π‘₯ = (𝑛 + 1) β†’ (𝐴 / π‘₯) = (𝐴 / (𝑛 + 1)))
272271fvoveq1d 7427 . . . . . . . . 9 (π‘₯ = (𝑛 + 1) β†’ (logβ€˜((𝐴 / π‘₯) + 1)) = (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))
27391nnzd 12589 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„€)
27495, 1eleqtrdi 2837 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑛 + 1) ∈ (β„€β‰₯β€˜1))
27511ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ 𝐴 ∈ β„‚)
276 elfznn 13536 . . . . . . . . . . . . . 14 (π‘₯ ∈ (1...(𝑛 + 1)) β†’ π‘₯ ∈ β„•)
277276adantl 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ π‘₯ ∈ β„•)
278277nncnd 12232 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ π‘₯ ∈ β„‚)
279277nnne0d 12266 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ π‘₯ β‰  0)
280275, 278, 279divcld 11994 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ (𝐴 / π‘₯) ∈ β„‚)
281 1cnd 11213 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ 1 ∈ β„‚)
282280, 281addcld 11237 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ ((𝐴 / π‘₯) + 1) ∈ β„‚)
2834ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ 𝐴 ∈ (β„‚ βˆ– (β„€ βˆ– β„•)))
284283, 277dmgmdivn0 26915 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ ((𝐴 / π‘₯) + 1) β‰  0)
285282, 284logcld 26459 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘₯ ∈ (1...(𝑛 + 1))) β†’ (logβ€˜((𝐴 / π‘₯) + 1)) ∈ β„‚)
286266, 268, 270, 272, 273, 274, 285telfsum 15756 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))) = ((logβ€˜((𝐴 / 1) + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
28790div1d 11986 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐴 / 1) = 𝐴)
288287fvoveq1d 7427 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (logβ€˜((𝐴 / 1) + 1)) = (logβ€˜(𝐴 + 1)))
289288oveq1d 7420 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜((𝐴 / 1) + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
290286, 289eqtrd 2766 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((logβ€˜((𝐴 / π‘˜) + 1)) βˆ’ (logβ€˜((𝐴 / (π‘˜ + 1)) + 1))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
291263, 264, 2903eqtr3d 2774 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1)))) = ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))))
292291oveq2d 7421 . . . . 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 2768 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) = (Ξ£π‘˜ ∈ (1...𝑛)(((𝐴 + 1) Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘˜) + 1))) βˆ’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1)))))
294170oveq2d 7421 . . . . . . . 8 (π‘š = π‘˜ β†’ (𝐴 Β· (logβ€˜((π‘š + 1) / π‘š))) = (𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))))
295 oveq2 7413 . . . . . . . . 9 (π‘š = π‘˜ β†’ (𝐴 / π‘š) = (𝐴 / π‘˜))
296295fvoveq1d 7427 . . . . . . . 8 (π‘š = π‘˜ β†’ (logβ€˜((𝐴 / π‘š) + 1)) = (logβ€˜((𝐴 / π‘˜) + 1)))
297294, 296oveq12d 7423 . . . . . . 7 (π‘š = π‘˜ β†’ ((𝐴 Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜((𝐴 / π‘š) + 1))) = ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))))
298 lgamcvg.g . . . . . . 7 𝐺 = (π‘š ∈ β„• ↦ ((𝐴 Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜((𝐴 / π‘š) + 1))))
299 ovex 7438 . . . . . . 7 ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) ∈ V
300297, 298, 299fvmpt 6992 . . . . . 6 (π‘˜ ∈ β„• β†’ (πΊβ€˜π‘˜) = ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))))
301166, 300syl 17 . . . . 5 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ π‘˜ ∈ (1...𝑛)) β†’ (πΊβ€˜π‘˜) = ((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))))
302301, 178, 210fsumser 15682 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Ξ£π‘˜ ∈ (1...𝑛)((𝐴 Β· (logβ€˜((π‘˜ + 1) / π‘˜))) βˆ’ (logβ€˜((𝐴 / π‘˜) + 1))) = (seq1( + , 𝐺)β€˜π‘›))
303159eqcomd 2732 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (𝑛 + 1)) + 1))) = ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›))
304197, 303oveq12d 7423 . . . 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 2774 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (seq1( + , 𝐺)β€˜π‘›) = ((seq1( + , (π‘š ∈ β„• ↦ (((𝐴 + 1) Β· (logβ€˜((π‘š + 1) / π‘š))) βˆ’ (logβ€˜(((𝐴 + 1) / π‘š) + 1)))))β€˜π‘›) βˆ’ ((π‘š ∈ β„• ↦ ((logβ€˜(𝐴 + 1)) βˆ’ (logβ€˜((𝐴 / (π‘š + 1)) + 1))))β€˜π‘›)))
3061, 2, 8, 10, 164, 200, 203, 305climsub 15584 . 2 (πœ‘ β†’ seq1( + , 𝐺) ⇝ (((log Ξ“β€˜(𝐴 + 1)) + (logβ€˜(𝐴 + 1))) βˆ’ (logβ€˜(𝐴 + 1))))
307 lgamcl 26928 . . . 4 ((𝐴 + 1) ∈ (β„‚ βˆ– (β„€ βˆ– β„•)) β†’ (log Ξ“β€˜(𝐴 + 1)) ∈ β„‚)
3087, 307syl 17 . . 3 (πœ‘ β†’ (log Ξ“β€˜(𝐴 + 1)) ∈ β„‚)
309308, 142pncand 11576 . 2 (πœ‘ β†’ (((log Ξ“β€˜(𝐴 + 1)) + (logβ€˜(𝐴 + 1))) βˆ’ (logβ€˜(𝐴 + 1))) = (log Ξ“β€˜(𝐴 + 1)))
310306, 309breqtrd 5167 1 (πœ‘ β†’ seq1( + , 𝐺) ⇝ (log Ξ“β€˜(𝐴 + 1)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆƒwrex 3064  Vcvv 3468   βˆ– cdif 3940   βŠ† wss 3943  {csn 4623   class class class wbr 5141   ↦ cmpt 5224  ran crn 5670   β†Ύ cres 5671   ∘ ccom 5673  βŸΆwf 6533  β€“1-1-ontoβ†’wf1o 6536  β€˜cfv 6537  (class class class)co 7405  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  -∞cmnf 11250  β„*cxr 11251   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448   / cdiv 11875  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  β„+crp 12980  (,]cioc 13331  ...cfz 13490  seqcseq 13972  abscabs 15187   ⇝ cli 15434  Ξ£csu 15638  βˆžMetcxmet 21225  ballcbl 21227  β€“cnβ†’ccncf 24751  logclog 26443  log Ξ“clgam 26903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-oadd 8471  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12981  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13334  df-ioc 13335  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15421  df-clim 15438  df-rlim 15439  df-sum 15639  df-ef 16017  df-sin 16019  df-cos 16020  df-tan 16021  df-pi 16022  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-starv 17221  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-unif 17229  df-hom 17230  df-cco 17231  df-rest 17377  df-topn 17378  df-0g 17396  df-gsum 17397  df-topgen 17398  df-pt 17399  df-prds 17402  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-submnd 18714  df-mulg 18996  df-cntz 19233  df-cmn 19702  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22751  df-topon 22768  df-topsp 22790  df-bases 22804  df-cld 22878  df-ntr 22879  df-cls 22880  df-nei 22957  df-lp 22995  df-perf 22996  df-cn 23086  df-cnp 23087  df-haus 23174  df-cmp 23246  df-tx 23421  df-hmeo 23614  df-fil 23705  df-fm 23797  df-flim 23798  df-flf 23799  df-xms 24181  df-ms 24182  df-tms 24183  df-cncf 24753  df-limc 25750  df-dv 25751  df-ulm 26268  df-log 26445  df-cxp 26446  df-lgam 26906
This theorem is referenced by:  lgamp1  26944
  Copyright terms: Public domain W3C validator