# Metamath Proof Explorer

## Theorem 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}=\left({n}\in ℕ⟼\frac{{n}!}{\sqrt{2{n}}{\left(\frac{{n}}{\mathrm{e}}\right)}^{{n}}}\right)$
stirlinglem4.2 ${⊢}{B}=\left({n}\in ℕ⟼\mathrm{log}{A}\left({n}\right)\right)$
stirlinglem4.3 ${⊢}{J}=\left({n}\in ℕ⟼\left(\frac{1+2{n}}{2}\right)\mathrm{log}\left(\frac{{n}+1}{{n}}\right)-1\right)$
Assertion stirlinglem4 ${⊢}{N}\in ℕ\to {B}\left({N}\right)-{B}\left({N}+1\right)={J}\left({N}\right)$

### Proof

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