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 40814
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 11925 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11610 . . . 4 (𝑁 ∈ ℕ → 1 ∈ ℤ)
3 1e0p1 11754 . . . . . . . 8 1 = (0 + 1)
43a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 1 = (0 + 1))
54seqeq1d 13014 . . . . . 6 (𝑁 ∈ ℕ → seq1( + , 𝐻) = seq(0 + 1)( + , 𝐻))
6 nn0uz 11924 . . . . . . 7 0 = (ℤ‘0)
7 0nn0 11509 . . . . . . . 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 6801 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
1211oveq1d 6808 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
1312oveq2d 6809 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1)))
1412oveq2d 6809 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))
1513, 14oveq12d 6811 . . . . . . . . . . 11 (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))
1615oveq2d 6809 . . . . . . . . . 10 (𝑘 = 𝑗 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
1716adantl 467 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 = 𝑗) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
18 simpr 471 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
19 2cnd 11295 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
20 2cnd 11295 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 2 ∈ ℂ)
21 nn0cn 11504 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
2220, 21mulcld 10262 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℂ)
23 1cnd 10258 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 1 ∈ ℂ)
2422, 23addcld 10261 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℂ)
2524adantl 467 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℂ)
26 0red 10243 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 ∈ ℝ)
27 2re 11292 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2827a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 2 ∈ ℝ)
29 nn0re 11503 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0𝑗 ∈ ℝ)
3028, 29remulcld 10272 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℝ)
31 1red 10257 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 1 ∈ ℝ)
32 0le2 11313 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
3332a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 2)
34 nn0ge0 11520 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 𝑗)
3528, 29, 33, 34mulge0d 10806 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 ≤ (2 · 𝑗))
36 0lt1 10752 . . . . . . . . . . . . . . . . 17 0 < 1
3736a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 < 1)
3830, 31, 35, 37addgegt0d 10803 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 < ((2 · 𝑗) + 1))
3926, 38ltned 10375 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 0 ≠ ((2 · 𝑗) + 1))
4039adantl 467 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 0 ≠ ((2 · 𝑗) + 1))
4140necomd 2998 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 0)
4225, 41reccld 10996 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑗) + 1)) ∈ ℂ)
43 nncn 11230 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
4443adantr 466 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑁 ∈ ℂ)
4519, 44mulcld 10262 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑁) ∈ ℂ)
46 1cnd 10258 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
4745, 46addcld 10261 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ∈ ℂ)
4827a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 2 ∈ ℝ)
49 nnre 11229 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
5048, 49remulcld 10272 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
51 1red 10257 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 1 ∈ ℝ)
5232a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 2)
53 0red 10243 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 ∈ ℝ)
54 nngt0 11251 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 < 𝑁)
5553, 49, 54ltled 10387 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
5648, 49, 52, 55mulge0d 10806 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 ≤ (2 · 𝑁))
5736a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 < 1)
5850, 51, 56, 57addgegt0d 10803 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 < ((2 · 𝑁) + 1))
5958gt0ne0d 10794 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ≠ 0)
6059adantr 466 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ≠ 0)
6147, 60reccld 10996 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
62 2nn0 11511 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
6362a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℕ0)
6463, 18nn0mulcld 11558 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
65 1nn0 11510 . . . . . . . . . . . . . 14 1 ∈ ℕ0
6665a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℕ0)
6764, 66nn0addcld 11557 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℕ0)
6861, 67expcld 13215 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)) ∈ ℂ)
6942, 68mulcld 10262 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) ∈ ℂ)
7019, 69mulcld 10262 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))) ∈ ℂ)
7110, 17, 18, 70fvmptd 6430 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
7271, 70eqeltrd 2850 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) ∈ ℂ)
739stirlinglem6 40813 . . . . . . 7 (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))
746, 8, 72, 73clim2ser 14593 . . . . . 6 (𝑁 ∈ ℕ → seq(0 + 1)( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
755, 74eqbrtrd 4808 . . . . 5 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
76 0z 11590 . . . . . . . 8 0 ∈ ℤ
77 seq1 13021 . . . . . . . 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 471 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → 𝑘 = 0)
8180oveq2d 6809 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · 𝑘) = (2 · 0))
8281oveq1d 6808 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((2 · 𝑘) + 1) = ((2 · 0) + 1))
8382oveq2d 6809 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 0) + 1)))
8482oveq2d 6809 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))
8583, 84oveq12d 6811 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))))
8685oveq2d 6809 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
87 2cnd 11295 . . . . . . . . 9 (𝑁 ∈ ℕ → 2 ∈ ℂ)
88 0cnd 10235 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 0 ∈ ℂ)
8987, 88mulcld 10262 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 0) ∈ ℂ)
90 1cnd 10258 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 1 ∈ ℂ)
9189, 90addcld 10261 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℂ)
9287mul01d 10437 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 0) = 0)
9392eqcomd 2777 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 = (2 · 0))
9493oveq1d 6808 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (0 + 1) = ((2 · 0) + 1))
954, 94eqtrd 2805 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 1 = ((2 · 0) + 1))
9657, 95breqtrd 4812 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 < ((2 · 0) + 1))
9796gt0ne0d 10794 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ≠ 0)
9891, 97reccld 10996 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) ∈ ℂ)
9987, 43mulcld 10262 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
10099, 90addcld 10261 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℂ)
101100, 59reccld 10996 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
10295, 65syl6eqelr 2859 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℕ0)
103101, 102expcld 13215 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) ∈ ℂ)
10498, 103mulcld 10262 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) ∈ ℂ)
10587, 104mulcld 10262 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) ∈ ℂ)
10679, 86, 8, 105fvmptd 6430 . . . . . . 7 (𝑁 ∈ ℕ → (𝐻‘0) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
10792oveq1d 6808 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 0) + 1) = (0 + 1))
108107, 3syl6eqr 2823 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((2 · 0) + 1) = 1)
109108oveq2d 6809 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = (1 / 1))
11090div1d 10995 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / 1) = 1)
111109, 110eqtrd 2805 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = 1)
112108oveq2d 6809 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = ((1 / ((2 · 𝑁) + 1))↑1))
113101exp1d 13210 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑1) = (1 / ((2 · 𝑁) + 1)))
114112, 113eqtrd 2805 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = (1 / ((2 · 𝑁) + 1)))
115111, 114oveq12d 6811 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 · (1 / ((2 · 𝑁) + 1))))
116101mulid2d 10260 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 · (1 / ((2 · 𝑁) + 1))) = (1 / ((2 · 𝑁) + 1)))
117115, 116eqtrd 2805 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 / ((2 · 𝑁) + 1)))
118117oveq2d 6809 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 · (1 / ((2 · 𝑁) + 1))))
11987, 90, 100, 59divassd 11038 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 · (1 / ((2 · 𝑁) + 1))))
12087mulid1d 10259 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 1) = 2)
121120oveq1d 6808 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 / ((2 · 𝑁) + 1)))
122118, 119, 1213eqtr2d 2811 . . . . . . 7 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 / ((2 · 𝑁) + 1)))
12378, 106, 1223eqtrd 2809 . . . . . 6 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (2 / ((2 · 𝑁) + 1)))
124123oveq2d 6809 . . . . 5 (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)) = ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12575, 124breqtrd 4812 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12690, 99addcld 10261 . . . . 5 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
127126halfcld 11479 . . . 4 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
128 seqex 13010 . . . . 5 seq1( + , 𝐾) ∈ V
129128a1i 11 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐾) ∈ V)
130 elnnuz 11926 . . . . . . 7 (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ‘1))
131130biimpi 206 . . . . . 6 (𝑗 ∈ ℕ → 𝑗 ∈ (ℤ‘1))
132131adantl 467 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
1339a1i 11 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))))))
134 oveq2 6801 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
135134oveq1d 6808 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
136135oveq2d 6809 . . . . . . . . . 10 (𝑘 = 𝑛 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑛) + 1)))
137135oveq2d 6809 . . . . . . . . . 10 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))
138136, 137oveq12d 6811 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
139138oveq2d 6809 . . . . . . . 8 (𝑘 = 𝑛 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
140139adantl 467 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) ∧ 𝑘 = 𝑛) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
141 elfzuz 12545 . . . . . . . . 9 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ (ℤ‘1))
142 elnnuz 11926 . . . . . . . . . 10 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
143142biimpri 218 . . . . . . . . 9 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ ℕ)
144 nnnn0 11501 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
145141, 143, 1443syl 18 . . . . . . . 8 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ0)
146145adantl 467 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ0)
147 2cnd 11295 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℂ)
148146nn0cnd 11555 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℂ)
149147, 148mulcld 10262 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℂ)
150 1cnd 10258 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℂ)
151149, 150addcld 10261 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℂ)
152 elfznn 12577 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
153 0red 10243 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 ∈ ℝ)
154 1red 10257 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℝ)
15527a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ)
156 nnre 11229 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
157155, 156remulcld 10272 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ)
158157, 154readdcld 10271 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ)
15936a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 < 1)
160 2rp 12040 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
161160a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ+)
162 nnrp 12045 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
163161, 162rpmulcld 12091 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ+)
164154, 163ltaddrp2d 12109 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 < ((2 · 𝑛) + 1))
165153, 154, 158, 159, 164lttrd 10400 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 0 < ((2 · 𝑛) + 1))
166165gt0ne0d 10794 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ≠ 0)
167152, 166syl 17 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑗) → ((2 · 𝑛) + 1) ≠ 0)
168167adantl 467 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ≠ 0)
169151, 168reccld 10996 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑛) + 1)) ∈ ℂ)
170101ad2antrr 705 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
17162a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℕ0)
172171, 146nn0mulcld 11558 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℕ0)
17365a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℕ0)
174172, 173nn0addcld 11557 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℕ0)
175170, 174expcld 13215 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) ∈ ℂ)
176169, 175mulcld 10262 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) ∈ ℂ)
177147, 176mulcld 10262 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) ∈ ℂ)
178133, 140, 146, 177fvmptd 6430 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
179178, 177eqeltrd 2850 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) ∈ ℂ)
180 addcl 10220 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
181180adantl 467 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
182132, 179, 181seqcl 13028 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐻)‘𝑗) ∈ ℂ)
183 1cnd 10258 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 1 ∈ ℂ)
184 2cnd 11295 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 2 ∈ ℂ)
18543ad2antrr 705 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑁 ∈ ℂ)
186184, 185mulcld 10262 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (2 · 𝑁) ∈ ℂ)
187183, 186addcld 10261 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (1 + (2 · 𝑁)) ∈ ℂ)
188187halfcld 11479 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
189 simprl 754 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑛 ∈ ℂ)
190 simprr 756 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑖 ∈ ℂ)
191188, 189, 190adddid 10266 . . . . 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 6809 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
195136, 194oveq12d 6811 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
196195adantl 467 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) ∧ 𝑘 = 𝑛) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
197152adantl 467 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ)
198170, 172expcld 13215 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) ∈ ℂ)
199169, 198mulcld 10262 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) ∈ ℂ)
200193, 196, 197, 199fvmptd 6430 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
201126ad2antrr 705 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) ∈ ℂ)
202 2ne0 11315 . . . . . . . . 9 2 ≠ 0
203202a1i 11 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ≠ 0)
204201, 147, 177, 203div32d 11026 . . . . . . 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 11008 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
206205oveq2d 6809 . . . . . . 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 10447 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
208100ad2antrr 705 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ∈ ℂ)
20959ad2antrr 705 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ≠ 0)
210174nn0zd 11682 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℤ)
211208, 209, 210exprecd 13223 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) = (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))))
212211oveq2d 6809 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
213208, 174expcld 13215 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ∈ ℂ)
214208, 209, 210expne0d 13221 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ≠ 0)
215201, 213, 214divrecd 11006 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
21643ad2antrr 705 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑁 ∈ ℂ)
217147, 216mulcld 10262 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑁) ∈ ℂ)
218150, 217addcomd 10440 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
219208, 172expcld 13215 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ∈ ℂ)
220219, 208mulcomd 10263 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)) = (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))
221218, 220oveq12d 6811 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
222208, 172expp1d 13216 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) = ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)))
223222oveq2d 6809 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))))
224 2z 11611 . . . . . . . . . . . . . . 15 2 ∈ ℤ
225224a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℤ)
226146nn0zd 11682 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℤ)
227225, 226zmulcld 11690 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℤ)
228208, 209, 227expne0d 13221 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ≠ 0)
229208, 208, 219, 209, 228divdiv1d 11034 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
230221, 223, 2293eqtr4d 2815 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
231212, 215, 2303eqtr2d 2811 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
232231oveq2d 6809 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
233208, 209dividd 11001 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1)
234 1exp 13096 . . . . . . . . . . . . 13 ((2 · 𝑛) ∈ ℤ → (1↑(2 · 𝑛)) = 1)
235227, 234syl 17 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1↑(2 · 𝑛)) = 1)
236233, 235eqtr4d 2808 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = (1↑(2 · 𝑛)))
237236oveq1d 6808 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
238150, 208, 209, 172expdivd 13229 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
239237, 238eqtr4d 2808 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
240239oveq2d 6809 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
241207, 232, 2403eqtrd 2809 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
242204, 206, 2413eqtrd 2809 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
243178eqcomd 2777 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = (𝐻𝑛))
244243oveq2d 6809 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
245200, 242, 2443eqtr2d 2811 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
246181, 191, 132, 179, 245seqdistr 13059 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐾)‘𝑗) = (((1 + (2 · 𝑁)) / 2) · (seq1( + , 𝐻)‘𝑗)))
2471, 2, 125, 127, 129, 182, 246climmulc2 14575 . . 3 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
24890, 99addcomd 10440 . . . . . 6 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
249248oveq1d 6808 . . . . 5 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = (((2 · 𝑁) + 1) / 2))
250249oveq1d 6808 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
251249, 127eqeltrrd 2851 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) ∈ ℂ)
25243, 90addcld 10261 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
253 nnne0 11255 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
254252, 43, 253divcld 11003 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
25549, 51readdcld 10271 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
25649ltp1d 11156 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
25753, 49, 255, 54, 256lttrd 10400 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
258257gt0ne0d 10794 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
259252, 43, 258, 253divne0d 11019 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
260254, 259logcld 24538 . . . . 5 (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
26187, 100, 59divcld 11003 . . . . 5 (𝑁 ∈ ℕ → (2 / ((2 · 𝑁) + 1)) ∈ ℂ)
262251, 260, 261subdid 10688 . . . 4 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))))
26399, 90addcomd 10440 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) = (1 + (2 · 𝑁)))
264263oveq1d 6808 . . . . . 6 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) = ((1 + (2 · 𝑁)) / 2))
265264oveq1d 6808 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
266202a1i 11 . . . . . 6 (𝑁 ∈ ℕ → 2 ≠ 0)
267100, 87, 59, 266divcan6d 11022 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1))) = 1)
268265, 267oveq12d 6811 . . . 4 (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
269250, 262, 2683eqtrd 2809 . . 3 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
270247, 269breqtrd 4812 . 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 6801 . . . . . . . 8 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
274273oveq2d 6809 . . . . . . 7 (𝑛 = 𝑁 → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
275274oveq1d 6808 . . . . . 6 (𝑛 = 𝑁 → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
276 oveq1 6800 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1))
277 id 22 . . . . . . . 8 (𝑛 = 𝑁𝑛 = 𝑁)
278276, 277oveq12d 6811 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
279278fveq2d 6336 . . . . . 6 (𝑛 = 𝑁 → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
280275, 279oveq12d 6811 . . . . 5 (𝑛 = 𝑁 → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
281280oveq1d 6808 . . . 4 (𝑛 = 𝑁 → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
282281adantl 467 . . 3 ((𝑁 ∈ ℕ ∧ 𝑛 = 𝑁) → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
283 id 22 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
284127, 260mulcld 10262 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
285284, 90subcld 10594 . . 3 (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
286272, 282, 283, 285fvmptd 6430 . 2 (𝑁 ∈ ℕ → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
287270, 286breqtrrd 4814 1 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  wne 2943  Vcvv 3351   class class class wbr 4786  cmpt 4863  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  cn 11222  2c2 11272  0cn0 11494  cz 11579  cuz 11888  +crp 12035  ...cfz 12533  seqcseq 13008  cexp 13067  cli 14423  logclog 24522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-xnn0 11566  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14015  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428  df-sum 14625  df-ef 15004  df-sin 15006  df-cos 15007  df-tan 15008  df-pi 15009  df-dvds 15190  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17957  df-cmn 18402  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-cmp 21411  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-xms 22345  df-ms 22346  df-tms 22347  df-cncf 22901  df-limc 23850  df-dv 23851  df-ulm 24351  df-log 24524
This theorem is referenced by:  stirlinglem9  40816
  Copyright terms: Public domain W3C validator