Metamath Proof Explorer

Theorem stirlinglem7

Description: Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem7.1 ⊢ 𝐽 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
stirlinglem7.2 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
stirlinglem7.3 ⊢ 𝐻 = ( 𝑘 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
Assertion stirlinglem7 ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( 𝐽 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 stirlinglem7.1 ⊢ 𝐽 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) )
2 stirlinglem7.2 ⊢ 𝐾 = ( 𝑘 ∈ ℕ ↦ ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) )
3 stirlinglem7.3 ⊢ 𝐻 = ( 𝑘 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
4 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
5 1zzd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
6 1e0p1 ⊢ 1 = ( 0 + 1 )
7 6 a1i ⊢ ( 𝑁 ∈ ℕ → 1 = ( 0 + 1 ) )
8 7 seqeq1d ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐻 ) = seq ( 0 + 1 ) ( + , 𝐻 ) )
9 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10 0nn0 ⊢ 0 ∈ ℕ0
11 10 a1i ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℕ0 )
12 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 2 · 𝑘 ) = ( 2 · 𝑗 ) )
13 12 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑗 ) + 1 ) )
14 13 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) )
15 13 oveq2d ⊢ ( 𝑘 = 𝑗 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) )
16 14 15 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) )
17 16 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) )
18 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
19 2cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 2 ∈ ℂ )
20 2cnd ⊢ ( 𝑗 ∈ ℕ0 → 2 ∈ ℂ )
21 nn0cn ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℂ )
22 20 21 mulcld ⊢ ( 𝑗 ∈ ℕ0 → ( 2 · 𝑗 ) ∈ ℂ )
23 1cnd ⊢ ( 𝑗 ∈ ℕ0 → 1 ∈ ℂ )
24 22 23 addcld ⊢ ( 𝑗 ∈ ℕ0 → ( ( 2 · 𝑗 ) + 1 ) ∈ ℂ )
25 24 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℂ )
26 0red ⊢ ( 𝑗 ∈ ℕ0 → 0 ∈ ℝ )
27 2re ⊢ 2 ∈ ℝ
28 27 a1i ⊢ ( 𝑗 ∈ ℕ0 → 2 ∈ ℝ )
29 nn0re ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℝ )
30 28 29 remulcld ⊢ ( 𝑗 ∈ ℕ0 → ( 2 · 𝑗 ) ∈ ℝ )
31 1red ⊢ ( 𝑗 ∈ ℕ0 → 1 ∈ ℝ )
32 0le2 ⊢ 0 ≤ 2
33 32 a1i ⊢ ( 𝑗 ∈ ℕ0 → 0 ≤ 2 )
34 nn0ge0 ⊢ ( 𝑗 ∈ ℕ0 → 0 ≤ 𝑗 )
35 28 29 33 34 mulge0d ⊢ ( 𝑗 ∈ ℕ0 → 0 ≤ ( 2 · 𝑗 ) )
36 0lt1 ⊢ 0 < 1
37 36 a1i ⊢ ( 𝑗 ∈ ℕ0 → 0 < 1 )
38 30 31 35 37 addgegt0d ⊢ ( 𝑗 ∈ ℕ0 → 0 < ( ( 2 · 𝑗 ) + 1 ) )
39 26 38 ltned ⊢ ( 𝑗 ∈ ℕ0 → 0 ≠ ( ( 2 · 𝑗 ) + 1 ) )
40 39 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 0 ≠ ( ( 2 · 𝑗 ) + 1 ) )
41 40 necomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 0 )
42 25 41 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℂ )
43 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
44 43 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
45 19 44 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 2 · 𝑁 ) ∈ ℂ )
46 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 1 ∈ ℂ )
47 45 46 addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
48 27 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
49 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
50 48 49 remulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
51 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
52 32 a1i ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 2 )
53 0red ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
54 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
55 53 49 54 ltled ⊢ ( 𝑁 ∈ ℕ → 0 ≤ 𝑁 )
56 48 49 52 55 mulge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 2 · 𝑁 ) )
57 36 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
58 50 51 56 57 addgegt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 · 𝑁 ) + 1 ) )
59 58 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
60 59 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
61 47 60 reccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
62 2nn0 ⊢ 2 ∈ ℕ0
63 62 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 2 ∈ ℕ0 )
64 63 18 nn0mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 2 · 𝑗 ) ∈ ℕ0 )
65 1nn0 ⊢ 1 ∈ ℕ0
66 65 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → 1 ∈ ℕ0 )
67 64 66 nn0addcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ0 )
68 61 67 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ∈ ℂ )
69 42 68 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ∈ ℂ )
70 19 69 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) ∈ ℂ )
71 3 17 18 70 fvmptd3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑗 ) = ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) )
72 71 70 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑗 ) ∈ ℂ )
73 3 stirlinglem6 ⊢ ( 𝑁 ∈ ℕ → seq 0 ( + , 𝐻 ) ⇝ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
74 9 11 72 73 clim2ser ⊢ ( 𝑁 ∈ ℕ → seq ( 0 + 1 ) ( + , 𝐻 ) ⇝ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( seq 0 ( + , 𝐻 ) ‘ 0 ) ) )
75 8 74 eqbrtrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐻 ) ⇝ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( seq 0 ( + , 𝐻 ) ‘ 0 ) ) )
76 0z ⊢ 0 ∈ ℤ
77 seq1 ⊢ ( 0 ∈ ℤ → ( seq 0 ( + , 𝐻 ) ‘ 0 ) = ( 𝐻 ‘ 0 ) )
78 76 77 mp1i ⊢ ( 𝑁 ∈ ℕ → ( seq 0 ( + , 𝐻 ) ‘ 0 ) = ( 𝐻 ‘ 0 ) )
79 3 a1i ⊢ ( 𝑁 ∈ ℕ → 𝐻 = ( 𝑘 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) )
80 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → 𝑘 = 0 )
81 80 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → ( 2 · 𝑘 ) = ( 2 · 0 ) )
82 81 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 0 ) + 1 ) )
83 82 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 0 ) + 1 ) ) )
84 82 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) )
85 83 84 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) )
86 85 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 = 0 ) → ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) ) )
87 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
88 0cnd ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℂ )
89 87 88 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 0 ) ∈ ℂ )
90 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
91 89 90 addcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 0 ) + 1 ) ∈ ℂ )
92 87 mul01d ⊢ ( 𝑁 ∈ ℕ → ( 2 · 0 ) = 0 )
93 92 eqcomd ⊢ ( 𝑁 ∈ ℕ → 0 = ( 2 · 0 ) )
94 93 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( 0 + 1 ) = ( ( 2 · 0 ) + 1 ) )
95 7 94 eqtrd ⊢ ( 𝑁 ∈ ℕ → 1 = ( ( 2 · 0 ) + 1 ) )
96 57 95 breqtrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 · 0 ) + 1 ) )
97 96 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 0 ) + 1 ) ≠ 0 )
98 91 97 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 0 ) + 1 ) ) ∈ ℂ )
99 87 43 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℂ )
100 99 90 addcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
101 100 59 reccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
102 95 65 eqeltrrdi ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 0 ) + 1 ) ∈ ℕ0 )
103 101 102 expcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ∈ ℂ )
104 98 103 mulcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) ∈ ℂ )
105 87 104 mulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) ) ∈ ℂ )
106 79 86 11 105 fvmptd ⊢ ( 𝑁 ∈ ℕ → ( 𝐻 ‘ 0 ) = ( 2 · ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) ) )
107 92 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 0 ) + 1 ) = ( 0 + 1 ) )
108 107 6 eqtr4di ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 0 ) + 1 ) = 1 )
109 108 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 0 ) + 1 ) ) = ( 1 / 1 ) )
110 90 div1d ⊢ ( 𝑁 ∈ ℕ → ( 1 / 1 ) = 1 )
111 109 110 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( ( 2 · 0 ) + 1 ) ) = 1 )
112 108 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ 1 ) )
113 101 exp1d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ 1 ) = ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) )
114 112 113 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) )
115 111 114 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) = ( 1 · ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ) )
116 101 mulid2d ⊢ ( 𝑁 ∈ ℕ → ( 1 · ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ) = ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) )
117 115 116 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) = ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) )
118 117 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) ) = ( 2 · ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ) )
119 87 90 100 59 divassd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) = ( 2 · ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ) )
120 87 mulid1d ⊢ ( 𝑁 ∈ ℕ → ( 2 · 1 ) = 2 )
121 120 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) = ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) )
122 118 119 121 3eqtr2d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 1 / ( ( 2 · 0 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 0 ) + 1 ) ) ) ) = ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) )
123 78 106 122 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( seq 0 ( + , 𝐻 ) ‘ 0 ) = ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) )
124 123 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( seq 0 ( + , 𝐻 ) ‘ 0 ) ) = ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) )
125 75 124 breqtrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐻 ) ⇝ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) )
126 90 99 addcld ⊢ ( 𝑁 ∈ ℕ → ( 1 + ( 2 · 𝑁 ) ) ∈ ℂ )
127 126 halfcld ⊢ ( 𝑁 ∈ ℕ → ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) ∈ ℂ )
128 seqex ⊢ seq 1 ( + , 𝐾 ) ∈ V
129 128 a1i ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ∈ V )
130 elnnuz ⊢ ( 𝑗 ∈ ℕ ↔ 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
131 130 biimpi ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
132 131 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
133 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 2 · 𝑘 ) = ( 2 · 𝑛 ) )
134 133 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
135 134 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
136 134 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
137 135 136 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) )
138 137 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
139 elfzuz ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
140 elnnuz ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
141 140 biimpri ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → 𝑛 ∈ ℕ )
142 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
143 139 141 142 3syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ0 )
144 143 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ0 )
145 2cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℂ )
146 144 nn0cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℂ )
147 145 146 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℂ )
148 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℂ )
149 147 148 addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
150 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ )
151 0red ⊢ ( 𝑛 ∈ ℕ → 0 ∈ ℝ )
152 1red ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
153 27 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ )
154 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
155 153 154 remulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ )
156 155 152 readdcld ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ )
157 36 a1i ⊢ ( 𝑛 ∈ ℕ → 0 < 1 )
158 2rp ⊢ 2 ∈ ℝ+
159 158 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ+ )
160 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
161 159 160 rpmulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ+ )
162 152 161 ltaddrp2d ⊢ ( 𝑛 ∈ ℕ → 1 < ( ( 2 · 𝑛 ) + 1 ) )
163 151 152 156 157 162 lttrd ⊢ ( 𝑛 ∈ ℕ → 0 < ( ( 2 · 𝑛 ) + 1 ) )
164 163 gt0ne0d ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
165 150 164 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
166 165 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
167 149 166 reccld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
168 101 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
169 62 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℕ0 )
170 169 144 nn0mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
171 65 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℕ0 )
172 170 171 nn0addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 )
173 168 172 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
174 167 173 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℂ )
175 145 174 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ ℂ )
176 3 138 144 175 fvmptd3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
177 176 175 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐻 ‘ 𝑛 ) ∈ ℂ )
178 addcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) → ( 𝑛 + 𝑖 ) ∈ ℂ )
179 178 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 𝑛 + 𝑖 ) ∈ ℂ )
180 132 177 179 seqcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑗 ) ∈ ℂ )
181 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 1 ∈ ℂ )
182 2cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 2 ∈ ℂ )
183 43 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 𝑁 ∈ ℂ )
184 182 183 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 2 · 𝑁 ) ∈ ℂ )
185 181 184 addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 1 + ( 2 · 𝑁 ) ) ∈ ℂ )
186 185 halfcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) ∈ ℂ )
187 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 𝑛 ∈ ℂ )
188 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 𝑖 ∈ ℂ )
189 186 187 188 adddid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 𝑛 + 𝑖 ) ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · 𝑛 ) + ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · 𝑖 ) ) )
190 133 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) )
191 135 190 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
192 150 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ )
193 168 170 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
194 167 193 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) ∈ ℂ )
195 2 191 192 194 fvmptd3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
196 126 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 + ( 2 · 𝑁 ) ) ∈ ℂ )
197 2ne0 ⊢ 2 ≠ 0
198 197 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ≠ 0 )
199 196 145 175 198 div32d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) / 2 ) ) )
200 174 145 198 divcan3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) / 2 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) )
201 200 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) / 2 ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
202 196 167 173 mul12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
203 100 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
204 59 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
205 172 nn0zd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ )
206 203 204 205 exprecd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) )
207 206 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
208 203 172 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
209 203 204 205 expne0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ≠ 0 )
210 196 208 209 divrecd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
211 43 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑁 ∈ ℂ )
212 145 211 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑁 ) ∈ ℂ )
213 148 212 addcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 + ( 2 · 𝑁 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
214 203 170 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
215 214 203 mulcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
216 213 215 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) )
217 203 170 expp1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) )
218 217 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) ) )
219 2z ⊢ 2 ∈ ℤ
220 219 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℤ )
221 144 nn0zd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℤ )
222 220 221 zmulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℤ )
223 203 204 222 expne0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ≠ 0 )
224 203 203 214 204 223 divdiv1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) )
225 216 218 224 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
226 207 210 225 3eqtr2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
227 226 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) )
228 203 204 dividd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) = 1 )
229 1exp ⊢ ( ( 2 · 𝑛 ) ∈ ℤ → ( 1 ↑ ( 2 · 𝑛 ) ) = 1 )
230 222 229 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 ↑ ( 2 · 𝑛 ) ) = 1 )
231 228 230 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) = ( 1 ↑ ( 2 · 𝑛 ) ) )
232 231 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( 1 ↑ ( 2 · 𝑛 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
233 148 203 204 170 expdivd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) = ( ( 1 ↑ ( 2 · 𝑛 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
234 232 233 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) )
235 234 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
236 202 227 235 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
237 199 201 236 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
238 176 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝐻 ‘ 𝑛 ) )
239 238 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 𝐻 ‘ 𝑛 ) ) )
240 195 237 239 3eqtr2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 𝐻 ‘ 𝑛 ) ) )
241 179 189 132 177 240 seqdistr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐾 ) ‘ 𝑗 ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( seq 1 ( + , 𝐻 ) ‘ 𝑗 ) ) )
242 4 5 125 127 129 180 241 climmulc2 ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
243 90 99 addcomd ⊢ ( 𝑁 ∈ ℕ → ( 1 + ( 2 · 𝑁 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
244 243 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
245 244 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
246 244 127 eqeltrrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ∈ ℂ )
247 43 90 addcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ )
248 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
249 247 43 248 divcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) ∈ ℂ )
250 49 51 readdcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
251 49 ltp1d ⊢ ( 𝑁 ∈ ℕ → 𝑁 < ( 𝑁 + 1 ) )
252 53 49 250 54 251 lttrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
253 252 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ≠ 0 )
254 247 43 253 248 divne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) ≠ 0 )
255 249 254 logcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℂ )
256 87 100 59 divcld ⊢ ( 𝑁 ∈ ℕ → ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
257 246 255 256 subdid ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
258 99 90 addcomd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) = ( 1 + ( 2 · 𝑁 ) ) )
259 258 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) )
260 259 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
261 197 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
262 100 87 59 261 divcan6d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) = 1 )
263 260 262 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
264 245 257 263 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
265 242 264 breqtrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
266 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 2 · 𝑛 ) = ( 2 · 𝑁 ) )
267 266 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 1 + ( 2 · 𝑛 ) ) = ( 1 + ( 2 · 𝑁 ) ) )
268 267 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) = ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) )
269 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 + 1 ) = ( 𝑁 + 1 ) )
270 id ⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
271 269 270 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 + 1 ) / 𝑛 ) = ( ( 𝑁 + 1 ) / 𝑁 ) )
272 271 fveq2d ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) = ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
273 268 272 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
274 273 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
275 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
276 127 255 mulcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ∈ ℂ )
277 276 90 subcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) ∈ ℂ )
278 1 274 275 277 fvmptd3 ⊢ ( 𝑁 ∈ ℕ → ( 𝐽 ‘ 𝑁 ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
279 265 278 breqtrrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( 𝐽 ‘ 𝑁 ) )