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 27022

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 12900	. . 3 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12628	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
3		eqid 2736	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))
4		lgamcvg.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
5		1nn0 12522	. . . . . 6 ⊢ 1 ∈ ℕ₀
6	5	a1i 11	. . . . 5 ⊢ (𝜑 → 1 ∈ ℕ₀)
7	4, 6	dmgmaddnn0 26994	. . . 4 ⊢ (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
8	3, 7	lgamcvg 27021	. . 3 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))))
9		seqex 14026	. . . 4 ⊢ seq1( + , 𝐺) ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐺) ∈ V)
11	4	eldifad 3943	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
12	11	abscld 15460	. . . . . . 7 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
13		arch 12503	. . . . . . 7 ⊢ ((abs‘𝐴) ∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
14	12, 13	syl 17	. . . . . 6 ⊢ (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟)
15		eqid 2736	. . . . . . . . 9 ⊢ (ℤ_≥‘𝑟) = (ℤ_≥‘𝑟)
16		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ)
17	16	nnzd 12620	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ)
18		eqid 2736	. . . . . . . . . . 11 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
19	18	logcn 26613	. . . . . . . . . 10 ⊢ (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ))
21		eqid 2736	. . . . . . . . . . . 12 ⊢ (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
22	21	dvlog2lem 26618	. . . . . . . . . . 11 ⊢ (1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖ (-∞(,]0))
23	11	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝐴 ∈ ℂ)
24		eluznn 12939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℕ)
25	24	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℕ → (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑚 ∈ ℕ))
26	25	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑚 ∈ ℕ))
27	26	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℕ)
28	27	nncnd 12261	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑚 ∈ ℂ)
29		1cnd 11235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℂ)
30	28, 29	addcld 11259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℂ)
31	27	peano2nnd 12262	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℕ)
32	31	nnne0d 12295	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ≠ 0)
33	23, 30, 32	divcld 12022	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ)
34	33, 29	addcld 11259	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)
35		ax-1cn 11192	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
36		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
37	36	cnmetdval 24714	. . . . . . . . . . . . . . 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 11600	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1)))
40	39	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1))))
41	23, 30, 32	absdivd 15479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1))))
42	31	nnred 12260	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℝ)
43	31	nnrpd 13054	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (𝑚 + 1) ∈ ℝ⁺)
44	43	rpge0d 13060	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 0 ≤ (𝑚 + 1))
45	42, 44	absidd 15446	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1))
46	45	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
47	41, 46	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1)))
48	38, 40, 47	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) = ((abs‘𝐴) / (𝑚 + 1)))
49	12	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) ∈ ℝ)
50	16	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ∈ ℕ)
51	50	nnred 12260	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ∈ ℝ)
52		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < 𝑟)
53		eluzle 12870	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (ℤ_≥‘𝑟) → 𝑟 ≤ 𝑚)
54	53	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 𝑟 ≤ 𝑚)
55		nnleltp1 12653	. . . . . . . . . . . . . . . . . 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 11401	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < (𝑚 + 1))
59	30	mulridd 11257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1))
60	58, 59	breqtrrd 5152	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1))
61		1red 11241	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℝ)
62	49, 61, 43	ltdivmuld 13107	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1)))
63	60, 62	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1)
64	48, 63	eqbrtrd 5146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) < 1)
65		cnxmet 24716	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
66	65	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
67		1rp 13017	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ⁺
68		rpxr 13023	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
69	67, 68	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → 1 ∈ ℝ^*)
70		elbl3 24336	. . . . . . . . . . . . 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 3961	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ (-∞(,]0)))
74	73	fmpttd 7110	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ_≥‘𝑟)⟶(ℂ ∖ (-∞(,]0)))
75	26	ssrdv 3969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ_≥‘𝑟) ⊆ ℕ)
76	75	resmptd 6032	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾ (ℤ_≥‘𝑟)) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))
77		nnex 12251	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ∈ V
78	77	mptex 7220	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V
79	78	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V)
80		oveq1 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
81	80	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1)))
82		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))
83		ovex 7443	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 / (𝑛 + 1)) ∈ V
84	81, 82, 83	fvmpt 6991	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
85	84	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1)))
86	1, 2, 11, 2, 79, 85	divcnvshft 15876	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0)
87		1cnd 11235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
88	77	mptex 7220	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V
89	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V)
90	11	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
91		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
92	91	nncnd 12261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
93		1cnd 11235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
94	92, 93	addcld 11259	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ)
95	91	peano2nnd 12262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
96	95	nnne0d 12295	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0)
97	90, 94, 96	divcld 12022	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ)
98	85, 97	eqeltrd 2835	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ)
99	81	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
100		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))
101		ovex 7443	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 / (𝑛 + 1)) + 1) ∈ V
102	99, 100, 101	fvmpt 6991	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
103	102	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1))
104	85	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1))
105	103, 104	eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1))
106	1, 2, 86, 87, 89, 98, 105	climaddc1 15656	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 + 1))
107		0p1e1 12367	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
108	106, 107	breqtrdi 5165	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
109	108	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
110		climres 15596	. . . . . . . . . . . 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 5148	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)
114	67	a1i 11	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ → 1 ∈ ℝ⁺)
115	18	ellogdm 26605	. . . . . . . . . . 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 24849	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ ∖ (-∞(,]0)))‘1))
119		logf1o 26530	. . . . . . . . . . 11 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
120		f1of 6823	. . . . . . . . . . 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 26608	. . . . . . . . . . 11 ⊢ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0})
123	122, 73	sselid 3961	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ_≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖ {0}))
124	121, 123	cofmpt 7127	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
125		frn 6718	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)):(ℤ_≥‘𝑟)⟶(ℂ ∖ (-∞(,]0)) → ran (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖ (-∞(,]0)))
126		cores 6243	. . . . . . . . . 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 6032	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) = (𝑚 ∈ (ℤ_≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))))
129	124, 127, 128	3eqtr4d 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘ (𝑚 ∈ (ℤ_≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)))
130		fvres 6900	. . . . . . . . . 10 ⊢ (1 ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
131	116, 130	mp1i 13	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = (log‘1))
132		log1 26551	. . . . . . . . 9 ⊢ (log‘1) = 0
133	131, 132	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘1) = 0)
134	118, 129, 133	3brtr3d 5155	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾ (ℤ_≥‘𝑟)) ⇝ 0)
135	77	mptex 7220	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V
136		climres 15596	. . . . . . . 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 3148	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)
140	11, 87	addcld 11259	. . . . . 6 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
141	7	dmgmn0 26993	. . . . . 6 ⊢ (𝜑 → (𝐴 + 1) ≠ 0)
142	140, 141	logcld 26536	. . . . 5 ⊢ (𝜑 → (log‘(𝐴 + 1)) ∈ ℂ)
143	77	mptex 7220	. . . . . 6 ⊢ (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V
144	143	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈ V)
145	81	fvoveq1d 7432	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
146		eqid 2736	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))
147		fvex 6894	. . . . . . . 8 ⊢ (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ V
148	145, 146, 147	fvmpt 6991	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
149	148	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
150	97, 93	addcld 11259	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ)
151	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
152	151, 95	dmgmdivn0 26995	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0)
153	150, 152	logcld 26536	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ)
154	149, 153	eqeltrd 2835	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ)
155	145	oveq2d 7426	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
156		eqid 2736	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))
157		ovex 7443	. . . . . . . 8 ⊢ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ V
158	155, 156, 157	fvmpt 6991	. . . . . . 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 7426	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
161	159, 160	eqtr4d 2774	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)))
162	1, 2, 139, 142, 144, 154, 161	climsubc2 15660	. . . 4 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ ((log‘(𝐴 + 1)) − 0))
163	142	subid1d 11588	. . . 4 ⊢ (𝜑 → ((log‘(𝐴 + 1)) − 0) = (log‘(𝐴 + 1)))
164	162, 163	breqtrd 5150	. . 3 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝ (log‘(𝐴 + 1)))
165		elfznn 13575	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
166	165	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
167		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1))
168		id 22	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
169	167, 168	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘))
170	169	fveq2d 6885	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘)))
171	170	oveq2d 7426	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))))
172		oveq2 7418	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘))
173	172	fvoveq1d 7432	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1)))
174	171, 173	oveq12d 7428	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))))
175		ovex 7443	. . . . . . 7 ⊢ (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V
176	174, 3, 175	fvmpt 6991	. . . . . 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 2845	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
179	11	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ)
180		1cnd 11235	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ)
181	179, 180	addcld 11259	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ)
182	166	peano2nnd 12262	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ)
183	182	nnrpd 13054	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℝ⁺)
184	166	nnrpd 13054	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ⁺)
185	183, 184	rpdivcld 13073	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈ ℝ⁺)
186	185	relogcld 26589	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ)
187	186	recnd 11268	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ)
188	181, 187	mulcld 11260	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
189	166	nncnd 12261	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ)
190	166	nnne0d 12295	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0)
191	181, 189, 190	divcld 12022	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ)
192	191, 180	addcld 11259	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ)
193	7	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
194	193, 166	dmgmdivn0 26995	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0)
195	192, 194	logcld 26536	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ)
196	188, 195	subcld 11599	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
197	177, 178, 196	fsumser 15751	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛))
198		fzfid 13996	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
199	198, 196	fsumcl 15754	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
200	197, 199	eqeltrrd 2836	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ)
201	142	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈ ℂ)
202	201, 153	subcld 11599	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) ∈ ℂ)
203	159, 202	eqeltrd 2835	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈ ℂ)
204	179, 187	mulcld 11260	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ)
205	179, 189, 190	divcld 12022	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ)
206	205, 180	addcld 11259	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ)
207	4	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
208	207, 166	dmgmdivn0 26995	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0)
209	206, 208	logcld 26536	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ)
210	204, 209	subcld 11599	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
211	198, 210	fsumcl 15754	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ)
212	199, 211	nncand 11604	. . . . 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 11648	. . . . . . . . 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 11601	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1)
215	214	oveq1d 7425	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘))))
216	181, 179, 187	subdird 11699	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))))
217	187	mullidd 11258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘)))
218	215, 216, 217	3eqtr3d 2779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘)))
219	218	oveq1d 7425	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))))
220	187, 195, 209	subsubd 11627	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))))
221	187, 195	subcld 11599	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ)
222	221, 209	addcomd 11442	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
223	209, 195, 187	subsub2d 11628	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))))
224	182	nncnd 12261	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ)
225	179, 224	addcld 11259	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ)
226	182	nnnn0d 12567	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ₀)
227		dmgmaddn0 26990	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ₀) → (𝐴 + (𝑘 + 1)) ≠ 0)
228	207, 226, 227	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0)
229	225, 228	logcld 26536	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ)
230	183	relogcld 26589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ)
231	230	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ)
232	184	relogcld 26589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ)
233	232	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ)
234	229, 231, 233	nnncan2d 11634	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
235	181, 189, 189, 190	divdird 12060	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)))
236	179, 189, 180	add32d 11468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘))
237	179, 189, 180	addassd 11262	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1)))
238	236, 237	eqtr3d 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1)))
239	238	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘))
240	189, 190	dividd 12020	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1)
241	240	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1))
242	235, 239, 241	3eqtr3rd 2780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘))
243	242	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘)))
244		logdiv2 26583	. . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)))
247	183, 184	relogdivd 26592	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘)))
248	246, 247	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))))
249	182	nnne0d 12295	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0)
250	179, 224, 224, 249	divdird 12060	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))))
251	224, 249	dividd 12020	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1)
252	251	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1))
253	250, 252	eqtr2d 2772	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))
254	253	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))))
255		logdiv2 26583	. . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1))))
258	234, 248, 257	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
259	258	oveq2d 7426	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
260	223, 259	eqtr3d 2773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
261	220, 222, 260	3eqtrd 2775	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
262	213, 219, 261	3eqtrd 2775	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
263	262	sumeq2dv 15723	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))))
264	198, 196, 210	fsumsub 15809	. . . . . . 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 7418	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘))
266	265	fvoveq1d 7432	. . . . . . . . 9 ⊢ (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
267		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1)))
268	267	fvoveq1d 7432	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1)))
269		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1))
270	269	fvoveq1d 7432	. . . . . . . . 9 ⊢ (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1)))
271		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1)))
272	271	fvoveq1d 7432	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1)))
273	91	nnzd 12620	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
274	95, 1	eleqtrdi 2845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ (ℤ_≥‘1))
275	11	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ)
276		elfznn 13575	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
277	276	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
278	277	nncnd 12261	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ)
279	277	nnne0d 12295	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0)
280	275, 278, 279	divcld 12022	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ)
281		1cnd 11235	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈ ℂ)
282	280, 281	addcld 11259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ)
283	4	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
284	283, 277	dmgmdivn0 26995	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0)
285	282, 284	logcld 26536	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ)
286	266, 268, 270, 272, 273, 274, 285	telfsum 15825	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
287	90	div1d 12014	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴)
288	287	fvoveq1d 7432	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1)))
289	288	oveq1d 7425	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
290	286, 289	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
291	263, 264, 290	3eqtr3d 2779	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))))
292	291	oveq2d 7426	. . . . 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 2773	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))))
294	170	oveq2d 7426	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘))))
295		oveq2 7418	. . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘))
296	295	fvoveq1d 7432	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1)))
297	294, 296	oveq12d 7428	. . . . . . 7 ⊢ (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
298		lgamcvg.g	. . . . . . 7 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
299		ovex 7443	. . . . . . 7 ⊢ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V
300	297, 298, 299	fvmpt 6991	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
301	166, 300	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))
302	301, 178, 210	fsumser 15751	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛))
303	159	eqcomd 2742	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))
304	197, 303	oveq12d 7428	. . . 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 2779	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛)))
306	1, 2, 8, 10, 164, 200, 203, 305	climsub 15655	. 2 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))))
307		lgamcl 27008	. . . 4 ⊢ ((𝐴 + 1) ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ)
308	7, 307	syl 17	. . 3 ⊢ (𝜑 → (log Γ‘(𝐴 + 1)) ∈ ℂ)
309	308, 142	pncand 11600	. 2 ⊢ (𝜑 → (((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1))) − (log‘(𝐴 + 1))) = (log Γ‘(𝐴 + 1)))
310	306, 309	breqtrd 5150	1 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∃wrex 3061 Vcvv 3464 ∖ cdif 3928 ⊆ wss 3931 {csn 4606 class class class wbr 5124 ↦ cmpt 5206 ran crn 5660 ↾ cres 5661 ∘ ccom 5663 ⟶wf 6532 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 -∞cmnf 11272 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 / cdiv 11899 ℕcn 12245 ℕ₀cn0 12506 ℤcz 12593 ℤ_≥cuz 12857 ℝ⁺crp 13013 (,]cioc 13368 ...cfz 13529 seqcseq 14024 abscabs 15258 ⇝ cli 15505 Σcsu 15707 ∞Metcxmet 21305 ballcbl 21307 –cn→ccncf 24825 logclog 26520 log Γclgam 26983

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 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212 ax-addf 11213

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-er 8724 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-fi 9428 df-sup 9459 df-inf 9460 df-oi 9529 df-dju 9920 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13371 df-ioc 13372 df-ico 13373 df-icc 13374 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-fac 14297 df-bc 14326 df-hash 14354 df-shft 15091 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-limsup 15492 df-clim 15509 df-rlim 15510 df-sum 15708 df-ef 16088 df-sin 16090 df-cos 16091 df-tan 16092 df-pi 16093 df-struct 17171 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-hom 17300 df-cco 17301 df-rest 17441 df-topn 17442 df-0g 17460 df-gsum 17461 df-topgen 17462 df-pt 17463 df-prds 17466 df-xrs 17521 df-qtop 17526 df-imas 17527 df-xps 17529 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-submnd 18767 df-mulg 19056 df-cntz 19305 df-cmn 19768 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-fbas 21317 df-fg 21318 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-nei 23041 df-lp 23079 df-perf 23080 df-cn 23170 df-cnp 23171 df-haus 23258 df-cmp 23330 df-tx 23505 df-hmeo 23698 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-xms 24264 df-ms 24265 df-tms 24266 df-cncf 24827 df-limc 25824 df-dv 25825 df-ulm 26343 df-log 26522 df-cxp 26523 df-lgam 26986

This theorem is referenced by: lgamp1 27024

W3C validator