stirlinglem13

Description: B is decreasing and has a lower bound, then it converges. Since B is log A , in another theorem it is proven that A converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem13.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
	stirlinglem13.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
Assertion	stirlinglem13	$⊢ \exists d \in ℝ B ⇝ d$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem13.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
2		stirlinglem13.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
3		vex	$⊢ y \in V$
4	2	elrnmpt	$⊢ y \in V \to (y \in ran B \leftrightarrow \exists n \in ℕ y = \log A (n))$
5	3 4	ax-mp	$⊢ y \in ran B \leftrightarrow \exists n \in ℕ y = \log A (n)$
6		simpr	$⊢ (n \in ℕ \land y = \log A (n)) \to y = \log A (n)$
7	1	stirlinglem2	$⊢ n \in ℕ \to A (n) \in ℝ^{+}$
8	7	relogcld	$⊢ n \in ℕ \to \log A (n) \in ℝ$
9	8	adantr	$⊢ (n \in ℕ \land y = \log A (n)) \to \log A (n) \in ℝ$
10	6 9	eqeltrd	$⊢ (n \in ℕ \land y = \log A (n)) \to y \in ℝ$
11	10	rexlimiva	$⊢ \exists n \in ℕ y = \log A (n) \to y \in ℝ$
12	5 11	sylbi	$⊢ y \in ran B \to y \in ℝ$
13	12	ssriv	$⊢ ran B \subseteq ℝ$
14		1nn	$⊢ 1 \in ℕ$
15	1	stirlinglem2	$⊢ 1 \in ℕ \to A (1) \in ℝ^{+}$
16		relogcl	$⊢ A (1) \in ℝ^{+} \to \log A (1) \in ℝ$
17	14 15 16	mp2b	$⊢ \log A (1) \in ℝ$
18		nfcv	$⊢ \underline{Ⅎ} n 1$
19		nfcv	$⊢ \underline{Ⅎ} n log$
20		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
21	1 20	nfcxfr	$⊢ \underline{Ⅎ} n A$
22	21 18	nffv	$⊢ \underline{Ⅎ} n A (1)$
23	19 22	nffv	$⊢ \underline{Ⅎ} n \log A (1)$
24		2fveq3	$⊢ n = 1 \to \log A (n) = \log A (1)$
25	18 23 24 2	fvmptf	$⊢ (1 \in ℕ \land \log A (1) \in ℝ) \to B (1) = \log A (1)$
26	14 17 25	mp2an	$⊢ B (1) = \log A (1)$
27		2fveq3	$⊢ j = 1 \to \log A (j) = \log A (1)$
28	27	rspceeqv	$⊢ (1 \in ℕ \land B (1) = \log A (1)) \to \exists j \in ℕ B (1) = \log A (j)$
29	14 26 28	mp2an	$⊢ \exists j \in ℕ B (1) = \log A (j)$
30	26 17	eqeltri	$⊢ B (1) \in ℝ$
31		nfcv	$⊢ \underline{Ⅎ} j \log A (n)$
32		nfcv	$⊢ \underline{Ⅎ} n j$
33	21 32	nffv	$⊢ \underline{Ⅎ} n A (j)$
34	19 33	nffv	$⊢ \underline{Ⅎ} n \log A (j)$
35		2fveq3	$⊢ n = j \to \log A (n) = \log A (j)$
36	31 34 35	cbvmpt	$⊢ (n \in ℕ ⟼ \log A (n)) = (j \in ℕ ⟼ \log A (j))$
37	2 36	eqtri	$⊢ B = (j \in ℕ ⟼ \log A (j))$
38	37	elrnmpt	$⊢ B (1) \in ℝ \to (B (1) \in ran B \leftrightarrow \exists j \in ℕ B (1) = \log A (j))$
39	30 38	ax-mp	$⊢ B (1) \in ran B \leftrightarrow \exists j \in ℕ B (1) = \log A (j)$
40	29 39	mpbir	$⊢ B (1) \in ran B$
41	40	ne0ii	$⊢ ran B \neq \emptyset$
42		4re	$⊢ 4 \in ℝ$
43		4ne0	$⊢ 4 \neq 0$
44	42 43	rereccli	$⊢ \frac{1}{4} \in ℝ$
45	30 44	resubcli	$⊢ B (1) - (\frac{1}{4}) \in ℝ$
46		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n (n + 1)}) = (n \in ℕ ⟼ \frac{1}{n (n + 1)})$
47	1 2 46	stirlinglem12	$⊢ j \in ℕ \to B (1) - (\frac{1}{4}) \leq B (j)$
48	47	rgen	$⊢ \forall j \in ℕ B (1) - (\frac{1}{4}) \leq B (j)$
49		breq1	$⊢ x = B (1) - (\frac{1}{4}) \to (x \leq B (j) \leftrightarrow B (1) - (\frac{1}{4}) \leq B (j))$
50	49	ralbidv	$⊢ x = B (1) - (\frac{1}{4}) \to (\forall j \in ℕ x \leq B (j) \leftrightarrow \forall j \in ℕ B (1) - (\frac{1}{4}) \leq B (j))$
51	50	rspcev	$⊢ (B (1) - (\frac{1}{4}) \in ℝ \land \forall j \in ℕ B (1) - (\frac{1}{4}) \leq B (j)) \to \exists x \in ℝ \forall j \in ℕ x \leq B (j)$
52	45 48 51	mp2an	$⊢ \exists x \in ℝ \forall j \in ℕ x \leq B (j)$
53		simpr	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to y \in ran B$
54	8	rgen	$⊢ \forall n \in ℕ \log A (n) \in ℝ$
55	2	fnmpt	$⊢ \forall n \in ℕ \log A (n) \in ℝ \to B Fn ℕ$
56		fvelrnb	$⊢ B Fn ℕ \to (y \in ran B \leftrightarrow \exists j \in ℕ B (j) = y)$
57	54 55 56	mp2b	$⊢ y \in ran B \leftrightarrow \exists j \in ℕ B (j) = y$
58	53 57	sylib	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to \exists j \in ℕ B (j) = y$
59		nfra1	$⊢ Ⅎ j \forall j \in ℕ x \leq B (j)$
60		nfv	$⊢ Ⅎ j y \in ran B$
61	59 60	nfan	$⊢ Ⅎ j (\forall j \in ℕ x \leq B (j) \land y \in ran B)$
62		nfv	$⊢ Ⅎ j x \leq y$
63		simp1l	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to \forall j \in ℕ x \leq B (j)$
64		simp2	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to j \in ℕ$
65		rsp	$⊢ \forall j \in ℕ x \leq B (j) \to (j \in ℕ \to x \leq B (j))$
66	63 64 65	sylc	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to x \leq B (j)$
67		simp3	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to B (j) = y$
68	66 67	breqtrd	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to x \leq y$
69	68	3exp	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to (j \in ℕ \to (B (j) = y \to x \leq y))$
70	61 62 69	rexlimd	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to (\exists j \in ℕ B (j) = y \to x \leq y)$
71	58 70	mpd	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to x \leq y$
72	71	ralrimiva	$⊢ \forall j \in ℕ x \leq B (j) \to \forall y \in ran B x \leq y$
73	72	reximi	$⊢ \exists x \in ℝ \forall j \in ℕ x \leq B (j) \to \exists x \in ℝ \forall y \in ran B x \leq y$
74	52 73	ax-mp	$⊢ \exists x \in ℝ \forall y \in ran B x \leq y$
75		infrecl	$⊢ (ran B \subseteq ℝ \land ran B \neq \emptyset \land \exists x \in ℝ \forall y \in ran B x \leq y) \to sup (ran B ℝ <) \in ℝ$
76	13 41 74 75	mp3an	$⊢ sup (ran B ℝ <) \in ℝ$
77		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
78		1zzd	$⊢ ⊤ \to 1 \in ℤ$
79	2 8	fmpti	$⊢ B : ℕ ⟶ ℝ$
80	79	a1i	$⊢ ⊤ \to B : ℕ ⟶ ℝ$
81		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
82	1	a1i	$⊢ j \in ℕ \to A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
83		simpr	$⊢ (j \in ℕ \land n = j + 1) \to n = j + 1$
84	83	fveq2d	$⊢ (j \in ℕ \land n = j + 1) \to n! = (j + 1)!$
85	83	oveq2d	$⊢ (j \in ℕ \land n = j + 1) \to 2 n = 2 (j + 1)$
86	85	fveq2d	$⊢ (j \in ℕ \land n = j + 1) \to \sqrt{2 n} = \sqrt{2 (j + 1)}$
87	83	oveq1d	$⊢ (j \in ℕ \land n = j + 1) \to \frac{n}{e} = \frac{j + 1}{e}$
88	87 83	oveq12d	$⊢ (j \in ℕ \land n = j + 1) \to {(\frac{n}{e})}^{n} = {(\frac{j + 1}{e})}^{j + 1}$
89	86 88	oveq12d	$⊢ (j \in ℕ \land n = j + 1) \to \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}$
90	84 89	oveq12d	$⊢ (j \in ℕ \land n = j + 1) \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} = \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}}$
91	81	nnnn0d	$⊢ j \in ℕ \to j + 1 \in ℕ_{0}$
92		faccl	$⊢ j + 1 \in ℕ_{0} \to (j + 1)! \in ℕ$
93		nncn	$⊢ (j + 1)! \in ℕ \to (j + 1)! \in ℂ$
94	91 92 93	3syl	$⊢ j \in ℕ \to (j + 1)! \in ℂ$
95		2cnd	$⊢ j \in ℕ \to 2 \in ℂ$
96		nncn	$⊢ j \in ℕ \to j \in ℂ$
97		1cnd	$⊢ j \in ℕ \to 1 \in ℂ$
98	96 97	addcld	$⊢ j \in ℕ \to j + 1 \in ℂ$
99	95 98	mulcld	$⊢ j \in ℕ \to 2 (j + 1) \in ℂ$
100	99	sqrtcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} \in ℂ$
101		ere	$⊢ e \in ℝ$
102	101	recni	$⊢ e \in ℂ$
103	102	a1i	$⊢ j \in ℕ \to e \in ℂ$
104		0re	$⊢ 0 \in ℝ$
105		epos	$⊢ 0 < e$
106	104 105	gtneii	$⊢ e \neq 0$
107	106	a1i	$⊢ j \in ℕ \to e \neq 0$
108	98 103 107	divcld	$⊢ j \in ℕ \to \frac{j + 1}{e} \in ℂ$
109	108 91	expcld	$⊢ j \in ℕ \to {(\frac{j + 1}{e})}^{j + 1} \in ℂ$
110	100 109	mulcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1} \in ℂ$
111		2rp	$⊢ 2 \in ℝ^{+}$
112	111	a1i	$⊢ j \in ℕ \to 2 \in ℝ^{+}$
113		nnre	$⊢ j \in ℕ \to j \in ℝ$
114	104	a1i	$⊢ j \in ℕ \to 0 \in ℝ$
115		1red	$⊢ j \in ℕ \to 1 \in ℝ$
116		0le1	$⊢ 0 \leq 1$
117	116	a1i	$⊢ j \in ℕ \to 0 \leq 1$
118		nnge1	$⊢ j \in ℕ \to 1 \leq j$
119	114 115 113 117 118	letrd	$⊢ j \in ℕ \to 0 \leq j$
120	113 119	ge0p1rpd	$⊢ j \in ℕ \to j + 1 \in ℝ^{+}$
121	112 120	rpmulcld	$⊢ j \in ℕ \to 2 (j + 1) \in ℝ^{+}$
122	121	sqrtgt0d	$⊢ j \in ℕ \to 0 < \sqrt{2 (j + 1)}$
123	122	gt0ne0d	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} \neq 0$
124	81	nnne0d	$⊢ j \in ℕ \to j + 1 \neq 0$
125	98 103 124 107	divne0d	$⊢ j \in ℕ \to \frac{j + 1}{e} \neq 0$
126		nnz	$⊢ j \in ℕ \to j \in ℤ$
127	126	peano2zd	$⊢ j \in ℕ \to j + 1 \in ℤ$
128	108 125 127	expne0d	$⊢ j \in ℕ \to {(\frac{j + 1}{e})}^{j + 1} \neq 0$
129	100 109 123 128	mulne0d	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1} \neq 0$
130	94 110 129	divcld	$⊢ j \in ℕ \to \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}} \in ℂ$
131	82 90 81 130	fvmptd	$⊢ j \in ℕ \to A (j + 1) = \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}}$
132		nnrp	$⊢ (j + 1)! \in ℕ \to (j + 1)! \in ℝ^{+}$
133	91 92 132	3syl	$⊢ j \in ℕ \to (j + 1)! \in ℝ^{+}$
134	121	rpsqrtcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} \in ℝ^{+}$
135		epr	$⊢ e \in ℝ^{+}$
136	135	a1i	$⊢ j \in ℕ \to e \in ℝ^{+}$
137	120 136	rpdivcld	$⊢ j \in ℕ \to \frac{j + 1}{e} \in ℝ^{+}$
138	137 127	rpexpcld	$⊢ j \in ℕ \to {(\frac{j + 1}{e})}^{j + 1} \in ℝ^{+}$
139	134 138	rpmulcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1} \in ℝ^{+}$
140	133 139	rpdivcld	$⊢ j \in ℕ \to \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}} \in ℝ^{+}$
141	131 140	eqeltrd	$⊢ j \in ℕ \to A (j + 1) \in ℝ^{+}$
142	141	relogcld	$⊢ j \in ℕ \to \log A (j + 1) \in ℝ$
143		nfcv	$⊢ \underline{Ⅎ} n (j + 1)$
144	21 143	nffv	$⊢ \underline{Ⅎ} n A (j + 1)$
145	19 144	nffv	$⊢ \underline{Ⅎ} n \log A (j + 1)$
146		2fveq3	$⊢ n = j + 1 \to \log A (n) = \log A (j + 1)$
147	143 145 146 2	fvmptf	$⊢ (j + 1 \in ℕ \land \log A (j + 1) \in ℝ) \to B (j + 1) = \log A (j + 1)$
148	81 142 147	syl2anc	$⊢ j \in ℕ \to B (j + 1) = \log A (j + 1)$
149	148 142	eqeltrd	$⊢ j \in ℕ \to B (j + 1) \in ℝ$
150	79	ffvelrni	$⊢ j \in ℕ \to B (j) \in ℝ$
151		eqid	$⊢ (z \in ℕ ⟼ (\frac{1}{2 z + 1}) {(\frac{1}{2 j + 1})}^{2 z}) = (z \in ℕ ⟼ (\frac{1}{2 z + 1}) {(\frac{1}{2 j + 1})}^{2 z})$
152	1 2 151	stirlinglem11	$⊢ j \in ℕ \to B (j + 1) < B (j)$
153	149 150 152	ltled	$⊢ j \in ℕ \to B (j + 1) \leq B (j)$
154	153	adantl	$⊢ (⊤ \land j \in ℕ) \to B (j + 1) \leq B (j)$
155	52	a1i	$⊢ ⊤ \to \exists x \in ℝ \forall j \in ℕ x \leq B (j)$
156	77 78 80 154 155	climinf	$⊢ ⊤ \to B ⇝ sup (ran B ℝ <)$
157	156	mptru	$⊢ B ⇝ sup (ran B ℝ <)$
158		breq2	$⊢ d = sup (ran B ℝ <) \to (B ⇝ d \leftrightarrow B ⇝ sup (ran B ℝ <))$
159	158	rspcev	$⊢ (sup (ran B ℝ <) \in ℝ \land B ⇝ sup (ran B ℝ <)) \to \exists d \in ℝ B ⇝ d$
160	76 157 159	mp2an	$⊢ \exists d \in ℝ B ⇝ d$

Metamath Proof Explorer

Theorem stirlinglem13

Proof