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 26981

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 12796	. . 3 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12524	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
3		eqid 2729	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))
4		lgamcvg.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
5		1nn0 12418	. . . . . 6 ⊢ 1 ∈ ℕ₀
6	5	a1i 11	. . . . 5 ⊢ (𝜑 → 1 ∈ ℕ₀)
7	4, 6	dmgmaddnn0 26953	. . . 4 ⊢ (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
8	3, 7	lgamcvg 26980	. . 3 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9		seqex 13928	. . . 4 ⊢ seq1( + , 𝐺) ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐺) ∈ V)
11	4	eldifad 3917	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
12	11	abscld 15364	. . . . . . 7 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
13		arch 12399	. . . . . . 7 ⊢ ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
14	12, 13	syl 17	. . . . . 6 ⊢ (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15		eqid 2729	. . . . . . . . 9 ⊢ (ℤ_≥‘𝑟) = (ℤ_≥‘𝑟)
16		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
17	16	nnzd 12516	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18		eqid 2729	. . . . . . . . . . 11 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
19	18	logcn 26572	. . . . . . . . . 10 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21		eqid 2729	. . . . . . . . . . . 12 ⊢ (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
22	21	dvlog2lem 26577	. . . . . . . . . . 11 ⊢ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
23	11	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝐴 ∈ ℂ)
24		eluznn 12837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℕ)
25	24	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑚 ∈ ℕ))
26	25	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑚 ∈ ℕ))
27	26	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℕ)
28	27	nncnd 12162	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℂ)
29		1cnd 11129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℂ)
30	28, 29	addcld 11153	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℂ)
31	27	peano2nnd 12163	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℕ)
32	31	nnne0d 12196	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ≠ 0)
33	23, 30, 32	divcld 11918	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
34	33, 29	addcld 11153	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35		ax-1cn 11086	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
36		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 24674	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
38	34, 35, 37	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)))
39	33, 29	pncand 11494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
40	39	fveq2d 6830	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
41	23, 30, 32	absdivd 15383	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
42	31	nnred 12161	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℝ)
43	31	nnrpd 12953	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℝ⁺)
44	43	rpge0d 12959	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 0 ≤ (𝑚 + 1))
45	42, 44	absidd 15348	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
46	45	oveq2d 7369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
47	41, 46	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
48	38, 40, 47	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
49	12	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) ∈ ℝ)
50	16	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ∈ ℕ)
51	50	nnred 12161	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ∈ ℝ)
52		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < 𝑟)
53		eluzle 12766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑟 ≤ 𝑚)
54	53	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ≤ 𝑚)
55		nnleltp1 12549	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1)))
56	50, 27, 55	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1)))
57	54, 56	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 < (𝑚 + 1))
58	49, 51, 42, 52, 57	lttrd 11295	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < (𝑚 + 1))
59	30	mulridd 11151	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
60	58, 59	breqtrrd 5123	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61		1red 11135	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℝ)
62	49, 61, 43	ltdivmuld 13006	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
63	60, 62	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
64	48, 63	eqbrtrd 5117	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65		cnxmet 24676	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
66	65	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
67		1rp 12915	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
68		rpxr 12921	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
69	67, 68	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℝ^*)
70		elbl3 24296	. . . . . . . . . . . . 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 838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1) ↔ (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1))
72	64, 71	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘ − ))1))
73	22, 72	sselid 3935	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
74	73	fmpttd 7053	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ_≥‘𝑟)⟶(ℂ ∖ (-∞(,]0)))
75	26	ssrdv 3943	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ_≥‘𝑟) ⊆ ℕ)
76	75	resmptd 5995	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
77		nnex 12152	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
78	77	mptex 7163	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
79	78	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
80		oveq1 7360	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
81	80	oveq2d 7369	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
82		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
83		ovex 7386	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 / (𝑛 + 1)) ∈ V
84	81, 82, 83	fvmpt 6934	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
85	84	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
86	1, 2, 11, 2, 79, 85	divcnvshft 15780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
87		1cnd 11129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
88	77	mptex 7163	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
89	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
90	11	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
91		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
92	91	nncnd 12162	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
93		1cnd 11129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
94	92, 93	addcld 11153	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
95	91	peano2nnd 12163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
96	95	nnne0d 12196	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
97	90, 94, 96	divcld 11918	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
98	85, 97	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
99	81	oveq1d 7368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
101		ovex 7386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 / (𝑛 + 1)) + 1) ∈ V
102	99, 100, 101	fvmpt 6934	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
103	102	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
104	85	oveq1d 7368	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105	103, 104	eqtr4d 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
106	1, 2, 86, 87, 89, 98, 105	climaddc1 15560	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
107		0p1e1 12263	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
108	106, 107	breqtrdi 5136	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
109	108	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
110		climres 15500	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
111	17, 88, 110	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1))
112	109, 111	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) ⇝ 1)
113	76, 112	eqbrtrrd 5119	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
114	67	a1i 11	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ → 1 ∈ ℝ⁺)
115	18	ellogdm 26564	. . . . . . . . . . 11 ⊢ (1 ∈ (ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈ ℝ → 1 ∈ ℝ⁺)))
116	35, 114, 115	mpbir2an 711	. . . . . . . . . 10 ⊢ 1 ∈ (ℂ ∖ (-∞(,]0))
117	116	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖ (-∞(,]0)))
118	15, 17, 20, 74, 113, 117	climcncf 24809	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
119		logf1o 26489	. . . . . . . . . . 11 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
120		f1of 6768	. . . . . . . . . . 11 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
121	119, 120	mp1i 13	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖ {0})⟶ran log)
122	18	logdmss 26567	. . . . . . . . . . 11 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
123	122, 73	sselid 3935	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
124	121, 123	cofmpt 7070	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
125		frn 6663	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ_≥‘𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
126		cores 6202	. . . . . . . . . 10 ⊢ (ran (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
127	74, 125, 126	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))))
128	75	resmptd 5995	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
129	124, 127, 128	3eqtr4d 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)))
130		fvres 6845	. . . . . . . . . 10 ⊢ (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
131	116, 130	mp1i 13	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
132		log1 26510	. . . . . . . . 9 ⊢ (log‘1) = 0
133	131, 132	eqtrdi 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
134	118, 129, 133	3brtr3d 5126	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0)
135	77	mptex 7163	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
136		climres 15500	. . . . . . . 8 ⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
137	17, 135, 136	sylancl 586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0))
138	134, 137	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
139	14, 138	rexlimddv 3136	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
140	11, 87	addcld 11153	. . . . . 6 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
141	7	dmgmn0 26952	. . . . . 6 ⊢ (𝜑 → (𝐴 + 1) ≠ 0)
142	140, 141	logcld 26495	. . . . 5 ⊢ (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
143	77	mptex 7163	. . . . . 6 ⊢ (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
144	143	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
145	81	fvoveq1d 7375	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
146		eqid 2729	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
147		fvex 6839	. . . . . . . 8 ⊢ (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148	145, 146, 147	fvmpt 6934	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
149	148	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
150	97, 93	addcld 11153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
151	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
152	151, 95	dmgmdivn0 26954	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
153	150, 152	logcld 26495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
154	149, 153	eqeltrd 2828	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
155	145	oveq2d 7369	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
156		eqid 2729	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
157		ovex 7386	. . . . . . . 8 ⊢ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158	155, 156, 157	fvmpt 6934	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
159	158	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
160	149	oveq2d 7369	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
161	159, 160	eqtr4d 2767	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
162	1, 2, 139, 142, 144, 154, 161	climsubc2 15564	. . . 4 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
163	142	subid1d 11482	. . . 4 ⊢ (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
164	162, 163	breqtrd 5121	. . 3 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
165		elfznn 13474	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
166	165	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
167		oveq1 7360	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
168		id 22	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
169	167, 168	oveq12d 7371	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
170	169	fveq2d 6830	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
171	170	oveq2d 7369	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
172		oveq2 7361	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
173	172	fvoveq1d 7375	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
174	171, 173	oveq12d 7371	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
175		ovex 7386	. . . . . . 7 ⊢ (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
176	174, 3, 175	fvmpt 6934	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
177	166, 176	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
178	91, 1	eleqtrdi 2838	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
179	11	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
180		1cnd 11129	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
181	179, 180	addcld 11153	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
182	166	peano2nnd 12163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
183	182	nnrpd 12953	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ⁺)
184	166	nnrpd 12953	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ⁺)
185	183, 184	rpdivcld 12972	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ⁺)
186	185	relogcld 26548	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
187	186	recnd 11162	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
188	181, 187	mulcld 11154	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
189	166	nncnd 12162	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
190	166	nnne0d 12196	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
191	181, 189, 190	divcld 11918	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
192	191, 180	addcld 11153	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
193	7	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
194	193, 166	dmgmdivn0 26954	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
195	192, 194	logcld 26495	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
196	188, 195	subcld 11493	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
197	177, 178, 196	fsumser 15655	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
198		fzfid 13898	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
199	198, 196	fsumcl 15658	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
200	197, 199	eqeltrrd 2829	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
201	142	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
202	201, 153	subcld 11493	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
203	159, 202	eqeltrd 2828	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
204	179, 187	mulcld 11154	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
205	179, 189, 190	divcld 11918	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
206	205, 180	addcld 11153	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
207	4	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
208	207, 166	dmgmdivn0 26954	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
209	206, 208	logcld 26495	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
210	204, 209	subcld 11493	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
211	198, 210	fsumcl 15658	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
212	199, 211	nncand 11498	. . . . 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 11542	. . . . . . . . 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 11495	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
215	214	oveq1d 7368	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
216	181, 179, 187	subdird 11595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
217	187	mullidd 11152	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
218	215, 216, 217	3eqtr3d 2772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
219	218	oveq1d 7368	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
220	187, 195, 209	subsubd 11521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
221	187, 195	subcld 11493	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
222	221, 209	addcomd 11336	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
223	209, 195, 187	subsub2d 11522	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
224	182	nncnd 12162	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
225	179, 224	addcld 11153	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
226	182	nnnn0d 12463	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ₀)
227		dmgmaddn0 26949	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ₀) → (𝐴 + (𝑘 + 1)) ≠ 0)
228	207, 226, 227	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
229	225, 228	logcld 26495	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
230	183	relogcld 26548	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
231	230	recnd 11162	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
232	184	relogcld 26548	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
233	232	recnd 11162	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
234	229, 231, 233	nnncan2d 11528	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
235	181, 189, 189, 190	divdird 11956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
236	179, 189, 180	add32d 11362	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
237	179, 189, 180	addassd 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
238	236, 237	eqtr3d 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
239	238	oveq1d 7368	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
240	189, 190	dividd 11916	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
241	240	oveq2d 7369	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
242	235, 239, 241	3eqtr3rd 2773	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
243	242	fveq2d 6830	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
244		logdiv2 26542	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ⁺) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
245	225, 228, 184, 244	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
246	243, 245	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
247	183, 184	relogdivd 26551	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
248	246, 247	oveq12d 7371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
249	182	nnne0d 12196	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
250	179, 224, 224, 249	divdird 11956	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
251	224, 249	dividd 11916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
252	251	oveq2d 7369	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
253	250, 252	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
254	253	fveq2d 6830	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
255		logdiv2 26542	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ⁺) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
256	225, 228, 183, 255	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
257	254, 256	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
258	234, 248, 257	3eqtr4d 2774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
259	258	oveq2d 7369	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
260	223, 259	eqtr3d 2766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
261	220, 222, 260	3eqtrd 2768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
262	213, 219, 261	3eqtrd 2768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
263	262	sumeq2dv 15627	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
264	198, 196, 210	fsumsub 15713	. . . . . . 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 7361	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
266	265	fvoveq1d 7375	. . . . . . . . 9 ⊢ (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
267		oveq2 7361	. . . . . . . . . 10 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
268	267	fvoveq1d 7375	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
269		oveq2 7361	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
270	269	fvoveq1d 7375	. . . . . . . . 9 ⊢ (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
271		oveq2 7361	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
272	271	fvoveq1d 7375	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
273	91	nnzd 12516	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
274	95, 1	eleqtrdi 2838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ_≥‘1))
275	11	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
276		elfznn 13474	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
277	276	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
278	277	nncnd 12162	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
279	277	nnne0d 12196	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
280	275, 278, 279	divcld 11918	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
281		1cnd 11129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
282	280, 281	addcld 11153	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
283	4	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
284	283, 277	dmgmdivn0 26954	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
285	282, 284	logcld 26495	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
286	266, 268, 270, 272, 273, 274, 285	telfsum 15729	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
287	90	div1d 11910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
288	287	fvoveq1d 7375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
289	288	oveq1d 7368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
290	286, 289	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
291	263, 264, 290	3eqtr3d 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
292	291	oveq2d 7369	. . . . 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 2766	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
294	170	oveq2d 7369	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
295		oveq2 7361	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
296	295	fvoveq1d 7375	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
297	294, 296	oveq12d 7371	. . . . . . 7 ⊢ (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
298		lgamcvg.g	. . . . . . 7 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
299		ovex 7386	. . . . . . 7 ⊢ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
300	297, 298, 299	fvmpt 6934	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
301	166, 300	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
302	301, 178, 210	fsumser 15655	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
303	159	eqcomd 2735	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
304	197, 303	oveq12d 7371	. . . 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 2772	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
306	1, 2, 8, 10, 164, 200, 203, 305	climsub 15559	. 2 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
307		lgamcl 26967	. . . 4 ⊢ ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
308	7, 307	syl 17	. . 3 ⊢ (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
309	308, 142	pncand 11494	. 2 ⊢ (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
310	306, 309	breqtrd 5121	1 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 Vcvv 3438 ∖ cdif 3902 ⊆ wss 3905 {csn 4579 class class class wbr 5095 ↦ cmpt 5176 ran crn 5624 ↾ cres 5625 ∘ ccom 5627 ⟶wf 6482 –1-1-onto→wf1o 6485 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 -∞cmnf 11166 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11365 / cdiv 11795 ℕcn 12146 ℕ₀cn0 12402 ℤcz 12489 ℤ_≥cuz 12753 ℝ⁺crp 12911 (,]cioc 13267 ...cfz 13428 seqcseq 13926 abscabs 15159 ⇝ cli 15409 Σcsu 15611 ∞Metcxmet 21264 ballcbl 21266 –cn→ccncf 24785 logclog 26479 log Γclgam 26942

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8632 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-dju 9816 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-q 12868 df-rp 12912 df-xneg 13032 df-xadd 13033 df-xmul 13034 df-ioo 13270 df-ioc 13271 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-fac 14199 df-bc 14228 df-hash 14256 df-shft 14992 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-limsup 15396 df-clim 15413 df-rlim 15414 df-sum 15612 df-ef 15992 df-sin 15994 df-cos 15995 df-tan 15996 df-pi 15997 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17344 df-topn 17345 df-0g 17363 df-gsum 17364 df-topgen 17365 df-pt 17366 df-prds 17369 df-xrs 17424 df-qtop 17429 df-imas 17430 df-xps 17432 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-submnd 18676 df-mulg 18965 df-cntz 19214 df-cmn 19679 df-psmet 21271 df-xmet 21272 df-met 21273 df-bl 21274 df-mopn 21275 df-fbas 21276 df-fg 21277 df-cnfld 21280 df-top 22797 df-topon 22814 df-topsp 22836 df-bases 22849 df-cld 22922 df-ntr 22923 df-cls 22924 df-nei 23001 df-lp 23039 df-perf 23040 df-cn 23130 df-cnp 23131 df-haus 23218 df-cmp 23290 df-tx 23465 df-hmeo 23658 df-fil 23749 df-fm 23841 df-flim 23842 df-flf 23843 df-xms 24224 df-ms 24225 df-tms 24226 df-cncf 24787 df-limc 25783 df-dv 25784 df-ulm 26302 df-log 26481 df-cxp 26482 df-lgam 26945

This theorem is referenced by: lgamp1 26983

W3C validator