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 φ$
	stirlinglem8.2	$⊢ \underline{Ⅎ} n A$
	stirlinglem8.3	$⊢ \underline{Ⅎ} n D$
	stirlinglem8.4	$⊢ D = (n \in ℕ ⟼ A (2 n))$
	stirlinglem8.5	$⊢ φ \to A : ℕ ⟶ ℝ^{+}$
	stirlinglem8.6	$⊢ F = (n \in ℕ ⟼ \frac{{A (n)}^{4}}{{D (n)}^{2}})$
	stirlinglem8.7	$⊢ L = (n \in ℕ ⟼ {A (n)}^{4})$
	stirlinglem8.8	$⊢ M = (n \in ℕ ⟼ {D (n)}^{2})$
	stirlinglem8.9	$⊢ (φ \land n \in ℕ) \to D (n) \in ℝ^{+}$
	stirlinglem8.10	$⊢ φ \to C \in ℝ^{+}$
	stirlinglem8.11	$⊢ φ \to A ⇝ C$
Assertion	stirlinglem8	$⊢ φ \to F ⇝ C^{2}$

Proof

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

Metamath Proof Explorer

Theorem stirlinglem8

Proof