lgamcvg2

Description: The series G converges to log_G ( A + 1 ) . (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Hypotheses	lgamcvg.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
	lgamcvg.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
Assertion	lgamcvg2	$⊢ φ \to seq 1 (+ G) ⇝ \log Γ (A + 1)$

Proof

Step	Hyp	Ref	Expression
1		lgamcvg.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
2		lgamcvg.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4		1zzd	$⊢ φ \to 1 \in ℤ$
5		eqid	$⊢ (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1)) = (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1))$
6		1nn0	$⊢ 1 \in ℕ_{0}$
7	6	a1i	$⊢ φ \to 1 \in ℕ_{0}$
8	2 7	dmgmaddnn0	$⊢ φ \to A + 1 \in (ℂ ∖ (ℤ ∖ ℕ))$
9	5 8	lgamcvg	$⊢ φ \to seq 1 (+ (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1))) ⇝ (\log Γ (A + 1) + \log (A + 1))$
10		seqex	$⊢ seq 1 (+ G) \in V$
11	10	a1i	$⊢ φ \to seq 1 (+ G) \in V$
12	2	eldifad	$⊢ φ \to A \in ℂ$
13	12	abscld	$⊢ φ \to \|A\| \in ℝ$
14		arch	$⊢ \|A\| \in ℝ \to \exists r \in ℕ \|A\| < r$
15	13 14	syl	$⊢ φ \to \exists r \in ℕ \|A\| < r$
16		eqid	$⊢ ℤ_{\geq r} = ℤ_{\geq r}$
17		simprl	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to r \in ℕ$
18	17	nnzd	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to r \in ℤ$
19		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
20	19	logcn	$⊢ ({log ↾}_{(ℂ ∖ (−∞, 0])}) : (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ$
21	20	a1i	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) : (ℂ ∖ (−∞, 0]) \underset{cn}{⟶} ℂ$
22		eqid	$⊢ 1 ball (abs \circ -) 1 = 1 ball (abs \circ -) 1$
23	22	dvlog2lem	$⊢ 1 ball (abs \circ -) 1 \subseteq ℂ ∖ (−∞, 0]$
24	12	ad2antrr	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to A \in ℂ$
25		eluznn	$⊢ (r \in ℕ \land m \in ℤ_{\geq r}) \to m \in ℕ$
26	25	ex	$⊢ r \in ℕ \to (m \in ℤ_{\geq r} \to m \in ℕ)$
27	26	ad2antrl	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (m \in ℤ_{\geq r} \to m \in ℕ)$
28	27	imp	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m \in ℕ$
29	28	nncnd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m \in ℂ$
30		1cnd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to 1 \in ℂ$
31	29 30	addcld	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m + 1 \in ℂ$
32	28	peano2nnd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m + 1 \in ℕ$
33	32	nnne0d	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m + 1 \neq 0$
34	24 31 33	divcld	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \frac{A}{m + 1} \in ℂ$
35	34 30	addcld	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (\frac{A}{m + 1}) + 1 \in ℂ$
36		ax-1cn	$⊢ 1 \in ℂ$
37		eqid	$⊢ abs \circ - = abs \circ -$
38	37	cnmetdval	$⊢ ((\frac{A}{m + 1}) + 1 \in ℂ \land 1 \in ℂ) \to ((\frac{A}{m + 1}) + 1) (abs \circ -) 1 = \|(\frac{A}{m + 1}) + 1 - 1\|$
39	35 36 38	sylancl	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to ((\frac{A}{m + 1}) + 1) (abs \circ -) 1 = \|(\frac{A}{m + 1}) + 1 - 1\|$
40	34 30	pncand	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (\frac{A}{m + 1}) + 1 - 1 = \frac{A}{m + 1}$
41	40	fveq2d	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|(\frac{A}{m + 1}) + 1 - 1\| = \|\frac{A}{m + 1}\|$
42	24 31 33	absdivd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|\frac{A}{m + 1}\| = \frac{\|A\|}{\|m + 1\|}$
43	32	nnred	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m + 1 \in ℝ$
44	32	nnrpd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to m + 1 \in ℝ^{+}$
45	44	rpge0d	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to 0 \leq m + 1$
46	43 45	absidd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|m + 1\| = m + 1$
47	46	oveq2d	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \frac{\|A\|}{\|m + 1\|} = \frac{\|A\|}{m + 1}$
48	42 47	eqtrd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|\frac{A}{m + 1}\| = \frac{\|A\|}{m + 1}$
49	39 41 48	3eqtrd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to ((\frac{A}{m + 1}) + 1) (abs \circ -) 1 = \frac{\|A\|}{m + 1}$
50	13	ad2antrr	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|A\| \in ℝ$
51	17	adantr	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to r \in ℕ$
52	51	nnred	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to r \in ℝ$
53		simplrr	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|A\| < r$
54		eluzle	$⊢ m \in ℤ_{\geq r} \to r \leq m$
55	54	adantl	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to r \leq m$
56		nnleltp1	$⊢ (r \in ℕ \land m \in ℕ) \to (r \leq m \leftrightarrow r < m + 1)$
57	51 28 56	syl2anc	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (r \leq m \leftrightarrow r < m + 1)$
58	55 57	mpbid	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to r < m + 1$
59	50 52 43 53 58	lttrd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|A\| < m + 1$
60	31	mulridd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (m + 1) \cdot 1 = m + 1$
61	59 60	breqtrrd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \|A\| < (m + 1) \cdot 1$
62		1red	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to 1 \in ℝ$
63	50 62 44	ltdivmuld	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (\frac{\|A\|}{m + 1} < 1 \leftrightarrow \|A\| < (m + 1) \cdot 1)$
64	61 63	mpbird	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to \frac{\|A\|}{m + 1} < 1$
65	49 64	eqbrtrd	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to ((\frac{A}{m + 1}) + 1) (abs \circ -) 1 < 1$
66		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
67	66	a1i	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to abs \circ - \in ∞Met (ℂ)$
68		1rp	$⊢ 1 \in ℝ^{+}$
69		rpxr	$⊢ 1 \in ℝ^{+} \to 1 \in ℝ^{*}$
70	68 69	mp1i	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to 1 \in ℝ^{*}$
71		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land 1 \in ℝ^{*}) \land (1 \in ℂ \land (\frac{A}{m + 1}) + 1 \in ℂ)) \to ((\frac{A}{m + 1}) + 1 \in (1 ball (abs \circ -) 1) \leftrightarrow ((\frac{A}{m + 1}) + 1) (abs \circ -) 1 < 1)$
72	67 70 30 35 71	syl22anc	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to ((\frac{A}{m + 1}) + 1 \in (1 ball (abs \circ -) 1) \leftrightarrow ((\frac{A}{m + 1}) + 1) (abs \circ -) 1 < 1)$
73	65 72	mpbird	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (\frac{A}{m + 1}) + 1 \in (1 ball (abs \circ -) 1)$
74	23 73	sselid	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (\frac{A}{m + 1}) + 1 \in (ℂ ∖ (−∞, 0])$
75	74	fmpttd	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) : ℤ_{\geq r} ⟶ ℂ ∖ (−∞, 0]$
76	27	ssrdv	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ℤ_{\geq r} \subseteq ℕ$
77	76	resmptd	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to {(m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ↾}_{ℤ_{\geq r}} = (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1)$
78		nnex	$⊢ ℕ \in V$
79	78	mptex	$⊢ (m \in ℕ ⟼ \frac{A}{m + 1}) \in V$
80	79	a1i	$⊢ φ \to (m \in ℕ ⟼ \frac{A}{m + 1}) \in V$
81		oveq1	$⊢ m = n \to m + 1 = n + 1$
82	81	oveq2d	$⊢ m = n \to \frac{A}{m + 1} = \frac{A}{n + 1}$
83		eqid	$⊢ (m \in ℕ ⟼ \frac{A}{m + 1}) = (m \in ℕ ⟼ \frac{A}{m + 1})$
84		ovex	$⊢ \frac{A}{n + 1} \in V$
85	82 83 84	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ \frac{A}{m + 1}) (n) = \frac{A}{n + 1}$
86	85	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \frac{A}{m + 1}) (n) = \frac{A}{n + 1}$
87	3 4 12 4 80 86	divcnvshft	$⊢ φ \to (m \in ℕ ⟼ \frac{A}{m + 1}) ⇝ 0$
88		1cnd	$⊢ φ \to 1 \in ℂ$
89	78	mptex	$⊢ (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) \in V$
90	89	a1i	$⊢ φ \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) \in V$
91	12	adantr	$⊢ (φ \land n \in ℕ) \to A \in ℂ$
92		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
93	92	nncnd	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
94		1cnd	$⊢ (φ \land n \in ℕ) \to 1 \in ℂ$
95	93 94	addcld	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℂ$
96	92	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
97	96	nnne0d	$⊢ (φ \land n \in ℕ) \to n + 1 \neq 0$
98	91 95 97	divcld	$⊢ (φ \land n \in ℕ) \to \frac{A}{n + 1} \in ℂ$
99	86 98	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \frac{A}{m + 1}) (n) \in ℂ$
100	82	oveq1d	$⊢ m = n \to (\frac{A}{m + 1}) + 1 = (\frac{A}{n + 1}) + 1$
101		eqid	$⊢ (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) = (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1)$
102		ovex	$⊢ (\frac{A}{n + 1}) + 1 \in V$
103	100 101 102	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) (n) = (\frac{A}{n + 1}) + 1$
104	103	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) (n) = (\frac{A}{n + 1}) + 1$
105	86	oveq1d	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \frac{A}{m + 1}) (n) + 1 = (\frac{A}{n + 1}) + 1$
106	104 105	eqtr4d	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) (n) = (m \in ℕ ⟼ \frac{A}{m + 1}) (n) + 1$
107	3 4 87 88 90 99 106	climaddc1	$⊢ φ \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ⇝ (0 + 1)$
108		0p1e1	$⊢ 0 + 1 = 1$
109	107 108	breqtrdi	$⊢ φ \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ⇝ 1$
110	109	adantr	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ⇝ 1$
111		climres	$⊢ (r \in ℤ \land (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) \in V) \to (({(m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ↾}_{ℤ_{\geq r}}) ⇝ 1 \leftrightarrow (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ⇝ 1)$
112	18 89 111	sylancl	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (({(m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ↾}_{ℤ_{\geq r}}) ⇝ 1 \leftrightarrow (m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ⇝ 1)$
113	110 112	mpbird	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({(m \in ℕ ⟼ (\frac{A}{m + 1}) + 1) ↾}_{ℤ_{\geq r}}) ⇝ 1$
114	77 113	eqbrtrrd	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) ⇝ 1$
115	68	a1i	$⊢ 1 \in ℝ \to 1 \in ℝ^{+}$
116	19	ellogdm	$⊢ 1 \in (ℂ ∖ (−∞, 0]) \leftrightarrow (1 \in ℂ \land (1 \in ℝ \to 1 \in ℝ^{+}))$
117	36 115 116	mpbir2an	$⊢ 1 \in (ℂ ∖ (−∞, 0])$
118	117	a1i	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to 1 \in (ℂ ∖ (−∞, 0])$
119	16 18 21 75 114 118	climcncf	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1)) ⇝ ({log ↾}_{(ℂ ∖ (−∞, 0])}) (1)$
120		logf1o	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log$
121		f1of	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to log : ℂ ∖ \{0\} ⟶ ran log$
122	120 121	mp1i	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to log : ℂ ∖ \{0\} ⟶ ran log$
123	19	logdmss	$⊢ ℂ ∖ (−∞, 0] \subseteq ℂ ∖ \{0\}$
124	123 74	sselid	$⊢ ((φ \land (r \in ℕ \land \|A\| < r)) \land m \in ℤ_{\geq r}) \to (\frac{A}{m + 1}) + 1 \in (ℂ ∖ \{0\})$
125	122 124	cofmpt	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to log \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) = (m \in ℤ_{\geq r} ⟼ \log ((\frac{A}{m + 1}) + 1))$
126		frn	$⊢ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) : ℤ_{\geq r} ⟶ ℂ ∖ (−∞, 0] \to ran (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) \subseteq ℂ ∖ (−∞, 0]$
127		cores	$⊢ ran (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) \subseteq ℂ ∖ (−∞, 0] \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) = log \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1)$
128	75 126 127	3syl	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) = log \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1)$
129	76	resmptd	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to {(m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ↾}_{ℤ_{\geq r}} = (m \in ℤ_{\geq r} ⟼ \log ((\frac{A}{m + 1}) + 1))$
130	125 128 129	3eqtr4d	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) \circ (m \in ℤ_{\geq r} ⟼ (\frac{A}{m + 1}) + 1) = {(m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ↾}_{ℤ_{\geq r}}$
131		fvres	$⊢ 1 \in (ℂ ∖ (−∞, 0]) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) (1) = \log 1$
132	117 131	mp1i	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) (1) = \log 1$
133		log1	$⊢ \log 1 = 0$
134	132 133	eqtrdi	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({log ↾}_{(ℂ ∖ (−∞, 0])}) (1) = 0$
135	119 130 134	3brtr3d	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to ({(m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ↾}_{ℤ_{\geq r}}) ⇝ 0$
136	78	mptex	$⊢ (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) \in V$
137		climres	$⊢ (r \in ℤ \land (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) \in V) \to (({(m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ↾}_{ℤ_{\geq r}}) ⇝ 0 \leftrightarrow (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ⇝ 0)$
138	18 136 137	sylancl	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (({(m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ↾}_{ℤ_{\geq r}}) ⇝ 0 \leftrightarrow (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ⇝ 0)$
139	135 138	mpbid	$⊢ (φ \land (r \in ℕ \land \|A\| < r)) \to (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ⇝ 0$
140	15 139	rexlimddv	$⊢ φ \to (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) ⇝ 0$
141	12 88	addcld	$⊢ φ \to A + 1 \in ℂ$
142	8	dmgmn0	$⊢ φ \to A + 1 \neq 0$
143	141 142	logcld	$⊢ φ \to \log (A + 1) \in ℂ$
144	78	mptex	$⊢ (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) \in V$
145	144	a1i	$⊢ φ \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) \in V$
146	82	fvoveq1d	$⊢ m = n \to \log ((\frac{A}{m + 1}) + 1) = \log ((\frac{A}{n + 1}) + 1)$
147		eqid	$⊢ (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) = (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1))$
148		fvex	$⊢ \log ((\frac{A}{n + 1}) + 1) \in V$
149	146 147 148	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) (n) = \log ((\frac{A}{n + 1}) + 1)$
150	149	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) (n) = \log ((\frac{A}{n + 1}) + 1)$
151	98 94	addcld	$⊢ (φ \land n \in ℕ) \to (\frac{A}{n + 1}) + 1 \in ℂ$
152	2	adantr	$⊢ (φ \land n \in ℕ) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
153	152 96	dmgmdivn0	$⊢ (φ \land n \in ℕ) \to (\frac{A}{n + 1}) + 1 \neq 0$
154	151 153	logcld	$⊢ (φ \land n \in ℕ) \to \log ((\frac{A}{n + 1}) + 1) \in ℂ$
155	150 154	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) (n) \in ℂ$
156	146	oveq2d	$⊢ m = n \to \log (A + 1) - \log ((\frac{A}{m + 1}) + 1) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
157		eqid	$⊢ (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) = (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1))$
158		ovex	$⊢ \log (A + 1) - \log ((\frac{A}{n + 1}) + 1) \in V$
159	156 157 158	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
160	159	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
161	150	oveq2d	$⊢ (φ \land n \in ℕ) \to \log (A + 1) - (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) (n) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
162	160 161	eqtr4d	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n) = \log (A + 1) - (m \in ℕ ⟼ \log ((\frac{A}{m + 1}) + 1)) (n)$
163	3 4 140 143 145 155 162	climsubc2	$⊢ φ \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) ⇝ (\log (A + 1) - 0)$
164	143	subid1d	$⊢ φ \to \log (A + 1) - 0 = \log (A + 1)$
165	163 164	breqtrd	$⊢ φ \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) ⇝ \log (A + 1)$
166		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
167	166	adantl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
168		oveq1	$⊢ m = k \to m + 1 = k + 1$
169		id	$⊢ m = k \to m = k$
170	168 169	oveq12d	$⊢ m = k \to \frac{m + 1}{m} = \frac{k + 1}{k}$
171	170	fveq2d	$⊢ m = k \to \log (\frac{m + 1}{m}) = \log (\frac{k + 1}{k})$
172	171	oveq2d	$⊢ m = k \to (A + 1) \log (\frac{m + 1}{m}) = (A + 1) \log (\frac{k + 1}{k})$
173		oveq2	$⊢ m = k \to \frac{A + 1}{m} = \frac{A + 1}{k}$
174	173	fvoveq1d	$⊢ m = k \to \log ((\frac{A + 1}{m}) + 1) = \log ((\frac{A + 1}{k}) + 1)$
175	172 174	oveq12d	$⊢ m = k \to (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1) = (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)$
176		ovex	$⊢ (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) \in V$
177	175 5 176	fvmpt	$⊢ k \in ℕ \to (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1)) (k) = (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)$
178	167 177	syl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1)) (k) = (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)$
179	92 3	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
180	12	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in ℂ$
181		1cnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 1 \in ℂ$
182	180 181	addcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + 1 \in ℂ$
183	167	peano2nnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k + 1 \in ℕ$
184	183	nnrpd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k + 1 \in ℝ^{+}$
185	167	nnrpd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℝ^{+}$
186	184 185	rpdivcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{k + 1}{k} \in ℝ^{+}$
187	186	relogcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) \in ℝ$
188	187	recnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) \in ℂ$
189	182 188	mulcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1) \log (\frac{k + 1}{k}) \in ℂ$
190	167	nncnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℂ$
191	167	nnne0d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \neq 0$
192	182 190 191	divcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{A + 1}{k} \in ℂ$
193	192 181	addcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A + 1}{k}) + 1 \in ℂ$
194	8	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + 1 \in (ℂ ∖ (ℤ ∖ ℕ))$
195	194 167	dmgmdivn0	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A + 1}{k}) + 1 \neq 0$
196	193 195	logcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A + 1}{k}) + 1) \in ℂ$
197	189 196	subcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) \in ℂ$
198	178 179 197	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) = seq 1 (+ (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1))) (n)$
199		fzfid	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \in Fin$
200	199 197	fsumcl	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) \in ℂ$
201	198 200	eqeltrrd	$⊢ (φ \land n \in ℕ) \to seq 1 (+ (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1))) (n) \in ℂ$
202	143	adantr	$⊢ (φ \land n \in ℕ) \to \log (A + 1) \in ℂ$
203	202 154	subcld	$⊢ (φ \land n \in ℕ) \to \log (A + 1) - \log ((\frac{A}{n + 1}) + 1) \in ℂ$
204	160 203	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n) \in ℂ$
205	180 188	mulcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \log (\frac{k + 1}{k}) \in ℂ$
206	180 190 191	divcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{A}{k} \in ℂ$
207	206 181	addcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A}{k}) + 1 \in ℂ$
208	2	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
209	208 167	dmgmdivn0	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A}{k}) + 1 \neq 0$
210	207 209	logcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A}{k}) + 1) \in ℂ$
211	205 210	subcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1) \in ℂ$
212	199 211	fsumcl	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) \in ℂ$
213	200 212	nncand	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - (\sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))) = \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))$
214	189 196 205 210	sub4d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) - (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) = (A + 1) \log (\frac{k + 1}{k}) - A \log (\frac{k + 1}{k}) - (\log ((\frac{A + 1}{k}) + 1) - \log ((\frac{A}{k}) + 1))$
215	180 181	pncan2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + 1 - A = 1$
216	215	oveq1d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1 - A) \log (\frac{k + 1}{k}) = 1 \log (\frac{k + 1}{k})$
217	182 180 188	subdird	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1 - A) \log (\frac{k + 1}{k}) = (A + 1) \log (\frac{k + 1}{k}) - A \log (\frac{k + 1}{k})$
218	188	mullidd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 1 \log (\frac{k + 1}{k}) = \log (\frac{k + 1}{k})$
219	216 217 218	3eqtr3d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1) \log (\frac{k + 1}{k}) - A \log (\frac{k + 1}{k}) = \log (\frac{k + 1}{k})$
220	219	oveq1d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1) \log (\frac{k + 1}{k}) - A \log (\frac{k + 1}{k}) - (\log ((\frac{A + 1}{k}) + 1) - \log ((\frac{A}{k}) + 1)) = \log (\frac{k + 1}{k}) - (\log ((\frac{A + 1}{k}) + 1) - \log ((\frac{A}{k}) + 1))$
221	188 196 210	subsubd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) - (\log ((\frac{A + 1}{k}) + 1) - \log ((\frac{A}{k}) + 1)) = \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) + \log ((\frac{A}{k}) + 1)$
222	188 196	subcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) \in ℂ$
223	222 210	addcomd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) + \log ((\frac{A}{k}) + 1) = \log ((\frac{A}{k}) + 1) + \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)$
224	210 196 188	subsub2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A}{k}) + 1) - (\log ((\frac{A + 1}{k}) + 1) - \log (\frac{k + 1}{k})) = \log ((\frac{A}{k}) + 1) + \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)$
225	183	nncnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k + 1 \in ℂ$
226	180 225	addcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + k + 1 \in ℂ$
227	183	nnnn0d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k + 1 \in ℕ_{0}$
228		dmgmaddn0	$⊢ (A \in (ℂ ∖ (ℤ ∖ ℕ)) \land k + 1 \in ℕ_{0}) \to A + k + 1 \neq 0$
229	208 227 228	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + k + 1 \neq 0$
230	226 229	logcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (A + k + 1) \in ℂ$
231	184	relogcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (k + 1) \in ℝ$
232	231	recnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (k + 1) \in ℂ$
233	185	relogcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log k \in ℝ$
234	233	recnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log k \in ℂ$
235	230 232 234	nnncan2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (A + k + 1) - \log k - (\log (k + 1) - \log k) = \log (A + k + 1) - \log (k + 1)$
236	182 190 190 191	divdird	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{A + 1 + k}{k} = (\frac{A + 1}{k}) + (\frac{k}{k})$
237	180 190 181	add32d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + k + 1 = A + 1 + k$
238	180 190 181	addassd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + k + 1 = A + k + 1$
239	237 238	eqtr3d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A + 1 + k = A + k + 1$
240	239	oveq1d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{A + 1 + k}{k} = \frac{A + k + 1}{k}$
241	190 191	dividd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{k}{k} = 1$
242	241	oveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A + 1}{k}) + (\frac{k}{k}) = (\frac{A + 1}{k}) + 1$
243	236 240 242	3eqtr3rd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A + 1}{k}) + 1 = \frac{A + k + 1}{k}$
244	243	fveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A + 1}{k}) + 1) = \log (\frac{A + k + 1}{k})$
245		logdiv2	$⊢ (A + k + 1 \in ℂ \land A + k + 1 \neq 0 \land k \in ℝ^{+}) \to \log (\frac{A + k + 1}{k}) = \log (A + k + 1) - \log k$
246	226 229 185 245	syl3anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{A + k + 1}{k}) = \log (A + k + 1) - \log k$
247	244 246	eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A + 1}{k}) + 1) = \log (A + k + 1) - \log k$
248	184 185	relogdivd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) = \log (k + 1) - \log k$
249	247 248	oveq12d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A + 1}{k}) + 1) - \log (\frac{k + 1}{k}) = \log (A + k + 1) - \log k - (\log (k + 1) - \log k)$
250	183	nnne0d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k + 1 \neq 0$
251	180 225 225 250	divdird	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{A + k + 1}{k + 1} = (\frac{A}{k + 1}) + (\frac{k + 1}{k + 1})$
252	225 250	dividd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \frac{k + 1}{k + 1} = 1$
253	252	oveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A}{k + 1}) + (\frac{k + 1}{k + 1}) = (\frac{A}{k + 1}) + 1$
254	251 253	eqtr2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (\frac{A}{k + 1}) + 1 = \frac{A + k + 1}{k + 1}$
255	254	fveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A}{k + 1}) + 1) = \log (\frac{A + k + 1}{k + 1})$
256		logdiv2	$⊢ (A + k + 1 \in ℂ \land A + k + 1 \neq 0 \land k + 1 \in ℝ^{+}) \to \log (\frac{A + k + 1}{k + 1}) = \log (A + k + 1) - \log (k + 1)$
257	226 229 184 256	syl3anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{A + k + 1}{k + 1}) = \log (A + k + 1) - \log (k + 1)$
258	255 257	eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A}{k + 1}) + 1) = \log (A + k + 1) - \log (k + 1)$
259	235 249 258	3eqtr4d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A + 1}{k}) + 1) - \log (\frac{k + 1}{k}) = \log ((\frac{A}{k + 1}) + 1)$
260	259	oveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A}{k}) + 1) - (\log ((\frac{A + 1}{k}) + 1) - \log (\frac{k + 1}{k})) = \log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1)$
261	224 260	eqtr3d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log ((\frac{A}{k}) + 1) + \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) = \log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1)$
262	221 223 261	3eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to \log (\frac{k + 1}{k}) - (\log ((\frac{A + 1}{k}) + 1) - \log ((\frac{A}{k}) + 1)) = \log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1)$
263	214 220 262	3eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) - (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) = \log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1)$
264	263	sumeq2dv	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) - (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))) = \sum_{k = 1}^{n} (\log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1))$
265	199 197 211	fsumsub	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1) - (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))) = \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))$
266		oveq2	$⊢ x = k \to \frac{A}{x} = \frac{A}{k}$
267	266	fvoveq1d	$⊢ x = k \to \log ((\frac{A}{x}) + 1) = \log ((\frac{A}{k}) + 1)$
268		oveq2	$⊢ x = k + 1 \to \frac{A}{x} = \frac{A}{k + 1}$
269	268	fvoveq1d	$⊢ x = k + 1 \to \log ((\frac{A}{x}) + 1) = \log ((\frac{A}{k + 1}) + 1)$
270		oveq2	$⊢ x = 1 \to \frac{A}{x} = \frac{A}{1}$
271	270	fvoveq1d	$⊢ x = 1 \to \log ((\frac{A}{x}) + 1) = \log ((\frac{A}{1}) + 1)$
272		oveq2	$⊢ x = n + 1 \to \frac{A}{x} = \frac{A}{n + 1}$
273	272	fvoveq1d	$⊢ x = n + 1 \to \log ((\frac{A}{x}) + 1) = \log ((\frac{A}{n + 1}) + 1)$
274	92	nnzd	$⊢ (φ \land n \in ℕ) \to n \in ℤ$
275	96 3	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℤ_{\geq 1}$
276	12	ad2antrr	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to A \in ℂ$
277		elfznn	$⊢ x \in (1 \dots n + 1) \to x \in ℕ$
278	277	adantl	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to x \in ℕ$
279	278	nncnd	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to x \in ℂ$
280	278	nnne0d	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to x \neq 0$
281	276 279 280	divcld	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to \frac{A}{x} \in ℂ$
282		1cnd	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to 1 \in ℂ$
283	281 282	addcld	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to (\frac{A}{x}) + 1 \in ℂ$
284	2	ad2antrr	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
285	284 278	dmgmdivn0	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to (\frac{A}{x}) + 1 \neq 0$
286	283 285	logcld	$⊢ ((φ \land n \in ℕ) \land x \in (1 \dots n + 1)) \to \log ((\frac{A}{x}) + 1) \in ℂ$
287	267 269 271 273 274 275 286	telfsum	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (\log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1)) = \log ((\frac{A}{1}) + 1) - \log ((\frac{A}{n + 1}) + 1)$
288	91	div1d	$⊢ (φ \land n \in ℕ) \to \frac{A}{1} = A$
289	288	fvoveq1d	$⊢ (φ \land n \in ℕ) \to \log ((\frac{A}{1}) + 1) = \log (A + 1)$
290	289	oveq1d	$⊢ (φ \land n \in ℕ) \to \log ((\frac{A}{1}) + 1) - \log ((\frac{A}{n + 1}) + 1) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
291	287 290	eqtrd	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (\log ((\frac{A}{k}) + 1) - \log ((\frac{A}{k + 1}) + 1)) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
292	264 265 291	3eqtr3d	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) = \log (A + 1) - \log ((\frac{A}{n + 1}) + 1)$
293	292	oveq2d	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - (\sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1))) = \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - (\log (A + 1) - \log ((\frac{A}{n + 1}) + 1))$
294	213 293	eqtr3d	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) = \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - (\log (A + 1) - \log ((\frac{A}{n + 1}) + 1))$
295	171	oveq2d	$⊢ m = k \to A \log (\frac{m + 1}{m}) = A \log (\frac{k + 1}{k})$
296		oveq2	$⊢ m = k \to \frac{A}{m} = \frac{A}{k}$
297	296	fvoveq1d	$⊢ m = k \to \log ((\frac{A}{m}) + 1) = \log ((\frac{A}{k}) + 1)$
298	295 297	oveq12d	$⊢ m = k \to A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
299		ovex	$⊢ A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1) \in V$
300	298 1 299	fvmpt	$⊢ k \in ℕ \to G (k) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
301	167 300	syl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to G (k) = A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)$
302	301 179 211	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (A \log (\frac{k + 1}{k}) - \log ((\frac{A}{k}) + 1)) = seq 1 (+ G) (n)$
303	160	eqcomd	$⊢ (φ \land n \in ℕ) \to \log (A + 1) - \log ((\frac{A}{n + 1}) + 1) = (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n)$
304	198 303	oveq12d	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} ((A + 1) \log (\frac{k + 1}{k}) - \log ((\frac{A + 1}{k}) + 1)) - (\log (A + 1) - \log ((\frac{A}{n + 1}) + 1)) = seq 1 (+ (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1))) (n) - (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n)$
305	294 302 304	3eqtr3d	$⊢ (φ \land n \in ℕ) \to seq 1 (+ G) (n) = seq 1 (+ (m \in ℕ ⟼ (A + 1) \log (\frac{m + 1}{m}) - \log ((\frac{A + 1}{m}) + 1))) (n) - (m \in ℕ ⟼ \log (A + 1) - \log ((\frac{A}{m + 1}) + 1)) (n)$
306	3 4 9 11 165 201 204 305	climsub	$⊢ φ \to seq 1 (+ G) ⇝ (\log Γ (A + 1) + \log (A + 1) - \log (A + 1))$
307		lgamcl	$⊢ A + 1 \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (A + 1) \in ℂ$
308	8 307	syl	$⊢ φ \to \log Γ (A + 1) \in ℂ$
309	308 143	pncand	$⊢ φ \to \log Γ (A + 1) + \log (A + 1) - \log (A + 1) = \log Γ (A + 1)$
310	306 309	breqtrd	$⊢ φ \to seq 1 (+ G) ⇝ \log Γ (A + 1)$

Metamath Proof Explorer

Theorem lgamcvg2

Proof