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	8	rgen	$⊢ \forall n \in ℕ \log A (n) \in ℝ$
54	2	fnmpt	$⊢ \forall n \in ℕ \log A (n) \in ℝ \to B Fn ℕ$
55		fvelrnb	$⊢ B Fn ℕ \to (y \in ran B \leftrightarrow \exists j \in ℕ B (j) = y)$
56	53 54 55	mp2b	$⊢ y \in ran B \leftrightarrow \exists j \in ℕ B (j) = y$
57	56	bilani	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to \exists j \in ℕ B (j) = y$
58		nfra1	$⊢ Ⅎ j \forall j \in ℕ x \leq B (j)$
59		nfv	$⊢ Ⅎ j y \in ran B$
60	58 59	nfan	$⊢ Ⅎ j (\forall j \in ℕ x \leq B (j) \land y \in ran B)$
61		nfv	$⊢ Ⅎ j x \leq y$
62		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)$
63		simp2	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to j \in ℕ$
64		rsp	$⊢ \forall j \in ℕ x \leq B (j) \to (j \in ℕ \to x \leq B (j))$
65	62 63 64	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)$
66		simp3	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to B (j) = y$
67	65 66	breqtrd	$⊢ ((\forall j \in ℕ x \leq B (j) \land y \in ran B) \land j \in ℕ \land B (j) = y) \to x \leq y$
68	67	3exp	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to (j \in ℕ \to (B (j) = y \to x \leq y))$
69	60 61 68	rexlimd	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to (\exists j \in ℕ B (j) = y \to x \leq y)$
70	57 69	mpd	$⊢ (\forall j \in ℕ x \leq B (j) \land y \in ran B) \to x \leq y$
71	70	ralrimiva	$⊢ \forall j \in ℕ x \leq B (j) \to \forall y \in ran B x \leq y$
72	71	reximi	$⊢ \exists x \in ℝ \forall j \in ℕ x \leq B (j) \to \exists x \in ℝ \forall y \in ran B x \leq y$
73	52 72	ax-mp	$⊢ \exists x \in ℝ \forall y \in ran B x \leq y$
74		infrecl	$⊢ (ran B \subseteq ℝ \land ran B \neq \emptyset \land \exists x \in ℝ \forall y \in ran B x \leq y) \to inf (ran B ℝ <) \in ℝ$
75	13 41 73 74	mp3an	$⊢ inf (ran B ℝ <) \in ℝ$
76		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
77		1zzd	$⊢ ⊤ \to 1 \in ℤ$
78	2 8	fmpti	$⊢ B : ℕ ⟶ ℝ$
79	78	a1i	$⊢ ⊤ \to B : ℕ ⟶ ℝ$
80		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
81	1	a1i	$⊢ j \in ℕ \to A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
82		simpr	$⊢ (j \in ℕ \land n = j + 1) \to n = j + 1$
83	82	fveq2d	$⊢ (j \in ℕ \land n = j + 1) \to n! = (j + 1)!$
84	82	oveq2d	$⊢ (j \in ℕ \land n = j + 1) \to 2 n = 2 (j + 1)$
85	84	fveq2d	$⊢ (j \in ℕ \land n = j + 1) \to \sqrt{2 n} = \sqrt{2 (j + 1)}$
86	82	oveq1d	$⊢ (j \in ℕ \land n = j + 1) \to \frac{n}{e} = \frac{j + 1}{e}$
87	86 82	oveq12d	$⊢ (j \in ℕ \land n = j + 1) \to {(\frac{n}{e})}^{n} = {(\frac{j + 1}{e})}^{j + 1}$
88	85 87	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}$
89	83 88	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}}$
90	80	nnnn0d	$⊢ j \in ℕ \to j + 1 \in ℕ_{0}$
91		faccl	$⊢ j + 1 \in ℕ_{0} \to (j + 1)! \in ℕ$
92		nncn	$⊢ (j + 1)! \in ℕ \to (j + 1)! \in ℂ$
93	90 91 92	3syl	$⊢ j \in ℕ \to (j + 1)! \in ℂ$
94		2cnd	$⊢ j \in ℕ \to 2 \in ℂ$
95		nncn	$⊢ j \in ℕ \to j \in ℂ$
96		1cnd	$⊢ j \in ℕ \to 1 \in ℂ$
97	95 96	addcld	$⊢ j \in ℕ \to j + 1 \in ℂ$
98	94 97	mulcld	$⊢ j \in ℕ \to 2 (j + 1) \in ℂ$
99	98	sqrtcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} \in ℂ$
100		ere	$⊢ e \in ℝ$
101	100	recni	$⊢ e \in ℂ$
102	101	a1i	$⊢ j \in ℕ \to e \in ℂ$
103		0re	$⊢ 0 \in ℝ$
104		epos	$⊢ 0 < e$
105	103 104	gtneii	$⊢ e \neq 0$
106	105	a1i	$⊢ j \in ℕ \to e \neq 0$
107	97 102 106	divcld	$⊢ j \in ℕ \to \frac{j + 1}{e} \in ℂ$
108	107 90	expcld	$⊢ j \in ℕ \to {(\frac{j + 1}{e})}^{j + 1} \in ℂ$
109	99 108	mulcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1} \in ℂ$
110		2rp	$⊢ 2 \in ℝ^{+}$
111	110	a1i	$⊢ j \in ℕ \to 2 \in ℝ^{+}$
112		nnre	$⊢ j \in ℕ \to j \in ℝ$
113	103	a1i	$⊢ j \in ℕ \to 0 \in ℝ$
114		1red	$⊢ j \in ℕ \to 1 \in ℝ$
115		0le1	$⊢ 0 \leq 1$
116	115	a1i	$⊢ j \in ℕ \to 0 \leq 1$
117		nnge1	$⊢ j \in ℕ \to 1 \leq j$
118	113 114 112 116 117	letrd	$⊢ j \in ℕ \to 0 \leq j$
119	112 118	ge0p1rpd	$⊢ j \in ℕ \to j + 1 \in ℝ^{+}$
120	111 119	rpmulcld	$⊢ j \in ℕ \to 2 (j + 1) \in ℝ^{+}$
121	120	sqrtgt0d	$⊢ j \in ℕ \to 0 < \sqrt{2 (j + 1)}$
122	121	gt0ne0d	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} \neq 0$
123	80	nnne0d	$⊢ j \in ℕ \to j + 1 \neq 0$
124	97 102 123 106	divne0d	$⊢ j \in ℕ \to \frac{j + 1}{e} \neq 0$
125		nnz	$⊢ j \in ℕ \to j \in ℤ$
126	125	peano2zd	$⊢ j \in ℕ \to j + 1 \in ℤ$
127	107 124 126	expne0d	$⊢ j \in ℕ \to {(\frac{j + 1}{e})}^{j + 1} \neq 0$
128	99 108 122 127	mulne0d	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1} \neq 0$
129	93 109 128	divcld	$⊢ j \in ℕ \to \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}} \in ℂ$
130	81 89 80 129	fvmptd	$⊢ j \in ℕ \to A (j + 1) = \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}}$
131		nnrp	$⊢ (j + 1)! \in ℕ \to (j + 1)! \in ℝ^{+}$
132	90 91 131	3syl	$⊢ j \in ℕ \to (j + 1)! \in ℝ^{+}$
133	120	rpsqrtcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} \in ℝ^{+}$
134		epr	$⊢ e \in ℝ^{+}$
135	134	a1i	$⊢ j \in ℕ \to e \in ℝ^{+}$
136	119 135	rpdivcld	$⊢ j \in ℕ \to \frac{j + 1}{e} \in ℝ^{+}$
137	136 126	rpexpcld	$⊢ j \in ℕ \to {(\frac{j + 1}{e})}^{j + 1} \in ℝ^{+}$
138	133 137	rpmulcld	$⊢ j \in ℕ \to \sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1} \in ℝ^{+}$
139	132 138	rpdivcld	$⊢ j \in ℕ \to \frac{(j + 1)!}{\sqrt{2 (j + 1)} {(\frac{j + 1}{e})}^{j + 1}} \in ℝ^{+}$
140	130 139	eqeltrd	$⊢ j \in ℕ \to A (j + 1) \in ℝ^{+}$
141	140	relogcld	$⊢ j \in ℕ \to \log A (j + 1) \in ℝ$
142		nfcv	$⊢ \underline{Ⅎ} n (j + 1)$
143	21 142	nffv	$⊢ \underline{Ⅎ} n A (j + 1)$
144	19 143	nffv	$⊢ \underline{Ⅎ} n \log A (j + 1)$
145		2fveq3	$⊢ n = j + 1 \to \log A (n) = \log A (j + 1)$
146	142 144 145 2	fvmptf	$⊢ (j + 1 \in ℕ \land \log A (j + 1) \in ℝ) \to B (j + 1) = \log A (j + 1)$
147	80 141 146	syl2anc	$⊢ j \in ℕ \to B (j + 1) = \log A (j + 1)$
148	147 141	eqeltrd	$⊢ j \in ℕ \to B (j + 1) \in ℝ$
149	78	ffvelcdmi	$⊢ j \in ℕ \to B (j) \in ℝ$
150		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})$
151	1 2 150	stirlinglem11	$⊢ j \in ℕ \to B (j + 1) < B (j)$
152	148 149 151	ltled	$⊢ j \in ℕ \to B (j + 1) \leq B (j)$
153	152	adantl	$⊢ (⊤ \land j \in ℕ) \to B (j + 1) \leq B (j)$
154	52	a1i	$⊢ ⊤ \to \exists x \in ℝ \forall j \in ℕ x \leq B (j)$
155	76 77 79 153 154	climinf	$⊢ ⊤ \to B ⇝ inf (ran B ℝ <)$
156	155	mptru	$⊢ B ⇝ inf (ran B ℝ <)$
157		breq2	$⊢ d = inf (ran B ℝ <) \to (B ⇝ d \leftrightarrow B ⇝ inf (ran B ℝ <))$
158	157	rspcev	$⊢ (inf (ran B ℝ <) \in ℝ \land B ⇝ inf (ran B ℝ <)) \to \exists d \in ℝ B ⇝ d$
159	75 156 158	mp2an	$⊢ \exists d \in ℝ B ⇝ d$

Metamath Proof Explorer

Theorem stirlinglem13

Proof