lgamcvg2 - Metamath Proof Explorer

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

Theorem lgamcvg2 27428

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.

Step	Hyp	Ref	Expression
1		nnuz 13042	. . 3 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12765	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
3		eqid 2763	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))
4		lgamcvg.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
5		1nn0 12660	. . . . . 6 ⊢ 1 ∈ ℕ₀
6	5	a1i 11	. . . . 5 ⊢ (𝜑 → 1 ∈ ℕ₀)
7	4, 6	dmgmaddnn0 27400	. . . 4 ⊢ (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
8	3, 7	lgamcvg 27427	. . 3 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9		seqex 14184	. . . 4 ⊢ seq1( + , 𝐺) ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐺) ∈ V)
11	4	eldifad 4054	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
12	11	abscld 15647	. . . . . . 7 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
13		arch 12641	. . . . . . 7 ⊢ ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
14	12, 13	syl 18	. . . . . 6 ⊢ (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15		eqid 2763	. . . . . . . . 9 ⊢ (ℤ_≥‘𝑟) = (ℤ_≥‘𝑟)
16		simprl 783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
17	16	nnzd 12757	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18		eqid 2763	. . . . . . . . . . 11 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
19	18	logcn 27021	. . . . . . . . . 10 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21		eqid 2763	. . . . . . . . . . . 12 ⊢ (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
22	21	dvlog2lem 27026	. . . . . . . . . . 11 ⊢ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
23	11	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝐴 ∈ ℂ)
24		eluznn 13083	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℕ)
25	24	ex 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑚 ∈ ℕ))
26	25	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑚 ∈ ℕ))
27	26	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℕ)
28	27	nncnd 12389	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℂ)
29		1cnd 11339	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℂ)
30	28, 29	addcld 11365	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℂ)
31	27	peano2nnd 12390	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℕ)
32	31	nnne0d 12426	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ≠ 0)
33	23, 30, 32	divcld 12131	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
34	33, 29	addcld 11365	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35		ax-1cn 11295	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
36		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 25133	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
38	34, 35, 37	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
39	33, 29	pncand 11707	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
40	39	fveq2d 6918	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
41	23, 30, 32	absdivd 15666	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
42	31	nnred 12388	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℝ)
43	31	nnrpd 13200	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℝ⁺)
44	43	rpge0d 13206	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 0 ≤ (𝑚 + 1))
45	42, 44	absidd 15631	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
46	45	oveq2d 7465	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
47	41, 46	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
48	38, 40, 47	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
49	12	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) ∈ ℝ)
50	16	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ∈ ℕ)
51	50	nnred 12388	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ∈ ℝ)
52		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < 𝑟)
53		eluzle 13016	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑟 ≤ 𝑚)
54	53	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ≤ 𝑚)
55		nnleltp1 12792	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1)))
56	50, 27, 55	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1)))
57	54, 56	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 < (𝑚 + 1))
58	49, 51, 42, 52, 57	lttrd 11508	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < (𝑚 + 1))
59	30	mulridd 11363	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
60	58, 59	breqtrrd 5137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61		1red 11346	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℝ)
62	49, 61, 43	ltdivmuld 13253	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
63	60, 62	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
64	48, 63	eqbrtrd 5131	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65		cnxmet 25135	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
66	65	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
67		1rp 13162	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
68		rpxr 13168	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
69	67, 68	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℝ^*)
70		elbl3 24755	. . . . . . . . . . . . 13 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (1 ∈ ℂ ∧ ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
71	66, 69, 29, 34, 70	syl22anc 852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
72	64, 71	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1))
73	22, 72	sselid 3911	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
74	73	fmpttd 7145	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ_≥‘𝑟)⟶(ℂ ∖ (-∞(,]0)))
75	26	ssrdv 3919	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ_≥‘𝑟) ⊆ ℕ)
76	75	resmptd 6048	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
77		nnex 12379	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
78	77	mptex 7258	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
79	78	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
80		oveq1 7456	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
81	80	oveq2d 7465	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
82		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
83		ovex 7482	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 / (𝑛 + 1)) ∈ V
84	81, 82, 83	fvmpt 7022	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
85	84	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
86	1, 2, 11, 2, 79, 85	divcnvshft 16065	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
87		1cnd 11339	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
88	77	mptex 7258	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
89	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
90	11	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
91		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
92	91	nncnd 12389	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
93		1cnd 11339	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
94	92, 93	addcld 11365	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
95	91	peano2nnd 12390	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
96	95	nnne0d 12426	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
97	90, 94, 96	divcld 12131	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
98	85, 97	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
99	81	oveq1d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
101		ovex 7482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 / (𝑛 + 1)) + 1) ∈ V
102	99, 100, 101	fvmpt 7022	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
103	102	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
104	85	oveq1d 7464	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105	103, 104	eqtr4d 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
106	1, 2, 86, 87, 89, 98, 105	climaddc1 15843	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
107		0p1e1 12501	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
108	106, 107	breqtrdi 5150	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
109	108	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
110		climres 15783	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
111	17, 88, 110	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
112	109, 111	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) ⇝ 1)
113	76, 112	eqbrtrrd 5133	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
114	67	a1i 11	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ → 1 ∈ ℝ⁺)
115	18	ellogdm 27013	. . . . . . . . . . 11 ⊢ (1 ∈ (ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈ ℝ → 1 ∈ ℝ⁺)))
116	35, 114, 115	mpbir2an 724	. . . . . . . . . 10 ⊢ 1 ∈ (ℂ ∖ (-∞(,]0))
117	116	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖ (-∞(,]0)))
118	15, 17, 20, 74, 113, 117	climcncf 25265	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
119		logf1o 26938	. . . . . . . . . . 11 ⊢ log:(ℂ ∖ {0})⟶1-1ontoran log
120		f1of 6852	. . . . . . . . . . 11 ⊢ (log:(ℂ ∖ {0})⟶1-1ontoran log → log:(ℂ ∖ {0})⟶ran log)
121	119, 120	mp1i 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖ {0})⟶ran log)
122	18	logdmss 27016	. . . . . . . . . . 11 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
123	122, 73	sselid 3911	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
124	121, 123	cofmpt 7163	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
125		frn 6745	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ_≥‘𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
126		cores 6267	. . . . . . . . . 10 ⊢ (ran (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
127	74, 125, 126	3syl 19	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
128	75	resmptd 6048	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
129	124, 127, 128	3eqtr4d 2808	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)))
130		fvres 6933	. . . . . . . . . 10 ⊢ (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
131	116, 130	mp1i 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
132		log1 26959	. . . . . . . . 9 ⊢ (log‘1) = 0
133	131, 132	eqtrdi 2814	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
134	118, 129, 133	3brtr3d 5140	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0)
135	77	mptex 7258	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
136		climres 15783	. . . . . . . 8 ⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
137	17, 135, 136	sylancl 598	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
138	134, 137	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
139	14, 138	rexlimddv 3173	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
140	11, 87	addcld 11365	. . . . . 6 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
141	7	dmgmn0 27399	. . . . . 6 ⊢ (𝜑 → (𝐴 + 1) ≠ 0)
142	140, 141	logcld 26944	. . . . 5 ⊢ (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
143	77	mptex 7258	. . . . . 6 ⊢ (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
144	143	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
145	81	fvoveq1d 7471	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
146		eqid 2763	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
147		fvex 6927	. . . . . . . 8 ⊢ (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148	145, 146, 147	fvmpt 7022	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
149	148	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
150	97, 93	addcld 11365	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
151	4	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
152	151, 95	dmgmdivn0 27401	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
153	150, 152	logcld 26944	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
154	149, 153	eqeltrd 2864	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
155	145	oveq2d 7465	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
156		eqid 2763	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
157		ovex 7482	. . . . . . . 8 ⊢ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158	155, 156, 157	fvmpt 7022	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
159	158	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
160	149	oveq2d 7465	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
161	159, 160	eqtr4d 2801	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
162	1, 2, 139, 142, 144, 154, 161	climsubc2 15847	. . . 4 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
163	142	subid1d 11695	. . . 4 ⊢ (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
164	162, 163	breqtrd 5135	. . 3 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
165		elfznn 13725	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
166	165	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
167		oveq1 7456	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
168		id 23	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
169	167, 168	oveq12d 7467	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
170	169	fveq2d 6918	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
171	170	oveq2d 7465	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
172		oveq2 7457	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
173	172	fvoveq1d 7471	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
174	171, 173	oveq12d 7467	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
175		ovex 7482	. . . . . . 7 ⊢ (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
176	174, 3, 175	fvmpt 7022	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
177	166, 176	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
178	91, 1	eleqtrdi 2874	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
179	11	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
180		1cnd 11339	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
181	179, 180	addcld 11365	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
182	166	peano2nnd 12390	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
183	182	nnrpd 13200	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ⁺)
184	166	nnrpd 13200	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ⁺)
185	183, 184	rpdivcld 13219	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ⁺)
186	185	relogcld 26997	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
187	186	recnd 11374	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
188	181, 187	mulcld 11366	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
189	166	nncnd 12389	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
190	166	nnne0d 12426	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
191	181, 189, 190	divcld 12131	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
192	191, 180	addcld 11365	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
193	7	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
194	193, 166	dmgmdivn0 27401	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
195	192, 194	logcld 26944	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
196	188, 195	subcld 11706	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
197	177, 178, 196	fsumser 15937	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
198		fzfid 14154	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
199	198, 196	fsumcl 15940	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
200	197, 199	eqeltrrd 2865	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
201	142	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
202	201, 153	subcld 11706	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
203	159, 202	eqeltrd 2864	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
204	179, 187	mulcld 11366	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
205	179, 189, 190	divcld 12131	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
206	205, 180	addcld 11365	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
207	4	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
208	207, 166	dmgmdivn0 27401	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
209	206, 208	logcld 26944	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
210	204, 209	subcld 11706	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
211	198, 210	fsumcl 15940	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
212	199, 211	nncand 11711	. . . . 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))))
213	188, 195, 204, 209	sub4d 11755	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
214	179, 180	pncan2d 11708	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
215	214	oveq1d 7464	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
216	181, 179, 187	subdird 11810	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
217	187	mullidd 11364	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
218	215, 216, 217	3eqtr3d 2806	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
219	218	oveq1d 7464	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
220	187, 195, 209	subsubd 11734	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
221	187, 195	subcld 11706	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
222	221, 209	addcomd 11549	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
223	209, 195, 187	subsub2d 11735	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
224	182	nncnd 12389	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
225	179, 224	addcld 11365	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
226	182	nnnn0d 12705	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ₀)
227		dmgmaddn0 27396	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ₀) → (𝐴 + (𝑘 + 1)) ≠ 0)
228	207, 226, 227	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
229	225, 228	logcld 26944	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
230	183	relogcld 26997	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
231	230	recnd 11374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
232	184	relogcld 26997	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
233	232	recnd 11374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
234	229, 231, 233	nnncan2d 11741	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
235	181, 189, 189, 190	divdird 12169	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
236	179, 189, 180	add32d 11575	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
237	179, 189, 180	addassd 11368	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
238	236, 237	eqtr3d 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
239	238	oveq1d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
240	189, 190	dividd 12129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
241	240	oveq2d 7465	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
242	235, 239, 241	3eqtr3rd 2807	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
243	242	fveq2d 6918	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
244		logdiv2 26991	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ⁺) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
245	225, 228, 184, 244	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
246	243, 245	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
247	183, 184	relogdivd 27000	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
248	246, 247	oveq12d 7467	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
249	182	nnne0d 12426	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
250	179, 224, 224, 249	divdird 12169	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
251	224, 249	dividd 12129	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
252	251	oveq2d 7465	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
253	250, 252	eqtr2d 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
254	253	fveq2d 6918	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
255		logdiv2 26991	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ⁺) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
256	225, 228, 183, 255	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
257	254, 256	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
258	234, 248, 257	3eqtr4d 2808	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
259	258	oveq2d 7465	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
260	223, 259	eqtr3d 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
261	220, 222, 260	3eqtrd 2802	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
262	213, 219, 261	3eqtrd 2802	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
263	262	sumeq2dv 15910	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
264	198, 196, 210	fsumsub 15995	. . . . . . 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 7457	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
266	265	fvoveq1d 7471	. . . . . . . . 9 ⊢ (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
267		oveq2 7457	. . . . . . . . . 10 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
268	267	fvoveq1d 7471	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
269		oveq2 7457	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
270	269	fvoveq1d 7471	. . . . . . . . 9 ⊢ (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
271		oveq2 7457	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
272	271	fvoveq1d 7471	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
273	91	nnzd 12757	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
274	95, 1	eleqtrdi 2874	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ_≥‘1))
275	11	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
276		elfznn 13725	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
277	276	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
278	277	nncnd 12389	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
279	277	nnne0d 12426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
280	275, 278, 279	divcld 12131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
281		1cnd 11339	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
282	280, 281	addcld 11365	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
283	4	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
284	283, 277	dmgmdivn0 27401	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
285	282, 284	logcld 26944	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
286	266, 268, 270, 272, 273, 274, 285	telfsum 16012	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
287	90	div1d 12123	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
288	287	fvoveq1d 7471	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
289	288	oveq1d 7464	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
290	286, 289	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
291	263, 264, 290	3eqtr3d 2806	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
292	291	oveq2d 7465	. . . . 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)))))
293	212, 292	eqtr3d 2800	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
294	170	oveq2d 7465	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
295		oveq2 7457	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
296	295	fvoveq1d 7471	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
297	294, 296	oveq12d 7467	. . . . . . 7 ⊢ (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
298		lgamcvg.g	. . . . . . 7 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
299		ovex 7482	. . . . . . 7 ⊢ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
300	297, 298, 299	fvmpt 7022	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
301	166, 300	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
302	301, 178, 210	fsumser 15937	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
303	159	eqcomd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
304	197, 303	oveq12d 7467	. . . 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))))‘𝑛)))
305	293, 302, 304	3eqtr3d 2806	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
306	1, 2, 8, 10, 164, 200, 203, 305	climsub 15842	. 2 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
307		lgamcl 27414	. . . 4 ⊢ ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
308	7, 307	syl 18	. . 3 ⊢ (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
309	308, 142	pncand 11707	. 2 ⊢ (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
310	306, 309	breqtrd 5135	1 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 {csn 4588 class class class wbr 5106 ↦ cmpt 5190 ran crn 5657 ↾ cres 5658 ∘ ccom 5660 ⟶wf 6560 ⟶1-1ontowf1o 6563 ‘cfv 6564 (class class class)co 7449 ℂcc 11235 ℝcr 11236 0cc0 11237 1c1 11238 + caddc 11240 · cmul 11242 -∞cmnf 11378 ℝ^*cxr 11379 < clt 11380 ≤ cle 11381 − cmin 11578 / cdiv 12011 ℕcn 12373 ℕ₀cn0 12644 ℤcz 12731 ℤ_≥cuz 13003 ℝ⁺crp 13158 (,]cioc 13515 ...cfz 13677 seqcseq 14182 abscabs 15442 ⇝ cli 15692 Σcsu 15894 ∞Metcxmet 21705 ballcbl 21707 –cn→ccncf 25241 logclog 26928 log Γclgam 27389

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315 ax-addf 11316

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-of 7723 df-om 7910 df-1st 8033 df-2nd 8034 df-supp 8213 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-oadd 8516 df-er 8753 df-map 8885 df-pm 8886 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-fsupp 9390 df-fi 9438 df-sup 9469 df-inf 9470 df-oi 9539 df-dju 10017 df-card 10055 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-z 12732 df-dec 12853 df-uz 13004 df-q 13114 df-rp 13159 df-xneg 13279 df-xadd 13280 df-xmul 13281 df-ioo 13518 df-ioc 13519 df-ico 13520 df-icc 13521 df-fz 13678 df-fzo 13827 df-fl 13970 df-mod 14048 df-seq 14183 df-exp 14243 df-fac 14457 df-bc 14486 df-hash 14514 df-shft 15261 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-limsup 15679 df-clim 15696 df-rlim 15697 df-sum 15895 df-ef 16274 df-sin 16276 df-cos 16277 df-tan 16278 df-pi 16279 df-struct 17366 df-sets 17383 df-slot 17401 df-ndx 17413 df-base 17429 df-ress 17450 df-plusg 17482 df-mulr 17483 df-starv 17484 df-sca 17485 df-vsca 17486 df-ip 17487 df-tset 17488 df-ple 17489 df-ds 17491 df-unif 17492 df-hom 17493 df-cco 17494 df-rest 17634 df-topn 17635 df-0g 17653 df-gsum 17654 df-topgen 17655 df-pt 17656 df-prds 17659 df-xrs 17715 df-qtop 17720 df-imas 17721 df-xps 17723 df-mre 17797 df-mrc 17798 df-acs 17800 df-mgm 18857 df-sgrp 18949 df-mnd 18965 df-submnd 19020 df-mulg 19319 df-cntz 19573 df-cmn 20038 df-psmet 21712 df-xmet 21713 df-met 21714 df-bl 21715 df-mopn 21716 df-fbas 21717 df-fg 21718 df-cnfld 21721 df-top 23256 df-topon 23273 df-topsp 23295 df-bases 23308 df-cld 23381 df-ntr 23382 df-cls 23383 df-nei 23460 df-lp 23498 df-perf 23499 df-cn 23589 df-cnp 23590 df-haus 23677 df-cmp 23749 df-tx 23925 df-hmeo 24118 df-fil 24209 df-fm 24301 df-flim 24302 df-flf 24303 df-xms 24683 df-ms 24684 df-tms 24685 df-cncf 25243 df-limc 26230 df-dv 26231 df-ulm 26750 df-log 26930 df-cxp 26931 df-lgam 27392

This theorem is used by: lgamp1 27430

W3C validator