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 mullidd ⊢ ( 𝑁 ∈ ℕ → ( 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 mulridd ⊢ ( 𝑁 ∈ ℕ → ( 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 bilani ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
132 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 2 · 𝑘 ) = ( 2 · 𝑛 ) )
133 132 oveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑛 ) + 1 ) )
134 133 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
135 133 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
136 134 135 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) )
137 136 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
138 elfzuz ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
139 elnnuz ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
140 139 biimpri ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → 𝑛 ∈ ℕ )
141 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
142 138 140 141 3syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ0 )
143 142 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ0 )
144 2cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℂ )
145 143 nn0cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℂ )
146 144 145 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℂ )
147 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℂ )
148 146 147 addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
149 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → 𝑛 ∈ ℕ )
150 0red ⊢ ( 𝑛 ∈ ℕ → 0 ∈ ℝ )
151 1red ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
152 27 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ )
153 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
154 152 153 remulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ )
155 154 151 readdcld ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ )
156 36 a1i ⊢ ( 𝑛 ∈ ℕ → 0 < 1 )
157 2rp ⊢ 2 ∈ ℝ+
158 157 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ+ )
159 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
160 158 159 rpmulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ+ )
161 151 160 ltaddrp2d ⊢ ( 𝑛 ∈ ℕ → 1 < ( ( 2 · 𝑛 ) + 1 ) )
162 150 151 155 156 161 lttrd ⊢ ( 𝑛 ∈ ℕ → 0 < ( ( 2 · 𝑛 ) + 1 ) )
163 162 gt0ne0d ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
164 149 163 syl ⊢ ( 𝑛 ∈ ( 1 ... 𝑗 ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
165 164 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
166 148 165 reccld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
167 101 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
168 62 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℕ0 )
169 168 143 nn0mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
170 65 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 1 ∈ ℕ0 )
171 169 170 nn0addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 )
172 167 171 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
173 166 172 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℂ )
174 144 173 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ ℂ )
175 3 137 143 174 fvmptd3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
176 175 174 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐻 ‘ 𝑛 ) ∈ ℂ )
177 addcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) → ( 𝑛 + 𝑖 ) ∈ ℂ )
178 177 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 𝑛 + 𝑖 ) ∈ ℂ )
179 131 176 178 seqcl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑗 ) ∈ ℂ )
180 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 1 ∈ ℂ )
181 2cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 2 ∈ ℂ )
182 43 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 𝑁 ∈ ℂ )
183 181 182 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 2 · 𝑁 ) ∈ ℂ )
184 180 183 addcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 1 + ( 2 · 𝑁 ) ) ∈ ℂ )
185 184 halfcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) ∈ ℂ )
186 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 𝑛 ∈ ℂ )
187 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → 𝑖 ∈ ℂ )
188 185 186 187 adddid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 𝑛 + 𝑖 ) ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · 𝑛 ) + ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · 𝑖 ) ) )
189 132 oveq2d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) )
190 134 189 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑘 ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
191 149 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℕ )
192 167 169 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
193 166 192 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) ∈ ℂ )
194 2 190 191 193 fvmptd3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
195 126 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 + ( 2 · 𝑁 ) ) ∈ ℂ )
196 2ne0 ⊢ 2 ≠ 0
197 196 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ≠ 0 )
198 195 144 174 197 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 ) ) )
199 173 144 197 divcan3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) / 2 ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) )
200 199 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) / 2 ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
201 195 166 172 mul12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
202 100 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
203 59 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑁 ) + 1 ) ≠ 0 )
204 171 nn0zd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℤ )
205 202 203 204 exprecd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) )
206 205 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
207 202 171 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
208 202 203 204 expne0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ≠ 0 )
209 195 207 208 divrecd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
210 43 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑁 ∈ ℂ )
211 144 210 mulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑁 ) ∈ ℂ )
212 147 211 addcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 + ( 2 · 𝑁 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
213 202 169 expcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
214 213 202 mulcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
215 212 214 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) )
216 202 169 expp1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) )
217 216 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) ) )
218 2z ⊢ 2 ∈ ℤ
219 218 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 2 ∈ ℤ )
220 143 nn0zd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → 𝑛 ∈ ℤ )
221 219 220 zmulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · 𝑛 ) ∈ ℤ )
222 202 203 221 expne0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ≠ 0 )
223 202 202 213 203 222 divdiv1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( ( ( 2 · 𝑁 ) + 1 ) · ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) )
224 215 217 223 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
225 206 209 224 3eqtr2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
226 225 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) )
227 202 203 dividd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) = 1 )
228 1exp ⊢ ( ( 2 · 𝑛 ) ∈ ℤ → ( 1 ↑ ( 2 · 𝑛 ) ) = 1 )
229 221 228 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 1 ↑ ( 2 · 𝑛 ) ) = 1 )
230 227 229 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) = ( 1 ↑ ( 2 · 𝑛 ) ) )
231 230 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( 1 ↑ ( 2 · 𝑛 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
232 147 202 203 169 expdivd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) = ( ( 1 ↑ ( 2 · 𝑛 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) )
233 231 232 eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) )
234 233 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( ( ( 2 · 𝑁 ) + 1 ) / ( ( 2 · 𝑁 ) + 1 ) ) / ( ( ( 2 · 𝑁 ) + 1 ) ↑ ( 2 · 𝑛 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
235 201 226 234 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( 1 + ( 2 · 𝑁 ) ) · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
236 198 200 235 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) = ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( 2 · 𝑛 ) ) ) )
237 175 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝐻 ‘ 𝑛 ) )
238 237 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 2 · ( ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) · ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 𝐻 ‘ 𝑛 ) ) )
239 194 236 238 3eqtr2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑗 ) ) → ( 𝐾 ‘ 𝑛 ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( 𝐻 ‘ 𝑛 ) ) )
240 178 188 131 176 239 seqdistr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐾 ) ‘ 𝑗 ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( seq 1 ( + , 𝐻 ) ‘ 𝑗 ) ) )
241 4 5 125 127 129 179 240 climmulc2 ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
242 90 99 addcomd ⊢ ( 𝑁 ∈ ℕ → ( 1 + ( 2 · 𝑁 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
243 242 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
244 243 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
245 243 127 eqeltrrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ∈ ℂ )
246 43 90 addcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ )
247 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
248 246 43 247 divcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) ∈ ℂ )
249 49 51 readdcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
250 49 ltp1d ⊢ ( 𝑁 ∈ ℕ → 𝑁 < ( 𝑁 + 1 ) )
251 53 49 249 54 250 lttrd ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
252 251 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ≠ 0 )
253 246 43 252 247 divne0d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) ≠ 0 )
254 248 253 logcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℂ )
255 87 100 59 divcld ⊢ ( 𝑁 ∈ ℕ → ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℂ )
256 245 254 255 subdid ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
257 99 90 addcomd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) = ( 1 + ( 2 · 𝑁 ) ) )
258 257 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) )
259 258 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
260 196 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
261 100 87 59 260 divcan6d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) = 1 )
262 259 261 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) · ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
263 244 256 262 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 2 / ( ( 2 · 𝑁 ) + 1 ) ) ) ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
264 241 263 breqtrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
265 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 2 · 𝑛 ) = ( 2 · 𝑁 ) )
266 265 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 1 + ( 2 · 𝑛 ) ) = ( 1 + ( 2 · 𝑁 ) ) )
267 266 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) = ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) )
268 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 + 1 ) = ( 𝑁 + 1 ) )
269 id ⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
270 268 269 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 + 1 ) / 𝑛 ) = ( ( 𝑁 + 1 ) / 𝑁 ) )
271 270 fveq2d ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) = ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
272 267 271 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) = ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
273 272 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ( ( 1 + ( 2 · 𝑛 ) ) / 2 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − 1 ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
274 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
275 127 254 mulcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ∈ ℂ )
276 275 90 subcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) ∈ ℂ )
277 1 273 274 276 fvmptd3 ⊢ ( 𝑁 ∈ ℕ → ( 𝐽 ‘ 𝑁 ) = ( ( ( ( 1 + ( 2 · 𝑁 ) ) / 2 ) · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − 1 ) )
278 264 277 breqtrrd ⊢ ( 𝑁 ∈ ℕ → seq 1 ( + , 𝐾 ) ⇝ ( 𝐽 ‘ 𝑁 ) )