Metamath Proof Explorer

Theorem stirlinglem1

Description: A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses stirlinglem1.1 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
stirlinglem1.2 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
stirlinglem1.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
stirlinglem1.4 ⊢ 𝐿 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
Assertion stirlinglem1 𝐻 ⇝ ( 1 / 2 )

Proof

Step Hyp Ref Expression
1 stirlinglem1.1 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) )
2 stirlinglem1.2 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
3 stirlinglem1.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
4 stirlinglem1.4 ⊢ 𝐿 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
7 ax-1cn ⊢ 1 ∈ ℂ
8 divcnv ⊢ ( 1 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
9 7 8 ax-mp ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0
10 4 9 eqbrtri ⊢ 𝐿 ⇝ 0
11 10 a1i ⊢ ( ⊤ → 𝐿 ⇝ 0 )
12 nnex ⊢ ℕ ∈ V
13 12 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ V
14 3 13 eqeltri ⊢ 𝐺 ∈ V
15 14 a1i ⊢ ( ⊤ → 𝐺 ∈ V )
16 4 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐿 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) )
17 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → 𝑛 = 𝑘 )
18 17 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
19 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
20 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
21 20 rpreccld ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
22 16 18 19 21 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐿 ‘ 𝑘 ) = ( 1 / 𝑘 ) )
23 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
24 22 23 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐿 ‘ 𝑘 ) ∈ ℝ )
25 24 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐿 ‘ 𝑘 ) ∈ ℝ )
26 3 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
27 17 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
28 27 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) )
29 28 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) )
30 2re ⊢ 2 ∈ ℝ
31 30 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ )
32 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
33 31 32 remulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ )
34 0le2 ⊢ 0 ≤ 2
35 34 a1i ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 2 )
36 20 rpge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 𝑘 )
37 31 32 35 36 mulge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 2 · 𝑘 ) )
38 33 37 ge0p1rpd ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℝ+ )
39 38 rpreccld ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ+ )
40 26 29 19 39 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) )
41 39 rpred ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ )
42 40 41 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
43 42 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
44 1red ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℝ )
45 0le1 ⊢ 0 ≤ 1
46 45 a1i ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 1 )
47 33 44 readdcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℝ )
48 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
49 48 mulid2d ⊢ ( 𝑘 ∈ ℕ → ( 1 · 𝑘 ) = 𝑘 )
50 1lt2 ⊢ 1 < 2
51 50 a1i ⊢ ( 𝑘 ∈ ℕ → 1 < 2 )
52 44 31 20 51 ltmul1dd ⊢ ( 𝑘 ∈ ℕ → ( 1 · 𝑘 ) < ( 2 · 𝑘 ) )
53 49 52 eqbrtrrd ⊢ ( 𝑘 ∈ ℕ → 𝑘 < ( 2 · 𝑘 ) )
54 33 ltp1d ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) < ( ( 2 · 𝑘 ) + 1 ) )
55 32 33 47 53 54 lttrd ⊢ ( 𝑘 ∈ ℕ → 𝑘 < ( ( 2 · 𝑘 ) + 1 ) )
56 32 47 55 ltled ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≤ ( ( 2 · 𝑘 ) + 1 ) )
57 20 38 44 46 56 lediv2ad ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ≤ ( 1 / 𝑘 ) )
58 57 40 22 3brtr4d ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐿 ‘ 𝑘 ) )
59 58 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐿 ‘ 𝑘 ) )
60 39 rpge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) )
61 60 40 breqtrrd ⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 𝐺 ‘ 𝑘 ) )
62 61 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐺 ‘ 𝑘 ) )
63 5 6 11 15 25 43 59 62 climsqz2 ⊢ ( ⊤ → 𝐺 ⇝ 0 )
64 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
65 12 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ V
66 2 65 eqeltri ⊢ 𝐹 ∈ V
67 66 a1i ⊢ ( ⊤ → 𝐹 ∈ V )
68 43 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
69 2 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐹 = ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
70 29 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) )
71 1cnd ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℂ )
72 2cnd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
73 72 48 mulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℂ )
74 73 71 addcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
75 38 rpne0d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ≠ 0 )
76 74 75 reccld ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
77 71 76 subcld ⊢ ( 𝑘 ∈ ℕ → ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) ∈ ℂ )
78 69 70 19 77 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) = ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) )
79 40 eqcomd ⊢ ( 𝑘 ∈ ℕ → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) = ( 𝐺 ‘ 𝑘 ) )
80 79 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 1 − ( 𝐺 ‘ 𝑘 ) ) )
81 78 80 eqtrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) = ( 1 − ( 𝐺 ‘ 𝑘 ) ) )
82 81 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 1 − ( 𝐺 ‘ 𝑘 ) ) )
83 5 6 63 64 67 68 82 climsubc2 ⊢ ( ⊤ → 𝐹 ⇝ ( 1 − 0 ) )
84 1m0e1 ⊢ ( 1 − 0 ) = 1
85 83 84 breqtrdi ⊢ ( ⊤ → 𝐹 ⇝ 1 )
86 64 halfcld ⊢ ( ⊤ → ( 1 / 2 ) ∈ ℂ )
87 12 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ V
88 1 87 eqeltri ⊢ 𝐻 ∈ V
89 88 a1i ⊢ ( ⊤ → 𝐻 ∈ V )
90 78 77 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
91 90 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
92 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
93 92 sqcld ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 2 ) ∈ ℂ )
94 93 mulid2d ⊢ ( 𝑛 ∈ ℕ → ( 1 · ( 𝑛 ↑ 2 ) ) = ( 𝑛 ↑ 2 ) )
95 94 eqcomd ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 2 ) = ( 1 · ( 𝑛 ↑ 2 ) ) )
96 2cnd ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
97 96 92 mulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℂ )
98 1cnd ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℂ )
99 92 97 98 adddid ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) = ( ( 𝑛 · ( 2 · 𝑛 ) ) + ( 𝑛 · 1 ) ) )
100 92 96 92 mul12d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( 2 · 𝑛 ) ) = ( 2 · ( 𝑛 · 𝑛 ) ) )
101 92 sqvald ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 2 ) = ( 𝑛 · 𝑛 ) )
102 101 eqcomd ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · 𝑛 ) = ( 𝑛 ↑ 2 ) )
103 102 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( 𝑛 · 𝑛 ) ) = ( 2 · ( 𝑛 ↑ 2 ) ) )
104 100 103 eqtrd ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( 2 · 𝑛 ) ) = ( 2 · ( 𝑛 ↑ 2 ) ) )
105 92 mulid1d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · 1 ) = 𝑛 )
106 104 105 oveq12d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 · ( 2 · 𝑛 ) ) + ( 𝑛 · 1 ) ) = ( ( 2 · ( 𝑛 ↑ 2 ) ) + 𝑛 ) )
107 2ne0 ⊢ 2 ≠ 0
108 107 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ≠ 0 )
109 92 96 108 divcan2d ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( 𝑛 / 2 ) ) = 𝑛 )
110 109 eqcomd ⊢ ( 𝑛 ∈ ℕ → 𝑛 = ( 2 · ( 𝑛 / 2 ) ) )
111 110 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · ( 𝑛 ↑ 2 ) ) + 𝑛 ) = ( ( 2 · ( 𝑛 ↑ 2 ) ) + ( 2 · ( 𝑛 / 2 ) ) ) )
112 92 halfcld ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / 2 ) ∈ ℂ )
113 96 93 112 adddid ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = ( ( 2 · ( 𝑛 ↑ 2 ) ) + ( 2 · ( 𝑛 / 2 ) ) ) )
114 111 113 eqtr4d ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · ( 𝑛 ↑ 2 ) ) + 𝑛 ) = ( 2 · ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) )
115 99 106 114 3eqtrd ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) = ( 2 · ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) )
116 95 115 oveq12d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 · ( 𝑛 ↑ 2 ) ) / ( 2 · ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) )
117 93 112 addcld ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ∈ ℂ )
118 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
119 2z ⊢ 2 ∈ ℤ
120 119 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℤ )
121 118 120 rpexpcld ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 2 ) ∈ ℝ+ )
122 118 rphalfcld ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / 2 ) ∈ ℝ+ )
123 121 122 rpaddcld ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ∈ ℝ+ )
124 123 rpne0d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ≠ 0 )
125 98 96 93 117 108 124 divmuldivd ⊢ ( 𝑛 ∈ ℕ → ( ( 1 / 2 ) · ( ( 𝑛 ↑ 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) = ( ( 1 · ( 𝑛 ↑ 2 ) ) / ( 2 · ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) )
126 93 112 pncand ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) − ( 𝑛 / 2 ) ) = ( 𝑛 ↑ 2 ) )
127 126 eqcomd ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 2 ) = ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) − ( 𝑛 / 2 ) ) )
128 127 oveq1d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = ( ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) − ( 𝑛 / 2 ) ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) )
129 117 112 117 124 divsubdird ⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) − ( 𝑛 / 2 ) ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = ( ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) − ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) )
130 117 124 dividd ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = 1 )
131 130 oveq1d ⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) − ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) = ( 1 − ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) )
132 128 129 131 3eqtrd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = ( 1 − ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) )
133 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
134 96 92 133 divcld ⊢ ( 𝑛 ∈ ℕ → ( 2 / 𝑛 ) ∈ ℂ )
135 96 92 108 133 divne0d ⊢ ( 𝑛 ∈ ℕ → ( 2 / 𝑛 ) ≠ 0 )
136 112 117 134 124 135 divcan5rd ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 / 2 ) · ( 2 / 𝑛 ) ) / ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) · ( 2 / 𝑛 ) ) ) = ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) )
137 92 96 133 108 divcan6d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / 2 ) · ( 2 / 𝑛 ) ) = 1 )
138 93 112 134 adddird ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) · ( 2 / 𝑛 ) ) = ( ( ( 𝑛 ↑ 2 ) · ( 2 / 𝑛 ) ) + ( ( 𝑛 / 2 ) · ( 2 / 𝑛 ) ) ) )
139 93 96 92 133 div12d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) · ( 2 / 𝑛 ) ) = ( 2 · ( ( 𝑛 ↑ 2 ) / 𝑛 ) ) )
140 1e2m1 ⊢ 1 = ( 2 − 1 )
141 140 oveq2i ⊢ ( 𝑛 ↑ 1 ) = ( 𝑛 ↑ ( 2 − 1 ) )
142 92 exp1d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 1 ) = 𝑛 )
143 92 133 120 expm1d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ ( 2 − 1 ) ) = ( ( 𝑛 ↑ 2 ) / 𝑛 ) )
144 141 142 143 3eqtr3a ⊢ ( 𝑛 ∈ ℕ → 𝑛 = ( ( 𝑛 ↑ 2 ) / 𝑛 ) )
145 144 eqcomd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / 𝑛 ) = 𝑛 )
146 145 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( 2 · ( ( 𝑛 ↑ 2 ) / 𝑛 ) ) = ( 2 · 𝑛 ) )
147 139 146 eqtrd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) · ( 2 / 𝑛 ) ) = ( 2 · 𝑛 ) )
148 147 137 oveq12d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ↑ 2 ) · ( 2 / 𝑛 ) ) + ( ( 𝑛 / 2 ) · ( 2 / 𝑛 ) ) ) = ( ( 2 · 𝑛 ) + 1 ) )
149 138 148 eqtrd ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) · ( 2 / 𝑛 ) ) = ( ( 2 · 𝑛 ) + 1 ) )
150 137 149 oveq12d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝑛 / 2 ) · ( 2 / 𝑛 ) ) / ( ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) · ( 2 / 𝑛 ) ) ) = ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
151 136 150 eqtr3d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
152 151 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( 1 − ( ( 𝑛 / 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) = ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
153 132 152 eqtrd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) = ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
154 153 oveq2d ⊢ ( 𝑛 ∈ ℕ → ( ( 1 / 2 ) · ( ( 𝑛 ↑ 2 ) / ( ( 𝑛 ↑ 2 ) + ( 𝑛 / 2 ) ) ) ) = ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
155 116 125 154 3eqtr2d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
156 155 mpteq2ia ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
157 1 156 eqtri ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
158 157 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
159 70 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
160 71 halfcld ⊢ ( 𝑘 ∈ ℕ → ( 1 / 2 ) ∈ ℂ )
161 160 77 mulcld ⊢ ( 𝑘 ∈ ℕ → ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ∈ ℂ )
162 158 159 19 161 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐻 ‘ 𝑘 ) = ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
163 78 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( 1 / 2 ) · ( 𝐹 ‘ 𝑘 ) ) = ( ( 1 / 2 ) · ( 1 − ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
164 162 163 eqtr4d ⊢ ( 𝑘 ∈ ℕ → ( 𝐻 ‘ 𝑘 ) = ( ( 1 / 2 ) · ( 𝐹 ‘ 𝑘 ) ) )
165 164 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( ( 1 / 2 ) · ( 𝐹 ‘ 𝑘 ) ) )
166 5 6 85 86 89 91 165 climmulc2 ⊢ ( ⊤ → 𝐻 ⇝ ( ( 1 / 2 ) · 1 ) )
167 166 mptru ⊢ 𝐻 ⇝ ( ( 1 / 2 ) · 1 )
168 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
169 168 mulid1i ⊢ ( ( 1 / 2 ) · 1 ) = ( 1 / 2 )
170 167 169 breqtri ⊢ 𝐻 ⇝ ( 1 / 2 )