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 46001
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 12946 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12674 . . . 4 (𝑁 ∈ ℕ → 1 ∈ ℤ)
3 1e0p1 12800 . . . . . . . 8 1 = (0 + 1)
43a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 1 = (0 + 1))
54seqeq1d 14058 . . . . . 6 (𝑁 ∈ ℕ → seq1( + , 𝐻) = seq(0 + 1)( + , 𝐻))
6 nn0uz 12945 . . . . . . 7 0 = (ℤ‘0)
7 0nn0 12568 . . . . . . . 8 0 ∈ ℕ0
87a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ ℕ0)
9 stirlinglem7.3 . . . . . . . . 9 𝐻 = (𝑘 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))
10 oveq2 7456 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
1110oveq1d 7463 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
1211oveq2d 7464 . . . . . . . . . . 11 (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1)))
1311oveq2d 7464 . . . . . . . . . . 11 (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))
1412, 13oveq12d 7466 . . . . . . . . . 10 (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))
1514oveq2d 7464 . . . . . . . . 9 (𝑘 = 𝑗 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
16 simpr 484 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
17 2cnd 12371 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
18 2cnd 12371 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 2 ∈ ℂ)
19 nn0cn 12563 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
2018, 19mulcld 11310 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℂ)
21 1cnd 11285 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 1 ∈ ℂ)
2220, 21addcld 11309 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℂ)
2322adantl 481 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℂ)
24 0red 11293 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 ∈ ℝ)
25 2re 12367 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2625a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 2 ∈ ℝ)
27 nn0re 12562 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0𝑗 ∈ ℝ)
2826, 27remulcld 11320 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℝ)
29 1red 11291 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 1 ∈ ℝ)
30 0le2 12395 . . . . . . . . . . . . . . . . . 18 0 ≤ 2
3130a1i 11 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 2)
32 nn0ge0 12578 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ0 → 0 ≤ 𝑗)
3326, 27, 31, 32mulge0d 11867 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 ≤ (2 · 𝑗))
34 0lt1 11812 . . . . . . . . . . . . . . . . 17 0 < 1
3534a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0 → 0 < 1)
3628, 29, 33, 35addgegt0d 11863 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ0 → 0 < ((2 · 𝑗) + 1))
3724, 36ltned 11426 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0 → 0 ≠ ((2 · 𝑗) + 1))
3837adantl 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 0 ≠ ((2 · 𝑗) + 1))
3938necomd 3002 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 0)
4023, 39reccld 12063 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑗) + 1)) ∈ ℂ)
41 nncn 12301 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
4241adantr 480 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 𝑁 ∈ ℂ)
4317, 42mulcld 11310 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑁) ∈ ℂ)
44 1cnd 11285 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
4543, 44addcld 11309 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ∈ ℂ)
4625a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 2 ∈ ℝ)
47 nnre 12300 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
4846, 47remulcld 11320 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
49 1red 11291 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 1 ∈ ℝ)
5030a1i 11 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 2)
51 0red 11293 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 ∈ ℝ)
52 nngt0 12324 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 0 < 𝑁)
5351, 47, 52ltled 11438 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
5446, 47, 50, 53mulge0d 11867 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 ≤ (2 · 𝑁))
5534a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 0 < 1)
5648, 49, 54, 55addgegt0d 11863 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 < ((2 · 𝑁) + 1))
5756gt0ne0d 11854 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ≠ 0)
5857adantr 480 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑁) + 1) ≠ 0)
5945, 58reccld 12063 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
60 2nn0 12570 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
6160a1i 11 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 2 ∈ ℕ0)
6261, 16nn0mulcld 12618 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
63 1nn0 12569 . . . . . . . . . . . . . 14 1 ∈ ℕ0
6463a1i 11 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → 1 ∈ ℕ0)
6562, 64nn0addcld 12617 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℕ0)
6659, 65expcld 14196 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)) ∈ ℂ)
6740, 66mulcld 11310 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) ∈ ℂ)
6817, 67mulcld 11310 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))) ∈ ℂ)
699, 15, 16, 68fvmptd3 7052 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
7069, 68eqeltrd 2844 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0) → (𝐻𝑗) ∈ ℂ)
719stirlinglem6 46000 . . . . . . 7 (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))
726, 8, 70, 71clim2ser 15703 . . . . . 6 (𝑁 ∈ ℕ → seq(0 + 1)( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
735, 72eqbrtrd 5188 . . . . 5 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)))
74 0z 12650 . . . . . . . 8 0 ∈ ℤ
75 seq1 14065 . . . . . . . 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 484 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → 𝑘 = 0)
7978oveq2d 7464 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · 𝑘) = (2 · 0))
8079oveq1d 7463 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((2 · 𝑘) + 1) = ((2 · 0) + 1))
8180oveq2d 7464 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 0) + 1)))
8280oveq2d 7464 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))
8381, 82oveq12d 7466 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))))
8483oveq2d 7464 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
85 2cnd 12371 . . . . . . . . 9 (𝑁 ∈ ℕ → 2 ∈ ℂ)
86 0cnd 11283 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 0 ∈ ℂ)
8785, 86mulcld 11310 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 0) ∈ ℂ)
88 1cnd 11285 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 1 ∈ ℂ)
8987, 88addcld 11309 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℂ)
9085mul01d 11489 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → (2 · 0) = 0)
9190eqcomd 2746 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 = (2 · 0))
9291oveq1d 7463 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (0 + 1) = ((2 · 0) + 1))
934, 92eqtrd 2780 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 1 = ((2 · 0) + 1))
9455, 93breqtrd 5192 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 0 < ((2 · 0) + 1))
9594gt0ne0d 11854 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ≠ 0)
9689, 95reccld 12063 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) ∈ ℂ)
9785, 41mulcld 11310 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
9897, 88addcld 11309 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℂ)
9998, 57reccld 12063 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
10093, 63eqeltrrdi 2853 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 0) + 1) ∈ ℕ0)
10199, 100expcld 14196 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) ∈ ℂ)
10296, 101mulcld 11310 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) ∈ ℂ)
10385, 102mulcld 11310 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) ∈ ℂ)
10477, 84, 8, 103fvmptd 7036 . . . . . . 7 (𝑁 ∈ ℕ → (𝐻‘0) = (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))))
10590oveq1d 7463 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → ((2 · 0) + 1) = (0 + 1))
106105, 3eqtr4di 2798 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((2 · 0) + 1) = 1)
107106oveq2d 7464 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = (1 / 1))
10888div1d 12062 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (1 / 1) = 1)
109107, 108eqtrd 2780 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (1 / ((2 · 0) + 1)) = 1)
110106oveq2d 7464 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = ((1 / ((2 · 𝑁) + 1))↑1))
11199exp1d 14191 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑1) = (1 / ((2 · 𝑁) + 1)))
112110, 111eqtrd 2780 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)) = (1 / ((2 · 𝑁) + 1)))
113109, 112oveq12d 7466 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 · (1 / ((2 · 𝑁) + 1))))
11499mullidd 11308 . . . . . . . . . 10 (𝑁 ∈ ℕ → (1 · (1 / ((2 · 𝑁) + 1))) = (1 / ((2 · 𝑁) + 1)))
115113, 114eqtrd 2780 . . . . . . . . 9 (𝑁 ∈ ℕ → ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 / ((2 · 𝑁) + 1)))
116115oveq2d 7464 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 · (1 / ((2 · 𝑁) + 1))))
11785, 88, 98, 57divassd 12105 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 · (1 / ((2 · 𝑁) + 1))))
11885mulridd 11307 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 1) = 2)
119118oveq1d 7463 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 1) / ((2 · 𝑁) + 1)) = (2 / ((2 · 𝑁) + 1)))
120116, 117, 1193eqtr2d 2786 . . . . . . 7 (𝑁 ∈ ℕ → (2 · ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1)))) = (2 / ((2 · 𝑁) + 1)))
12176, 104, 1203eqtrd 2784 . . . . . 6 (𝑁 ∈ ℕ → (seq0( + , 𝐻)‘0) = (2 / ((2 · 𝑁) + 1)))
122121oveq2d 7464 . . . . 5 (𝑁 ∈ ℕ → ((log‘((𝑁 + 1) / 𝑁)) − (seq0( + , 𝐻)‘0)) = ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12373, 122breqtrd 5192 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐻) ⇝ ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1))))
12488, 97addcld 11309 . . . . 5 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) ∈ ℂ)
125124halfcld 12538 . . . 4 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
126 seqex 14054 . . . . 5 seq1( + , 𝐾) ∈ V
127126a1i 11 . . . 4 (𝑁 ∈ ℕ → seq1( + , 𝐾) ∈ V)
128 elnnuz 12947 . . . . . . 7 (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ‘1))
129128biimpi 216 . . . . . 6 (𝑗 ∈ ℕ → 𝑗 ∈ (ℤ‘1))
130129adantl 481 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ‘1))
131 oveq2 7456 . . . . . . . . . . 11 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
132131oveq1d 7463 . . . . . . . . . 10 (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1))
133132oveq2d 7464 . . . . . . . . 9 (𝑘 = 𝑛 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑛) + 1)))
134132oveq2d 7464 . . . . . . . . 9 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))
135133, 134oveq12d 7466 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
136135oveq2d 7464 . . . . . . 7 (𝑘 = 𝑛 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
137 elfzuz 13580 . . . . . . . . 9 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ (ℤ‘1))
138 elnnuz 12947 . . . . . . . . . 10 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
139138biimpri 228 . . . . . . . . 9 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ ℕ)
140 nnnn0 12560 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
141137, 139, 1403syl 18 . . . . . . . 8 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ0)
142141adantl 481 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ0)
143 2cnd 12371 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℂ)
144142nn0cnd 12615 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℂ)
145143, 144mulcld 11310 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℂ)
146 1cnd 11285 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℂ)
147145, 146addcld 11309 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℂ)
148 elfznn 13613 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
149 0red 11293 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 ∈ ℝ)
150 1red 11291 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℝ)
15125a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ)
152 nnre 12300 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
153151, 152remulcld 11320 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ)
154153, 150readdcld 11319 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ)
15534a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 0 < 1)
156 2rp 13062 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
157156a1i 11 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 2 ∈ ℝ+)
158 nnrp 13068 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
159157, 158rpmulcld 13115 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ+)
160150, 159ltaddrp2d 13133 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 < ((2 · 𝑛) + 1))
161149, 150, 154, 155, 160lttrd 11451 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 0 < ((2 · 𝑛) + 1))
162161gt0ne0d 11854 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ≠ 0)
163148, 162syl 17 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑗) → ((2 · 𝑛) + 1) ≠ 0)
164163adantl 481 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ≠ 0)
165147, 164reccld 12063 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑛) + 1)) ∈ ℂ)
16699ad2antrr 725 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ)
16760a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℕ0)
168167, 142nn0mulcld 12618 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℕ0)
16963a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℕ0)
170168, 169nn0addcld 12617 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℕ0)
171166, 170expcld 14196 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) ∈ ℂ)
172165, 171mulcld 11310 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) ∈ ℂ)
173143, 172mulcld 11310 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) ∈ ℂ)
1749, 136, 142, 173fvmptd3 7052 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
175174, 173eqeltrd 2844 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻𝑛) ∈ ℂ)
176 addcl 11266 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
177176adantl 481 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
178130, 175, 177seqcl 14073 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐻)‘𝑗) ∈ ℂ)
179 1cnd 11285 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 1 ∈ ℂ)
180 2cnd 12371 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 2 ∈ ℂ)
18141ad2antrr 725 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑁 ∈ ℂ)
182180, 181mulcld 11310 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (2 · 𝑁) ∈ ℂ)
183179, 182addcld 11309 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (1 + (2 · 𝑁)) ∈ ℂ)
184183halfcld 12538 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → ((1 + (2 · 𝑁)) / 2) ∈ ℂ)
185 simprl 770 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑛 ∈ ℂ)
186 simprr 772 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑖 ∈ ℂ)
187184, 185, 186adddid 11314 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (((1 + (2 · 𝑁)) / 2) · (𝑛 + 𝑖)) = ((((1 + (2 · 𝑁)) / 2) · 𝑛) + (((1 + (2 · 𝑁)) / 2) · 𝑖)))
188 stirlinglem7.2 . . . . . . 7 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))))
189131oveq2d 7464 . . . . . . . 8 (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
190133, 189oveq12d 7466 . . . . . . 7 (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
191148adantl 481 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ)
192166, 168expcld 14196 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) ∈ ℂ)
193165, 192mulcld 11310 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) ∈ ℂ)
194188, 190, 191, 193fvmptd3 7052 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
195124ad2antrr 725 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) ∈ ℂ)
196 2ne0 12397 . . . . . . . . 9 2 ≠ 0
197196a1i 11 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ≠ 0)
198195, 143, 173, 197div32d 12093 . . . . . . 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 12075 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))
200199oveq2d 7464 . . . . . . 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 11499 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))))
20298ad2antrr 725 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ∈ ℂ)
20357ad2antrr 725 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ≠ 0)
204170nn0zd 12665 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℤ)
205202, 203, 204exprecd 14204 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) = (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))))
206205oveq2d 7464 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
207202, 170expcld 14196 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ∈ ℂ)
208202, 203, 204expne0d 14202 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ≠ 0)
209195, 207, 208divrecd 12073 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)))))
21041ad2antrr 725 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑁 ∈ ℂ)
211143, 210mulcld 11310 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑁) ∈ ℂ)
212146, 211addcomd 11492 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
213202, 168expcld 14196 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ∈ ℂ)
214213, 202mulcomd 11311 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)) = (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))
215212, 214oveq12d 7466 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
216202, 168expp1d 14197 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) = ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)))
217216oveq2d 7464 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))))
218 2z 12675 . . . . . . . . . . . . . . 15 2 ∈ ℤ
219218a1i 11 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℤ)
220142nn0zd 12665 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℤ)
221219, 220zmulcld 12753 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℤ)
222202, 203, 221expne0d 14202 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ≠ 0)
223202, 202, 213, 203, 222divdiv1d 12101 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
224215, 217, 2233eqtr4d 2790 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
225206, 209, 2243eqtr2d 2786 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
226225oveq2d 7464 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))))
227202, 203dividd 12068 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1)
228 1exp 14142 . . . . . . . . . . . . 13 ((2 · 𝑛) ∈ ℤ → (1↑(2 · 𝑛)) = 1)
229221, 228syl 17 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1↑(2 · 𝑛)) = 1)
230227, 229eqtr4d 2783 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = (1↑(2 · 𝑛)))
231230oveq1d 7463 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
232146, 202, 203, 168expdivd 14210 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))
233231, 232eqtr4d 2783 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))
234233oveq2d 7464 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
235201, 226, 2343eqtrd 2784 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
236198, 200, 2353eqtrd 2784 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))))
237174eqcomd 2746 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) = (𝐻𝑛))
238237oveq2d 7464 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
239194, 236, 2383eqtr2d 2786 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾𝑛) = (((1 + (2 · 𝑁)) / 2) · (𝐻𝑛)))
240177, 187, 130, 175, 239seqdistr 14104 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐾)‘𝑗) = (((1 + (2 · 𝑁)) / 2) · (seq1( + , 𝐻)‘𝑗)))
2411, 2, 123, 125, 127, 178, 240climmulc2 15683 . . 3 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
24288, 97addcomd 11492 . . . . . 6 (𝑁 ∈ ℕ → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1))
243242oveq1d 7463 . . . . 5 (𝑁 ∈ ℕ → ((1 + (2 · 𝑁)) / 2) = (((2 · 𝑁) + 1) / 2))
244243oveq1d 7463 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))))
245243, 125eqeltrrd 2845 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) ∈ ℂ)
24641, 88addcld 11309 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
247 nnne0 12327 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
248246, 41, 247divcld 12070 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
24947, 49readdcld 11319 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
25047ltp1d 12225 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
25151, 47, 249, 52, 250lttrd 11451 . . . . . . . 8 (𝑁 ∈ ℕ → 0 < (𝑁 + 1))
252251gt0ne0d 11854 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0)
253246, 41, 252, 247divne0d 12086 . . . . . 6 (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0)
254248, 253logcld 26630 . . . . 5 (𝑁 ∈ ℕ → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
25585, 98, 57divcld 12070 . . . . 5 (𝑁 ∈ ℕ → (2 / ((2 · 𝑁) + 1)) ∈ ℂ)
256245, 254, 255subdid 11746 . . . 4 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))))
25797, 88addcomd 11492 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) = (1 + (2 · 𝑁)))
258257oveq1d 7463 . . . . . 6 (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / 2) = ((1 + (2 · 𝑁)) / 2))
259258oveq1d 7463 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
260196a1i 11 . . . . . 6 (𝑁 ∈ ℕ → 2 ≠ 0)
26198, 85, 57, 260divcan6d 12089 . . . . 5 (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1))) = 1)
262259, 261oveq12d 7466 . . . 4 (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / 2) · (log‘((𝑁 + 1) / 𝑁))) − ((((2 · 𝑁) + 1) / 2) · (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
263244, 256, 2623eqtrd 2784 . . 3 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · ((log‘((𝑁 + 1) / 𝑁)) − (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
264241, 263breqtrd 5192 . 2 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
265 stirlinglem7.1 . . 3 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1))
266 oveq2 7456 . . . . . . 7 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
267266oveq2d 7464 . . . . . 6 (𝑛 = 𝑁 → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁)))
268267oveq1d 7463 . . . . 5 (𝑛 = 𝑁 → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2))
269 oveq1 7455 . . . . . . 7 (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1))
270 id 22 . . . . . . 7 (𝑛 = 𝑁𝑛 = 𝑁)
271269, 270oveq12d 7466 . . . . . 6 (𝑛 = 𝑁 → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁))
272271fveq2d 6924 . . . . 5 (𝑛 = 𝑁 → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁)))
273268, 272oveq12d 7466 . . . 4 (𝑛 = 𝑁 → (((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))))
274273oveq1d 7463 . . 3 (𝑛 = 𝑁 → ((((1 + (2 · 𝑛)) / 2) · (log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
275 id 22 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
276125, 254mulcld 11310 . . . 4 (𝑁 ∈ ℕ → (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
277276, 88subcld 11647 . . 3 (𝑁 ∈ ℕ → ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
278265, 274, 275, 277fvmptd3 7052 . 2 (𝑁 ∈ ℕ → (𝐽𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1))
279264, 278breqtrrd 5194 1 (𝑁 ∈ ℕ → seq1( + , 𝐾) ⇝ (𝐽𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2108  wne 2946  Vcvv 3488   class class class wbr 5166  cmpt 5249  cfv 6573  (class class class)co 7448  cc 11182  cr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189   < clt 11324  cle 11325  cmin 11520   / cdiv 11947  cn 12293  2c2 12348  0cn0 12553  cz 12639  cuz 12903  +crp 13057  ...cfz 13567  seqcseq 14052  cexp 14112  cli 15530  logclog 26614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-xnn0 12626  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ioc 13412  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-fac 14323  df-bc 14352  df-hash 14380  df-shft 15116  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-limsup 15517  df-clim 15534  df-rlim 15535  df-sum 15735  df-ef 16115  df-sin 16117  df-cos 16118  df-tan 16119  df-pi 16120  df-dvds 16303  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-starv 17326  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-unif 17334  df-hom 17335  df-cco 17336  df-rest 17482  df-topn 17483  df-0g 17501  df-gsum 17502  df-topgen 17503  df-pt 17504  df-prds 17507  df-xrs 17562  df-qtop 17567  df-imas 17568  df-xps 17570  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-submnd 18819  df-mulg 19108  df-cntz 19357  df-cmn 19824  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-fbas 21384  df-fg 21385  df-cnfld 21388  df-top 22921  df-topon 22938  df-topsp 22960  df-bases 22974  df-cld 23048  df-ntr 23049  df-cls 23050  df-nei 23127  df-lp 23165  df-perf 23166  df-cn 23256  df-cnp 23257  df-haus 23344  df-cmp 23416  df-tx 23591  df-hmeo 23784  df-fil 23875  df-fm 23967  df-flim 23968  df-flf 23969  df-xms 24351  df-ms 24352  df-tms 24353  df-cncf 24923  df-limc 25921  df-dv 25922  df-ulm 26438  df-log 26616
This theorem is referenced by:  stirlinglem9  46003
  Copyright terms: Public domain W3C validator