Theorem gamcvg2lem

Description: Lemma for gamcvg2 . (Contributed by Mario Carneiro, 10-Jul-2017)

	Ref	Expression
Hypotheses	gamcvg2.f	⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) )
	gamcvg2.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
	gamcvg2.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
Assertion	gamcvg2lem	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , 𝐺 ) ) = seq 1 ( · , 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		gamcvg2.f	⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) )
2		gamcvg2.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3		gamcvg2.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
4		addcl	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑛 + 𝑥 ) ∈ ℂ )
5	4	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑛 + 𝑥 ) ∈ ℂ )
6		simpll	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝜑 )
7		elfznn	⊢ ( 𝑛 ∈ ( 1 ... 𝑘 ) → 𝑛 ∈ ℕ )
8	7	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℕ )
9		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
10		id	⊢ ( 𝑚 = 𝑛 → 𝑚 = 𝑛 )
11	9 10	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 + 1 ) / 𝑚 ) = ( ( 𝑛 + 1 ) / 𝑛 ) )
12	11	fveq2d	⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) = ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
13	12	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
14		oveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐴 / 𝑚 ) = ( 𝐴 / 𝑛 ) )
15	14	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 / 𝑚 ) + 1 ) = ( ( 𝐴 / 𝑛 ) + 1 ) )
16	15	fveq2d	⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) = ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) )
17	13 16	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) )
18		ovex	⊢ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ∈ V
19	17 3 18	fvmpt	⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) )
21	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
22	21	eldifad	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℂ )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
24	23	peano2nnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
25	24	nnrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℝ+ )
26	23	nnrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ+ )
27	25 26	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / 𝑛 ) ∈ ℝ+ )
28	27	relogcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℝ )
29	28	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℂ )
30	22 29	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ∈ ℂ )
31	23	nncnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
32	23	nnne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
33	22 31 32	divcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 / 𝑛 ) ∈ ℂ )
34		1cnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℂ )
35	33 34	addcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 / 𝑛 ) + 1 ) ∈ ℂ )
36	21 23	dmgmdivn0	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 / 𝑛 ) + 1 ) ≠ 0 )
37	35 36	logcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ∈ ℂ )
38	30 37	subcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ∈ ℂ )
39	20 38	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ )
40	6 8 39	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ )
41		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
42		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
43	41 42	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
44		efadd	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( exp ‘ ( 𝑛 + 𝑥 ) ) = ( ( exp ‘ 𝑛 ) · ( exp ‘ 𝑥 ) ) )
45	44	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( exp ‘ ( 𝑛 + 𝑥 ) ) = ( ( exp ‘ 𝑛 ) · ( exp ‘ 𝑥 ) ) )
46		efsub	⊢ ( ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ∈ ℂ ∧ ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ∈ ℂ ) → ( exp ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) = ( ( exp ‘ ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) / ( exp ‘ ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) )
47	30 37 46	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( exp ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) = ( ( exp ‘ ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) / ( exp ‘ ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) )
48	31 34	addcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℂ )
49	48 31 32	divcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / 𝑛 ) ∈ ℂ )
50	24	nnne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ≠ 0 )
51	48 31 50 32	divne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / 𝑛 ) ≠ 0 )
52	49 51 22	cxpefd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) )
53	52	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( exp ‘ ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) = ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) )
54		eflog	⊢ ( ( ( ( 𝐴 / 𝑛 ) + 1 ) ∈ ℂ ∧ ( ( 𝐴 / 𝑛 ) + 1 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) = ( ( 𝐴 / 𝑛 ) + 1 ) )
55	35 36 54	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( exp ‘ ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) = ( ( 𝐴 / 𝑛 ) + 1 ) )
56	53 55	oveq12d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( exp ‘ ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) / ( exp ‘ ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) = ( ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑛 ) + 1 ) ) )
57	47 56	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( exp ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) = ( ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑛 ) + 1 ) ) )
58	20	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( exp ‘ ( 𝐺 ‘ 𝑛 ) ) = ( exp ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑛 ) + 1 ) ) ) ) )
59	11	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) = ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) )
60	59 15	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) = ( ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑛 ) + 1 ) ) )
61		ovex	⊢ ( ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑛 ) + 1 ) ) ∈ V
62	60 1 61	fvmpt	⊢ ( 𝑛 ∈ ℕ → ( 𝐹 ‘ 𝑛 ) = ( ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑛 ) + 1 ) ) )
63	62	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( ( ( 𝑛 + 1 ) / 𝑛 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑛 ) + 1 ) ) )
64	57 58 63	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( exp ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) )
65	6 8 64	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( exp ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 𝐹 ‘ 𝑛 ) )
66	5 40 43 45 65	seqhomo	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( exp ‘ ( seq 1 ( + , 𝐺 ) ‘ 𝑘 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
67	66	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( exp ‘ ( seq 1 ( + , 𝐺 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
68		eff	⊢ exp : ℂ ⟶ ℂ
69	68	a1i	⊢ ( 𝜑 → exp : ℂ ⟶ ℂ )
70		1z	⊢ 1 ∈ ℤ
71	70	a1i	⊢ ( 𝜑 → 1 ∈ ℤ )
72	42 71 39	serf	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℂ )
73		fcompt	⊢ ( ( exp : ℂ ⟶ ℂ ∧ seq 1 ( + , 𝐺 ) : ℕ ⟶ ℂ ) → ( exp ∘ seq 1 ( + , 𝐺 ) ) = ( 𝑘 ∈ ℕ ↦ ( exp ‘ ( seq 1 ( + , 𝐺 ) ‘ 𝑘 ) ) ) )
74	69 72 73	syl2anc	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , 𝐺 ) ) = ( 𝑘 ∈ ℕ ↦ ( exp ‘ ( seq 1 ( + , 𝐺 ) ‘ 𝑘 ) ) ) )
75		seqfn	⊢ ( 1 ∈ ℤ → seq 1 ( · , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
76	70 75	mp1i	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
77	42	fneq2i	⊢ ( seq 1 ( · , 𝐹 ) Fn ℕ ↔ seq 1 ( · , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
78	76 77	sylibr	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) Fn ℕ )
79		dffn5	⊢ ( seq 1 ( · , 𝐹 ) Fn ℕ ↔ seq 1 ( · , 𝐹 ) = ( 𝑘 ∈ ℕ ↦ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
80	78 79	sylib	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) = ( 𝑘 ∈ ℕ ↦ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
81	67 74 80	3eqtr4d	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , 𝐺 ) ) = seq 1 ( · , 𝐹 ) )