gamcvg2lem

	Ref	Expression
Hypotheses	gamcvg2.f	$⊢ F = (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1})$
	gamcvg2.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
	gamcvg2.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
Assertion	gamcvg2lem	$⊢ φ \to \exp \circ seq 1 (+ G) = seq 1 (\times F)$

Proof

Step	Hyp	Ref	Expression
1		gamcvg2.f	$⊢ F = (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1})$
2		gamcvg2.a	$⊢ φ \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
3		gamcvg2.g	$⊢ G = (m \in ℕ ⟼ A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1))$
4		addcl	$⊢ (n \in ℂ \land x \in ℂ) \to n + x \in ℂ$
5	4	adantl	$⊢ ((φ \land k \in ℕ) \land (n \in ℂ \land x \in ℂ)) \to n + x \in ℂ$
6		simpll	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to φ$
7		elfznn	$⊢ n \in (1 \dots k) \to n \in ℕ$
8	7	adantl	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \in ℕ$
9		oveq1	$⊢ m = n \to m + 1 = n + 1$
10		id	$⊢ m = n \to m = n$
11	9 10	oveq12d	$⊢ m = n \to \frac{m + 1}{m} = \frac{n + 1}{n}$
12	11	fveq2d	$⊢ m = n \to \log (\frac{m + 1}{m}) = \log (\frac{n + 1}{n})$
13	12	oveq2d	$⊢ m = n \to A \log (\frac{m + 1}{m}) = A \log (\frac{n + 1}{n})$
14		oveq2	$⊢ m = n \to \frac{A}{m} = \frac{A}{n}$
15	14	oveq1d	$⊢ m = n \to (\frac{A}{m}) + 1 = (\frac{A}{n}) + 1$
16	15	fveq2d	$⊢ m = n \to \log ((\frac{A}{m}) + 1) = \log ((\frac{A}{n}) + 1)$
17	13 16	oveq12d	$⊢ m = n \to A \log (\frac{m + 1}{m}) - \log ((\frac{A}{m}) + 1) = A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)$
18		ovex	$⊢ A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1) \in V$
19	17 3 18	fvmpt	$⊢ n \in ℕ \to G (n) = A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)$
20	19	adantl	$⊢ (φ \land n \in ℕ) \to G (n) = A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)$
21	2	adantr	$⊢ (φ \land n \in ℕ) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
22	21	eldifad	$⊢ (φ \land n \in ℕ) \to A \in ℂ$
23		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
24	23	peano2nnd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℕ$
25	24	nnrpd	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℝ^{+}$
26	23	nnrpd	$⊢ (φ \land n \in ℕ) \to n \in ℝ^{+}$
27	25 26	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{n + 1}{n} \in ℝ^{+}$
28	27	relogcld	$⊢ (φ \land n \in ℕ) \to \log (\frac{n + 1}{n}) \in ℝ$
29	28	recnd	$⊢ (φ \land n \in ℕ) \to \log (\frac{n + 1}{n}) \in ℂ$
30	22 29	mulcld	$⊢ (φ \land n \in ℕ) \to A \log (\frac{n + 1}{n}) \in ℂ$
31	23	nncnd	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
32	23	nnne0d	$⊢ (φ \land n \in ℕ) \to n \neq 0$
33	22 31 32	divcld	$⊢ (φ \land n \in ℕ) \to \frac{A}{n} \in ℂ$
34		1cnd	$⊢ (φ \land n \in ℕ) \to 1 \in ℂ$
35	33 34	addcld	$⊢ (φ \land n \in ℕ) \to (\frac{A}{n}) + 1 \in ℂ$
36	21 23	dmgmdivn0	$⊢ (φ \land n \in ℕ) \to (\frac{A}{n}) + 1 \neq 0$
37	35 36	logcld	$⊢ (φ \land n \in ℕ) \to \log ((\frac{A}{n}) + 1) \in ℂ$
38	30 37	subcld	$⊢ (φ \land n \in ℕ) \to A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1) \in ℂ$
39	20 38	eqeltrd	$⊢ (φ \land n \in ℕ) \to G (n) \in ℂ$
40	6 8 39	syl2anc	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to G (n) \in ℂ$
41		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
42		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
43	41 42	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
44		efadd	$⊢ (n \in ℂ \land x \in ℂ) \to e^{n + x} = e^{n} e^{x}$
45	44	adantl	$⊢ ((φ \land k \in ℕ) \land (n \in ℂ \land x \in ℂ)) \to e^{n + x} = e^{n} e^{x}$
46		efsub	$⊢ (A \log (\frac{n + 1}{n}) \in ℂ \land \log ((\frac{A}{n}) + 1) \in ℂ) \to e^{A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)} = \frac{e^{A \log (\frac{n + 1}{n})}}{e^{\log ((\frac{A}{n}) + 1)}}$
47	30 37 46	syl2anc	$⊢ (φ \land n \in ℕ) \to e^{A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)} = \frac{e^{A \log (\frac{n + 1}{n})}}{e^{\log ((\frac{A}{n}) + 1)}}$
48	31 34	addcld	$⊢ (φ \land n \in ℕ) \to n + 1 \in ℂ$
49	48 31 32	divcld	$⊢ (φ \land n \in ℕ) \to \frac{n + 1}{n} \in ℂ$
50	24	nnne0d	$⊢ (φ \land n \in ℕ) \to n + 1 \neq 0$
51	48 31 50 32	divne0d	$⊢ (φ \land n \in ℕ) \to \frac{n + 1}{n} \neq 0$
52	49 51 22	cxpefd	$⊢ (φ \land n \in ℕ) \to {(\frac{n + 1}{n})}^{A} = e^{A \log (\frac{n + 1}{n})}$
53	52	eqcomd	$⊢ (φ \land n \in ℕ) \to e^{A \log (\frac{n + 1}{n})} = {(\frac{n + 1}{n})}^{A}$
54		eflog	$⊢ ((\frac{A}{n}) + 1 \in ℂ \land (\frac{A}{n}) + 1 \neq 0) \to e^{\log ((\frac{A}{n}) + 1)} = (\frac{A}{n}) + 1$
55	35 36 54	syl2anc	$⊢ (φ \land n \in ℕ) \to e^{\log ((\frac{A}{n}) + 1)} = (\frac{A}{n}) + 1$
56	53 55	oveq12d	$⊢ (φ \land n \in ℕ) \to \frac{e^{A \log (\frac{n + 1}{n})}}{e^{\log ((\frac{A}{n}) + 1)}} = \frac{{(\frac{n + 1}{n})}^{A}}{(\frac{A}{n}) + 1}$
57	47 56	eqtrd	$⊢ (φ \land n \in ℕ) \to e^{A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)} = \frac{{(\frac{n + 1}{n})}^{A}}{(\frac{A}{n}) + 1}$
58	20	fveq2d	$⊢ (φ \land n \in ℕ) \to e^{G (n)} = e^{A \log (\frac{n + 1}{n}) - \log ((\frac{A}{n}) + 1)}$
59	11	oveq1d	$⊢ m = n \to {(\frac{m + 1}{m})}^{A} = {(\frac{n + 1}{n})}^{A}$
60	59 15	oveq12d	$⊢ m = n \to \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1} = \frac{{(\frac{n + 1}{n})}^{A}}{(\frac{A}{n}) + 1}$
61		ovex	$⊢ \frac{{(\frac{n + 1}{n})}^{A}}{(\frac{A}{n}) + 1} \in V$
62	60 1 61	fvmpt	$⊢ n \in ℕ \to F (n) = \frac{{(\frac{n + 1}{n})}^{A}}{(\frac{A}{n}) + 1}$
63	62	adantl	$⊢ (φ \land n \in ℕ) \to F (n) = \frac{{(\frac{n + 1}{n})}^{A}}{(\frac{A}{n}) + 1}$
64	57 58 63	3eqtr4d	$⊢ (φ \land n \in ℕ) \to e^{G (n)} = F (n)$
65	6 8 64	syl2anc	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to e^{G (n)} = F (n)$
66	5 40 43 45 65	seqhomo	$⊢ (φ \land k \in ℕ) \to e^{seq 1 (+ G) (k)} = seq 1 (\times F) (k)$
67	66	mpteq2dva	$⊢ φ \to (k \in ℕ ⟼ e^{seq 1 (+ G) (k)}) = (k \in ℕ ⟼ seq 1 (\times F) (k))$
68		eff	$⊢ \exp : ℂ ⟶ ℂ$
69	68	a1i	$⊢ φ \to \exp : ℂ ⟶ ℂ$
70		1z	$⊢ 1 \in ℤ$
71	70	a1i	$⊢ φ \to 1 \in ℤ$
72	42 71 39	serf	$⊢ φ \to seq 1 (+ G) : ℕ ⟶ ℂ$
73		fcompt	$⊢ (\exp : ℂ ⟶ ℂ \land seq 1 (+ G) : ℕ ⟶ ℂ) \to \exp \circ seq 1 (+ G) = (k \in ℕ ⟼ e^{seq 1 (+ G) (k)})$
74	69 72 73	syl2anc	$⊢ φ \to \exp \circ seq 1 (+ G) = (k \in ℕ ⟼ e^{seq 1 (+ G) (k)})$
75		seqfn	$⊢ 1 \in ℤ \to seq 1 (\times F) Fn ℤ_{\geq 1}$
76	70 75	mp1i	$⊢ φ \to seq 1 (\times F) Fn ℤ_{\geq 1}$
77	42	fneq2i	$⊢ seq 1 (\times F) Fn ℕ \leftrightarrow seq 1 (\times F) Fn ℤ_{\geq 1}$
78	76 77	sylibr	$⊢ φ \to seq 1 (\times F) Fn ℕ$
79		dffn5	$⊢ seq 1 (\times F) Fn ℕ \leftrightarrow seq 1 (\times F) = (k \in ℕ ⟼ seq 1 (\times F) (k))$
80	78 79	sylib	$⊢ φ \to seq 1 (\times F) = (k \in ℕ ⟼ seq 1 (\times F) (k))$
81	67 74 80	3eqtr4d	$⊢ φ \to \exp \circ seq 1 (+ G) = seq 1 (\times F)$

Metamath Proof Explorer

Theorem gamcvg2lem

Proof