Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem7 Structured version   Visualization version   GIF version

Theorem stirlinglem7 39630
Description: Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
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
Ref Expression
stirlinglem7 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽𝑁))
Distinct variable groups:   𝑘,𝑛   𝑛,𝐻   𝑛,𝐾   𝑘,𝑁,𝑛
Allowed substitution hints:   𝐻(𝑘)   𝐽(𝑘,𝑛)   𝐾(𝑘)

Proof of Theorem stirlinglem7
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11675 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11360 . . . 4 (𝑁 ∈ ℕ → 1 ∈ ℤ)
3 1e0p1 11504 . . . . . . . 8 1 = (0 + 1)
43a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 1 = (0 + 1))
54seqeq1d 12755 . . . . . 6 (𝑁 ∈ ℕ → seq1( + , 𝐻) = seq(0 + 1)( + , 𝐻))
6 nn0uz 11674 . . . . . . 7 0 = (ℤ‘0)
7 0nn0 11259 . . . . . . . 8 0 ∈ ℕ0
87a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ ℕ0)
9 stirlinglem7.3 . . . . . . . . . 10 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))
109a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))))))
11 oveq2 6618 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
1211oveq1d 6625 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
1312oveq2d 6626 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1)))
1412oveq2d 6626 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))
1513, 14oveq12d 6628 . . . . . . . . . . 11 (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))
1615oveq2d 6626 . . . . . . . . . 10 (𝑘 = 𝑗 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
1716adantl 482 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 = 𝑗) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
18 simpr 477 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
19 2cnd 11045 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
20 2cnd 11045 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 2 ∈ ℂ)
21 nn0cn 11254 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
2220, 21mulcld 10012 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℂ)
23 1cnd 10008 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 1 ∈ ℂ)
2422, 23addcld 10011 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℂ)
2524adantl 482 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℂ)
26 0red 9993 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 ∈ ℝ)
27 2re 11042 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2827a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 2 ∈ ℝ)
29 nn0re 11253 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0𝑗 ∈ ℝ)
3028, 29remulcld 10022 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℝ)
31 1red 10007 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 1 ∈ ℝ)
32 0le2 11063 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
3332a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 2)
34 nn0ge0 11270 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 𝑗)
3528, 29, 33, 34mulge0d 10556 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 ≤ (2 · 𝑗))
36 0lt1 10502 . . . . . . . . . . . . . . . . 17 0 < 1
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 < 1)
3830, 31, 35, 37addgegt0d 10553 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 < ((2 · 𝑗) + 1))
3926, 38ltned 10125 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 0 ≠ ((2 · 𝑗) + 1))
4039adantl 482 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 0 ≠ ((2 · 𝑗) + 1))
4140necomd 2845 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 0)
4225, 41reccld 10746 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑗) + 1)) ∈ ℂ)
43 nncn 10980 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
4443adantr 481 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑁 ∈ ℂ)
4519, 44mulcld 10012 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑁) ∈ ℂ)
46 1cnd 10008 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
4745, 46addcld 10011 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ∈ ℂ)
4827a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 2 ∈ ℝ)
49 nnre 10979 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
5048, 49remulcld 10022 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
51 1red 10007 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 1 ∈ ℝ)
5232a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 2)
53 0red 9993 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 ∈ ℝ)
54 nngt0 11001 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 < 𝑁)
5553, 49, 54ltled 10137 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
5648, 49, 52, 55mulge0d 10556 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 ≤ (2 · 𝑁))
5736a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 < 1)
5850, 51, 56, 57addgegt0d 10553 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 < ((2 · 𝑁) + 1))
5958gt0ne0d 10544 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ≠ 0)
6059adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ≠ 0)
6147, 60reccld 10746 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
62 2nn0 11261 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
6362a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℕ0)
6463, 18nn0mulcld 11308 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
65 1nn0 11260 . . . . . . . . . . . . . 14 1 ∈ ℕ0
6665a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℕ0)
6764, 66nn0addcld 11307 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℕ0)
6861, 67expcld 12956 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)) ∈ ℂ)
6942, 68mulcld 10012 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) ∈ ℂ)
7019, 69mulcld 10012 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))) ∈ ℂ)
7110, 17, 18, 70fvmptd 6250 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
7271, 70eqeltrd 2698 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) ∈ ℂ)
739stirlinglem6 39629 . . . . . . 7 (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))
746, 8, 72, 73clim2ser 14327 . . . . . 6 (𝑁 ∈ ℕ → seq(0 + 1)( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
755, 74eqbrtrd 4640 . . . . 5 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
76 0z 11340 . . . . . . . 8 0 ∈ ℤ
77 seq1 12762 . . . . . . . 8 (0 ∈ ℤ → (seq0( + , 𝐻)‘0) = (𝐻‘0))
7876, 77mp1i 13 . . . . . . 7 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (𝐻‘0))
799a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))))))
80 simpr 477 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → 𝑘 = 0)
8180oveq2d 6626 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · 𝑘) = (2 · 0))
8281oveq1d 6625 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((2 · 𝑘) + 1) = ((2 · 0) + 1))
8382oveq2d 6626 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 0) + 1)))
8482oveq2d 6626 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))
8583, 84oveq12d 6628 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))))
8685oveq2d 6626 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
87 2cnd 11045 . . . . . . . . 9 (𝑁 ∈ ℕ → 2 ∈ ℂ)
88 0cnd 9985 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 0 ∈ ℂ)
8987, 88mulcld 10012 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 0) ∈ ℂ)
90 1cnd 10008 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 1 ∈ ℂ)
9189, 90addcld 10011 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℂ)
9287mul01d 10187 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 0) = 0)
9392eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 = (2 · 0))
9493oveq1d 6625 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (0 + 1) = ((2 · 0) + 1))
954, 94eqtrd 2655 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 1 = ((2 · 0) + 1))
9657, 95breqtrd 4644 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 < ((2 · 0) + 1))
9796gt0ne0d 10544 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ≠ 0)
9891, 97reccld 10746 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) ∈ ℂ)
9987, 43mulcld 10012 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
10099, 90addcld 10011 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℂ)
101100, 59reccld 10746 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
10295, 65syl6eqelr 2707 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℕ0)
103101, 102expcld 12956 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) ∈ ℂ)
10498, 103mulcld 10012 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) ∈ ℂ)
10587, 104mulcld 10012 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) ∈ ℂ)
10679, 86, 8, 105fvmptd 6250 . . . . . . 7 (𝑁 ∈ ℕ → (𝐻‘0) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
10792oveq1d 6625 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 0) + 1) = (0 + 1))
108107, 3syl6eqr 2673 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((2 · 0) + 1) = 1)
109108oveq2d 6626 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = (1 / 1))
11090div1d 10745 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / 1) = 1)
111109, 110eqtrd 2655 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = 1)
112108oveq2d 6626 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = ((1 / ((2 · 𝑁) + 1))↑1))
113101exp1d 12951 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑1) = (1 / ((2 · 𝑁) + 1)))
114112, 113eqtrd 2655 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = (1 / ((2 · 𝑁) + 1)))
115111, 114oveq12d 6628 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 · (1 / ((2 · 𝑁) + 1))))
116101mulid2d 10010 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 · (1 / ((2 · 𝑁) + 1))) = (1 / ((2 · 𝑁) + 1)))
117115, 116eqtrd 2655 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 / ((2 · 𝑁) + 1)))
118117oveq2d 6626 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 · (1 / ((2 · 𝑁) + 1))))
11987, 90, 100, 59divassd 10788 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 · (1 / ((2 · 𝑁) + 1))))
12087mulid1d 10009 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 1) = 2)
121120oveq1d 6625 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 / ((2 · 𝑁) + 1)))
122118, 119, 1213eqtr2d 2661 . . . . . . 7 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 / ((2 · 𝑁) + 1)))
12378, 106, 1223eqtrd 2659 . . . . . 6 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (2 / ((2 · 𝑁) + 1)))
124123oveq2d 6626 . . . . 5 (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)) = ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12575, 124breqtrd 4644 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12690, 99addcld 10011 . . . . 5 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
127126halfcld 11229 . . . 4 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
128 seqex 12751 . . . . 5 seq1( + , 𝐾) ∈ V
129128a1i 11 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐾) ∈ V)
130 elnnuz 11676 . . . . . . 7 (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ‘1))
131130biimpi 206 . . . . . 6 (𝑗 ∈ ℕ → 𝑗 ∈ (ℤ‘1))
132131adantl 482 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
1339a1i 11 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))))))
134 oveq2 6618 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
135134oveq1d 6625 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
136135oveq2d 6626 . . . . . . . . . 10 (𝑘 = 𝑛 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑛) + 1)))
137135oveq2d 6626 . . . . . . . . . 10 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))
138136, 137oveq12d 6628 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
139138oveq2d 6626 . . . . . . . 8 (𝑘 = 𝑛 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
140139adantl 482 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) ∧ 𝑘 = 𝑛) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
141 elfzuz 12288 . . . . . . . . 9 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ (ℤ‘1))
142 elnnuz 11676 . . . . . . . . . 10 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
143142biimpri 218 . . . . . . . . 9 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ ℕ)
144 nnnn0 11251 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
145141, 143, 1443syl 18 . . . . . . . 8 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ0)
146145adantl 482 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ0)
147 2cnd 11045 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℂ)
148146nn0cnd 11305 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℂ)
149147, 148mulcld 10012 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℂ)
150 1cnd 10008 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℂ)
151149, 150addcld 10011 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℂ)
152 elfznn 12320 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
153 0red 9993 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 ∈ ℝ)
154 1red 10007 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℝ)
15527a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ)
156 nnre 10979 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
157155, 156remulcld 10022 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ)
158157, 154readdcld 10021 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ)
15936a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 < 1)
160 2rp 11789 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
161160a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ+)
162 nnrp 11794 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
163161, 162rpmulcld 11840 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ+)
164154, 163ltaddrp2d 11858 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 < ((2 · 𝑛) + 1))
165153, 154, 158, 159, 164lttrd 10150 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 0 < ((2 · 𝑛) + 1))
166165gt0ne0d 10544 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ≠ 0)
167152, 166syl 17 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑗) → ((2 · 𝑛) + 1) ≠ 0)
168167adantl 482 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ≠ 0)
169151, 168reccld 10746 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑛) + 1)) ∈ ℂ)
170101ad2antrr 761 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
17162a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℕ0)
172171, 146nn0mulcld 11308 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℕ0)
17365a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℕ0)
174172, 173nn0addcld 11307 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℕ0)
175170, 174expcld 12956 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) ∈ ℂ)
176169, 175mulcld 10012 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) ∈ ℂ)
177147, 176mulcld 10012 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) ∈ ℂ)
178133, 140, 146, 177fvmptd 6250 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
179178, 177eqeltrd 2698 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) ∈ ℂ)
180 addcl 9970 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
181180adantl 482 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
182132, 179, 181seqcl 12769 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐻)‘𝑗) ∈ ℂ)
183 1cnd 10008 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 1 ∈ ℂ)
184 2cnd 11045 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 2 ∈ ℂ)
18543ad2antrr 761 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑁 ∈ ℂ)
186184, 185mulcld 10012 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (2 · 𝑁) ∈ ℂ)
187183, 186addcld 10011 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (1 + (2 · 𝑁)) ∈ ℂ)
188187halfcld 11229 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
189 simprl 793 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑛 ∈ ℂ)
190 simprr 795 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑖 ∈ ℂ)
191188, 189, 190adddid 10016 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (((1 + (2 · 𝑁)) / 2) · (𝑛 + 𝑖)) = ((((1 + (2 · 𝑁)) / 2) · 𝑛) + (((1 + (2 · 𝑁)) / 2) · 𝑖)))
192 stirlinglem7.2 . . . . . . . 8 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))
193192a1i 11 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)))))
194134oveq2d 6626 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
195136, 194oveq12d 6628 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
196195adantl 482 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) ∧ 𝑘 = 𝑛) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
197152adantl 482 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ)
198170, 172expcld 12956 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) ∈ ℂ)
199169, 198mulcld 10012 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) ∈ ℂ)
200193, 196, 197, 199fvmptd 6250 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
201126ad2antrr 761 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) ∈ ℂ)
202 2ne0 11065 . . . . . . . . 9 2 ≠ 0
203202a1i 11 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ≠ 0)
204201, 147, 177, 203div32d 10776 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (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)))
205176, 147, 203divcan3d 10758 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
206205oveq2d 6626 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2)) = ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
207201, 169, 175mul12d 10197 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
208100ad2antrr 761 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ∈ ℂ)
20959ad2antrr 761 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ≠ 0)
210174nn0zd 11432 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℤ)
211208, 209, 210exprecd 12964 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) = (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))))
212211oveq2d 6626 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
213208, 174expcld 12956 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ∈ ℂ)
214208, 209, 210expne0d 12962 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ≠ 0)
215201, 213, 214divrecd 10756 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
21643ad2antrr 761 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑁 ∈ ℂ)
217147, 216mulcld 10012 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑁) ∈ ℂ)
218150, 217addcomd 10190 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
219208, 172expcld 12956 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ∈ ℂ)
220219, 208mulcomd 10013 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)) = (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))
221218, 220oveq12d 6628 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
222208, 172expp1d 12957 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) = ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)))
223222oveq2d 6626 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))))
224 2z 11361 . . . . . . . . . . . . . . 15 2 ∈ ℤ
225224a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℤ)
226146nn0zd 11432 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℤ)
227225, 226zmulcld 11440 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℤ)
228208, 209, 227expne0d 12962 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ≠ 0)
229208, 208, 219, 209, 228divdiv1d 10784 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
230221, 223, 2293eqtr4d 2665 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
231212, 215, 2303eqtr2d 2661 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
232231oveq2d 6626 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
233208, 209dividd 10751 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1)
234 1exp 12837 . . . . . . . . . . . . 13 ((2 · 𝑛) ∈ ℤ → (1↑(2 · 𝑛)) = 1)
235227, 234syl 17 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1↑(2 · 𝑛)) = 1)
236233, 235eqtr4d 2658 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = (1↑(2 · 𝑛)))
237236oveq1d 6625 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
238150, 208, 209, 172expdivd 12970 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
239237, 238eqtr4d 2658 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
240239oveq2d 6626 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
241207, 232, 2403eqtrd 2659 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
242204, 206, 2413eqtrd 2659 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
243178eqcomd 2627 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = (𝐻𝑛))
244243oveq2d 6626 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
245200, 242, 2443eqtr2d 2661 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
246181, 191, 132, 179, 245seqdistr 12800 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐾)‘𝑗) = (((1 + (2 · 𝑁)) / 2) · (seq1( + , 𝐻)‘𝑗)))
2471, 2, 125, 127, 129, 182, 246climmulc2 14309 . . 3 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
24890, 99addcomd 10190 . . . . . 6 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
249248oveq1d 6625 . . . . 5 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = (((2 · 𝑁) + 1) / 2))
250249oveq1d 6625 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
251249, 127eqeltrrd 2699 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) ∈ ℂ)
25243, 90addcld 10011 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
253 nnne0 11005 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
254252, 43, 253divcld 10753 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
25549, 51readdcld 10021 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
25649ltp1d 10906 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
25753, 49, 255, 54, 256lttrd 10150 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
258257gt0ne0d 10544 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
259252, 43, 258, 253divne0d 10769 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
260254, 259logcld 24238 . . . . 5 (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
26187, 100, 59divcld 10753 . . . . 5 (𝑁 ∈ ℕ → (2 / ((2 · 𝑁) + 1)) ∈ ℂ)
262251, 260, 261subdid 10438 . . . 4 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))))
26399, 90addcomd 10190 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) = (1 + (2 · 𝑁)))
264263oveq1d 6625 . . . . . 6 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) = ((1 + (2 · 𝑁)) / 2))
265264oveq1d 6625 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
266202a1i 11 . . . . . 6 (𝑁 ∈ ℕ → 2 ≠ 0)
267100, 87, 59, 266divcan6d 10772 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1))) = 1)
268265, 267oveq12d 6628 . . . 4 (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
269250, 262, 2683eqtrd 2659 . . 3 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
270247, 269breqtrd 4644 . 2 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
271 stirlinglem7.1 . . . 4 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
272271a1i 11 . . 3 (𝑁 ∈ ℕ → 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1)))
273 oveq2 6618 . . . . . . . 8 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
274273oveq2d 6626 . . . . . . 7 (𝑛 = 𝑁 → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
275274oveq1d 6625 . . . . . 6 (𝑛 = 𝑁 → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
276 oveq1 6617 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1))
277 id 22 . . . . . . . 8 (𝑛 = 𝑁𝑛 = 𝑁)
278276, 277oveq12d 6628 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
279278fveq2d 6157 . . . . . 6 (𝑛 = 𝑁 → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
280275, 279oveq12d 6628 . . . . 5 (𝑛 = 𝑁 → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
281280oveq1d 6625 . . . 4 (𝑛 = 𝑁 → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
282281adantl 482 . . 3 ((𝑁 ∈ ℕ ∧ 𝑛 = 𝑁) → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
283 id 22 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
284127, 260mulcld 10012 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
285284, 90subcld 10344 . . 3 (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
286272, 282, 283, 285fvmptd 6250 . 2 (𝑁 ∈ ℕ → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
287270, 286breqtrrd 4646 1 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wne 2790  Vcvv 3189   class class class wbr 4618  cmpt 4678  cfv 5852  (class class class)co 6610  cc 9886  cr 9887  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893   < clt 10026  cle 10027  cmin 10218   / cdiv 10636  cn 10972  2c2 11022  0cn0 11244  cz 11329  cuz 11639  +crp 11784  ...cfz 12276  seqcseq 12749  cexp 12808  cli 14157  logclog 24222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966  ax-addf 9967  ax-mulf 9968
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7861  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fsupp 8228  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-xnn0 11316  df-z 11330  df-dec 11446  df-uz 11640  df-q 11741  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-ioo 12129  df-ioc 12130  df-ico 12131  df-icc 12132  df-fz 12277  df-fzo 12415  df-fl 12541  df-mod 12617  df-seq 12750  df-exp 12809  df-fac 13009  df-bc 13038  df-hash 13066  df-shft 13749  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-limsup 14144  df-clim 14161  df-rlim 14162  df-sum 14359  df-ef 14734  df-sin 14736  df-cos 14737  df-tan 14738  df-pi 14739  df-dvds 14919  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-starv 15888  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-unif 15897  df-hom 15898  df-cco 15899  df-rest 16015  df-topn 16016  df-0g 16034  df-gsum 16035  df-topgen 16036  df-pt 16037  df-prds 16040  df-xrs 16094  df-qtop 16099  df-imas 16100  df-xps 16102  df-mre 16178  df-mrc 16179  df-acs 16181  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-submnd 17268  df-mulg 17473  df-cntz 17682  df-cmn 18127  df-psmet 19670  df-xmet 19671  df-met 19672  df-bl 19673  df-mopn 19674  df-fbas 19675  df-fg 19676  df-cnfld 19679  df-top 20631  df-topon 20648  df-topsp 20661  df-bases 20674  df-cld 20746  df-ntr 20747  df-cls 20748  df-nei 20825  df-lp 20863  df-perf 20864  df-cn 20954  df-cnp 20955  df-haus 21042  df-cmp 21113  df-tx 21288  df-hmeo 21481  df-fil 21573  df-fm 21665  df-flim 21666  df-flf 21667  df-xms 22048  df-ms 22049  df-tms 22050  df-cncf 22604  df-limc 23553  df-dv 23554  df-ulm 24052  df-log 24224
This theorem is referenced by:  stirlinglem9  39632
  Copyright terms: Public domain W3C validator