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

Theorem stirlinglem1 45491
Description: A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Hypotheses
Ref Expression
stirlinglem1.1 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
stirlinglem1.2 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
stirlinglem1.3 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
stirlinglem1.4 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
Assertion
Ref Expression
stirlinglem1 𝐻 ⇝ (1 / 2)

Proof of Theorem stirlinglem1
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nnuz 12903 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12631 . . . 4 (⊤ → 1 ∈ ℤ)
3 stirlinglem1.4 . . . . . . . . 9 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4 ax-1cn 11204 . . . . . . . . . 10 1 ∈ ℂ
5 divcnv 15839 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
64, 5ax-mp 5 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
73, 6eqbrtri 5173 . . . . . . . 8 𝐿 ⇝ 0
87a1i 11 . . . . . . 7 (⊤ → 𝐿 ⇝ 0)
9 stirlinglem1.3 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10 nnex 12256 . . . . . . . . . 10 ℕ ∈ V
1110mptex 7241 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
129, 11eqeltri 2825 . . . . . . . 8 𝐺 ∈ V
1312a1i 11 . . . . . . 7 (⊤ → 𝐺 ∈ V)
143a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15 simpr 483 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
1615oveq2d 7442 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17 id 22 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18 nnrp 13025 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
1918rpreccld 13066 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
2014, 16, 17, 19fvmptd 7017 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐿𝑘) = (1 / 𝑘))
21 nnrecre 12292 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
2220, 21eqeltrd 2829 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐿𝑘) ∈ ℝ)
2322adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿𝑘) ∈ ℝ)
249a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
2515oveq2d 7442 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
2625oveq1d 7441 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
2726oveq2d 7442 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28 2re 12324 . . . . . . . . . . . . . 14 2 ∈ ℝ
2928a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℝ)
30 nnre 12257 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
3129, 30remulcld 11282 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32 0le2 12352 . . . . . . . . . . . . . 14 0 ≤ 2
3332a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 0 ≤ 2)
3418rpge0d 13060 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 0 ≤ 𝑘)
3529, 30, 33, 34mulge0d 11829 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
3631, 35ge0p1rpd 13086 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
3736rpreccld 13066 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
3824, 27, 17, 37fvmptd 7017 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐺𝑘) = (1 / ((2 · 𝑘) + 1)))
3937rpred 13056 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
4038, 39eqeltrd 2829 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ∈ ℝ)
4140adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
42 1red 11253 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℝ)
43 0le1 11775 . . . . . . . . . . 11 0 ≤ 1
4443a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 0 ≤ 1)
4531, 42readdcld 11281 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46 nncn 12258 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
4746mullidd 11270 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48 1lt2 12421 . . . . . . . . . . . . . . 15 1 < 2
4948a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 1 < 2)
5042, 29, 18, 49ltmul1dd 13111 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
5147, 50eqbrtrrd 5176 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
5231ltp1d 12182 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
5330, 31, 45, 51, 52lttrd 11413 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
5430, 45, 53ltled 11400 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
5518, 36, 42, 44, 54lediv2ad 13078 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
5655, 38, 203brtr4d 5184 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ≤ (𝐿𝑘))
5756adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐿𝑘))
5837rpge0d 13060 . . . . . . . . 9 (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
5958, 38breqtrrd 5180 . . . . . . . 8 (𝑘 ∈ ℕ → 0 ≤ (𝐺𝑘))
6059adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))
611, 2, 8, 13, 23, 41, 57, 60climsqz2 15626 . . . . . 6 (⊤ → 𝐺 ⇝ 0)
62 1cnd 11247 . . . . . 6 (⊤ → 1 ∈ ℂ)
63 stirlinglem1.2 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
6410mptex 7241 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
6563, 64eqeltri 2825 . . . . . . 7 𝐹 ∈ V
6665a1i 11 . . . . . 6 (⊤ → 𝐹 ∈ V)
6741recnd 11280 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℂ)
6863a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
6927oveq2d 7442 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70 1cnd 11247 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℂ)
71 2cnd 12328 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℂ)
7271, 46mulcld 11272 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
7372, 70addcld 11271 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
7436rpne0d 13061 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
7573, 74reccld 12021 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
7670, 75subcld 11609 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
7768, 69, 17, 76fvmptd 7017 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐹𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
7838eqcomd 2734 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺𝑘))
7978oveq2d 7442 . . . . . . . 8 (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺𝑘)))
8077, 79eqtrd 2768 . . . . . . 7 (𝑘 ∈ ℕ → (𝐹𝑘) = (1 − (𝐺𝑘)))
8180adantl 480 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (1 − (𝐺𝑘)))
821, 2, 61, 62, 66, 67, 81climsubc2 15623 . . . . 5 (⊤ → 𝐹 ⇝ (1 − 0))
83 1m0e1 12371 . . . . 5 (1 − 0) = 1
8482, 83breqtrdi 5193 . . . 4 (⊤ → 𝐹 ⇝ 1)
8562halfcld 12495 . . . 4 (⊤ → (1 / 2) ∈ ℂ)
86 stirlinglem1.1 . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
8710mptex 7241 . . . . . 6 (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
8886, 87eqeltri 2825 . . . . 5 𝐻 ∈ V
8988a1i 11 . . . 4 (⊤ → 𝐻 ∈ V)
9077, 76eqeltrd 2829 . . . . 5 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
9190adantl 480 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
92 nncn 12258 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
9392sqcld 14148 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
9493mullidd 11270 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
9594eqcomd 2734 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96 2cnd 12328 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 2 ∈ ℂ)
9796, 92mulcld 11272 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98 1cnd 11247 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℂ)
9992, 97, 98adddid 11276 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
10092, 96, 92mul12d 11461 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
10192sqvald 14147 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102101eqcomd 2734 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103102oveq2d 7442 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104100, 103eqtrd 2768 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
10592mulridd 11269 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106104, 105oveq12d 7444 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107 2ne0 12354 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
108107a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 2 ≠ 0)
10992, 96, 108divcan2d 12030 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110109eqcomd 2734 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111110oveq2d 7442 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
11292halfcld 12495 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
11396, 93, 112adddid 11276 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114111, 113eqtr4d 2771 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
11599, 106, 1143eqtrd 2772 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
11695, 115oveq12d 7444 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
11793, 112addcld 11271 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118 nnrp 13025 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119 2z 12632 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
120119a1i 11 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 2 ∈ ℤ)
121118, 120rpexpcld 14249 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122118rphalfcld 13068 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123121, 122rpaddcld 13071 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124123rpne0d 13061 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
12598, 96, 93, 117, 108, 124divmuldivd 12069 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
12693, 112pncand 11610 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127126eqcomd 2734 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128127oveq1d 7441 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129117, 112, 117, 124divsubdird 12067 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130117, 124dividd 12026 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131130oveq1d 7441 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132128, 129, 1313eqtrd 2772 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133 nnne0 12284 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
13496, 92, 133divcld 12028 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
13596, 92, 108, 133divne0d 12044 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136112, 117, 134, 124, 135divcan5rd 12055 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
13792, 96, 133, 108divcan6d 12047 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
13893, 112, 134adddird 11277 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
13993, 96, 92, 133div12d 12064 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140 1e2m1 12377 . . . . . . . . . . . . . . . . . . . . . . 23 1 = (2 − 1)
141140oveq2i 7437 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛↑1) = (𝑛↑(2 − 1))
14292exp1d 14145 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
14392, 133, 120expm1d 14160 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144141, 142, 1433eqtr3a 2792 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145144eqcomd 2734 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146145oveq2d 7442 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147139, 146eqtrd 2768 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148147, 137oveq12d 7444 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149138, 148eqtrd 2768 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150137, 149oveq12d 7444 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151136, 150eqtr3d 2770 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152151oveq2d 7442 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153132, 152eqtrd 2768 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154153oveq2d 7442 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155116, 125, 1543eqtr2d 2774 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156155mpteq2ia 5255 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
15786, 156eqtri 2756 . . . . . . . 8 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158157a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
15969oveq2d 7442 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
16070halfcld 12495 . . . . . . . 8 (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161160, 76mulcld 11272 . . . . . . 7 (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162158, 159, 17, 161fvmptd 7017 . . . . . 6 (𝑘 ∈ ℕ → (𝐻𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
16377oveq2d 7442 . . . . . 6 (𝑘 ∈ ℕ → ((1 / 2) · (𝐹𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164162, 163eqtr4d 2771 . . . . 5 (𝑘 ∈ ℕ → (𝐻𝑘) = ((1 / 2) · (𝐹𝑘)))
165164adantl 480 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻𝑘) = ((1 / 2) · (𝐹𝑘)))
1661, 2, 84, 85, 89, 91, 165climmulc2 15621 . . 3 (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167166mptru 1540 . 2 𝐻 ⇝ ((1 / 2) · 1)
168 halfcn 12465 . . 3 (1 / 2) ∈ ℂ
169168mulridi 11256 . 2 ((1 / 2) · 1) = (1 / 2)
170167, 169breqtri 5177 1 𝐻 ⇝ (1 / 2)
Colors of variables: wff setvar class
Syntax hints:  wa 394   = wceq 1533  wtru 1534  wcel 2098  wne 2937  Vcvv 3473   class class class wbr 5152  cmpt 5235  cfv 6553  (class class class)co 7426  cc 11144  cr 11145  0cc0 11146  1c1 11147   + caddc 11149   · cmul 11151   < clt 11286  cle 11287  cmin 11482   / cdiv 11909  cn 12250  2c2 12305  cz 12596  +crp 13014  cexp 14066  cli 15468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-z 12597  df-uz 12861  df-rp 13015  df-fl 13797  df-seq 14007  df-exp 14067  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-clim 15472  df-rlim 15473
This theorem is referenced by:  stirlinglem15  45505
  Copyright terms: Public domain W3C validator