| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12921 | . . . 4
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12648 | . . . 4
⊢ (⊤
→ 1 ∈ ℤ) | 
| 3 |  | stirlinglem1.4 | . . . . . . . . 9
⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) | 
| 4 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 5 |  | divcnv 15889 | . . . . . . . . . 10
⊢ (1 ∈
ℂ → (𝑛 ∈
ℕ ↦ (1 / 𝑛))
⇝ 0) | 
| 6 | 4, 5 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ (1 /
𝑛)) ⇝
0 | 
| 7 | 3, 6 | eqbrtri 5164 | . . . . . . . 8
⊢ 𝐿 ⇝ 0 | 
| 8 | 7 | a1i 11 | . . . . . . 7
⊢ (⊤
→ 𝐿 ⇝
0) | 
| 9 |  | stirlinglem1.3 | . . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 ·
𝑛) + 1))) | 
| 10 |  | nnex 12272 | . . . . . . . . . 10
⊢ ℕ
∈ V | 
| 11 | 10 | mptex 7243 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ (1 / ((2
· 𝑛) + 1))) ∈
V | 
| 12 | 9, 11 | eqeltri 2837 | . . . . . . . 8
⊢ 𝐺 ∈ V | 
| 13 | 12 | a1i 11 | . . . . . . 7
⊢ (⊤
→ 𝐺 ∈
V) | 
| 14 | 3 | a1i 11 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))) | 
| 15 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘) | 
| 16 | 15 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘)) | 
| 17 |  | id 22 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ) | 
| 18 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) | 
| 19 | 18 | rpreccld 13087 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) | 
| 20 | 14, 16, 17, 19 | fvmptd 7023 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) = (1 / 𝑘)) | 
| 21 |  | nnrecre 12308 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) | 
| 22 | 20, 21 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) ∈ ℝ) | 
| 23 | 22 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐿‘𝑘) ∈ ℝ) | 
| 24 | 9 | a1i 11 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 ·
𝑛) + 1)))) | 
| 25 | 15 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘)) | 
| 26 | 25 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1)) | 
| 27 | 26 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1))) | 
| 28 |  | 2re 12340 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ | 
| 29 | 28 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) | 
| 30 |  | nnre 12273 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) | 
| 31 | 29, 30 | remulcld 11291 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℝ) | 
| 32 |  | 0le2 12368 | . . . . . . . . . . . . . 14
⊢ 0 ≤
2 | 
| 33 | 32 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 0 ≤
2) | 
| 34 | 18 | rpge0d 13081 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 0 ≤
𝑘) | 
| 35 | 29, 30, 33, 34 | mulge0d 11840 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 ≤ (2
· 𝑘)) | 
| 36 | 31, 35 | ge0p1rpd 13107 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 1) ∈
ℝ+) | 
| 37 | 36 | rpreccld 13087 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (1 / ((2
· 𝑘) + 1)) ∈
ℝ+) | 
| 38 | 24, 27, 17, 37 | fvmptd 7023 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (1 / ((2 · 𝑘) + 1))) | 
| 39 | 37 | rpred 13077 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 / ((2
· 𝑘) + 1)) ∈
ℝ) | 
| 40 | 38, 39 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ) | 
| 41 | 40 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) | 
| 42 |  | 1red 11262 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ∈
ℝ) | 
| 43 |  | 0le1 11786 | . . . . . . . . . . 11
⊢ 0 ≤
1 | 
| 44 | 43 | a1i 11 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 0 ≤
1) | 
| 45 | 31, 42 | readdcld 11290 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 1) ∈
ℝ) | 
| 46 |  | nncn 12274 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 47 | 46 | mullidd 11279 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (1
· 𝑘) = 𝑘) | 
| 48 |  | 1lt2 12437 | . . . . . . . . . . . . . . 15
⊢ 1 <
2 | 
| 49 | 48 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 1 <
2) | 
| 50 | 42, 29, 18, 49 | ltmul1dd 13132 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (1
· 𝑘) < (2
· 𝑘)) | 
| 51 | 47, 50 | eqbrtrrd 5167 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘)) | 
| 52 | 31 | ltp1d 12198 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) < ((2
· 𝑘) +
1)) | 
| 53 | 30, 31, 45, 51, 52 | lttrd 11422 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1)) | 
| 54 | 30, 45, 53 | ltled 11409 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1)) | 
| 55 | 18, 36, 42, 44, 54 | lediv2ad 13099 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 / ((2
· 𝑘) + 1)) ≤ (1 /
𝑘)) | 
| 56 | 55, 38, 20 | 3brtr4d 5175 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐿‘𝑘)) | 
| 57 | 56 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ≤ (𝐿‘𝑘)) | 
| 58 | 37 | rpge0d 13081 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ ((2 · 𝑘) +
1))) | 
| 59 | 58, 38 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 0 ≤
(𝐺‘𝑘)) | 
| 60 | 59 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 0 ≤ (𝐺‘𝑘)) | 
| 61 | 1, 2, 8, 13, 23, 41, 57, 60 | climsqz2 15678 | . . . . . 6
⊢ (⊤
→ 𝐺 ⇝
0) | 
| 62 |  | 1cnd 11256 | . . . . . 6
⊢ (⊤
→ 1 ∈ ℂ) | 
| 63 |  | stirlinglem1.2 | . . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2
· 𝑛) +
1)))) | 
| 64 | 10 | mptex 7243 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (1
− (1 / ((2 · 𝑛) + 1)))) ∈ V | 
| 65 | 63, 64 | eqeltri 2837 | . . . . . . 7
⊢ 𝐹 ∈ V | 
| 66 | 65 | a1i 11 | . . . . . 6
⊢ (⊤
→ 𝐹 ∈
V) | 
| 67 | 41 | recnd 11289 | . . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℂ) | 
| 68 | 63 | a1i 11 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2
· 𝑛) +
1))))) | 
| 69 | 27 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2
· 𝑘) +
1)))) | 
| 70 |  | 1cnd 11256 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ∈
ℂ) | 
| 71 |  | 2cnd 12344 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 2 ∈
ℂ) | 
| 72 | 71, 46 | mulcld 11281 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℂ) | 
| 73 | 72, 70 | addcld 11280 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 1) ∈
ℂ) | 
| 74 | 36 | rpne0d 13082 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((2
· 𝑘) + 1) ≠
0) | 
| 75 | 73, 74 | reccld 12036 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (1 / ((2
· 𝑘) + 1)) ∈
ℂ) | 
| 76 | 70, 75 | subcld 11620 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1
− (1 / ((2 · 𝑘) + 1))) ∈ ℂ) | 
| 77 | 68, 69, 17, 76 | fvmptd 7023 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (1 / ((2 · 𝑘) + 1)))) | 
| 78 | 38 | eqcomd 2743 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 / ((2
· 𝑘) + 1)) = (𝐺‘𝑘)) | 
| 79 | 78 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (1
− (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺‘𝑘))) | 
| 80 | 77, 79 | eqtrd 2777 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (𝐺‘𝑘))) | 
| 81 | 80 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) = (1 − (𝐺‘𝑘))) | 
| 82 | 1, 2, 61, 62, 66, 67, 81 | climsubc2 15675 | . . . . 5
⊢ (⊤
→ 𝐹 ⇝ (1 −
0)) | 
| 83 |  | 1m0e1 12387 | . . . . 5
⊢ (1
− 0) = 1 | 
| 84 | 82, 83 | breqtrdi 5184 | . . . 4
⊢ (⊤
→ 𝐹 ⇝
1) | 
| 85 | 62 | halfcld 12511 | . . . 4
⊢ (⊤
→ (1 / 2) ∈ ℂ) | 
| 86 |  | stirlinglem1.1 | . . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) | 
| 87 | 10 | mptex 7243 | . . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V | 
| 88 | 86, 87 | eqeltri 2837 | . . . . 5
⊢ 𝐻 ∈ V | 
| 89 | 88 | a1i 11 | . . . 4
⊢ (⊤
→ 𝐻 ∈
V) | 
| 90 | 77, 76 | eqeltrd 2841 | . . . . 5
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ) | 
| 91 | 90 | adantl 481 | . . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) | 
| 92 |  | nncn 12274 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 93 | 92 | sqcld 14184 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈
ℂ) | 
| 94 | 93 | mullidd 11279 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1
· (𝑛↑2)) =
(𝑛↑2)) | 
| 95 | 94 | eqcomd 2743 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2))) | 
| 96 |  | 2cnd 12344 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) | 
| 97 | 96, 92 | mulcld 11281 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) | 
| 98 |  | 1cnd 11256 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) | 
| 99 | 92, 97, 98 | adddid 11285 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1))) | 
| 100 | 92, 96, 92 | mul12d 11470 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛))) | 
| 101 | 92 | sqvald 14183 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛)) | 
| 102 | 101 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2)) | 
| 103 | 102 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· (𝑛 · 𝑛)) = (2 · (𝑛↑2))) | 
| 104 | 100, 103 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2))) | 
| 105 | 92 | mulridd 11278 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛) | 
| 106 | 104, 105 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛)) | 
| 107 |  | 2ne0 12370 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 | 
| 108 | 107 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 2 ≠
0) | 
| 109 | 92, 96, 108 | divcan2d 12045 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (2
· (𝑛 / 2)) = 𝑛) | 
| 110 | 109 | eqcomd 2743 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2))) | 
| 111 | 110 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((2
· (𝑛↑2)) +
𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2)))) | 
| 112 | 92 | halfcld 12511 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈
ℂ) | 
| 113 | 96, 93, 112 | adddid 11285 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (2
· ((𝑛↑2) +
(𝑛 / 2))) = ((2 ·
(𝑛↑2)) + (2 ·
(𝑛 / 2)))) | 
| 114 | 111, 113 | eqtr4d 2780 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((2
· (𝑛↑2)) +
𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2)))) | 
| 115 | 99, 106, 114 | 3eqtrd 2781 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2)))) | 
| 116 | 95, 115 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2))))) | 
| 117 | 93, 112 | addcld 11280 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ) | 
| 118 |  | nnrp 13046 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) | 
| 119 |  | 2z 12649 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ | 
| 120 | 119 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 2 ∈
ℤ) | 
| 121 | 118, 120 | rpexpcld 14286 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈
ℝ+) | 
| 122 | 118 | rphalfcld 13089 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈
ℝ+) | 
| 123 | 121, 122 | rpaddcld 13092 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈
ℝ+) | 
| 124 | 123 | rpne0d 13082 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0) | 
| 125 | 98, 96, 93, 117, 108, 124 | divmuldivd 12084 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((1 / 2)
· ((𝑛↑2) /
((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2))))) | 
| 126 | 93, 112 | pncand 11621 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2)) | 
| 127 | 126 | eqcomd 2743 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2))) | 
| 128 | 127 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2)))) | 
| 129 | 117, 112,
117, 124 | divsubdird 12082 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))) | 
| 130 | 117, 124 | dividd 12041 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1) | 
| 131 | 130 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))) | 
| 132 | 128, 129,
131 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))) | 
| 133 |  | nnne0 12300 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) | 
| 134 | 96, 92, 133 | divcld 12043 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (2 /
𝑛) ∈
ℂ) | 
| 135 | 96, 92, 108, 133 | divne0d 12059 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (2 /
𝑛) ≠ 0) | 
| 136 | 112, 117,
134, 124, 135 | divcan5rd 12070 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) | 
| 137 | 92, 96, 133, 108 | divcan6d 12062 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1) | 
| 138 | 93, 112, 134 | adddird 11286 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛)))) | 
| 139 | 93, 96, 92, 133 | div12d 12079 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛))) | 
| 140 |  | 1e2m1 12393 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 = (2
− 1) | 
| 141 | 140 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛↑1) = (𝑛↑(2 − 1)) | 
| 142 | 92 | exp1d 14181 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛) | 
| 143 | 92, 133, 120 | expm1d 14196 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛)) | 
| 144 | 141, 142,
143 | 3eqtr3a 2801 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛)) | 
| 145 | 144 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛) | 
| 146 | 145 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (2
· ((𝑛↑2) /
𝑛)) = (2 · 𝑛)) | 
| 147 | 139, 146 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛)) | 
| 148 | 147, 137 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1)) | 
| 149 | 138, 148 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1)) | 
| 150 | 137, 149 | oveq12d 7449 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1))) | 
| 151 | 136, 150 | eqtr3d 2779 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1))) | 
| 152 | 151 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1
− ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1)))) | 
| 153 | 132, 152 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1)))) | 
| 154 | 153 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((1 / 2)
· ((𝑛↑2) /
((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1
− (1 / ((2 · 𝑛) + 1))))) | 
| 155 | 116, 125,
154 | 3eqtr2d 2783 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 /
((2 · 𝑛) +
1))))) | 
| 156 | 155 | mpteq2ia 5245 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1
− (1 / ((2 · 𝑛) + 1))))) | 
| 157 | 86, 156 | eqtri 2765 | . . . . . . . 8
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1
− (1 / ((2 · 𝑛) + 1))))) | 
| 158 | 157 | a1i 11 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1
− (1 / ((2 · 𝑛) + 1)))))) | 
| 159 | 69 | oveq2d 7447 | . . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 /
((2 · 𝑛) + 1)))) =
((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1))))) | 
| 160 | 70 | halfcld 12511 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (1 / 2)
∈ ℂ) | 
| 161 | 160, 76 | mulcld 11281 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → ((1 / 2)
· (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ) | 
| 162 | 158, 159,
17, 161 | fvmptd 7023 | . . . . . 6
⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (1 − (1 / ((2
· 𝑘) +
1))))) | 
| 163 | 77 | oveq2d 7447 | . . . . . 6
⊢ (𝑘 ∈ ℕ → ((1 / 2)
· (𝐹‘𝑘)) = ((1 / 2) · (1
− (1 / ((2 · 𝑘) + 1))))) | 
| 164 | 162, 163 | eqtr4d 2780 | . . . . 5
⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘))) | 
| 165 | 164 | adantl 481 | . . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘))) | 
| 166 | 1, 2, 84, 85, 89, 91, 165 | climmulc2 15673 | . . 3
⊢ (⊤
→ 𝐻 ⇝ ((1 / 2)
· 1)) | 
| 167 | 166 | mptru 1547 | . 2
⊢ 𝐻 ⇝ ((1 / 2) ·
1) | 
| 168 |  | halfcn 12481 | . . 3
⊢ (1 / 2)
∈ ℂ | 
| 169 | 168 | mulridi 11265 | . 2
⊢ ((1 / 2)
· 1) = (1 / 2) | 
| 170 | 167, 169 | breqtri 5168 | 1
⊢ 𝐻 ⇝ (1 /
2) |