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 38870
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 11463 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11149 . . . 4 (⊤ → 1 ∈ ℤ)
3 stirlinglem1.4 . . . . . . . . 9 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4 ax-1cn 9749 . . . . . . . . . 10 1 ∈ ℂ
5 divcnv 14293 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
64, 5ax-mp 5 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
73, 6eqbrtri 4502 . . . . . . . 8 𝐿 ⇝ 0
87a1i 11 . . . . . . 7 (⊤ → 𝐿 ⇝ 0)
9 stirlinglem1.3 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10 nnex 10781 . . . . . . . . . 10 ℕ ∈ V
1110mptex 6267 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
129, 11eqeltri 2588 . . . . . . . 8 𝐺 ∈ V
1312a1i 11 . . . . . . 7 (⊤ → 𝐺 ∈ V)
143a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15 simpr 475 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
1615oveq2d 6442 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17 id 22 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18 nnrp 11584 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
1918rpreccld 11624 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
2014, 16, 17, 19fvmptd 6081 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐿𝑘) = (1 / 𝑘))
21 nnrecre 10812 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
2220, 21eqeltrd 2592 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐿𝑘) ∈ ℝ)
2322adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿𝑘) ∈ ℝ)
249a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
2515oveq2d 6442 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
2625oveq1d 6441 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
2726oveq2d 6442 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28 2re 10845 . . . . . . . . . . . . . 14 2 ∈ ℝ
2928a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℝ)
30 nnre 10782 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
3129, 30remulcld 9825 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32 0le2 10866 . . . . . . . . . . . . . 14 0 ≤ 2
3332a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 0 ≤ 2)
3418rpge0d 11618 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 0 ≤ 𝑘)
3529, 30, 33, 34mulge0d 10353 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
3631, 35ge0p1rpd 11644 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
3736rpreccld 11624 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
3824, 27, 17, 37fvmptd 6081 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐺𝑘) = (1 / ((2 · 𝑘) + 1)))
3937rpred 11614 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
4038, 39eqeltrd 2592 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ∈ ℝ)
4140adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
42 1red 9810 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℝ)
43 0le1 10300 . . . . . . . . . . 11 0 ≤ 1
4443a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 0 ≤ 1)
4531, 42readdcld 9824 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46 nncn 10783 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
4746mulid2d 9813 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48 1lt2 10949 . . . . . . . . . . . . . . 15 1 < 2
4948a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 1 < 2)
5042, 29, 18, 49ltmul1dd 11669 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
5147, 50eqbrtrrd 4505 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
5231ltp1d 10704 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
5330, 31, 45, 51, 52lttrd 9949 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
5430, 45, 53ltled 9936 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
5518, 36, 42, 44, 54lediv2ad 11636 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
5655, 38, 203brtr4d 4513 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ≤ (𝐿𝑘))
5756adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐿𝑘))
5837rpge0d 11618 . . . . . . . . 9 (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
5958, 38breqtrrd 4509 . . . . . . . 8 (𝑘 ∈ ℕ → 0 ≤ (𝐺𝑘))
6059adantl 480 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))
611, 2, 8, 13, 23, 41, 57, 60climsqz2 14086 . . . . . 6 (⊤ → 𝐺 ⇝ 0)
62 1cnd 9811 . . . . . 6 (⊤ → 1 ∈ ℂ)
63 stirlinglem1.2 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
6410mptex 6267 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
6563, 64eqeltri 2588 . . . . . . 7 𝐹 ∈ V
6665a1i 11 . . . . . 6 (⊤ → 𝐹 ∈ V)
6741recnd 9823 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℂ)
6863a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
6927oveq2d 6442 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70 1cnd 9811 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℂ)
71 2cnd 10848 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℂ)
7271, 46mulcld 9815 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
7372, 70addcld 9814 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
7436rpne0d 11619 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
7573, 74reccld 10543 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
7670, 75subcld 10143 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
7768, 69, 17, 76fvmptd 6081 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐹𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
7838eqcomd 2520 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺𝑘))
7978oveq2d 6442 . . . . . . . 8 (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺𝑘)))
8077, 79eqtrd 2548 . . . . . . 7 (𝑘 ∈ ℕ → (𝐹𝑘) = (1 − (𝐺𝑘)))
8180adantl 480 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (1 − (𝐺𝑘)))
821, 2, 61, 62, 66, 67, 81climsubc2 14083 . . . . 5 (⊤ → 𝐹 ⇝ (1 − 0))
83 1m0e1 10886 . . . . 5 (1 − 0) = 1
8482, 83syl6breq 4522 . . . 4 (⊤ → 𝐹 ⇝ 1)
8562halfcld 11032 . . . 4 (⊤ → (1 / 2) ∈ ℂ)
86 stirlinglem1.1 . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
8710mptex 6267 . . . . . 6 (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
8886, 87eqeltri 2588 . . . . 5 𝐻 ∈ V
8988a1i 11 . . . 4 (⊤ → 𝐻 ∈ V)
9077, 76eqeltrd 2592 . . . . 5 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
9190adantl 480 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
92 nncn 10783 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
9392sqcld 12736 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
9493mulid2d 9813 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
9594eqcomd 2520 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96 2cnd 10848 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 2 ∈ ℂ)
9796, 92mulcld 9815 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98 1cnd 9811 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℂ)
9992, 97, 98adddid 9819 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
10092, 96, 92mul12d 9996 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
10192sqvald 12735 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102101eqcomd 2520 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103102oveq2d 6442 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104100, 103eqtrd 2548 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
10592mulid1d 9812 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106104, 105oveq12d 6444 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107 2ne0 10868 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
108107a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 2 ≠ 0)
10992, 96, 108divcan2d 10552 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110109eqcomd 2520 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111110oveq2d 6442 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
11292halfcld 11032 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
11396, 93, 112adddid 9819 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114111, 113eqtr4d 2551 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
11599, 106, 1143eqtrd 2552 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
11695, 115oveq12d 6444 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
11793, 112addcld 9814 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118 nnrp 11584 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119 2z 11150 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
120119a1i 11 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 2 ∈ ℤ)
121118, 120rpexpcld 12762 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122118rphalfcld 11626 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123121, 122rpaddcld 11629 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124123rpne0d 11619 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
12598, 96, 93, 117, 108, 124divmuldivd 10591 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
12693, 112pncand 10144 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127126eqcomd 2520 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128127oveq1d 6441 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129117, 112, 117, 124divsubdird 10589 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130117, 124dividd 10548 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131130oveq1d 6441 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132128, 129, 1313eqtrd 2552 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133 nnne0 10808 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
13496, 92, 133divcld 10550 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
13596, 92, 108, 133divne0d 10566 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136112, 117, 134, 124, 135divcan5rd 10577 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
13792, 96, 133, 108divcan6d 10569 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
13893, 112, 134adddird 9820 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
13993, 96, 92, 133div12d 10586 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140 1e2m1 10891 . . . . . . . . . . . . . . . . . . . . . . 23 1 = (2 − 1)
141140oveq2i 6437 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛↑1) = (𝑛↑(2 − 1))
14292exp1d 12733 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
14392, 133, 120expm1d 12748 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144141, 142, 1433eqtr3a 2572 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145144eqcomd 2520 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146145oveq2d 6442 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147139, 146eqtrd 2548 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148147, 137oveq12d 6444 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149138, 148eqtrd 2548 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150137, 149oveq12d 6444 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151136, 150eqtr3d 2550 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152151oveq2d 6442 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153132, 152eqtrd 2548 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154153oveq2d 6442 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155116, 125, 1543eqtr2d 2554 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156155mpteq2ia 4566 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
15786, 156eqtri 2536 . . . . . . . 8 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158157a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
15969oveq2d 6442 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
16070halfcld 11032 . . . . . . . 8 (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161160, 76mulcld 9815 . . . . . . 7 (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162158, 159, 17, 161fvmptd 6081 . . . . . 6 (𝑘 ∈ ℕ → (𝐻𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
16377oveq2d 6442 . . . . . 6 (𝑘 ∈ ℕ → ((1 / 2) · (𝐹𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164162, 163eqtr4d 2551 . . . . 5 (𝑘 ∈ ℕ → (𝐻𝑘) = ((1 / 2) · (𝐹𝑘)))
165164adantl 480 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻𝑘) = ((1 / 2) · (𝐹𝑘)))
1661, 2, 84, 85, 89, 91, 165climmulc2 14081 . . 3 (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167166trud 1483 . 2 𝐻 ⇝ ((1 / 2) · 1)
168 halfcn 11002 . . 3 (1 / 2) ∈ ℂ
169168mulid1i 9797 . 2 ((1 / 2) · 1) = (1 / 2)
170167, 169breqtri 4506 1 𝐻 ⇝ (1 / 2)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wtru 1475  wcel 1938  wne 2684  Vcvv 3077   class class class wbr 4481  cmpt 4541  cfv 5689  (class class class)co 6426  cc 9689  cr 9690  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696   < clt 9829  cle 9830  cmin 10017   / cdiv 10433  cn 10775  2c2 10825  cz 11118  +crp 11574  cexp 12590  cli 13929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-om 6834  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-er 7505  df-pm 7623  df-en 7718  df-dom 7719  df-sdom 7720  df-sup 8107  df-inf 8108  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-n0 11048  df-z 11119  df-uz 11428  df-rp 11575  df-fl 12323  df-seq 12532  df-exp 12591  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-clim 13933  df-rlim 13934
This theorem is referenced by:  stirlinglem15  38884
  Copyright terms: Public domain W3C validator