Theorem stirlinglem3

Description: Long but simple algebraic transformations are applied to show that V , the Wallis formula for π , can be expressed in terms of A , the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the A , in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem3.1	$$⊢A=\left(n\in \mathbb{N}⟼\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)$$
	stirlinglem3.2	$$⊢D=\left(n\in \mathbb{N}⟼A\left(2n\right)\right)$$
	stirlinglem3.3	$$⊢E=\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)$$
	stirlinglem3.4	$$⊢V=\left(n\in \mathbb{N}⟼\frac{\frac{2^{4n}{n!}^4}{{2n!}^2}}{2n+1}\right)$$
Assertion	stirlinglem3	$$⊢V=\left(n\in \mathbb{N}⟼\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem3.1	$$⊢A=\left(n\in \mathbb{N}⟼\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)$$
2		stirlinglem3.2	$$⊢D=\left(n\in \mathbb{N}⟼A\left(2n\right)\right)$$
3		stirlinglem3.3	$$⊢E=\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)$$
4		stirlinglem3.4	$$⊢V=\left(n\in \mathbb{N}⟼\frac{\frac{2^{4n}{n!}^4}{{2n!}^2}}{2n+1}\right)$$
5		nnnn0	$$⊢n\in \mathbb{N}\to n\in {\mathbb{N}}_0$$
6		faccl	$$⊢n\in {\mathbb{N}}_0\to n!\in \mathbb{N}$$
7		nncn	$$⊢n!\in \mathbb{N}\to n!\in ℂ$$
8	5 6 7	3syl	$$⊢n\in \mathbb{N}\to n!\in ℂ$$
9		2cnd	$$⊢n\in \mathbb{N}\to 2\in ℂ$$
10		nncn	$$⊢n\in \mathbb{N}\to n\in ℂ$$
11	9 10	mulcld	$$⊢n\in \mathbb{N}\to 2n\in ℂ$$
12	11	sqrtcld	$$⊢n\in \mathbb{N}\to \sqrt{2n}\in ℂ$$
13		ere	$$⊢\mathrm{e}\in ℝ$$
14	13	recni	$$⊢\mathrm{e}\in ℂ$$
15	14	a1i	$$⊢n\in \mathbb{N}\to \mathrm{e}\in ℂ$$
16		epos	$$⊢0<\mathrm{e}$$
17	13 16	gt0ne0ii	$$⊢\mathrm{e}\ne 0$$
18	17	a1i	$$⊢n\in \mathbb{N}\to \mathrm{e}\ne 0$$
19	10 15 18	divcld	$$⊢n\in \mathbb{N}\to \frac{n}{\mathrm{e}}\in ℂ$$
20	19 5	expcld	$$⊢n\in \mathbb{N}\to {\left(\frac{n}{\mathrm{e}}\right)}^n\in ℂ$$
21	12 20	mulcld	$$⊢n\in \mathbb{N}\to \sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\in ℂ$$
22		2rp	$$⊢2\in {ℝ}^{+}$$
23	22	a1i	$$⊢n\in \mathbb{N}\to 2\in {ℝ}^{+}$$
24		nnrp	$$⊢n\in \mathbb{N}\to n\in {ℝ}^{+}$$
25	23 24	rpmulcld	$$⊢n\in \mathbb{N}\to 2n\in {ℝ}^{+}$$
26	25	sqrtgt0d	$$⊢n\in \mathbb{N}\to 0<\sqrt{2n}$$
27	26	gt0ne0d	$$⊢n\in \mathbb{N}\to \sqrt{2n}\ne 0$$
28		nnne0	$$⊢n\in \mathbb{N}\to n\ne 0$$
29	10 15 28 18	divne0d	$$⊢n\in \mathbb{N}\to \frac{n}{\mathrm{e}}\ne 0$$
30		nnz	$$⊢n\in \mathbb{N}\to n\in \mathbb{Z}$$
31	19 29 30	expne0d	$$⊢n\in \mathbb{N}\to {\left(\frac{n}{\mathrm{e}}\right)}^n\ne 0$$
32	12 20 27 31	mulne0d	$$⊢n\in \mathbb{N}\to \sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\ne 0$$
33	8 21 32	divcld	$$⊢n\in \mathbb{N}\to \frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\in ℂ$$
34	1	fvmpt2	$$⊢\left(n\in \mathbb{N}\wedge \frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\in ℂ\right)\to A\left(n\right)=\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}$$
35	33 34	mpdan	$$⊢n\in \mathbb{N}\to A\left(n\right)=\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}$$
36	35	oveq1d	$$⊢n\in \mathbb{N}\to {A\left(n\right)}^4={\left(\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)}^4$$
37	3	fvmpt2	$$⊢\left(n\in \mathbb{N}\wedge \sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\in ℂ\right)\to E\left(n\right)=\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n$$
38	21 37	mpdan	$$⊢n\in \mathbb{N}\to E\left(n\right)=\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n$$
39	38	oveq1d	$$⊢n\in \mathbb{N}\to {E\left(n\right)}^4={\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4$$
40	36 39	oveq12d	$$⊢n\in \mathbb{N}\to {A\left(n\right)}^4{E\left(n\right)}^4={\left(\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)}^4{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4$$
41		4nn0	$$⊢4\in {\mathbb{N}}_0$$
42	41	a1i	$$⊢n\in \mathbb{N}\to 4\in {\mathbb{N}}_0$$
43	8 21 32 42	expdivd	$$⊢n\in \mathbb{N}\to {\left(\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)}^4=\frac{{n!}^4}{{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4}$$
44	43	oveq1d	$$⊢n\in \mathbb{N}\to {\left(\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)}^4{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4=\left(\frac{{n!}^4}{{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4}\right){\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4$$
45	8 42	expcld	$$⊢n\in \mathbb{N}\to {n!}^4\in ℂ$$
46	21 42	expcld	$$⊢n\in \mathbb{N}\to {\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4\in ℂ$$
47	42	nn0zd	$$⊢n\in \mathbb{N}\to 4\in \mathbb{Z}$$
48	21 32 47	expne0d	$$⊢n\in \mathbb{N}\to {\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4\ne 0$$
49	45 46 48	divcan1d	$$⊢n\in \mathbb{N}\to \left(\frac{{n!}^4}{{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4}\right){\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4={n!}^4$$
50	40 44 49	3eqtrd	$$⊢n\in \mathbb{N}\to {A\left(n\right)}^4{E\left(n\right)}^4={n!}^4$$
51	50	eqcomd	$$⊢n\in \mathbb{N}\to {n!}^4={A\left(n\right)}^4{E\left(n\right)}^4$$
52	51	oveq2d	$$⊢n\in \mathbb{N}\to 2^{4n}{n!}^4=2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4$$
53		2nn0	$$⊢2\in {\mathbb{N}}_0$$
54	53	a1i	$$⊢n\in \mathbb{N}\to 2\in {\mathbb{N}}_0$$
55	54 5	nn0mulcld	$$⊢n\in \mathbb{N}\to 2n\in {\mathbb{N}}_0$$
56		faccl	$$⊢2n\in {\mathbb{N}}_0\to 2n!\in \mathbb{N}$$
57		nncn	$$⊢2n!\in \mathbb{N}\to 2n!\in ℂ$$
58	55 56 57	3syl	$$⊢n\in \mathbb{N}\to 2n!\in ℂ$$
59	58	sqcld	$$⊢n\in \mathbb{N}\to {2n!}^2\in ℂ$$
60	9 11	mulcld	$$⊢n\in \mathbb{N}\to 22n\in ℂ$$
61	60	sqrtcld	$$⊢n\in \mathbb{N}\to \sqrt{22n}\in ℂ$$
62	11 15 18	divcld	$$⊢n\in \mathbb{N}\to \frac{2n}{\mathrm{e}}\in ℂ$$
63	62 55	expcld	$$⊢n\in \mathbb{N}\to {\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\in ℂ$$
64	61 63	mulcld	$$⊢n\in \mathbb{N}\to \sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\in ℂ$$
65	64	sqcld	$$⊢n\in \mathbb{N}\to {\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2\in ℂ$$
66	23 25	rpmulcld	$$⊢n\in \mathbb{N}\to 22n\in {ℝ}^{+}$$
67	66	sqrtgt0d	$$⊢n\in \mathbb{N}\to 0<\sqrt{22n}$$
68	67	gt0ne0d	$$⊢n\in \mathbb{N}\to \sqrt{22n}\ne 0$$
69	23	rpne0d	$$⊢n\in \mathbb{N}\to 2\ne 0$$
70	9 10 69 28	mulne0d	$$⊢n\in \mathbb{N}\to 2n\ne 0$$
71	11 15 70 18	divne0d	$$⊢n\in \mathbb{N}\to \frac{2n}{\mathrm{e}}\ne 0$$
72		2z	$$⊢2\in \mathbb{Z}$$
73	72	a1i	$$⊢n\in \mathbb{N}\to 2\in \mathbb{Z}$$
74	73 30	zmulcld	$$⊢n\in \mathbb{N}\to 2n\in \mathbb{Z}$$
75	62 71 74	expne0d	$$⊢n\in \mathbb{N}\to {\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\ne 0$$
76	61 63 68 75	mulne0d	$$⊢n\in \mathbb{N}\to \sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\ne 0$$
77	64 76 73	expne0d	$$⊢n\in \mathbb{N}\to {\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2\ne 0$$
78	59 65 77	divcan1d	$$⊢n\in \mathbb{N}\to \left(\frac{{2n!}^2}{{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2}\right){\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2={2n!}^2$$
79	58 64 76 54	expdivd	$$⊢n\in \mathbb{N}\to {\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2=\frac{{2n!}^2}{{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2}$$
80	79	eqcomd	$$⊢n\in \mathbb{N}\to \frac{{2n!}^2}{{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2}={\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2$$
81	80	oveq1d	$$⊢n\in \mathbb{N}\to \left(\frac{{2n!}^2}{{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2}\right){\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2={\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2$$
82	78 81	eqtr3d	$$⊢n\in \mathbb{N}\to {2n!}^2={\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2$$
83		fveq2	$$⊢n=m\to n!=m!$$
84		oveq2	$$⊢n=m\to 2n=2m$$
85	84	fveq2d	$$⊢n=m\to \sqrt{2n}=\sqrt{2m}$$
86		oveq1	$$⊢n=m\to \frac{n}{\mathrm{e}}=\frac{m}{\mathrm{e}}$$
87		id	$$⊢n=m\to n=m$$
88	86 87	oveq12d	$$⊢n=m\to {\left(\frac{n}{\mathrm{e}}\right)}^n={\left(\frac{m}{\mathrm{e}}\right)}^m$$
89	85 88	oveq12d	$$⊢n=m\to \sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n=\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m$$
90	83 89	oveq12d	$$⊢n=m\to \frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}=\frac{m!}{\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m}$$
91	90	cbvmptv	$$⊢\left(n\in \mathbb{N}⟼\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)=\left(m\in \mathbb{N}⟼\frac{m!}{\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m}\right)$$
92	1 91	eqtri	$$⊢A=\left(m\in \mathbb{N}⟼\frac{m!}{\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m}\right)$$
93		fveq2	$$⊢m=2n\to m!=2n!$$
94		oveq2	$$⊢m=2n\to 2m=22n$$
95	94	fveq2d	$$⊢m=2n\to \sqrt{2m}=\sqrt{22n}$$
96		oveq1	$$⊢m=2n\to \frac{m}{\mathrm{e}}=\frac{2n}{\mathrm{e}}$$
97		id	$$⊢m=2n\to m=2n$$
98	96 97	oveq12d	$$⊢m=2n\to {\left(\frac{m}{\mathrm{e}}\right)}^m={\left(\frac{2n}{\mathrm{e}}\right)}^{2n}$$
99	95 98	oveq12d	$$⊢m=2n\to \sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m=\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}$$
100	93 99	oveq12d	$$⊢m=2n\to \frac{m!}{\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m}=\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}$$
101		2nn	$$⊢2\in \mathbb{N}$$
102	101	a1i	$$⊢n\in \mathbb{N}\to 2\in \mathbb{N}$$
103		id	$$⊢n\in \mathbb{N}\to n\in \mathbb{N}$$
104	102 103	nnmulcld	$$⊢n\in \mathbb{N}\to 2n\in \mathbb{N}$$
105	58 64 76	divcld	$$⊢n\in \mathbb{N}\to \frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\in ℂ$$
106	92 100 104 105	fvmptd3	$$⊢n\in \mathbb{N}\to A\left(2n\right)=\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}$$
107	106	oveq1d	$$⊢n\in \mathbb{N}\to {A\left(2n\right)}^2={\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2$$
108	107	eqcomd	$$⊢n\in \mathbb{N}\to {\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2={A\left(2n\right)}^2$$
109	108	oveq1d	$$⊢n\in \mathbb{N}\to {\left(\frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\right)}^2{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2={A\left(2n\right)}^2{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2$$
110		eqidd	$$⊢n\in \mathbb{N}\to \left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)=\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)$$
111	99	adantl	$$⊢\left(n\in \mathbb{N}\wedge m=2n\right)\to \sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m=\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}$$
112	110 111 104 64	fvmptd	$$⊢n\in \mathbb{N}\to \left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)=\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}$$
113	112	oveq1d	$$⊢n\in \mathbb{N}\to {\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)}^2={\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2$$
114	113	eqcomd	$$⊢n\in \mathbb{N}\to {\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2={\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)}^2$$
115	114	oveq2d	$$⊢n\in \mathbb{N}\to {A\left(2n\right)}^2{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2={A\left(2n\right)}^2{\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)}^2$$
116	82 109 115	3eqtrd	$$⊢n\in \mathbb{N}\to {2n!}^2={A\left(2n\right)}^2{\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)}^2$$
117	89	cbvmptv	$$⊢\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)=\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)$$
118	117	a1i	$$⊢n\in \mathbb{N}\to \left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)=\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)$$
119	118	fveq1d	$$⊢n\in \mathbb{N}\to \left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)=\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)$$
120	119	eqcomd	$$⊢n\in \mathbb{N}\to \left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)=\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)$$
121	120	oveq1d	$$⊢n\in \mathbb{N}\to {\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)}^2={\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)}^2$$
122	121	oveq2d	$$⊢n\in \mathbb{N}\to {A\left(2n\right)}^2{\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)\left(2n\right)}^2={A\left(2n\right)}^2{\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)}^2$$
123	106 105	eqeltrd	$$⊢n\in \mathbb{N}\to A\left(2n\right)\in ℂ$$
124	2	fvmpt2	$$⊢\left(n\in \mathbb{N}\wedge A\left(2n\right)\in ℂ\right)\to D\left(n\right)=A\left(2n\right)$$
125	123 124	mpdan	$$⊢n\in \mathbb{N}\to D\left(n\right)=A\left(2n\right)$$
126	125	eqcomd	$$⊢n\in \mathbb{N}\to A\left(2n\right)=D\left(n\right)$$
127	126	oveq1d	$$⊢n\in \mathbb{N}\to {A\left(2n\right)}^2={D\left(n\right)}^2$$
128	3	a1i	$$⊢n\in \mathbb{N}\to E=\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)$$
129	128	fveq1d	$$⊢n\in \mathbb{N}\to E\left(2n\right)=\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)$$
130	129	eqcomd	$$⊢n\in \mathbb{N}\to \left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)=E\left(2n\right)$$
131	130	oveq1d	$$⊢n\in \mathbb{N}\to {\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)}^2={E\left(2n\right)}^2$$
132	127 131	oveq12d	$$⊢n\in \mathbb{N}\to {A\left(2n\right)}^2{\left(n\in \mathbb{N}⟼\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n\right)\left(2n\right)}^2={D\left(n\right)}^2{E\left(2n\right)}^2$$
133	116 122 132	3eqtrd	$$⊢n\in \mathbb{N}\to {2n!}^2={D\left(n\right)}^2{E\left(2n\right)}^2$$
134	52 133	oveq12d	$$⊢n\in \mathbb{N}\to \frac{2^{4n}{n!}^4}{{2n!}^2}=\frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}$$
135	134	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\frac{2^{4n}{n!}^4}{{2n!}^2}}{2n+1}=\frac{\frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}$$
136	135	mpteq2ia	$$⊢\left(n\in \mathbb{N}⟼\frac{\frac{2^{4n}{n!}^4}{{2n!}^2}}{2n+1}\right)=\left(n\in \mathbb{N}⟼\frac{\frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}\right)$$
137	42 5	nn0mulcld	$$⊢n\in \mathbb{N}\to 4n\in {\mathbb{N}}_0$$
138	9 137	expcld	$$⊢n\in \mathbb{N}\to 2^{4n}\in ℂ$$
139	50 45	eqeltrd	$$⊢n\in \mathbb{N}\to {A\left(n\right)}^4{E\left(n\right)}^4\in ℂ$$
140	138 139	mulcomd	$$⊢n\in \mathbb{N}\to 2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4={A\left(n\right)}^4{E\left(n\right)}^4{2}^{4n}$$
141	140	oveq1d	$$⊢n\in \mathbb{N}\to \frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}=\frac{{A\left(n\right)}^4{E\left(n\right)}^4{2}^{4n}}{{D\left(n\right)}^2{E\left(2n\right)}^2}$$
142	141	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}=\frac{\frac{{A\left(n\right)}^4{E\left(n\right)}^4{2}^{4n}}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}$$
143	125 123	eqeltrd	$$⊢n\in \mathbb{N}\to D\left(n\right)\in ℂ$$
144	143	sqcld	$$⊢n\in \mathbb{N}\to {D\left(n\right)}^2\in ℂ$$
145	128 118	eqtrd	$$⊢n\in \mathbb{N}\to E=\left(m\in \mathbb{N}⟼\sqrt{2m}{\left(\frac{m}{\mathrm{e}}\right)}^m\right)$$
146	145 111 104 64	fvmptd	$$⊢n\in \mathbb{N}\to E\left(2n\right)=\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}$$
147	146 64	eqeltrd	$$⊢n\in \mathbb{N}\to E\left(2n\right)\in ℂ$$
148	147	sqcld	$$⊢n\in \mathbb{N}\to {E\left(2n\right)}^2\in ℂ$$
149		nnne0	$$⊢2n!\in \mathbb{N}\to 2n!\ne 0$$
150	55 56 149	3syl	$$⊢n\in \mathbb{N}\to 2n!\ne 0$$
151	58 64 150 76	divne0d	$$⊢n\in \mathbb{N}\to \frac{2n!}{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}\ne 0$$
152	106 151	eqnetrd	$$⊢n\in \mathbb{N}\to A\left(2n\right)\ne 0$$
153	125 152	eqnetrd	$$⊢n\in \mathbb{N}\to D\left(n\right)\ne 0$$
154	143 153 73	expne0d	$$⊢n\in \mathbb{N}\to {D\left(n\right)}^2\ne 0$$
155	146 76	eqnetrd	$$⊢n\in \mathbb{N}\to E\left(2n\right)\ne 0$$
156	147 155 73	expne0d	$$⊢n\in \mathbb{N}\to {E\left(2n\right)}^2\ne 0$$
157	139 144 138 148 154 156	divmuldivd	$$⊢n\in \mathbb{N}\to \left(\frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)=\frac{{A\left(n\right)}^4{E\left(n\right)}^4{2}^{4n}}{{D\left(n\right)}^2{E\left(2n\right)}^2}$$
158	157	eqcomd	$$⊢n\in \mathbb{N}\to \frac{{A\left(n\right)}^4{E\left(n\right)}^4{2}^{4n}}{{D\left(n\right)}^2{E\left(2n\right)}^2}=\left(\frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)$$
159	158	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\frac{{A\left(n\right)}^4{E\left(n\right)}^4{2}^{4n}}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}=\frac{\left(\frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}$$
160	35 33	eqeltrd	$$⊢n\in \mathbb{N}\to A\left(n\right)\in ℂ$$
161	160 42	expcld	$$⊢n\in \mathbb{N}\to {A\left(n\right)}^4\in ℂ$$
162	39 46	eqeltrd	$$⊢n\in \mathbb{N}\to {E\left(n\right)}^4\in ℂ$$
163	161 162 144 154	div23d	$$⊢n\in \mathbb{N}\to \frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4$$
164	163	oveq1d	$$⊢n\in \mathbb{N}\to \left(\frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)$$
165	164	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\frac{\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}$$
166	161 144 154	divcld	$$⊢n\in \mathbb{N}\to \frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\in ℂ$$
167	138 148 156	divcld	$$⊢n\in \mathbb{N}\to \frac{2^{4n}}{{E\left(2n\right)}^2}\in ℂ$$
168	166 162 167	mulassd	$$⊢n\in \mathbb{N}\to \left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)$$
169	168	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\frac{\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}$$
170	162 167	mulcld	$$⊢n\in \mathbb{N}\to {E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)\in ℂ$$
171		1cnd	$$⊢n\in \mathbb{N}\to 1\in ℂ$$
172	11 171	addcld	$$⊢n\in \mathbb{N}\to 2n+1\in ℂ$$
173		0red	$$⊢n\in \mathbb{N}\to 0\in ℝ$$
174	104	nnred	$$⊢n\in \mathbb{N}\to 2n\in ℝ$$
175		2re	$$⊢2\in ℝ$$
176	175	a1i	$$⊢n\in \mathbb{N}\to 2\in ℝ$$
177		nnre	$$⊢n\in \mathbb{N}\to n\in ℝ$$
178	176 177	remulcld	$$⊢n\in \mathbb{N}\to 2n\in ℝ$$
179		1red	$$⊢n\in \mathbb{N}\to 1\in ℝ$$
180	178 179	readdcld	$$⊢n\in \mathbb{N}\to 2n+1\in ℝ$$
181	104	nngt0d	$$⊢n\in \mathbb{N}\to 0<2n$$
182	174	ltp1d	$$⊢n\in \mathbb{N}\to 2n<2n+1$$
183	173 174 180 181 182	lttrd	$$⊢n\in \mathbb{N}\to 0<2n+1$$
184	183	gt0ne0d	$$⊢n\in \mathbb{N}\to 2n+1\ne 0$$
185	166 170 172 184	divassd	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{{E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}\right)$$
186	162 138 148 156	div12d	$$⊢n\in \mathbb{N}\to {E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)=2^{4n}\left(\frac{{E\left(n\right)}^4}{{E\left(2n\right)}^2}\right)$$
187	12 20 42	mulexpd	$$⊢n\in \mathbb{N}\to {\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4={\sqrt{2n}}^4{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4$$
188	61 63	sqmuld	$$⊢n\in \mathbb{N}\to {\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2={\sqrt{22n}}^2{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2$$
189	187 188	oveq12d	$$⊢n\in \mathbb{N}\to \frac{{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4}{{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2}=\frac{{\sqrt{2n}}^4{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\sqrt{22n}}^2{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}$$
190	146	oveq1d	$$⊢n\in \mathbb{N}\to {E\left(2n\right)}^2={\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2$$
191	39 190	oveq12d	$$⊢n\in \mathbb{N}\to \frac{{E\left(n\right)}^4}{{E\left(2n\right)}^2}=\frac{{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}^4}{{\sqrt{22n}{\left(\frac{2n}{\mathrm{e}}\right)}^{2n}}^2}$$
192	12 42	expcld	$$⊢n\in \mathbb{N}\to {\sqrt{2n}}^4\in ℂ$$
193	61	sqcld	$$⊢n\in \mathbb{N}\to {\sqrt{22n}}^2\in ℂ$$
194	20 42	expcld	$$⊢n\in \mathbb{N}\to {\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4\in ℂ$$
195	63	sqcld	$$⊢n\in \mathbb{N}\to {\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2\in ℂ$$
196	61 68 73	expne0d	$$⊢n\in \mathbb{N}\to {\sqrt{22n}}^2\ne 0$$
197	63 75 73	expne0d	$$⊢n\in \mathbb{N}\to {\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2\ne 0$$
198	192 193 194 195 196 197	divmuldivd	$$⊢n\in \mathbb{N}\to \left(\frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}\right)\left(\frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}\right)=\frac{{\sqrt{2n}}^4{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\sqrt{22n}}^2{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}$$
199	189 191 198	3eqtr4d	$$⊢n\in \mathbb{N}\to \frac{{E\left(n\right)}^4}{{E\left(2n\right)}^2}=\left(\frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}\right)\left(\frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}\right)$$
200	199	oveq2d	$$⊢n\in \mathbb{N}\to 2^{4n}\left(\frac{{E\left(n\right)}^4}{{E\left(2n\right)}^2}\right)=2^{4n}\left(\frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}\right)\left(\frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}\right)$$
201	66	rprege0d	$$⊢n\in \mathbb{N}\to \left(22n\in ℝ\wedge 0\le 22n\right)$$
202		resqrtth	$$⊢\left(22n\in ℝ\wedge 0\le 22n\right)\to {\sqrt{22n}}^2=22n$$
203	201 202	syl	$$⊢n\in \mathbb{N}\to {\sqrt{22n}}^2=22n$$
204	203	oveq2d	$$⊢n\in \mathbb{N}\to \frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}=\frac{{\sqrt{2n}}^4}{22n}$$
205		2t2e4	$$⊢2\cdot 2=4$$
206	205	eqcomi	$$⊢4=2\cdot 2$$
207	206	a1i	$$⊢n\in \mathbb{N}\to 4=2\cdot 2$$
208	207	oveq2d	$$⊢n\in \mathbb{N}\to {\sqrt{2n}}^4={\sqrt{2n}}^{2\cdot 2}$$
209	12 54 54	expmuld	$$⊢n\in \mathbb{N}\to {\sqrt{2n}}^{2\cdot 2}={\left({\sqrt{2n}}^2\right)}^2$$
210	25	rprege0d	$$⊢n\in \mathbb{N}\to \left(2n\in ℝ\wedge 0\le 2n\right)$$
211		resqrtth	$$⊢\left(2n\in ℝ\wedge 0\le 2n\right)\to {\sqrt{2n}}^2=2n$$
212	210 211	syl	$$⊢n\in \mathbb{N}\to {\sqrt{2n}}^2=2n$$
213	212	oveq1d	$$⊢n\in \mathbb{N}\to {\left({\sqrt{2n}}^2\right)}^2={2n}^2$$
214	208 209 213	3eqtrd	$$⊢n\in \mathbb{N}\to {\sqrt{2n}}^4={2n}^2$$
215	9 9 10	mulassd	$$⊢n\in \mathbb{N}\to 2\cdot 2n=22n$$
216	205	a1i	$$⊢n\in \mathbb{N}\to 2\cdot 2=4$$
217	216	oveq1d	$$⊢n\in \mathbb{N}\to 2\cdot 2n=4n$$
218	215 217	eqtr3d	$$⊢n\in \mathbb{N}\to 22n=4n$$
219	214 218	oveq12d	$$⊢n\in \mathbb{N}\to \frac{{\sqrt{2n}}^4}{22n}=\frac{{2n}^2}{4n}$$
220	9 10	sqmuld	$$⊢n\in \mathbb{N}\to {2n}^2=2^2{n}^2$$
221		sq2	$$⊢2^2=4$$
222	221	a1i	$$⊢n\in \mathbb{N}\to 2^2=4$$
223	222	oveq1d	$$⊢n\in \mathbb{N}\to 2^2{n}^2=4n^2$$
224	220 223	eqtrd	$$⊢n\in \mathbb{N}\to {2n}^2=4n^2$$
225	224	oveq1d	$$⊢n\in \mathbb{N}\to \frac{{2n}^2}{4n}=\frac{4n^2}{4n}$$
226		4cn	$$⊢4\in ℂ$$
227		4ne0	$$⊢4\ne 0$$
228	226 227	dividi	$$⊢\frac{4}{4}=1$$
229	228	a1i	$$⊢n\in \mathbb{N}\to \frac{4}{4}=1$$
230	10	sqvald	$$⊢n\in \mathbb{N}\to n^2=nn$$
231	230	oveq1d	$$⊢n\in \mathbb{N}\to \frac{n^2}{n}=\frac{nn}{n}$$
232	10 10 28	divcan4d	$$⊢n\in \mathbb{N}\to \frac{nn}{n}=n$$
233	231 232	eqtrd	$$⊢n\in \mathbb{N}\to \frac{n^2}{n}=n$$
234	229 233	oveq12d	$$⊢n\in \mathbb{N}\to \left(\frac{4}{4}\right)\left(\frac{n^2}{n}\right)=1n$$
235	42	nn0cnd	$$⊢n\in \mathbb{N}\to 4\in ℂ$$
236	10	sqcld	$$⊢n\in \mathbb{N}\to n^2\in ℂ$$
237	227	a1i	$$⊢n\in \mathbb{N}\to 4\ne 0$$
238	235 235 236 10 237 28	divmuldivd	$$⊢n\in \mathbb{N}\to \left(\frac{4}{4}\right)\left(\frac{n^2}{n}\right)=\frac{4n^2}{4n}$$
239	10	mullidd	$$⊢n\in \mathbb{N}\to 1n=n$$
240	234 238 239	3eqtr3d	$$⊢n\in \mathbb{N}\to \frac{4n^2}{4n}=n$$
241	225 240	eqtrd	$$⊢n\in \mathbb{N}\to \frac{{2n}^2}{4n}=n$$
242	204 219 241	3eqtrd	$$⊢n\in \mathbb{N}\to \frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}=n$$
243	10 235	mulcomd	$$⊢n\in \mathbb{N}\to n\cdot 4=4n$$
244	243	oveq2d	$$⊢n\in \mathbb{N}\to {\left(\frac{n}{\mathrm{e}}\right)}^{n\cdot 4}={\left(\frac{n}{\mathrm{e}}\right)}^{4n}$$
245	19 42 5	expmuld	$$⊢n\in \mathbb{N}\to {\left(\frac{n}{\mathrm{e}}\right)}^{n\cdot 4}={\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4$$
246	10 15 18 137	expdivd	$$⊢n\in \mathbb{N}\to {\left(\frac{n}{\mathrm{e}}\right)}^{4n}=\frac{n^{4n}}{{\mathrm{e}}^{4n}}$$
247	244 245 246	3eqtr3d	$$⊢n\in \mathbb{N}\to {\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4=\frac{n^{4n}}{{\mathrm{e}}^{4n}}$$
248	9 10 9	mul32d	$$⊢n\in \mathbb{N}\to 2n\cdot 2=2\cdot 2n$$
249	248 217	eqtrd	$$⊢n\in \mathbb{N}\to 2n\cdot 2=4n$$
250	249	oveq2d	$$⊢n\in \mathbb{N}\to {\left(\frac{2n}{\mathrm{e}}\right)}^{2n\cdot 2}={\left(\frac{2n}{\mathrm{e}}\right)}^{4n}$$
251	62 54 55	expmuld	$$⊢n\in \mathbb{N}\to {\left(\frac{2n}{\mathrm{e}}\right)}^{2n\cdot 2}={\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2$$
252	11 15 18 137	expdivd	$$⊢n\in \mathbb{N}\to {\left(\frac{2n}{\mathrm{e}}\right)}^{4n}=\frac{{2n}^{4n}}{{\mathrm{e}}^{4n}}$$
253	250 251 252	3eqtr3d	$$⊢n\in \mathbb{N}\to {\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2=\frac{{2n}^{4n}}{{\mathrm{e}}^{4n}}$$
254	247 253	oveq12d	$$⊢n\in \mathbb{N}\to \frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}=\frac{\frac{n^{4n}}{{\mathrm{e}}^{4n}}}{\frac{{2n}^{4n}}{{\mathrm{e}}^{4n}}}$$
255	247 194	eqeltrrd	$$⊢n\in \mathbb{N}\to \frac{n^{4n}}{{\mathrm{e}}^{4n}}\in ℂ$$
256	11 137	expcld	$$⊢n\in \mathbb{N}\to {2n}^{4n}\in ℂ$$
257	15 137	expcld	$$⊢n\in \mathbb{N}\to {\mathrm{e}}^{4n}\in ℂ$$
258	47 30	zmulcld	$$⊢n\in \mathbb{N}\to 4n\in \mathbb{Z}$$
259	11 70 258	expne0d	$$⊢n\in \mathbb{N}\to {2n}^{4n}\ne 0$$
260	15 18 258	expne0d	$$⊢n\in \mathbb{N}\to {\mathrm{e}}^{4n}\ne 0$$
261	255 256 257 259 260	divdiv2d	$$⊢n\in \mathbb{N}\to \frac{\frac{n^{4n}}{{\mathrm{e}}^{4n}}}{\frac{{2n}^{4n}}{{\mathrm{e}}^{4n}}}=\frac{\left(\frac{n^{4n}}{{\mathrm{e}}^{4n}}\right){\mathrm{e}}^{4n}}{{2n}^{4n}}$$
262	10 137	expcld	$$⊢n\in \mathbb{N}\to n^{4n}\in ℂ$$
263	262 257 260	divcan1d	$$⊢n\in \mathbb{N}\to \left(\frac{n^{4n}}{{\mathrm{e}}^{4n}}\right){\mathrm{e}}^{4n}=n^{4n}$$
264	263	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{n^{4n}}{{\mathrm{e}}^{4n}}\right){\mathrm{e}}^{4n}}{{2n}^{4n}}=\frac{n^{4n}}{{2n}^{4n}}$$
265	9 10 137	mulexpd	$$⊢n\in \mathbb{N}\to {2n}^{4n}=2^{4n}{n}^{4n}$$
266	265	oveq2d	$$⊢n\in \mathbb{N}\to \frac{n^{4n}}{{2n}^{4n}}=\frac{n^{4n}}{2^{4n}{n}^{4n}}$$
267	138 262	mulcomd	$$⊢n\in \mathbb{N}\to 2^{4n}{n}^{4n}=n^{4n}{2}^{4n}$$
268	267	oveq2d	$$⊢n\in \mathbb{N}\to \frac{n^{4n}}{2^{4n}{n}^{4n}}=\frac{n^{4n}}{n^{4n}{2}^{4n}}$$
269	10 28 258	expne0d	$$⊢n\in \mathbb{N}\to n^{4n}\ne 0$$
270	9 69 258	expne0d	$$⊢n\in \mathbb{N}\to 2^{4n}\ne 0$$
271	262 262 138 269 270	divdiv1d	$$⊢n\in \mathbb{N}\to \frac{\frac{n^{4n}}{n^{4n}}}{2^{4n}}=\frac{n^{4n}}{n^{4n}{2}^{4n}}$$
272	262 269	dividd	$$⊢n\in \mathbb{N}\to \frac{n^{4n}}{n^{4n}}=1$$
273	272	oveq1d	$$⊢n\in \mathbb{N}\to \frac{\frac{n^{4n}}{n^{4n}}}{2^{4n}}=\frac{1}{2^{4n}}$$
274	268 271 273	3eqtr2d	$$⊢n\in \mathbb{N}\to \frac{n^{4n}}{2^{4n}{n}^{4n}}=\frac{1}{2^{4n}}$$
275	264 266 274	3eqtrd	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{n^{4n}}{{\mathrm{e}}^{4n}}\right){\mathrm{e}}^{4n}}{{2n}^{4n}}=\frac{1}{2^{4n}}$$
276	254 261 275	3eqtrd	$$⊢n\in \mathbb{N}\to \frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}=\frac{1}{2^{4n}}$$
277	242 276	oveq12d	$$⊢n\in \mathbb{N}\to \left(\frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}\right)\left(\frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}\right)=n\left(\frac{1}{2^{4n}}\right)$$
278	277	oveq2d	$$⊢n\in \mathbb{N}\to 2^{4n}\left(\frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}\right)\left(\frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}\right)=2^{4n}n\left(\frac{1}{2^{4n}}\right)$$
279	138 270	reccld	$$⊢n\in \mathbb{N}\to \frac{1}{2^{4n}}\in ℂ$$
280	138 10 279	mul12d	$$⊢n\in \mathbb{N}\to 2^{4n}n\left(\frac{1}{2^{4n}}\right)=n{2}^{4n}\left(\frac{1}{2^{4n}}\right)$$
281	10	mulridd	$$⊢n\in \mathbb{N}\to n\cdot 1=n$$
282	138 270	recidd	$$⊢n\in \mathbb{N}\to 2^{4n}\left(\frac{1}{2^{4n}}\right)=1$$
283	282	oveq2d	$$⊢n\in \mathbb{N}\to n{2}^{4n}\left(\frac{1}{2^{4n}}\right)=n\cdot 1$$
284	281 283 233	3eqtr4d	$$⊢n\in \mathbb{N}\to n{2}^{4n}\left(\frac{1}{2^{4n}}\right)=\frac{n^2}{n}$$
285	278 280 284	3eqtrd	$$⊢n\in \mathbb{N}\to 2^{4n}\left(\frac{{\sqrt{2n}}^4}{{\sqrt{22n}}^2}\right)\left(\frac{{\left({\left(\frac{n}{\mathrm{e}}\right)}^n\right)}^4}{{\left({\left(\frac{2n}{\mathrm{e}}\right)}^{2n}\right)}^2}\right)=\frac{n^2}{n}$$
286	186 200 285	3eqtrd	$$⊢n\in \mathbb{N}\to {E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)=\frac{n^2}{n}$$
287	286	oveq1d	$$⊢n\in \mathbb{N}\to \frac{{E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\frac{\frac{n^2}{n}}{2n+1}$$
288	236 10 172 28 184	divdiv1d	$$⊢n\in \mathbb{N}\to \frac{\frac{n^2}{n}}{2n+1}=\frac{n^2}{n\left(2n+1\right)}$$
289	287 288	eqtrd	$$⊢n\in \mathbb{N}\to \frac{{E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\frac{n^2}{n\left(2n+1\right)}$$
290	289	oveq2d	$$⊢n\in \mathbb{N}\to \left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{{E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}\right)=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)$$
291	185 290	eqtrd	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right){E\left(n\right)}^4\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)$$
292	165 169 291	3eqtrd	$$⊢n\in \mathbb{N}\to \frac{\left(\frac{{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{2^{4n}}{{E\left(2n\right)}^2}\right)}{2n+1}=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)$$
293	142 159 292	3eqtrd	$$⊢n\in \mathbb{N}\to \frac{\frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}=\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)$$
294	293	mpteq2ia	$$⊢\left(n\in \mathbb{N}⟼\frac{\frac{2^{4n}{A\left(n\right)}^4{E\left(n\right)}^4}{{D\left(n\right)}^2{E\left(2n\right)}^2}}{2n+1}\right)=\left(n\in \mathbb{N}⟼\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)\right)$$
295	4 136 294	3eqtri	$$⊢V=\left(n\in \mathbb{N}⟼\left(\frac{{A\left(n\right)}^4}{{D\left(n\right)}^2}\right)\left(\frac{n^2}{n\left(2n+1\right)}\right)\right)$$