Theorem stirlinglem2

Description: A maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypothesis	stirlinglem2.1	$$⊢A=\left(n\in \mathbb{N}⟼\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)$$
Assertion	stirlinglem2	$$⊢N\in \mathbb{N}\to A\left(N\right)\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem2.1	$$⊢A=\left(n\in \mathbb{N}⟼\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)$$
2		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
3		faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$
4		nnrp	$$⊢N!\in \mathbb{N}\to N!\in {ℝ}^{+}$$
5	2 3 4	3syl	$$⊢N\in \mathbb{N}\to N!\in {ℝ}^{+}$$
6		2rp	$$⊢2\in {ℝ}^{+}$$
7	6	a1i	$$⊢N\in \mathbb{N}\to 2\in {ℝ}^{+}$$
8		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
9	7 8	rpmulcld	$$⊢N\in \mathbb{N}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
10	9	rpsqrtcld	$$⊢N\in \mathbb{N}\to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in {ℝ}^{+}$$
11		epr	$$⊢\mathrm{e}\in {ℝ}^{+}$$
12	11	a1i	$$⊢N\in \mathbb{N}\to \mathrm{e}\in {ℝ}^{+}$$
13	8 12	rpdivcld	$$⊢N\in \mathbb{N}\to \frac{N}{\mathrm{e}}\in {ℝ}^{+}$$
14		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
15	13 14	rpexpcld	$$⊢N\in \mathbb{N}\to {\left(\frac{N}{\mathrm{e}}\right)}^N\in {ℝ}^{+}$$
16	10 15	rpmulcld	$$⊢N\in \mathbb{N}\to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N\in {ℝ}^{+}$$
17	5 16	rpdivcld	$$⊢N\in \mathbb{N}\to \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}$$
18		fveq2	$$⊢n=k\to n!=k!$$
19		oveq2	$$⊢n=k\to 2n=2k$$
20	19	fveq2d	$$⊢n=k\to \sqrt{2n}=\sqrt{2k}$$
21		oveq1	$$⊢n=k\to \frac{n}{\mathrm{e}}=\frac{k}{\mathrm{e}}$$
22		id	$$⊢n=k\to n=k$$
23	21 22	oveq12d	$$⊢n=k\to {\left(\frac{n}{\mathrm{e}}\right)}^n={\left(\frac{k}{\mathrm{e}}\right)}^k$$
24	20 23	oveq12d	$$⊢n=k\to \sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n=\sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k$$
25	18 24	oveq12d	$$⊢n=k\to \frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}=\frac{k!}{\sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k}$$
26	25	cbvmptv	$$⊢\left(n\in \mathbb{N}⟼\frac{n!}{\sqrt{2n}{\left(\frac{n}{\mathrm{e}}\right)}^n}\right)=\left(k\in \mathbb{N}⟼\frac{k!}{\sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k}\right)$$
27	1 26	eqtri	$$⊢A=\left(k\in \mathbb{N}⟼\frac{k!}{\sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k}\right)$$
28	27	a1i	$$⊢\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\to A=\left(k\in \mathbb{N}⟼\frac{k!}{\sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k}\right)$$
29		simpr	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to k=N$$
30	29	fveq2d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to k!=N!$$
31	29	oveq2d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to 2k=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
32	31	fveq2d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to \sqrt{2k}=\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
33	29	oveq1d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to \frac{k}{\mathrm{e}}=\frac{N}{\mathrm{e}}$$
34	33 29	oveq12d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to {\left(\frac{k}{\mathrm{e}}\right)}^k={\left(\frac{N}{\mathrm{e}}\right)}^N$$
35	32 34	oveq12d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to \sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k=\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N$$
36	30 35	oveq12d	$$⊢\left(\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\wedge k=N\right)\to \frac{k!}{\sqrt{2k}{\left(\frac{k}{\mathrm{e}}\right)}^k}=\frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}$$
37		simpl	$$⊢\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\to N\in \mathbb{N}$$
38		simpr	$$⊢\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\to \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}$$
39	28 36 37 38	fvmptd	$$⊢\left(N\in \mathbb{N}\wedge \frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}\in {ℝ}^{+}\right)\to A\left(N\right)=\frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}$$
40	17 39	mpdan	$$⊢N\in \mathbb{N}\to A\left(N\right)=\frac{N!}{\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{\left(\frac{N}{\mathrm{e}}\right)}^N}$$
41	40 17	eqeltrd	$$⊢N\in \mathbb{N}\to A\left(N\right)\in {ℝ}^{+}$$