stirlinglem4

Description: Algebraic manipulation of ( ( B n ) - ( B ( n + 1 ) ) ) . It will be used in other theorems to show that B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlinglem4.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
	stirlinglem4.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
	stirlinglem4.3	$⊢ J = (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1)$
Assertion	stirlinglem4	$⊢ N \in ℕ \to B (N) - B (N + 1) = J (N)$

Proof

Step	Hyp	Ref	Expression
1		stirlinglem4.1	$⊢ A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
2		stirlinglem4.2	$⊢ B = (n \in ℕ ⟼ \log A (n))$
3		stirlinglem4.3	$⊢ J = (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1)$
4		nnre	$⊢ N \in ℕ \to N \in ℝ$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6	5	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N$
7	4 6	ge0p1rpd	$⊢ N \in ℕ \to N + 1 \in ℝ^{+}$
8		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
9	7 8	rpdivcld	$⊢ N \in ℕ \to \frac{N + 1}{N} \in ℝ^{+}$
10	9	rpsqrtcld	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} \in ℝ^{+}$
11		nnz	$⊢ N \in ℕ \to N \in ℤ$
12	9 11	rpexpcld	$⊢ N \in ℕ \to {(\frac{N + 1}{N})}^{N} \in ℝ^{+}$
13	10 12	rpmulcld	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N} \in ℝ^{+}$
14		epr	$⊢ e \in ℝ^{+}$
15	14	a1i	$⊢ N \in ℕ \to e \in ℝ^{+}$
16	13 15	relogdivd	$⊢ N \in ℕ \to \log (\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}}{e}) = \log \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N} - \log e$
17	10 12	relogmuld	$⊢ N \in ℕ \to \log \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N} = \log \sqrt{\frac{N + 1}{N}} + \log {(\frac{N + 1}{N})}^{N}$
18		logsqrt	$⊢ \frac{N + 1}{N} \in ℝ^{+} \to \log \sqrt{\frac{N + 1}{N}} = \frac{\log (\frac{N + 1}{N})}{2}$
19	9 18	syl	$⊢ N \in ℕ \to \log \sqrt{\frac{N + 1}{N}} = \frac{\log (\frac{N + 1}{N})}{2}$
20		relogexp	$⊢ (\frac{N + 1}{N} \in ℝ^{+} \land N \in ℤ) \to \log {(\frac{N + 1}{N})}^{N} = N \log (\frac{N + 1}{N})$
21	9 11 20	syl2anc	$⊢ N \in ℕ \to \log {(\frac{N + 1}{N})}^{N} = N \log (\frac{N + 1}{N})$
22	19 21	oveq12d	$⊢ N \in ℕ \to \log \sqrt{\frac{N + 1}{N}} + \log {(\frac{N + 1}{N})}^{N} = (\frac{\log (\frac{N + 1}{N})}{2}) + N \log (\frac{N + 1}{N})$
23	17 22	eqtrd	$⊢ N \in ℕ \to \log \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N} = (\frac{\log (\frac{N + 1}{N})}{2}) + N \log (\frac{N + 1}{N})$
24		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
25	24	nncnd	$⊢ N \in ℕ \to N + 1 \in ℂ$
26		nncn	$⊢ N \in ℕ \to N \in ℂ$
27		nnne0	$⊢ N \in ℕ \to N \neq 0$
28	25 26 27	divcld	$⊢ N \in ℕ \to \frac{N + 1}{N} \in ℂ$
29	24	nnne0d	$⊢ N \in ℕ \to N + 1 \neq 0$
30	25 26 29 27	divne0d	$⊢ N \in ℕ \to \frac{N + 1}{N} \neq 0$
31	28 30	logcld	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) \in ℂ$
32		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
33		2rp	$⊢ 2 \in ℝ^{+}$
34	33	a1i	$⊢ N \in ℕ \to 2 \in ℝ^{+}$
35	34	rpne0d	$⊢ N \in ℕ \to 2 \neq 0$
36	31 32 35	divrec2d	$⊢ N \in ℕ \to \frac{\log (\frac{N + 1}{N})}{2} = (\frac{1}{2}) \log (\frac{N + 1}{N})$
37	36	oveq1d	$⊢ N \in ℕ \to (\frac{\log (\frac{N + 1}{N})}{2}) + N \log (\frac{N + 1}{N}) = (\frac{1}{2}) \log (\frac{N + 1}{N}) + N \log (\frac{N + 1}{N})$
38		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
39	38	halfcld	$⊢ N \in ℕ \to \frac{1}{2} \in ℂ$
40	39 26 31	adddird	$⊢ N \in ℕ \to ((\frac{1}{2}) + N) \log (\frac{N + 1}{N}) = (\frac{1}{2}) \log (\frac{N + 1}{N}) + N \log (\frac{N + 1}{N})$
41	26 32 35	divcan4d	$⊢ N \in ℕ \to \frac{N \cdot 2}{2} = N$
42	26 32	mulcomd	$⊢ N \in ℕ \to N \cdot 2 = 2 \cdot N$
43	42	oveq1d	$⊢ N \in ℕ \to \frac{N \cdot 2}{2} = \frac{2 \cdot N}{2}$
44	41 43	eqtr3d	$⊢ N \in ℕ \to N = \frac{2 \cdot N}{2}$
45	44	oveq2d	$⊢ N \in ℕ \to (\frac{1}{2}) + N = (\frac{1}{2}) + (\frac{2 \cdot N}{2})$
46	32 26	mulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℂ$
47	38 46 32 35	divdird	$⊢ N \in ℕ \to \frac{1 + 2 \cdot N}{2} = (\frac{1}{2}) + (\frac{2 \cdot N}{2})$
48	45 47	eqtr4d	$⊢ N \in ℕ \to (\frac{1}{2}) + N = \frac{1 + 2 \cdot N}{2}$
49	48	oveq1d	$⊢ N \in ℕ \to ((\frac{1}{2}) + N) \log (\frac{N + 1}{N}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N})$
50	40 49	eqtr3d	$⊢ N \in ℕ \to (\frac{1}{2}) \log (\frac{N + 1}{N}) + N \log (\frac{N + 1}{N}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N})$
51	23 37 50	3eqtrd	$⊢ N \in ℕ \to \log \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N} = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N})$
52		loge	$⊢ \log e = 1$
53	52	a1i	$⊢ N \in ℕ \to \log e = 1$
54	51 53	oveq12d	$⊢ N \in ℕ \to \log \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N} - \log e = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
55	16 54	eqtrd	$⊢ N \in ℕ \to \log (\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}}{e}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
56	1	stirlinglem2	$⊢ N \in ℕ \to A (N) \in ℝ^{+}$
57	56	relogcld	$⊢ N \in ℕ \to \log A (N) \in ℝ$
58		nfcv	$⊢ \underline{Ⅎ} n N$
59		nfcv	$⊢ \underline{Ⅎ} n log$
60		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
61	1 60	nfcxfr	$⊢ \underline{Ⅎ} n A$
62	61 58	nffv	$⊢ \underline{Ⅎ} n A (N)$
63	59 62	nffv	$⊢ \underline{Ⅎ} n \log A (N)$
64		2fveq3	$⊢ n = N \to \log A (n) = \log A (N)$
65	58 63 64 2	fvmptf	$⊢ (N \in ℕ \land \log A (N) \in ℝ) \to B (N) = \log A (N)$
66	57 65	mpdan	$⊢ N \in ℕ \to B (N) = \log A (N)$
67		nfcv	$⊢ \underline{Ⅎ} k \log A (n)$
68		nfcv	$⊢ \underline{Ⅎ} n k$
69	61 68	nffv	$⊢ \underline{Ⅎ} n A (k)$
70	59 69	nffv	$⊢ \underline{Ⅎ} n \log A (k)$
71		2fveq3	$⊢ n = k \to \log A (n) = \log A (k)$
72	67 70 71	cbvmpt	$⊢ (n \in ℕ ⟼ \log A (n)) = (k \in ℕ ⟼ \log A (k))$
73	2 72	eqtri	$⊢ B = (k \in ℕ ⟼ \log A (k))$
74	73	a1i	$⊢ N \in ℕ \to B = (k \in ℕ ⟼ \log A (k))$
75		simpr	$⊢ (N \in ℕ \land k = N + 1) \to k = N + 1$
76	75	fveq2d	$⊢ (N \in ℕ \land k = N + 1) \to A (k) = A (N + 1)$
77	76	fveq2d	$⊢ (N \in ℕ \land k = N + 1) \to \log A (k) = \log A (N + 1)$
78	1	stirlinglem2	$⊢ N + 1 \in ℕ \to A (N + 1) \in ℝ^{+}$
79	24 78	syl	$⊢ N \in ℕ \to A (N + 1) \in ℝ^{+}$
80	79	relogcld	$⊢ N \in ℕ \to \log A (N + 1) \in ℝ$
81	74 77 24 80	fvmptd	$⊢ N \in ℕ \to B (N + 1) = \log A (N + 1)$
82	66 81	oveq12d	$⊢ N \in ℕ \to B (N) - B (N + 1) = \log A (N) - \log A (N + 1)$
83	56 79	relogdivd	$⊢ N \in ℕ \to \log (\frac{A (N)}{A (N + 1)}) = \log A (N) - \log A (N + 1)$
84		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
85		nnrp	$⊢ N! \in ℕ \to N! \in ℝ^{+}$
86	5 84 85	3syl	$⊢ N \in ℕ \to N! \in ℝ^{+}$
87	34 8	rpmulcld	$⊢ N \in ℕ \to 2 \cdot N \in ℝ^{+}$
88	87	rpsqrtcld	$⊢ N \in ℕ \to \sqrt{2 \cdot N} \in ℝ^{+}$
89	8 15	rpdivcld	$⊢ N \in ℕ \to \frac{N}{e} \in ℝ^{+}$
90	89 11	rpexpcld	$⊢ N \in ℕ \to {(\frac{N}{e})}^{N} \in ℝ^{+}$
91	88 90	rpmulcld	$⊢ N \in ℕ \to \sqrt{2 \cdot N} {(\frac{N}{e})}^{N} \in ℝ^{+}$
92	86 91	rpdivcld	$⊢ N \in ℕ \to \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}$
93	1	a1i	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to A = (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
94		simpr	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to n = N$
95	94	fveq2d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to n! = N!$
96	94	oveq2d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to 2 n = 2 \cdot N$
97	96	fveq2d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to \sqrt{2 n} = \sqrt{2 \cdot N}$
98	94	oveq1d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to \frac{n}{e} = \frac{N}{e}$
99	98 94	oveq12d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to {(\frac{n}{e})}^{n} = {(\frac{N}{e})}^{N}$
100	97 99	oveq12d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 \cdot N} {(\frac{N}{e})}^{N}$
101	95 100	oveq12d	$⊢ ((N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \land n = N) \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} = \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
102		simpl	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to N \in ℕ$
103	86	rpcnd	$⊢ N \in ℕ \to N! \in ℂ$
104	103	adantr	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to N! \in ℂ$
105		2cnd	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to 2 \in ℂ$
106	102	nncnd	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to N \in ℂ$
107	105 106	mulcld	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to 2 \cdot N \in ℂ$
108	107	sqrtcld	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \sqrt{2 \cdot N} \in ℂ$
109		ere	$⊢ e \in ℝ$
110	109	recni	$⊢ e \in ℂ$
111	110	a1i	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to e \in ℂ$
112		0re	$⊢ 0 \in ℝ$
113		epos	$⊢ 0 < e$
114	112 113	gtneii	$⊢ e \neq 0$
115	114	a1i	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to e \neq 0$
116	106 111 115	divcld	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \frac{N}{e} \in ℂ$
117	102	nnnn0d	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to N \in ℕ_{0}$
118	116 117	expcld	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to {(\frac{N}{e})}^{N} \in ℂ$
119	108 118	mulcld	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \sqrt{2 \cdot N} {(\frac{N}{e})}^{N} \in ℂ$
120	88	rpne0d	$⊢ N \in ℕ \to \sqrt{2 \cdot N} \neq 0$
121	120	adantr	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \sqrt{2 \cdot N} \neq 0$
122	102	nnne0d	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to N \neq 0$
123	106 111 122 115	divne0d	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \frac{N}{e} \neq 0$
124	102	nnzd	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to N \in ℤ$
125	116 123 124	expne0d	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to {(\frac{N}{e})}^{N} \neq 0$
126	108 118 121 125	mulne0d	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \sqrt{2 \cdot N} {(\frac{N}{e})}^{N} \neq 0$
127	104 119 126	divcld	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℂ$
128	93 101 102 127	fvmptd	$⊢ (N \in ℕ \land \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} \in ℝ^{+}) \to A (N) = \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
129	92 128	mpdan	$⊢ N \in ℕ \to A (N) = \frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
130		nfcv	$⊢ \underline{Ⅎ} k (\frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}})$
131		nfcv	$⊢ \underline{Ⅎ} n (\frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}})$
132		fveq2	$⊢ n = k \to n! = k!$
133		oveq2	$⊢ n = k \to 2 n = 2 k$
134	133	fveq2d	$⊢ n = k \to \sqrt{2 n} = \sqrt{2 k}$
135		oveq1	$⊢ n = k \to \frac{n}{e} = \frac{k}{e}$
136		id	$⊢ n = k \to n = k$
137	135 136	oveq12d	$⊢ n = k \to {(\frac{n}{e})}^{n} = {(\frac{k}{e})}^{k}$
138	134 137	oveq12d	$⊢ n = k \to \sqrt{2 n} {(\frac{n}{e})}^{n} = \sqrt{2 k} {(\frac{k}{e})}^{k}$
139	132 138	oveq12d	$⊢ n = k \to \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}} = \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}}$
140	130 131 139	cbvmpt	$⊢ (n \in ℕ ⟼ \frac{n!}{\sqrt{2 n} {(\frac{n}{e})}^{n}}) = (k \in ℕ ⟼ \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}})$
141	1 140	eqtri	$⊢ A = (k \in ℕ ⟼ \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}})$
142	141	a1i	$⊢ N \in ℕ \to A = (k \in ℕ ⟼ \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}})$
143	75	fveq2d	$⊢ (N \in ℕ \land k = N + 1) \to k! = (N + 1)!$
144	75	oveq2d	$⊢ (N \in ℕ \land k = N + 1) \to 2 k = 2 (N + 1)$
145	144	fveq2d	$⊢ (N \in ℕ \land k = N + 1) \to \sqrt{2 k} = \sqrt{2 (N + 1)}$
146	75	oveq1d	$⊢ (N \in ℕ \land k = N + 1) \to \frac{k}{e} = \frac{N + 1}{e}$
147	146 75	oveq12d	$⊢ (N \in ℕ \land k = N + 1) \to {(\frac{k}{e})}^{k} = {(\frac{N + 1}{e})}^{N + 1}$
148	145 147	oveq12d	$⊢ (N \in ℕ \land k = N + 1) \to \sqrt{2 k} {(\frac{k}{e})}^{k} = \sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}$
149	143 148	oveq12d	$⊢ (N \in ℕ \land k = N + 1) \to \frac{k!}{\sqrt{2 k} {(\frac{k}{e})}^{k}} = \frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}$
150	24	nnnn0d	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
151		faccl	$⊢ N + 1 \in ℕ_{0} \to (N + 1)! \in ℕ$
152		nnrp	$⊢ (N + 1)! \in ℕ \to (N + 1)! \in ℝ^{+}$
153	150 151 152	3syl	$⊢ N \in ℕ \to (N + 1)! \in ℝ^{+}$
154	34 7	rpmulcld	$⊢ N \in ℕ \to 2 (N + 1) \in ℝ^{+}$
155	154	rpsqrtcld	$⊢ N \in ℕ \to \sqrt{2 (N + 1)} \in ℝ^{+}$
156	7 15	rpdivcld	$⊢ N \in ℕ \to \frac{N + 1}{e} \in ℝ^{+}$
157	11	peano2zd	$⊢ N \in ℕ \to N + 1 \in ℤ$
158	156 157	rpexpcld	$⊢ N \in ℕ \to {(\frac{N + 1}{e})}^{N + 1} \in ℝ^{+}$
159	155 158	rpmulcld	$⊢ N \in ℕ \to \sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1} \in ℝ^{+}$
160	153 159	rpdivcld	$⊢ N \in ℕ \to \frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}} \in ℝ^{+}$
161	142 149 24 160	fvmptd	$⊢ N \in ℕ \to A (N + 1) = \frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}$
162	129 161	oveq12d	$⊢ N \in ℕ \to \frac{A (N)}{A (N + 1)} = \frac{\frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}}{\frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}$
163		facp1	$⊢ N \in ℕ_{0} \to (N + 1)! = N! (N + 1)$
164	5 163	syl	$⊢ N \in ℕ \to (N + 1)! = N! (N + 1)$
165	164	oveq1d	$⊢ N \in ℕ \to \frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}} = \frac{N! (N + 1)}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}$
166	159	rpcnd	$⊢ N \in ℕ \to \sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1} \in ℂ$
167	159	rpne0d	$⊢ N \in ℕ \to \sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1} \neq 0$
168	103 25 166 167	divassd	$⊢ N \in ℕ \to \frac{N! (N + 1)}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}} = N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})$
169	165 168	eqtrd	$⊢ N \in ℕ \to \frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}} = N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})$
170	169	oveq2d	$⊢ N \in ℕ \to \frac{\frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}}{\frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}} = \frac{\frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})}$
171	91	rpcnd	$⊢ N \in ℕ \to \sqrt{2 \cdot N} {(\frac{N}{e})}^{N} \in ℂ$
172	25 166 167	divcld	$⊢ N \in ℕ \to \frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}} \in ℂ$
173	103 172	mulcld	$⊢ N \in ℕ \to N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}) \in ℂ$
174	91	rpne0d	$⊢ N \in ℕ \to \sqrt{2 \cdot N} {(\frac{N}{e})}^{N} \neq 0$
175	86	rpne0d	$⊢ N \in ℕ \to N! \neq 0$
176	25 166 29 167	divne0d	$⊢ N \in ℕ \to \frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}} \neq 0$
177	103 172 175 176	mulne0d	$⊢ N \in ℕ \to N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}) \neq 0$
178	103 171 173 174 177	divdiv32d	$⊢ N \in ℕ \to \frac{\frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})} = \frac{\frac{N!}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
179	103 103 172 175 176	divdiv1d	$⊢ N \in ℕ \to \frac{\frac{N!}{N!}}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}} = \frac{N!}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})}$
180	179	eqcomd	$⊢ N \in ℕ \to \frac{N!}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})} = \frac{\frac{N!}{N!}}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}$
181	180	oveq1d	$⊢ N \in ℕ \to \frac{\frac{N!}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} = \frac{\frac{\frac{N!}{N!}}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
182	103 175	dividd	$⊢ N \in ℕ \to \frac{N!}{N!} = 1$
183	182	oveq1d	$⊢ N \in ℕ \to \frac{\frac{N!}{N!}}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}} = \frac{1}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}$
184	183	oveq1d	$⊢ N \in ℕ \to \frac{\frac{\frac{N!}{N!}}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} = \frac{\frac{1}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
185	25 166 29 167	recdivd	$⊢ N \in ℕ \to \frac{1}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}} = \frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}$
186	185	oveq1d	$⊢ N \in ℕ \to \frac{\frac{1}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} = \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
187	166 25 29	divcld	$⊢ N \in ℕ \to \frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1} \in ℂ$
188	88	rpcnd	$⊢ N \in ℕ \to \sqrt{2 \cdot N} \in ℂ$
189	90	rpcnd	$⊢ N \in ℕ \to {(\frac{N}{e})}^{N} \in ℂ$
190	90	rpne0d	$⊢ N \in ℕ \to {(\frac{N}{e})}^{N} \neq 0$
191	187 188 189 120 190	divdiv1d	$⊢ N \in ℕ \to \frac{\frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N}}}{{(\frac{N}{e})}^{N}} = \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}$
192	166 25 188 29 120	divdiv32d	$⊢ N \in ℕ \to \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N}} = \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{\sqrt{2 \cdot N}}}{N + 1}$
193	155	rpcnd	$⊢ N \in ℕ \to \sqrt{2 (N + 1)} \in ℂ$
194	158	rpcnd	$⊢ N \in ℕ \to {(\frac{N + 1}{e})}^{N + 1} \in ℂ$
195	193 194 188 120	div23d	$⊢ N \in ℕ \to \frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{\sqrt{2 \cdot N}} = (\frac{\sqrt{2 (N + 1)}}{\sqrt{2 \cdot N}}) {(\frac{N + 1}{e})}^{N + 1}$
196	34	rpred	$⊢ N \in ℕ \to 2 \in ℝ$
197	34	rpge0d	$⊢ N \in ℕ \to 0 \leq 2$
198	24	nnred	$⊢ N \in ℕ \to N + 1 \in ℝ$
199	150	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N + 1$
200	196 197 198 199	sqrtmuld	$⊢ N \in ℕ \to \sqrt{2 (N + 1)} = \sqrt{2} \sqrt{N + 1}$
201	196 197 4 6	sqrtmuld	$⊢ N \in ℕ \to \sqrt{2 \cdot N} = \sqrt{2} \sqrt{N}$
202	200 201	oveq12d	$⊢ N \in ℕ \to \frac{\sqrt{2 (N + 1)}}{\sqrt{2 \cdot N}} = \frac{\sqrt{2} \sqrt{N + 1}}{\sqrt{2} \sqrt{N}}$
203	32	sqrtcld	$⊢ N \in ℕ \to \sqrt{2} \in ℂ$
204	25	sqrtcld	$⊢ N \in ℕ \to \sqrt{N + 1} \in ℂ$
205	26	sqrtcld	$⊢ N \in ℕ \to \sqrt{N} \in ℂ$
206	34	rpsqrtcld	$⊢ N \in ℕ \to \sqrt{2} \in ℝ^{+}$
207	206	rpne0d	$⊢ N \in ℕ \to \sqrt{2} \neq 0$
208	8	rpsqrtcld	$⊢ N \in ℕ \to \sqrt{N} \in ℝ^{+}$
209	208	rpne0d	$⊢ N \in ℕ \to \sqrt{N} \neq 0$
210	203 203 204 205 207 209	divmuldivd	$⊢ N \in ℕ \to (\frac{\sqrt{2}}{\sqrt{2}}) (\frac{\sqrt{N + 1}}{\sqrt{N}}) = \frac{\sqrt{2} \sqrt{N + 1}}{\sqrt{2} \sqrt{N}}$
211	203 207	dividd	$⊢ N \in ℕ \to \frac{\sqrt{2}}{\sqrt{2}} = 1$
212	198 199 8	sqrtdivd	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} = \frac{\sqrt{N + 1}}{\sqrt{N}}$
213	212	eqcomd	$⊢ N \in ℕ \to \frac{\sqrt{N + 1}}{\sqrt{N}} = \sqrt{\frac{N + 1}{N}}$
214	211 213	oveq12d	$⊢ N \in ℕ \to (\frac{\sqrt{2}}{\sqrt{2}}) (\frac{\sqrt{N + 1}}{\sqrt{N}}) = 1 \sqrt{\frac{N + 1}{N}}$
215	202 210 214	3eqtr2d	$⊢ N \in ℕ \to \frac{\sqrt{2 (N + 1)}}{\sqrt{2 \cdot N}} = 1 \sqrt{\frac{N + 1}{N}}$
216	215	oveq1d	$⊢ N \in ℕ \to (\frac{\sqrt{2 (N + 1)}}{\sqrt{2 \cdot N}}) {(\frac{N + 1}{e})}^{N + 1} = 1 \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}$
217	28	sqrtcld	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} \in ℂ$
218	217	mullidd	$⊢ N \in ℕ \to 1 \sqrt{\frac{N + 1}{N}} = \sqrt{\frac{N + 1}{N}}$
219	218	oveq1d	$⊢ N \in ℕ \to 1 \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1} = \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}$
220	195 216 219	3eqtrd	$⊢ N \in ℕ \to \frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{\sqrt{2 \cdot N}} = \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}$
221	220	oveq1d	$⊢ N \in ℕ \to \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{\sqrt{2 \cdot N}}}{N + 1} = \frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}$
222	192 221	eqtrd	$⊢ N \in ℕ \to \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N}} = \frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}$
223	222	oveq1d	$⊢ N \in ℕ \to \frac{\frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N}}}{{(\frac{N}{e})}^{N}} = \frac{\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{{(\frac{N}{e})}^{N}}$
224	191 223	eqtr3d	$⊢ N \in ℕ \to \frac{\frac{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} = \frac{\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{{(\frac{N}{e})}^{N}}$
225	217 194	mulcld	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1} \in ℂ$
226	225 25 189 29 190	divdiv32d	$⊢ N \in ℕ \to \frac{\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{{(\frac{N}{e})}^{N}} = \frac{\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}}}{N + 1}$
227	217 194 189 190	divassd	$⊢ N \in ℕ \to \frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}} = \sqrt{\frac{N + 1}{N}} (\frac{{(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}})$
228	15	rpcnd	$⊢ N \in ℕ \to e \in ℂ$
229	15	rpne0d	$⊢ N \in ℕ \to e \neq 0$
230	25 228 229 150	expdivd	$⊢ N \in ℕ \to {(\frac{N + 1}{e})}^{N + 1} = \frac{{(N + 1)}^{N + 1}}{e^{N + 1}}$
231	26 228 229 5	expdivd	$⊢ N \in ℕ \to {(\frac{N}{e})}^{N} = \frac{N^{N}}{e^{N}}$
232	230 231	oveq12d	$⊢ N \in ℕ \to \frac{{(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}} = \frac{\frac{{(N + 1)}^{N + 1}}{e^{N + 1}}}{\frac{N^{N}}{e^{N}}}$
233	232	oveq2d	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} (\frac{{(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}}) = \sqrt{\frac{N + 1}{N}} (\frac{\frac{{(N + 1)}^{N + 1}}{e^{N + 1}}}{\frac{N^{N}}{e^{N}}})$
234	25 150	expcld	$⊢ N \in ℕ \to {(N + 1)}^{N + 1} \in ℂ$
235	228 150	expcld	$⊢ N \in ℕ \to e^{N + 1} \in ℂ$
236	26 5	expcld	$⊢ N \in ℕ \to N^{N} \in ℂ$
237	228 5	expcld	$⊢ N \in ℕ \to e^{N} \in ℂ$
238	228 229 157	expne0d	$⊢ N \in ℕ \to e^{N + 1} \neq 0$
239	228 229 11	expne0d	$⊢ N \in ℕ \to e^{N} \neq 0$
240	26 27 11	expne0d	$⊢ N \in ℕ \to N^{N} \neq 0$
241	234 235 236 237 238 239 240	divdivdivd	$⊢ N \in ℕ \to \frac{\frac{{(N + 1)}^{N + 1}}{e^{N + 1}}}{\frac{N^{N}}{e^{N}}} = \frac{{(N + 1)}^{N + 1} e^{N}}{e^{N + 1} N^{N}}$
242	234 237	mulcomd	$⊢ N \in ℕ \to {(N + 1)}^{N + 1} e^{N} = e^{N} {(N + 1)}^{N + 1}$
243	242	oveq1d	$⊢ N \in ℕ \to \frac{{(N + 1)}^{N + 1} e^{N}}{e^{N + 1} N^{N}} = \frac{e^{N} {(N + 1)}^{N + 1}}{e^{N + 1} N^{N}}$
244	237 235 234 236 238 240	divmuldivd	$⊢ N \in ℕ \to (\frac{e^{N}}{e^{N + 1}}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = \frac{e^{N} {(N + 1)}^{N + 1}}{e^{N + 1} N^{N}}$
245	228 5	expp1d	$⊢ N \in ℕ \to e^{N + 1} = e^{N} e$
246	245	oveq2d	$⊢ N \in ℕ \to \frac{e^{N}}{e^{N + 1}} = \frac{e^{N}}{e^{N} e}$
247	237 237 228 239 229	divdiv1d	$⊢ N \in ℕ \to \frac{\frac{e^{N}}{e^{N}}}{e} = \frac{e^{N}}{e^{N} e}$
248	237 239	dividd	$⊢ N \in ℕ \to \frac{e^{N}}{e^{N}} = 1$
249	248	oveq1d	$⊢ N \in ℕ \to \frac{\frac{e^{N}}{e^{N}}}{e} = \frac{1}{e}$
250	246 247 249	3eqtr2d	$⊢ N \in ℕ \to \frac{e^{N}}{e^{N + 1}} = \frac{1}{e}$
251	250	oveq1d	$⊢ N \in ℕ \to (\frac{e^{N}}{e^{N + 1}}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})$
252	244 251	eqtr3d	$⊢ N \in ℕ \to \frac{e^{N} {(N + 1)}^{N + 1}}{e^{N + 1} N^{N}} = (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})$
253	241 243 252	3eqtrd	$⊢ N \in ℕ \to \frac{\frac{{(N + 1)}^{N + 1}}{e^{N + 1}}}{\frac{N^{N}}{e^{N}}} = (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})$
254	253	oveq2d	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} (\frac{\frac{{(N + 1)}^{N + 1}}{e^{N + 1}}}{\frac{N^{N}}{e^{N}}}) = \sqrt{\frac{N + 1}{N}} (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})$
255	227 233 254	3eqtrd	$⊢ N \in ℕ \to \frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}} = \sqrt{\frac{N + 1}{N}} (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})$
256	255	oveq1d	$⊢ N \in ℕ \to \frac{\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{{(\frac{N}{e})}^{N}}}{N + 1} = \frac{\sqrt{\frac{N + 1}{N}} (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{N + 1}$
257	234 236 240	divcld	$⊢ N \in ℕ \to \frac{{(N + 1)}^{N + 1}}{N^{N}} \in ℂ$
258	38 228 257 229	div32d	$⊢ N \in ℕ \to (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = 1 (\frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e})$
259	257 228 229	divcld	$⊢ N \in ℕ \to \frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e} \in ℂ$
260	259	mullidd	$⊢ N \in ℕ \to 1 (\frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e}) = \frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e}$
261	258 260	eqtrd	$⊢ N \in ℕ \to (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = \frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e}$
262	261	oveq2d	$⊢ N \in ℕ \to (\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = (\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e})$
263	228 229	reccld	$⊢ N \in ℕ \to \frac{1}{e} \in ℂ$
264	263 257	mulcld	$⊢ N \in ℕ \to (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) \in ℂ$
265	217 264 25 29	div23d	$⊢ N \in ℕ \to \frac{\sqrt{\frac{N + 1}{N}} (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{N + 1} = (\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})$
266	217 25 29	divcld	$⊢ N \in ℕ \to \frac{\sqrt{\frac{N + 1}{N}}}{N + 1} \in ℂ$
267	266 257 228 229	divassd	$⊢ N \in ℕ \to \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e} = (\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{e})$
268	262 265 267	3eqtr4d	$⊢ N \in ℕ \to \frac{\sqrt{\frac{N + 1}{N}} (\frac{1}{e}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{N + 1} = \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e}$
269	226 256 268	3eqtrd	$⊢ N \in ℕ \to \frac{\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{e})}^{N + 1}}{N + 1}}{{(\frac{N}{e})}^{N}} = \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e}$
270	186 224 269	3eqtrd	$⊢ N \in ℕ \to \frac{\frac{1}{\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} = \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e}$
271	181 184 270	3eqtrd	$⊢ N \in ℕ \to \frac{\frac{N!}{N! (\frac{N + 1}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}})}}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}} = \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e}$
272	170 178 271	3eqtrd	$⊢ N \in ℕ \to \frac{\frac{N!}{\sqrt{2 \cdot N} {(\frac{N}{e})}^{N}}}{\frac{(N + 1)!}{\sqrt{2 (N + 1)} {(\frac{N + 1}{e})}^{N + 1}}} = \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e}$
273	217 25 257 29	div32d	$⊢ N \in ℕ \to (\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = \sqrt{\frac{N + 1}{N}} (\frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{N + 1})$
274	25 5	expp1d	$⊢ N \in ℕ \to {(N + 1)}^{N + 1} = {(N + 1)}^{N} (N + 1)$
275	274	oveq1d	$⊢ N \in ℕ \to \frac{{(N + 1)}^{N + 1}}{N + 1} = \frac{{(N + 1)}^{N} (N + 1)}{N + 1}$
276	25 5	expcld	$⊢ N \in ℕ \to {(N + 1)}^{N} \in ℂ$
277	276 25 29	divcan4d	$⊢ N \in ℕ \to \frac{{(N + 1)}^{N} (N + 1)}{N + 1} = {(N + 1)}^{N}$
278	275 277	eqtrd	$⊢ N \in ℕ \to \frac{{(N + 1)}^{N + 1}}{N + 1} = {(N + 1)}^{N}$
279	278	oveq1d	$⊢ N \in ℕ \to \frac{\frac{{(N + 1)}^{N + 1}}{N + 1}}{N^{N}} = \frac{{(N + 1)}^{N}}{N^{N}}$
280	234 236 25 240 29	divdiv32d	$⊢ N \in ℕ \to \frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{N + 1} = \frac{\frac{{(N + 1)}^{N + 1}}{N + 1}}{N^{N}}$
281	25 26 27 5	expdivd	$⊢ N \in ℕ \to {(\frac{N + 1}{N})}^{N} = \frac{{(N + 1)}^{N}}{N^{N}}$
282	279 280 281	3eqtr4d	$⊢ N \in ℕ \to \frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{N + 1} = {(\frac{N + 1}{N})}^{N}$
283	282	oveq2d	$⊢ N \in ℕ \to \sqrt{\frac{N + 1}{N}} (\frac{\frac{{(N + 1)}^{N + 1}}{N^{N}}}{N + 1}) = \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}$
284	273 283	eqtrd	$⊢ N \in ℕ \to (\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}}) = \sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}$
285	284	oveq1d	$⊢ N \in ℕ \to \frac{(\frac{\sqrt{\frac{N + 1}{N}}}{N + 1}) (\frac{{(N + 1)}^{N + 1}}{N^{N}})}{e} = \frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}}{e}$
286	162 272 285	3eqtrd	$⊢ N \in ℕ \to \frac{A (N)}{A (N + 1)} = \frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}}{e}$
287	286	fveq2d	$⊢ N \in ℕ \to \log (\frac{A (N)}{A (N + 1)}) = \log (\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}}{e})$
288	82 83 287	3eqtr2d	$⊢ N \in ℕ \to B (N) - B (N + 1) = \log (\frac{\sqrt{\frac{N + 1}{N}} {(\frac{N + 1}{N})}^{N}}{e})$
289	38 46	addcld	$⊢ N \in ℕ \to 1 + 2 \cdot N \in ℂ$
290	289	halfcld	$⊢ N \in ℕ \to \frac{1 + 2 \cdot N}{2} \in ℂ$
291	290 31	mulcld	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) \in ℂ$
292	291 38	subcld	$⊢ N \in ℕ \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ$
293	3	a1i	$⊢ (N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \to J = (n \in ℕ ⟼ (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1)$
294		simpr	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to n = N$
295	294	oveq2d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to 2 n = 2 \cdot N$
296	295	oveq2d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to 1 + 2 n = 1 + 2 \cdot N$
297	296	oveq1d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to \frac{1 + 2 n}{2} = \frac{1 + 2 \cdot N}{2}$
298	294	oveq1d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to n + 1 = N + 1$
299	298 294	oveq12d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to \frac{n + 1}{n} = \frac{N + 1}{N}$
300	299	fveq2d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to \log (\frac{n + 1}{n}) = \log (\frac{N + 1}{N})$
301	297 300	oveq12d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N})$
302	301	oveq1d	$⊢ ((N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \land n = N) \to (\frac{1 + 2 n}{2}) \log (\frac{n + 1}{n}) - 1 = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
303		simpl	$⊢ (N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \to N \in ℕ$
304		simpr	$⊢ (N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \to (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ$
305	293 302 303 304	fvmptd	$⊢ (N \in ℕ \land (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1 \in ℂ) \to J (N) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
306	292 305	mpdan	$⊢ N \in ℕ \to J (N) = (\frac{1 + 2 \cdot N}{2}) \log (\frac{N + 1}{N}) - 1$
307	55 288 306	3eqtr4d	$⊢ N \in ℕ \to B (N) - B (N + 1) = J (N)$

Metamath Proof Explorer

Theorem stirlinglem4

Proof