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 44633
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 12849 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12577 . . . 4 (𝑁 ∈ ℕ → 1 ∈ ℤ)
3 1e0p1 12703 . . . . . . . 8 1 = (0 + 1)
43a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 1 = (0 + 1))
54seqeq1d 13956 . . . . . 6 (𝑁 ∈ ℕ → seq1( + , 𝐻) = seq(0 + 1)( + , 𝐻))
6 nn0uz 12848 . . . . . . 7 0 = (ℤ‘0)
7 0nn0 12471 . . . . . . . 8 0 ∈ ℕ0
87a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ ℕ0)
9 stirlinglem7.3 . . . . . . . . 9 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))
10 oveq2 7402 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
1110oveq1d 7409 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
1211oveq2d 7410 . . . . . . . . . . 11 (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1)))
1311oveq2d 7410 . . . . . . . . . . 11 (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))
1412, 13oveq12d 7412 . . . . . . . . . 10 (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))
1514oveq2d 7410 . . . . . . . . 9 (𝑘 = 𝑗 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
16 simpr 485 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
17 2cnd 12274 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
18 2cnd 12274 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 2 ∈ ℂ)
19 nn0cn 12466 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
2018, 19mulcld 11218 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℂ)
21 1cnd 11193 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 1 ∈ ℂ)
2220, 21addcld 11217 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℂ)
2322adantl 482 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℂ)
24 0red 11201 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 ∈ ℝ)
25 2re 12270 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2625a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 2 ∈ ℝ)
27 nn0re 12465 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0𝑗 ∈ ℝ)
2826, 27remulcld 11228 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℝ)
29 1red 11199 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 1 ∈ ℝ)
30 0le2 12298 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
3130a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 2)
32 nn0ge0 12481 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 𝑗)
3326, 27, 31, 32mulge0d 11775 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 ≤ (2 · 𝑗))
34 0lt1 11720 . . . . . . . . . . . . . . . . 17 0 < 1
3534a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 < 1)
3628, 29, 33, 35addgegt0d 11771 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 < ((2 · 𝑗) + 1))
3724, 36ltned 11334 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 0 ≠ ((2 · 𝑗) + 1))
3837adantl 482 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 0 ≠ ((2 · 𝑗) + 1))
3938necomd 2996 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 0)
4023, 39reccld 11967 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑗) + 1)) ∈ ℂ)
41 nncn 12204 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
4241adantr 481 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑁 ∈ ℂ)
4317, 42mulcld 11218 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑁) ∈ ℂ)
44 1cnd 11193 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
4543, 44addcld 11217 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ∈ ℂ)
4625a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 2 ∈ ℝ)
47 nnre 12203 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
4846, 47remulcld 11228 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
49 1red 11199 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 1 ∈ ℝ)
5030a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 2)
51 0red 11201 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 ∈ ℝ)
52 nngt0 12227 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 < 𝑁)
5351, 47, 52ltled 11346 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
5446, 47, 50, 53mulge0d 11775 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 ≤ (2 · 𝑁))
5534a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 < 1)
5648, 49, 54, 55addgegt0d 11771 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 < ((2 · 𝑁) + 1))
5756gt0ne0d 11762 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ≠ 0)
5857adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ≠ 0)
5945, 58reccld 11967 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
60 2nn0 12473 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
6160a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℕ0)
6261, 16nn0mulcld 12521 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
63 1nn0 12472 . . . . . . . . . . . . . 14 1 ∈ ℕ0
6463a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℕ0)
6562, 64nn0addcld 12520 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℕ0)
6659, 65expcld 14095 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)) ∈ ℂ)
6740, 66mulcld 11218 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) ∈ ℂ)
6817, 67mulcld 11218 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))) ∈ ℂ)
699, 15, 16, 68fvmptd3 7008 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
7069, 68eqeltrd 2833 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) ∈ ℂ)
719stirlinglem6 44632 . . . . . . 7 (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))
726, 8, 70, 71clim2ser 15585 . . . . . 6 (𝑁 ∈ ℕ → seq(0 + 1)( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
735, 72eqbrtrd 5164 . . . . 5 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
74 0z 12553 . . . . . . . 8 0 ∈ ℤ
75 seq1 13963 . . . . . . . 8 (0 ∈ ℤ → (seq0( + , 𝐻)‘0) = (𝐻‘0))
7674, 75mp1i 13 . . . . . . 7 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (𝐻‘0))
779a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))))))
78 simpr 485 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → 𝑘 = 0)
7978oveq2d 7410 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · 𝑘) = (2 · 0))
8079oveq1d 7409 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((2 · 𝑘) + 1) = ((2 · 0) + 1))
8180oveq2d 7410 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 0) + 1)))
8280oveq2d 7410 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))
8381, 82oveq12d 7412 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))))
8483oveq2d 7410 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
85 2cnd 12274 . . . . . . . . 9 (𝑁 ∈ ℕ → 2 ∈ ℂ)
86 0cnd 11191 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 0 ∈ ℂ)
8785, 86mulcld 11218 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 0) ∈ ℂ)
88 1cnd 11193 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 1 ∈ ℂ)
8987, 88addcld 11217 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℂ)
9085mul01d 11397 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 0) = 0)
9190eqcomd 2738 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 = (2 · 0))
9291oveq1d 7409 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (0 + 1) = ((2 · 0) + 1))
934, 92eqtrd 2772 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 1 = ((2 · 0) + 1))
9455, 93breqtrd 5168 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 < ((2 · 0) + 1))
9594gt0ne0d 11762 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ≠ 0)
9689, 95reccld 11967 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) ∈ ℂ)
9785, 41mulcld 11218 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
9897, 88addcld 11217 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℂ)
9998, 57reccld 11967 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
10093, 63eqeltrrdi 2842 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℕ0)
10199, 100expcld 14095 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) ∈ ℂ)
10296, 101mulcld 11218 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) ∈ ℂ)
10385, 102mulcld 11218 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) ∈ ℂ)
10477, 84, 8, 103fvmptd 6992 . . . . . . 7 (𝑁 ∈ ℕ → (𝐻‘0) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
10590oveq1d 7409 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 0) + 1) = (0 + 1))
106105, 3eqtr4di 2790 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((2 · 0) + 1) = 1)
107106oveq2d 7410 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = (1 / 1))
10888div1d 11966 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / 1) = 1)
109107, 108eqtrd 2772 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = 1)
110106oveq2d 7410 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = ((1 / ((2 · 𝑁) + 1))↑1))
11199exp1d 14090 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑1) = (1 / ((2 · 𝑁) + 1)))
112110, 111eqtrd 2772 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = (1 / ((2 · 𝑁) + 1)))
113109, 112oveq12d 7412 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 · (1 / ((2 · 𝑁) + 1))))
11499mullidd 11216 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 · (1 / ((2 · 𝑁) + 1))) = (1 / ((2 · 𝑁) + 1)))
115113, 114eqtrd 2772 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 / ((2 · 𝑁) + 1)))
116115oveq2d 7410 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 · (1 / ((2 · 𝑁) + 1))))
11785, 88, 98, 57divassd 12009 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 · (1 / ((2 · 𝑁) + 1))))
11885mulridd 11215 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 1) = 2)
119118oveq1d 7409 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 / ((2 · 𝑁) + 1)))
120116, 117, 1193eqtr2d 2778 . . . . . . 7 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 / ((2 · 𝑁) + 1)))
12176, 104, 1203eqtrd 2776 . . . . . 6 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (2 / ((2 · 𝑁) + 1)))
122121oveq2d 7410 . . . . 5 (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)) = ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12373, 122breqtrd 5168 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12488, 97addcld 11217 . . . . 5 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
125124halfcld 12441 . . . 4 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
126 seqex 13952 . . . . 5 seq1( + , 𝐾) ∈ V
127126a1i 11 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐾) ∈ V)
128 elnnuz 12850 . . . . . . 7 (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ‘1))
129128biimpi 215 . . . . . 6 (𝑗 ∈ ℕ → 𝑗 ∈ (ℤ‘1))
130129adantl 482 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
131 oveq2 7402 . . . . . . . . . . 11 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
132131oveq1d 7409 . . . . . . . . . 10 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
133132oveq2d 7410 . . . . . . . . 9 (𝑘 = 𝑛 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑛) + 1)))
134132oveq2d 7410 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))
135133, 134oveq12d 7412 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
136135oveq2d 7410 . . . . . . 7 (𝑘 = 𝑛 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
137 elfzuz 13481 . . . . . . . . 9 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ (ℤ‘1))
138 elnnuz 12850 . . . . . . . . . 10 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
139138biimpri 227 . . . . . . . . 9 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ ℕ)
140 nnnn0 12463 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
141137, 139, 1403syl 18 . . . . . . . 8 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ0)
142141adantl 482 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ0)
143 2cnd 12274 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℂ)
144142nn0cnd 12518 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℂ)
145143, 144mulcld 11218 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℂ)
146 1cnd 11193 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℂ)
147145, 146addcld 11217 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℂ)
148 elfznn 13514 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
149 0red 11201 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 ∈ ℝ)
150 1red 11199 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℝ)
15125a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ)
152 nnre 12203 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
153151, 152remulcld 11228 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ)
154153, 150readdcld 11227 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ)
15534a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 < 1)
156 2rp 12963 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
157156a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ+)
158 nnrp 12969 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
159157, 158rpmulcld 13016 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ+)
160150, 159ltaddrp2d 13034 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 < ((2 · 𝑛) + 1))
161149, 150, 154, 155, 160lttrd 11359 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 0 < ((2 · 𝑛) + 1))
162161gt0ne0d 11762 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ≠ 0)
163148, 162syl 17 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑗) → ((2 · 𝑛) + 1) ≠ 0)
164163adantl 482 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ≠ 0)
165147, 164reccld 11967 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑛) + 1)) ∈ ℂ)
16699ad2antrr 724 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
16760a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℕ0)
168167, 142nn0mulcld 12521 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℕ0)
16963a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℕ0)
170168, 169nn0addcld 12520 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℕ0)
171166, 170expcld 14095 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) ∈ ℂ)
172165, 171mulcld 11218 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) ∈ ℂ)
173143, 172mulcld 11218 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) ∈ ℂ)
1749, 136, 142, 173fvmptd3 7008 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
175174, 173eqeltrd 2833 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) ∈ ℂ)
176 addcl 11176 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
177176adantl 482 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
178130, 175, 177seqcl 13972 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐻)‘𝑗) ∈ ℂ)
179 1cnd 11193 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 1 ∈ ℂ)
180 2cnd 12274 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 2 ∈ ℂ)
18141ad2antrr 724 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑁 ∈ ℂ)
182180, 181mulcld 11218 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (2 · 𝑁) ∈ ℂ)
183179, 182addcld 11217 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (1 + (2 · 𝑁)) ∈ ℂ)
184183halfcld 12441 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
185 simprl 769 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑛 ∈ ℂ)
186 simprr 771 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑖 ∈ ℂ)
187184, 185, 186adddid 11222 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (((1 + (2 · 𝑁)) / 2) · (𝑛 + 𝑖)) = ((((1 + (2 · 𝑁)) / 2) · 𝑛) + (((1 + (2 · 𝑁)) / 2) · 𝑖)))
188 stirlinglem7.2 . . . . . . 7 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))
189131oveq2d 7410 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
190133, 189oveq12d 7412 . . . . . . 7 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
191148adantl 482 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ)
192166, 168expcld 14095 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) ∈ ℂ)
193165, 192mulcld 11218 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) ∈ ℂ)
194188, 190, 191, 193fvmptd3 7008 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
195124ad2antrr 724 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) ∈ ℂ)
196 2ne0 12300 . . . . . . . . 9 2 ≠ 0
197196a1i 11 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ≠ 0)
198195, 143, 173, 197div32d 11997 . . . . . . 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)))
199172, 143, 197divcan3d 11979 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
200199oveq2d 7410 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2)) = ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
201195, 165, 171mul12d 11407 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
20298ad2antrr 724 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ∈ ℂ)
20357ad2antrr 724 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ≠ 0)
204170nn0zd 12568 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℤ)
205202, 203, 204exprecd 14103 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) = (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))))
206205oveq2d 7410 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
207202, 170expcld 14095 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ∈ ℂ)
208202, 203, 204expne0d 14101 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ≠ 0)
209195, 207, 208divrecd 11977 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
21041ad2antrr 724 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑁 ∈ ℂ)
211143, 210mulcld 11218 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑁) ∈ ℂ)
212146, 211addcomd 11400 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
213202, 168expcld 14095 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ∈ ℂ)
214213, 202mulcomd 11219 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)) = (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))
215212, 214oveq12d 7412 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
216202, 168expp1d 14096 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) = ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)))
217216oveq2d 7410 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))))
218 2z 12578 . . . . . . . . . . . . . . 15 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℤ)
220142nn0zd 12568 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℤ)
221219, 220zmulcld 12656 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℤ)
222202, 203, 221expne0d 14101 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ≠ 0)
223202, 202, 213, 203, 222divdiv1d 12005 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
224215, 217, 2233eqtr4d 2782 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
225206, 209, 2243eqtr2d 2778 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
226225oveq2d 7410 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
227202, 203dividd 11972 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1)
228 1exp 14041 . . . . . . . . . . . . 13 ((2 · 𝑛) ∈ ℤ → (1↑(2 · 𝑛)) = 1)
229221, 228syl 17 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1↑(2 · 𝑛)) = 1)
230227, 229eqtr4d 2775 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = (1↑(2 · 𝑛)))
231230oveq1d 7409 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
232146, 202, 203, 168expdivd 14109 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
233231, 232eqtr4d 2775 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
234233oveq2d 7410 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
235201, 226, 2343eqtrd 2776 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
236198, 200, 2353eqtrd 2776 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
237174eqcomd 2738 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = (𝐻𝑛))
238237oveq2d 7410 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
239194, 236, 2383eqtr2d 2778 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
240177, 187, 130, 175, 239seqdistr 14003 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐾)‘𝑗) = (((1 + (2 · 𝑁)) / 2) · (seq1( + , 𝐻)‘𝑗)))
2411, 2, 123, 125, 127, 178, 240climmulc2 15565 . . 3 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
24288, 97addcomd 11400 . . . . . 6 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
243242oveq1d 7409 . . . . 5 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = (((2 · 𝑁) + 1) / 2))
244243oveq1d 7409 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
245243, 125eqeltrrd 2834 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) ∈ ℂ)
24641, 88addcld 11217 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
247 nnne0 12230 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
248246, 41, 247divcld 11974 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
24947, 49readdcld 11227 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
25047ltp1d 12128 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
25151, 47, 249, 52, 250lttrd 11359 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
252251gt0ne0d 11762 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
253246, 41, 252, 247divne0d 11990 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
254248, 253logcld 26010 . . . . 5 (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
25585, 98, 57divcld 11974 . . . . 5 (𝑁 ∈ ℕ → (2 / ((2 · 𝑁) + 1)) ∈ ℂ)
256245, 254, 255subdid 11654 . . . 4 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))))
25797, 88addcomd 11400 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) = (1 + (2 · 𝑁)))
258257oveq1d 7409 . . . . . 6 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) = ((1 + (2 · 𝑁)) / 2))
259258oveq1d 7409 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
260196a1i 11 . . . . . 6 (𝑁 ∈ ℕ → 2 ≠ 0)
26198, 85, 57, 260divcan6d 11993 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1))) = 1)
262259, 261oveq12d 7412 . . . 4 (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
263244, 256, 2623eqtrd 2776 . . 3 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
264241, 263breqtrd 5168 . 2 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
265 stirlinglem7.1 . . 3 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
266 oveq2 7402 . . . . . . 7 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
267266oveq2d 7410 . . . . . 6 (𝑛 = 𝑁 → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
268267oveq1d 7409 . . . . 5 (𝑛 = 𝑁 → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
269 oveq1 7401 . . . . . . 7 (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1))
270 id 22 . . . . . . 7 (𝑛 = 𝑁𝑛 = 𝑁)
271269, 270oveq12d 7412 . . . . . 6 (𝑛 = 𝑁 → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
272271fveq2d 6883 . . . . 5 (𝑛 = 𝑁 → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
273268, 272oveq12d 7412 . . . 4 (𝑛 = 𝑁 → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
274273oveq1d 7409 . . 3 (𝑛 = 𝑁 → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
275 id 22 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
276125, 254mulcld 11218 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
277276, 88subcld 11555 . . 3 (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
278265, 274, 275, 277fvmptd3 7008 . 2 (𝑁 ∈ ℕ → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
279264, 278breqtrrd 5170 1 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2940  Vcvv 3474   class class class wbr 5142  cmpt 5225  cfv 6533  (class class class)co 7394  cc 11092  cr 11093  0cc0 11094  1c1 11095   + caddc 11097   · cmul 11099   < clt 11232  cle 11233  cmin 11428   / cdiv 11855  cn 12196  2c2 12251  0cn0 12456  cz 12542  cuz 12806  +crp 12958  ...cfz 13468  seqcseq 13950  cexp 14011  cli 15412  logclog 25994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709  ax-inf2 9620  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171  ax-pre-sup 11172  ax-addf 11173  ax-mulf 11174
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-se 5626  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-of 7654  df-om 7840  df-1st 7959  df-2nd 7960  df-supp 8131  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-rdg 8394  df-1o 8450  df-2o 8451  df-oadd 8454  df-er 8688  df-map 8807  df-pm 8808  df-ixp 8877  df-en 8925  df-dom 8926  df-sdom 8927  df-fin 8928  df-fsupp 9347  df-fi 9390  df-sup 9421  df-inf 9422  df-oi 9489  df-card 9918  df-pnf 11234  df-mnf 11235  df-xr 11236  df-ltxr 11237  df-le 11238  df-sub 11430  df-neg 11431  df-div 11856  df-nn 12197  df-2 12259  df-3 12260  df-4 12261  df-5 12262  df-6 12263  df-7 12264  df-8 12265  df-9 12266  df-n0 12457  df-xnn0 12529  df-z 12543  df-dec 12662  df-uz 12807  df-q 12917  df-rp 12959  df-xneg 13076  df-xadd 13077  df-xmul 13078  df-ioo 13312  df-ioc 13313  df-ico 13314  df-icc 13315  df-fz 13469  df-fzo 13612  df-fl 13741  df-mod 13819  df-seq 13951  df-exp 14012  df-fac 14218  df-bc 14247  df-hash 14275  df-shft 14998  df-cj 15030  df-re 15031  df-im 15032  df-sqrt 15166  df-abs 15167  df-limsup 15399  df-clim 15416  df-rlim 15417  df-sum 15617  df-ef 15995  df-sin 15997  df-cos 15998  df-tan 15999  df-pi 16000  df-dvds 16182  df-struct 17064  df-sets 17081  df-slot 17099  df-ndx 17111  df-base 17129  df-ress 17158  df-plusg 17194  df-mulr 17195  df-starv 17196  df-sca 17197  df-vsca 17198  df-ip 17199  df-tset 17200  df-ple 17201  df-ds 17203  df-unif 17204  df-hom 17205  df-cco 17206  df-rest 17352  df-topn 17353  df-0g 17371  df-gsum 17372  df-topgen 17373  df-pt 17374  df-prds 17377  df-xrs 17432  df-qtop 17437  df-imas 17438  df-xps 17440  df-mre 17514  df-mrc 17515  df-acs 17517  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-submnd 18650  df-mulg 18925  df-cntz 19149  df-cmn 19616  df-psmet 20872  df-xmet 20873  df-met 20874  df-bl 20875  df-mopn 20876  df-fbas 20877  df-fg 20878  df-cnfld 20881  df-top 22327  df-topon 22344  df-topsp 22366  df-bases 22380  df-cld 22454  df-ntr 22455  df-cls 22456  df-nei 22533  df-lp 22571  df-perf 22572  df-cn 22662  df-cnp 22663  df-haus 22750  df-cmp 22822  df-tx 22997  df-hmeo 23190  df-fil 23281  df-fm 23373  df-flim 23374  df-flf 23375  df-xms 23757  df-ms 23758  df-tms 23759  df-cncf 24325  df-limc 25314  df-dv 25315  df-ulm 25820  df-log 25996
This theorem is referenced by:  stirlinglem9  44635
  Copyright terms: Public domain W3C validator