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

Theorem stirlinglem1 40060
 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 11720 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11405 . . . 4 (⊤ → 1 ∈ ℤ)
3 stirlinglem1.4 . . . . . . . . 9 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4 ax-1cn 9991 . . . . . . . . . 10 1 ∈ ℂ
5 divcnv 14579 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
64, 5ax-mp 5 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
73, 6eqbrtri 4672 . . . . . . . 8 𝐿 ⇝ 0
87a1i 11 . . . . . . 7 (⊤ → 𝐿 ⇝ 0)
9 stirlinglem1.3 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10 nnex 11023 . . . . . . . . . 10 ℕ ∈ V
1110mptex 6483 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
129, 11eqeltri 2696 . . . . . . . 8 𝐺 ∈ V
1312a1i 11 . . . . . . 7 (⊤ → 𝐺 ∈ V)
143a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15 simpr 477 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
1615oveq2d 6663 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17 id 22 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18 nnrp 11839 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
1918rpreccld 11879 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
2014, 16, 17, 19fvmptd 6286 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐿𝑘) = (1 / 𝑘))
21 nnrecre 11054 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
2220, 21eqeltrd 2700 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐿𝑘) ∈ ℝ)
2322adantl 482 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿𝑘) ∈ ℝ)
249a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
2515oveq2d 6663 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
2625oveq1d 6662 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
2726oveq2d 6663 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28 2re 11087 . . . . . . . . . . . . . 14 2 ∈ ℝ
2928a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℝ)
30 nnre 11024 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
3129, 30remulcld 10067 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32 0le2 11108 . . . . . . . . . . . . . 14 0 ≤ 2
3332a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 0 ≤ 2)
3418rpge0d 11873 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 0 ≤ 𝑘)
3529, 30, 33, 34mulge0d 10601 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
3631, 35ge0p1rpd 11899 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
3736rpreccld 11879 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
3824, 27, 17, 37fvmptd 6286 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐺𝑘) = (1 / ((2 · 𝑘) + 1)))
3937rpred 11869 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
4038, 39eqeltrd 2700 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ∈ ℝ)
4140adantl 482 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
42 1red 10052 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℝ)
43 0le1 10548 . . . . . . . . . . 11 0 ≤ 1
4443a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 0 ≤ 1)
4531, 42readdcld 10066 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46 nncn 11025 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
4746mulid2d 10055 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48 1lt2 11191 . . . . . . . . . . . . . . 15 1 < 2
4948a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 1 < 2)
5042, 29, 18, 49ltmul1dd 11924 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
5147, 50eqbrtrrd 4675 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
5231ltp1d 10951 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
5330, 31, 45, 51, 52lttrd 10195 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
5430, 45, 53ltled 10182 . . . . . . . . . 10 (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
5518, 36, 42, 44, 54lediv2ad 11891 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
5655, 38, 203brtr4d 4683 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ≤ (𝐿𝑘))
5756adantl 482 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐿𝑘))
5837rpge0d 11873 . . . . . . . . 9 (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
5958, 38breqtrrd 4679 . . . . . . . 8 (𝑘 ∈ ℕ → 0 ≤ (𝐺𝑘))
6059adantl 482 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))
611, 2, 8, 13, 23, 41, 57, 60climsqz2 14366 . . . . . 6 (⊤ → 𝐺 ⇝ 0)
62 1cnd 10053 . . . . . 6 (⊤ → 1 ∈ ℂ)
63 stirlinglem1.2 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
6410mptex 6483 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
6563, 64eqeltri 2696 . . . . . . 7 𝐹 ∈ V
6665a1i 11 . . . . . 6 (⊤ → 𝐹 ∈ V)
6741recnd 10065 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℂ)
6863a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
6927oveq2d 6663 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70 1cnd 10053 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℂ)
71 2cnd 11090 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 2 ∈ ℂ)
7271, 46mulcld 10057 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
7372, 70addcld 10056 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
7436rpne0d 11874 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
7573, 74reccld 10791 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
7670, 75subcld 10389 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
7768, 69, 17, 76fvmptd 6286 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐹𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
7838eqcomd 2627 . . . . . . . . 9 (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺𝑘))
7978oveq2d 6663 . . . . . . . 8 (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺𝑘)))
8077, 79eqtrd 2655 . . . . . . 7 (𝑘 ∈ ℕ → (𝐹𝑘) = (1 − (𝐺𝑘)))
8180adantl 482 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (1 − (𝐺𝑘)))
821, 2, 61, 62, 66, 67, 81climsubc2 14363 . . . . 5 (⊤ → 𝐹 ⇝ (1 − 0))
83 1m0e1 11128 . . . . 5 (1 − 0) = 1
8482, 83syl6breq 4692 . . . 4 (⊤ → 𝐹 ⇝ 1)
8562halfcld 11274 . . . 4 (⊤ → (1 / 2) ∈ ℂ)
86 stirlinglem1.1 . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
8710mptex 6483 . . . . . 6 (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
8886, 87eqeltri 2696 . . . . 5 𝐻 ∈ V
8988a1i 11 . . . 4 (⊤ → 𝐻 ∈ V)
9077, 76eqeltrd 2700 . . . . 5 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
9190adantl 482 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
92 nncn 11025 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
9392sqcld 13001 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
9493mulid2d 10055 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
9594eqcomd 2627 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96 2cnd 11090 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 2 ∈ ℂ)
9796, 92mulcld 10057 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98 1cnd 10053 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 1 ∈ ℂ)
9992, 97, 98adddid 10061 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
10092, 96, 92mul12d 10242 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
10192sqvald 13000 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102101eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103102oveq2d 6663 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104100, 103eqtrd 2655 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
10592mulid1d 10054 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106104, 105oveq12d 6665 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107 2ne0 11110 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
108107a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 2 ≠ 0)
10992, 96, 108divcan2d 10800 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110109eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111110oveq2d 6663 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
11292halfcld 11274 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
11396, 93, 112adddid 10061 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114111, 113eqtr4d 2658 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
11599, 106, 1143eqtrd 2659 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
11695, 115oveq12d 6665 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
11793, 112addcld 10056 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118 nnrp 11839 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119 2z 11406 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
120119a1i 11 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 2 ∈ ℤ)
121118, 120rpexpcld 13027 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122118rphalfcld 11881 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123121, 122rpaddcld 11884 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124123rpne0d 11874 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
12598, 96, 93, 117, 108, 124divmuldivd 10839 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
12693, 112pncand 10390 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127126eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128127oveq1d 6662 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129117, 112, 117, 124divsubdird 10837 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130117, 124dividd 10796 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131130oveq1d 6662 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132128, 129, 1313eqtrd 2659 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133 nnne0 11050 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
13496, 92, 133divcld 10798 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
13596, 92, 108, 133divne0d 10814 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136112, 117, 134, 124, 135divcan5rd 10825 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
13792, 96, 133, 108divcan6d 10817 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
13893, 112, 134adddird 10062 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
13993, 96, 92, 133div12d 10834 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140 1e2m1 11133 . . . . . . . . . . . . . . . . . . . . . . 23 1 = (2 − 1)
141140oveq2i 6658 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛↑1) = (𝑛↑(2 − 1))
14292exp1d 12998 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
14392, 133, 120expm1d 13013 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144141, 142, 1433eqtr3a 2679 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145144eqcomd 2627 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146145oveq2d 6663 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147139, 146eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148147, 137oveq12d 6665 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149138, 148eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150137, 149oveq12d 6665 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151136, 150eqtr3d 2657 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152151oveq2d 6663 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153132, 152eqtrd 2655 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154153oveq2d 6663 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155116, 125, 1543eqtr2d 2661 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156155mpteq2ia 4738 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
15786, 156eqtri 2643 . . . . . . . 8 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158157a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
15969oveq2d 6663 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
16070halfcld 11274 . . . . . . . 8 (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161160, 76mulcld 10057 . . . . . . 7 (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162158, 159, 17, 161fvmptd 6286 . . . . . 6 (𝑘 ∈ ℕ → (𝐻𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
16377oveq2d 6663 . . . . . 6 (𝑘 ∈ ℕ → ((1 / 2) · (𝐹𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164162, 163eqtr4d 2658 . . . . 5 (𝑘 ∈ ℕ → (𝐻𝑘) = ((1 / 2) · (𝐹𝑘)))
165164adantl 482 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻𝑘) = ((1 / 2) · (𝐹𝑘)))
1661, 2, 84, 85, 89, 91, 165climmulc2 14361 . . 3 (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167166trud 1492 . 2 𝐻 ⇝ ((1 / 2) · 1)
168 halfcn 11244 . . 3 (1 / 2) ∈ ℂ
169168mulid1i 10039 . 2 ((1 / 2) · 1) = (1 / 2)
170167, 169breqtri 4676 1 𝐻 ⇝ (1 / 2)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 384   = wceq 1482  ⊤wtru 1483   ∈ wcel 1989   ≠ wne 2793  Vcvv 3198   class class class wbr 4651   ↦ cmpt 4727  ‘cfv 5886  (class class class)co 6647  ℂcc 9931  ℝcr 9932  0cc0 9933  1c1 9934   + caddc 9936   · cmul 9938   < clt 10071   ≤ cle 10072   − cmin 10263   / cdiv 10681  ℕcn 11017  2c2 11067  ℤcz 11374  ℝ+crp 11829  ↑cexp 12855   ⇝ cli 14209 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-er 7739  df-pm 7857  df-en 7953  df-dom 7954  df-sdom 7955  df-sup 8345  df-inf 8346  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-rp 11830  df-fl 12588  df-seq 12797  df-exp 12856  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-rlim 14214 This theorem is referenced by:  stirlinglem15  40074
 Copyright terms: Public domain W3C validator