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 44311
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 12806 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12534 . . . 4 (𝑁 ∈ ℕ → 1 ∈ ℤ)
3 1e0p1 12660 . . . . . . . 8 1 = (0 + 1)
43a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 1 = (0 + 1))
54seqeq1d 13912 . . . . . 6 (𝑁 ∈ ℕ → seq1( + , 𝐻) = seq(0 + 1)( + , 𝐻))
6 nn0uz 12805 . . . . . . 7 0 = (ℤ‘0)
7 0nn0 12428 . . . . . . . 8 0 ∈ ℕ0
87a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ ℕ0)
9 stirlinglem7.3 . . . . . . . . 9 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))
10 oveq2 7365 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
1110oveq1d 7372 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
1211oveq2d 7373 . . . . . . . . . . 11 (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1)))
1311oveq2d 7373 . . . . . . . . . . 11 (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))
1412, 13oveq12d 7375 . . . . . . . . . 10 (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))
1514oveq2d 7373 . . . . . . . . 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 12231 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
18 2cnd 12231 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 2 ∈ ℂ)
19 nn0cn 12423 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
2018, 19mulcld 11175 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℂ)
21 1cnd 11150 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 1 ∈ ℂ)
2220, 21addcld 11174 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℂ)
2322adantl 482 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℂ)
24 0red 11158 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 ∈ ℝ)
25 2re 12227 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2625a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 2 ∈ ℝ)
27 nn0re 12422 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0𝑗 ∈ ℝ)
2826, 27remulcld 11185 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℝ)
29 1red 11156 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 1 ∈ ℝ)
30 0le2 12255 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
3130a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 2)
32 nn0ge0 12438 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 𝑗)
3326, 27, 31, 32mulge0d 11732 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 ≤ (2 · 𝑗))
34 0lt1 11677 . . . . . . . . . . . . . . . . 17 0 < 1
3534a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 < 1)
3628, 29, 33, 35addgegt0d 11728 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 < ((2 · 𝑗) + 1))
3724, 36ltned 11291 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 0 ≠ ((2 · 𝑗) + 1))
3837adantl 482 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 0 ≠ ((2 · 𝑗) + 1))
3938necomd 2999 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 0)
4023, 39reccld 11924 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑗) + 1)) ∈ ℂ)
41 nncn 12161 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
4241adantr 481 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑁 ∈ ℂ)
4317, 42mulcld 11175 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑁) ∈ ℂ)
44 1cnd 11150 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
4543, 44addcld 11174 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ∈ ℂ)
4625a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 2 ∈ ℝ)
47 nnre 12160 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
4846, 47remulcld 11185 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
49 1red 11156 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 1 ∈ ℝ)
5030a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 2)
51 0red 11158 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 ∈ ℝ)
52 nngt0 12184 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 < 𝑁)
5351, 47, 52ltled 11303 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
5446, 47, 50, 53mulge0d 11732 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 ≤ (2 · 𝑁))
5534a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 < 1)
5648, 49, 54, 55addgegt0d 11728 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 < ((2 · 𝑁) + 1))
5756gt0ne0d 11719 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ≠ 0)
5857adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ≠ 0)
5945, 58reccld 11924 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
60 2nn0 12430 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
6160a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℕ0)
6261, 16nn0mulcld 12478 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
63 1nn0 12429 . . . . . . . . . . . . . 14 1 ∈ ℕ0
6463a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℕ0)
6562, 64nn0addcld 12477 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℕ0)
6659, 65expcld 14051 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)) ∈ ℂ)
6740, 66mulcld 11175 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) ∈ ℂ)
6817, 67mulcld 11175 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))) ∈ ℂ)
699, 15, 16, 68fvmptd3 6971 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
7069, 68eqeltrd 2838 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) ∈ ℂ)
719stirlinglem6 44310 . . . . . . 7 (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))
726, 8, 70, 71clim2ser 15539 . . . . . 6 (𝑁 ∈ ℕ → seq(0 + 1)( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
735, 72eqbrtrd 5127 . . . . 5 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
74 0z 12510 . . . . . . . 8 0 ∈ ℤ
75 seq1 13919 . . . . . . . 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 7373 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · 𝑘) = (2 · 0))
8079oveq1d 7372 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((2 · 𝑘) + 1) = ((2 · 0) + 1))
8180oveq2d 7373 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 0) + 1)))
8280oveq2d 7373 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))
8381, 82oveq12d 7375 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))))
8483oveq2d 7373 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
85 2cnd 12231 . . . . . . . . 9 (𝑁 ∈ ℕ → 2 ∈ ℂ)
86 0cnd 11148 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 0 ∈ ℂ)
8785, 86mulcld 11175 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 0) ∈ ℂ)
88 1cnd 11150 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 1 ∈ ℂ)
8987, 88addcld 11174 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℂ)
9085mul01d 11354 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 0) = 0)
9190eqcomd 2742 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 = (2 · 0))
9291oveq1d 7372 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (0 + 1) = ((2 · 0) + 1))
934, 92eqtrd 2776 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 1 = ((2 · 0) + 1))
9455, 93breqtrd 5131 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 < ((2 · 0) + 1))
9594gt0ne0d 11719 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ≠ 0)
9689, 95reccld 11924 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) ∈ ℂ)
9785, 41mulcld 11175 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
9897, 88addcld 11174 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℂ)
9998, 57reccld 11924 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
10093, 63eqeltrrdi 2847 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℕ0)
10199, 100expcld 14051 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) ∈ ℂ)
10296, 101mulcld 11175 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) ∈ ℂ)
10385, 102mulcld 11175 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) ∈ ℂ)
10477, 84, 8, 103fvmptd 6955 . . . . . . 7 (𝑁 ∈ ℕ → (𝐻‘0) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
10590oveq1d 7372 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 0) + 1) = (0 + 1))
106105, 3eqtr4di 2794 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((2 · 0) + 1) = 1)
107106oveq2d 7373 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = (1 / 1))
10888div1d 11923 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / 1) = 1)
109107, 108eqtrd 2776 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = 1)
110106oveq2d 7373 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = ((1 / ((2 · 𝑁) + 1))↑1))
11199exp1d 14046 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑1) = (1 / ((2 · 𝑁) + 1)))
112110, 111eqtrd 2776 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = (1 / ((2 · 𝑁) + 1)))
113109, 112oveq12d 7375 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 · (1 / ((2 · 𝑁) + 1))))
11499mulid2d 11173 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 · (1 / ((2 · 𝑁) + 1))) = (1 / ((2 · 𝑁) + 1)))
115113, 114eqtrd 2776 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 / ((2 · 𝑁) + 1)))
116115oveq2d 7373 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 · (1 / ((2 · 𝑁) + 1))))
11785, 88, 98, 57divassd 11966 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 · (1 / ((2 · 𝑁) + 1))))
11885mulid1d 11172 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 1) = 2)
119118oveq1d 7372 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 / ((2 · 𝑁) + 1)))
120116, 117, 1193eqtr2d 2782 . . . . . . 7 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 / ((2 · 𝑁) + 1)))
12176, 104, 1203eqtrd 2780 . . . . . 6 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (2 / ((2 · 𝑁) + 1)))
122121oveq2d 7373 . . . . 5 (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)) = ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12373, 122breqtrd 5131 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12488, 97addcld 11174 . . . . 5 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
125124halfcld 12398 . . . 4 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
126 seqex 13908 . . . . 5 seq1( + , 𝐾) ∈ V
127126a1i 11 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐾) ∈ V)
128 elnnuz 12807 . . . . . . 7 (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ‘1))
129128biimpi 215 . . . . . 6 (𝑗 ∈ ℕ → 𝑗 ∈ (ℤ‘1))
130129adantl 482 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
131 oveq2 7365 . . . . . . . . . . 11 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
132131oveq1d 7372 . . . . . . . . . 10 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
133132oveq2d 7373 . . . . . . . . 9 (𝑘 = 𝑛 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑛) + 1)))
134132oveq2d 7373 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))
135133, 134oveq12d 7375 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
136135oveq2d 7373 . . . . . . 7 (𝑘 = 𝑛 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
137 elfzuz 13437 . . . . . . . . 9 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ (ℤ‘1))
138 elnnuz 12807 . . . . . . . . . 10 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
139138biimpri 227 . . . . . . . . 9 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ ℕ)
140 nnnn0 12420 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
141137, 139, 1403syl 18 . . . . . . . 8 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ0)
142141adantl 482 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ0)
143 2cnd 12231 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℂ)
144142nn0cnd 12475 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℂ)
145143, 144mulcld 11175 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℂ)
146 1cnd 11150 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℂ)
147145, 146addcld 11174 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℂ)
148 elfznn 13470 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
149 0red 11158 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 ∈ ℝ)
150 1red 11156 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℝ)
15125a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ)
152 nnre 12160 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
153151, 152remulcld 11185 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ)
154153, 150readdcld 11184 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ)
15534a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 < 1)
156 2rp 12920 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
157156a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ+)
158 nnrp 12926 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
159157, 158rpmulcld 12973 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ+)
160150, 159ltaddrp2d 12991 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 < ((2 · 𝑛) + 1))
161149, 150, 154, 155, 160lttrd 11316 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 0 < ((2 · 𝑛) + 1))
162161gt0ne0d 11719 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ≠ 0)
163148, 162syl 17 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑗) → ((2 · 𝑛) + 1) ≠ 0)
164163adantl 482 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ≠ 0)
165147, 164reccld 11924 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑛) + 1)) ∈ ℂ)
16699ad2antrr 724 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
16760a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℕ0)
168167, 142nn0mulcld 12478 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℕ0)
16963a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℕ0)
170168, 169nn0addcld 12477 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℕ0)
171166, 170expcld 14051 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) ∈ ℂ)
172165, 171mulcld 11175 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) ∈ ℂ)
173143, 172mulcld 11175 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) ∈ ℂ)
1749, 136, 142, 173fvmptd3 6971 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
175174, 173eqeltrd 2838 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) ∈ ℂ)
176 addcl 11133 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
177176adantl 482 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
178130, 175, 177seqcl 13928 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐻)‘𝑗) ∈ ℂ)
179 1cnd 11150 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 1 ∈ ℂ)
180 2cnd 12231 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 2 ∈ ℂ)
18141ad2antrr 724 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑁 ∈ ℂ)
182180, 181mulcld 11175 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (2 · 𝑁) ∈ ℂ)
183179, 182addcld 11174 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (1 + (2 · 𝑁)) ∈ ℂ)
184183halfcld 12398 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
185 simprl 769 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑛 ∈ ℂ)
186 simprr 771 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑖 ∈ ℂ)
187184, 185, 186adddid 11179 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (((1 + (2 · 𝑁)) / 2) · (𝑛 + 𝑖)) = ((((1 + (2 · 𝑁)) / 2) · 𝑛) + (((1 + (2 · 𝑁)) / 2) · 𝑖)))
188 stirlinglem7.2 . . . . . . 7 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))
189131oveq2d 7373 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
190133, 189oveq12d 7375 . . . . . . 7 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
191148adantl 482 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ)
192166, 168expcld 14051 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) ∈ ℂ)
193165, 192mulcld 11175 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) ∈ ℂ)
194188, 190, 191, 193fvmptd3 6971 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
195124ad2antrr 724 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) ∈ ℂ)
196 2ne0 12257 . . . . . . . . 9 2 ≠ 0
197196a1i 11 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ≠ 0)
198195, 143, 173, 197div32d 11954 . . . . . . 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 11936 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
200199oveq2d 7373 . . . . . . 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 11364 . . . . . . . 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 12525 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℤ)
205202, 203, 204exprecd 14059 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) = (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))))
206205oveq2d 7373 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
207202, 170expcld 14051 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ∈ ℂ)
208202, 203, 204expne0d 14057 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ≠ 0)
209195, 207, 208divrecd 11934 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
21041ad2antrr 724 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑁 ∈ ℂ)
211143, 210mulcld 11175 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑁) ∈ ℂ)
212146, 211addcomd 11357 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
213202, 168expcld 14051 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ∈ ℂ)
214213, 202mulcomd 11176 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)) = (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))
215212, 214oveq12d 7375 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
216202, 168expp1d 14052 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) = ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)))
217216oveq2d 7373 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))))
218 2z 12535 . . . . . . . . . . . . . . 15 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℤ)
220142nn0zd 12525 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℤ)
221219, 220zmulcld 12613 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℤ)
222202, 203, 221expne0d 14057 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ≠ 0)
223202, 202, 213, 203, 222divdiv1d 11962 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
224215, 217, 2233eqtr4d 2786 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
225206, 209, 2243eqtr2d 2782 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
226225oveq2d 7373 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
227202, 203dividd 11929 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1)
228 1exp 13997 . . . . . . . . . . . . 13 ((2 · 𝑛) ∈ ℤ → (1↑(2 · 𝑛)) = 1)
229221, 228syl 17 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1↑(2 · 𝑛)) = 1)
230227, 229eqtr4d 2779 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = (1↑(2 · 𝑛)))
231230oveq1d 7372 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
232146, 202, 203, 168expdivd 14065 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
233231, 232eqtr4d 2779 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
234233oveq2d 7373 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
235201, 226, 2343eqtrd 2780 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
236198, 200, 2353eqtrd 2780 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
237174eqcomd 2742 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = (𝐻𝑛))
238237oveq2d 7373 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
239194, 236, 2383eqtr2d 2782 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
240177, 187, 130, 175, 239seqdistr 13959 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐾)‘𝑗) = (((1 + (2 · 𝑁)) / 2) · (seq1( + , 𝐻)‘𝑗)))
2411, 2, 123, 125, 127, 178, 240climmulc2 15519 . . 3 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
24288, 97addcomd 11357 . . . . . 6 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
243242oveq1d 7372 . . . . 5 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = (((2 · 𝑁) + 1) / 2))
244243oveq1d 7372 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
245243, 125eqeltrrd 2839 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) ∈ ℂ)
24641, 88addcld 11174 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
247 nnne0 12187 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
248246, 41, 247divcld 11931 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
24947, 49readdcld 11184 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
25047ltp1d 12085 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
25151, 47, 249, 52, 250lttrd 11316 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
252251gt0ne0d 11719 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
253246, 41, 252, 247divne0d 11947 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
254248, 253logcld 25926 . . . . 5 (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
25585, 98, 57divcld 11931 . . . . 5 (𝑁 ∈ ℕ → (2 / ((2 · 𝑁) + 1)) ∈ ℂ)
256245, 254, 255subdid 11611 . . . 4 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))))
25797, 88addcomd 11357 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) = (1 + (2 · 𝑁)))
258257oveq1d 7372 . . . . . 6 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) = ((1 + (2 · 𝑁)) / 2))
259258oveq1d 7372 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
260196a1i 11 . . . . . 6 (𝑁 ∈ ℕ → 2 ≠ 0)
26198, 85, 57, 260divcan6d 11950 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1))) = 1)
262259, 261oveq12d 7375 . . . 4 (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
263244, 256, 2623eqtrd 2780 . . 3 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
264241, 263breqtrd 5131 . 2 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
265 stirlinglem7.1 . . 3 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
266 oveq2 7365 . . . . . . 7 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
267266oveq2d 7373 . . . . . 6 (𝑛 = 𝑁 → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
268267oveq1d 7372 . . . . 5 (𝑛 = 𝑁 → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
269 oveq1 7364 . . . . . . 7 (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1))
270 id 22 . . . . . . 7 (𝑛 = 𝑁𝑛 = 𝑁)
271269, 270oveq12d 7375 . . . . . 6 (𝑛 = 𝑁 → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
272271fveq2d 6846 . . . . 5 (𝑛 = 𝑁 → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
273268, 272oveq12d 7375 . . . 4 (𝑛 = 𝑁 → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
274273oveq1d 7372 . . 3 (𝑛 = 𝑁 → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
275 id 22 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
276125, 254mulcld 11175 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
277276, 88subcld 11512 . . 3 (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
278265, 274, 275, 277fvmptd3 6971 . 2 (𝑁 ∈ ℕ → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
279264, 278breqtrrd 5133 1 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2943  Vcvv 3445   class class class wbr 5105  cmpt 5188  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  +crp 12915  ...cfz 13424  seqcseq 13906  cexp 13967  cli 15366  logclog 25910
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-cos 15953  df-tan 15954  df-pi 15955  df-dvds 16137  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231  df-ulm 25736  df-log 25912
This theorem is referenced by:  stirlinglem9  44313
  Copyright terms: Public domain W3C validator