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	mullidd	⊢ ( 𝑘 ∈ ℕ → ( 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	mullidd	⊢ ( 𝑛 ∈ ℕ → ( 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	mulridd	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · 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	mulridi	⊢ ( ( 1 / 2 ) · 1 ) = ( 1 / 2 )
170	167 169	breqtri	⊢ 𝐻 ⇝ ( 1 / 2 )