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 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem4.2 ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 𝐴 ‘ 𝑛 ) ) )
stirlinglem4.3 ⊢ 𝐽 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
Assertion stirlinglem4 ( 𝑁 ∈ ℕ → ( ( 𝐵 ‘ 𝑁 ) − ( 𝐵 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐽 ‘ 𝑁 ) )

Proof

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