# Metamath Proof Explorer

## Theorem stirlinglem8

Description: If A converges to C , then F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem8.1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
stirlinglem8.2 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
stirlinglem8.3 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{D}$
stirlinglem8.4 ${⊢}{D}=\left({n}\in ℕ⟼{A}\left(2{n}\right)\right)$
stirlinglem8.5 ${⊢}{\phi }\to {A}:ℕ⟶{ℝ}^{+}$
stirlinglem8.6 ${⊢}{F}=\left({n}\in ℕ⟼\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}\right)$
stirlinglem8.7 ${⊢}{L}=\left({n}\in ℕ⟼{{A}\left({n}\right)}^{4}\right)$
stirlinglem8.8 ${⊢}{M}=\left({n}\in ℕ⟼{{D}\left({n}\right)}^{2}\right)$
stirlinglem8.9 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right)\in {ℝ}^{+}$
stirlinglem8.10 ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
stirlinglem8.11 ${⊢}{\phi }\to {A}⇝{C}$
Assertion stirlinglem8 ${⊢}{\phi }\to {F}⇝{{C}}^{2}$

### Proof

Step Hyp Ref Expression
1 stirlinglem8.1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
2 stirlinglem8.2 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
3 stirlinglem8.3 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{D}$
4 stirlinglem8.4 ${⊢}{D}=\left({n}\in ℕ⟼{A}\left(2{n}\right)\right)$
5 stirlinglem8.5 ${⊢}{\phi }\to {A}:ℕ⟶{ℝ}^{+}$
6 stirlinglem8.6 ${⊢}{F}=\left({n}\in ℕ⟼\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}\right)$
7 stirlinglem8.7 ${⊢}{L}=\left({n}\in ℕ⟼{{A}\left({n}\right)}^{4}\right)$
8 stirlinglem8.8 ${⊢}{M}=\left({n}\in ℕ⟼{{D}\left({n}\right)}^{2}\right)$
9 stirlinglem8.9 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right)\in {ℝ}^{+}$
10 stirlinglem8.10 ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
11 stirlinglem8.11 ${⊢}{\phi }\to {A}⇝{C}$
12 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{{A}\left({n}\right)}^{4}\right)$
13 7 12 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{L}$
14 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{{D}\left({n}\right)}^{2}\right)$
15 8 14 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{M}$
16 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}\right)$
17 6 16 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{F}$
18 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
19 1zzd ${⊢}{\phi }\to 1\in ℤ$
20 rrpsscn ${⊢}{ℝ}^{+}\subseteq ℂ$
21 fss ${⊢}\left({A}:ℕ⟶{ℝ}^{+}\wedge {ℝ}^{+}\subseteq ℂ\right)\to {A}:ℕ⟶ℂ$
22 5 20 21 sylancl ${⊢}{\phi }\to {A}:ℕ⟶ℂ$
23 4nn0 ${⊢}4\in {ℕ}_{0}$
24 23 a1i ${⊢}{\phi }\to 4\in {ℕ}_{0}$
25 nnex ${⊢}ℕ\in \mathrm{V}$
26 25 mptex ${⊢}\left({n}\in ℕ⟼{{A}\left({n}\right)}^{4}\right)\in \mathrm{V}$
27 7 26 eqeltri ${⊢}{L}\in \mathrm{V}$
28 27 a1i ${⊢}{\phi }\to {L}\in \mathrm{V}$
29 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
30 5 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\left({n}\right)\in {ℝ}^{+}$
31 30 rpcnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\left({n}\right)\in ℂ$
32 23 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 4\in {ℕ}_{0}$
33 31 32 expcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{A}\left({n}\right)}^{4}\in ℂ$
34 7 fvmpt2 ${⊢}\left({n}\in ℕ\wedge {{A}\left({n}\right)}^{4}\in ℂ\right)\to {L}\left({n}\right)={{A}\left({n}\right)}^{4}$
35 29 33 34 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {L}\left({n}\right)={{A}\left({n}\right)}^{4}$
36 1 2 13 18 19 22 11 24 28 35 climexp ${⊢}{\phi }\to {L}⇝{{C}}^{4}$
37 25 mptex ${⊢}\left({n}\in ℕ⟼\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}\right)\in \mathrm{V}$
38 6 37 eqeltri ${⊢}{F}\in \mathrm{V}$
39 38 a1i ${⊢}{\phi }\to {F}\in \mathrm{V}$
40 22 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}:ℕ⟶ℂ$
41 2nn ${⊢}2\in ℕ$
42 41 a1i ${⊢}{n}\in ℕ\to 2\in ℕ$
43 id ${⊢}{n}\in ℕ\to {n}\in ℕ$
44 42 43 nnmulcld ${⊢}{n}\in ℕ\to 2{n}\in ℕ$
45 44 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 2{n}\in ℕ$
46 40 45 ffvelrnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\left(2{n}\right)\in ℂ$
47 1 46 4 fmptdf ${⊢}{\phi }\to {D}:ℕ⟶ℂ$
48 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼2{n}\right)$
49 fex ${⊢}\left({A}:ℕ⟶ℂ\wedge ℕ\in \mathrm{V}\right)\to {A}\in \mathrm{V}$
50 22 25 49 sylancl ${⊢}{\phi }\to {A}\in \mathrm{V}$
51 1nn ${⊢}1\in ℕ$
52 2cnd ${⊢}{\phi }\to 2\in ℂ$
53 1cnd ${⊢}{\phi }\to 1\in ℂ$
54 52 53 mulcld ${⊢}{\phi }\to 2\cdot 1\in ℂ$
55 oveq2 ${⊢}{n}=1\to 2{n}=2\cdot 1$
56 eqid ${⊢}\left({n}\in ℕ⟼2{n}\right)=\left({n}\in ℕ⟼2{n}\right)$
57 55 56 fvmptg ${⊢}\left(1\in ℕ\wedge 2\cdot 1\in ℂ\right)\to \left({n}\in ℕ⟼2{n}\right)\left(1\right)=2\cdot 1$
58 51 54 57 sylancr ${⊢}{\phi }\to \left({n}\in ℕ⟼2{n}\right)\left(1\right)=2\cdot 1$
59 41 a1i ${⊢}{\phi }\to 2\in ℕ$
60 51 a1i ${⊢}{\phi }\to 1\in ℕ$
61 59 60 nnmulcld ${⊢}{\phi }\to 2\cdot 1\in ℕ$
62 58 61 eqeltrd ${⊢}{\phi }\to \left({n}\in ℕ⟼2{n}\right)\left(1\right)\in ℕ$
63 1red ${⊢}{n}\in ℕ\to 1\in ℝ$
64 42 nnred ${⊢}{n}\in ℕ\to 2\in ℝ$
65 44 nnred ${⊢}{n}\in ℕ\to 2{n}\in ℝ$
66 42 nnge1d ${⊢}{n}\in ℕ\to 1\le 2$
67 63 64 65 66 leadd2dd ${⊢}{n}\in ℕ\to 2{n}+1\le 2{n}+2$
68 56 fvmpt2 ${⊢}\left({n}\in ℕ\wedge 2{n}\in ℕ\right)\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)=2{n}$
69 44 68 mpdan ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)=2{n}$
70 69 oveq1d ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1=2{n}+1$
71 oveq2 ${⊢}{n}={k}\to 2{n}=2{k}$
72 71 cbvmptv ${⊢}\left({n}\in ℕ⟼2{n}\right)=\left({k}\in ℕ⟼2{k}\right)$
73 72 a1i ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)=\left({k}\in ℕ⟼2{k}\right)$
74 simpr ${⊢}\left({n}\in ℕ\wedge {k}={n}+1\right)\to {k}={n}+1$
75 74 oveq2d ${⊢}\left({n}\in ℕ\wedge {k}={n}+1\right)\to 2{k}=2\left({n}+1\right)$
76 peano2nn ${⊢}{n}\in ℕ\to {n}+1\in ℕ$
77 42 76 nnmulcld ${⊢}{n}\in ℕ\to 2\left({n}+1\right)\in ℕ$
78 73 75 76 77 fvmptd ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)=2\left({n}+1\right)$
79 2cnd ${⊢}{n}\in ℕ\to 2\in ℂ$
80 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
81 1cnd ${⊢}{n}\in ℕ\to 1\in ℂ$
82 79 80 81 adddid ${⊢}{n}\in ℕ\to 2\left({n}+1\right)=2{n}+2\cdot 1$
83 79 mulid1d ${⊢}{n}\in ℕ\to 2\cdot 1=2$
84 83 oveq2d ${⊢}{n}\in ℕ\to 2{n}+2\cdot 1=2{n}+2$
85 78 82 84 3eqtrd ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)=2{n}+2$
86 67 70 85 3brtr4d ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\le \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)$
87 44 nnzd ${⊢}{n}\in ℕ\to 2{n}\in ℤ$
88 69 87 eqeltrd ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)\in ℤ$
89 88 peano2zd ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\in ℤ$
90 77 nnzd ${⊢}{n}\in ℕ\to 2\left({n}+1\right)\in ℤ$
91 78 90 eqeltrd ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\in ℤ$
92 eluz ${⊢}\left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\in ℤ\wedge \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\in ℤ\right)\to \left(\left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\in {ℤ}_{\ge \left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\right)}↔\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\le \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\right)$
93 89 91 92 syl2anc ${⊢}{n}\in ℕ\to \left(\left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\in {ℤ}_{\ge \left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\right)}↔\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\le \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\right)$
94 86 93 mpbird ${⊢}{n}\in ℕ\to \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\in {ℤ}_{\ge \left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\right)}$
95 94 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({n}\in ℕ⟼2{n}\right)\left({n}+1\right)\in {ℤ}_{\ge \left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)+1\right)}$
96 25 mptex ${⊢}\left({n}\in ℕ⟼{A}\left(2{n}\right)\right)\in \mathrm{V}$
97 4 96 eqeltri ${⊢}{D}\in \mathrm{V}$
98 97 a1i ${⊢}{\phi }\to {D}\in \mathrm{V}$
99 4 fvmpt2 ${⊢}\left({n}\in ℕ\wedge {A}\left(2{n}\right)\in ℂ\right)\to {D}\left({n}\right)={A}\left(2{n}\right)$
100 29 46 99 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right)={A}\left(2{n}\right)$
101 69 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({n}\in ℕ⟼2{n}\right)\left({n}\right)=2{n}$
102 101 eqcomd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 2{n}=\left({n}\in ℕ⟼2{n}\right)\left({n}\right)$
103 102 fveq2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\left(2{n}\right)={A}\left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)\right)$
104 100 103 eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right)={A}\left(\left({n}\in ℕ⟼2{n}\right)\left({n}\right)\right)$
105 1 2 3 48 18 19 50 31 11 62 95 98 104 climsuse ${⊢}{\phi }\to {D}⇝{C}$
106 2nn0 ${⊢}2\in {ℕ}_{0}$
107 106 a1i ${⊢}{\phi }\to 2\in {ℕ}_{0}$
108 25 mptex ${⊢}\left({n}\in ℕ⟼{{D}\left({n}\right)}^{2}\right)\in \mathrm{V}$
109 8 108 eqeltri ${⊢}{M}\in \mathrm{V}$
110 109 a1i ${⊢}{\phi }\to {M}\in \mathrm{V}$
111 9 rpcnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right)\in ℂ$
112 111 sqcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{D}\left({n}\right)}^{2}\in ℂ$
113 8 fvmpt2 ${⊢}\left({n}\in ℕ\wedge {{D}\left({n}\right)}^{2}\in ℂ\right)\to {M}\left({n}\right)={{D}\left({n}\right)}^{2}$
114 29 112 113 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({n}\right)={{D}\left({n}\right)}^{2}$
115 1 3 15 18 19 47 105 107 110 114 climexp ${⊢}{\phi }\to {M}⇝{{C}}^{2}$
116 10 rpcnd ${⊢}{\phi }\to {C}\in ℂ$
117 10 rpne0d ${⊢}{\phi }\to {C}\ne 0$
118 2z ${⊢}2\in ℤ$
119 118 a1i ${⊢}{\phi }\to 2\in ℤ$
120 116 117 119 expne0d ${⊢}{\phi }\to {{C}}^{2}\ne 0$
121 1 33 7 fmptdf ${⊢}{\phi }\to {L}:ℕ⟶ℂ$
122 121 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {L}\left({n}\right)\in ℂ$
123 114 112 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({n}\right)\in ℂ$
124 100 oveq1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{D}\left({n}\right)}^{2}={{A}\left(2{n}\right)}^{2}$
125 114 124 eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({n}\right)={{A}\left(2{n}\right)}^{2}$
126 100 9 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\left(2{n}\right)\in {ℝ}^{+}$
127 118 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 2\in ℤ$
128 126 127 rpexpcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{A}\left(2{n}\right)}^{2}\in {ℝ}^{+}$
129 125 128 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({n}\right)\in {ℝ}^{+}$
130 129 rpne0d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({n}\right)\ne 0$
131 130 neneqd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ¬{M}\left({n}\right)=0$
132 0cn ${⊢}0\in ℂ$
133 elsn2g ${⊢}0\in ℂ\to \left({M}\left({n}\right)\in \left\{0\right\}↔{M}\left({n}\right)=0\right)$
134 132 133 ax-mp ${⊢}{M}\left({n}\right)\in \left\{0\right\}↔{M}\left({n}\right)=0$
135 131 134 sylnibr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ¬{M}\left({n}\right)\in \left\{0\right\}$
136 123 135 eldifd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\left({n}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
137 32 nn0zd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 4\in ℤ$
138 30 137 rpexpcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{A}\left({n}\right)}^{4}\in {ℝ}^{+}$
139 9 127 rpexpcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{D}\left({n}\right)}^{2}\in {ℝ}^{+}$
140 138 139 rpdivcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}\in {ℝ}^{+}$
141 6 fvmpt2 ${⊢}\left({n}\in ℕ\wedge \frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}\in {ℝ}^{+}\right)\to {F}\left({n}\right)=\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}$
142 29 140 141 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)=\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}$
143 7 fvmpt2 ${⊢}\left({n}\in ℕ\wedge {{A}\left({n}\right)}^{4}\in {ℝ}^{+}\right)\to {L}\left({n}\right)={{A}\left({n}\right)}^{4}$
144 29 138 143 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {L}\left({n}\right)={{A}\left({n}\right)}^{4}$
145 144 114 oveq12d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{L}\left({n}\right)}{{M}\left({n}\right)}=\frac{{{A}\left({n}\right)}^{4}}{{{D}\left({n}\right)}^{2}}$
146 142 145 eqtr4d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}\left({n}\right)=\frac{{L}\left({n}\right)}{{M}\left({n}\right)}$
147 1 13 15 17 18 19 36 39 115 120 122 136 146 climdivf ${⊢}{\phi }\to {F}⇝\left(\frac{{{C}}^{4}}{{{C}}^{2}}\right)$
148 2cn ${⊢}2\in ℂ$
149 2p2e4 ${⊢}2+2=4$
150 148 148 149 mvlladdi ${⊢}2=4-2$
151 150 a1i ${⊢}{\phi }\to 2=4-2$
152 151 oveq2d ${⊢}{\phi }\to {{C}}^{2}={{C}}^{4-2}$
153 24 nn0zd ${⊢}{\phi }\to 4\in ℤ$
154 116 117 119 153 expsubd ${⊢}{\phi }\to {{C}}^{4-2}=\frac{{{C}}^{4}}{{{C}}^{2}}$
155 152 154 eqtrd ${⊢}{\phi }\to {{C}}^{2}=\frac{{{C}}^{4}}{{{C}}^{2}}$
156 147 155 breqtrrd ${⊢}{\phi }\to {F}⇝{{C}}^{2}$