Metamath Proof Explorer

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 ( · , 𝐹 ) )