wallispilem5

Description: The sequence H converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017)

	Ref	Expression
Hypotheses	wallispilem5.1	$⊢ F = (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))$
	wallispilem5.2	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
	wallispilem5.3	$⊢ G = (n \in ℕ ⟼ \frac{I (2 n)}{I (2 n + 1)})$
	wallispilem5.4	$⊢ H = (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}))$
	wallispilem5.5	$⊢ L = (n \in ℕ ⟼ \frac{2 n + 1}{2 n})$
Assertion	wallispilem5	$⊢ H ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		wallispilem5.1	$⊢ F = (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))$
2		wallispilem5.2	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
3		wallispilem5.3	$⊢ G = (n \in ℕ ⟼ \frac{I (2 n)}{I (2 n + 1)})$
4		wallispilem5.4	$⊢ H = (n \in ℕ ⟼ (\frac{π}{2}) (\frac{1}{seq 1 (\times F) (n)}))$
5		wallispilem5.5	$⊢ L = (n \in ℕ ⟼ \frac{2 n + 1}{2 n})$
6	1 2 3 4	wallispilem4	$⊢ G = H$
7		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
8		1zzd	$⊢ ⊤ \to 1 \in ℤ$
9		2cnd	$⊢ ⊤ \to 2 \in ℂ$
10		2ne0	$⊢ 2 \neq 0$
11	10	a1i	$⊢ ⊤ \to 2 \neq 0$
12		1cnd	$⊢ ⊤ \to 1 \in ℂ$
13	5 9 11 12	clim1fr1	$⊢ ⊤ \to L ⇝ 1$
14		nnex	$⊢ ℕ \in V$
15	14	mptex	$⊢ (n \in ℕ ⟼ \frac{I (2 n)}{I (2 n + 1)}) \in V$
16	3 15	eqeltri	$⊢ G \in V$
17	16	a1i	$⊢ ⊤ \to G \in V$
18		2nn0	$⊢ 2 \in ℕ_{0}$
19	18	a1i	$⊢ n \in ℕ \to 2 \in ℕ_{0}$
20		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
21	19 20	nn0mulcld	$⊢ n \in ℕ \to 2 n \in ℕ_{0}$
22		1nn0	$⊢ 1 \in ℕ_{0}$
23	22	a1i	$⊢ n \in ℕ \to 1 \in ℕ_{0}$
24	21 23	nn0addcld	$⊢ n \in ℕ \to 2 n + 1 \in ℕ_{0}$
25	24	nn0red	$⊢ n \in ℕ \to 2 n + 1 \in ℝ$
26	21	nn0red	$⊢ n \in ℕ \to 2 n \in ℝ$
27		2cnd	$⊢ n \in ℕ \to 2 \in ℂ$
28		nncn	$⊢ n \in ℕ \to n \in ℂ$
29	10	a1i	$⊢ n \in ℕ \to 2 \neq 0$
30		nnne0	$⊢ n \in ℕ \to n \neq 0$
31	27 28 29 30	mulne0d	$⊢ n \in ℕ \to 2 n \neq 0$
32	25 26 31	redivcld	$⊢ n \in ℕ \to \frac{2 n + 1}{2 n} \in ℝ$
33	5 32	fmpti	$⊢ L : ℕ ⟶ ℝ$
34	33	a1i	$⊢ ⊤ \to L : ℕ ⟶ ℝ$
35	34	ffvelcdmda	$⊢ (⊤ \land k \in ℕ) \to L (k) \in ℝ$
36	2	wallispilem3	$⊢ 2 n \in ℕ_{0} \to I (2 n) \in ℝ^{+}$
37	21 36	syl	$⊢ n \in ℕ \to I (2 n) \in ℝ^{+}$
38	37	rpred	$⊢ n \in ℕ \to I (2 n) \in ℝ$
39	2	wallispilem3	$⊢ 2 n + 1 \in ℕ_{0} \to I (2 n + 1) \in ℝ^{+}$
40	24 39	syl	$⊢ n \in ℕ \to I (2 n + 1) \in ℝ^{+}$
41	38 40	rerpdivcld	$⊢ n \in ℕ \to \frac{I (2 n)}{I (2 n + 1)} \in ℝ$
42	3 41	fmpti	$⊢ G : ℕ ⟶ ℝ$
43	42	a1i	$⊢ ⊤ \to G : ℕ ⟶ ℝ$
44	43	ffvelcdmda	$⊢ (⊤ \land k \in ℕ) \to G (k) \in ℝ$
45	18	a1i	$⊢ k \in ℕ \to 2 \in ℕ_{0}$
46		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
47	45 46	nn0mulcld	$⊢ k \in ℕ \to 2 k \in ℕ_{0}$
48	2	wallispilem3	$⊢ 2 k \in ℕ_{0} \to I (2 k) \in ℝ^{+}$
49	47 48	syl	$⊢ k \in ℕ \to I (2 k) \in ℝ^{+}$
50	49	rpred	$⊢ k \in ℕ \to I (2 k) \in ℝ$
51		2nn	$⊢ 2 \in ℕ$
52	51	a1i	$⊢ k \in ℕ \to 2 \in ℕ$
53		id	$⊢ k \in ℕ \to k \in ℕ$
54	52 53	nnmulcld	$⊢ k \in ℕ \to 2 k \in ℕ$
55		nnm1nn0	$⊢ 2 k \in ℕ \to 2 k - 1 \in ℕ_{0}$
56	54 55	syl	$⊢ k \in ℕ \to 2 k - 1 \in ℕ_{0}$
57	2	wallispilem3	$⊢ 2 k - 1 \in ℕ_{0} \to I (2 k - 1) \in ℝ^{+}$
58	56 57	syl	$⊢ k \in ℕ \to I (2 k - 1) \in ℝ^{+}$
59	58	rpred	$⊢ k \in ℕ \to I (2 k - 1) \in ℝ$
60	22	a1i	$⊢ k \in ℕ \to 1 \in ℕ_{0}$
61	47 60	nn0addcld	$⊢ k \in ℕ \to 2 k + 1 \in ℕ_{0}$
62	2	wallispilem3	$⊢ 2 k + 1 \in ℕ_{0} \to I (2 k + 1) \in ℝ^{+}$
63	61 62	syl	$⊢ k \in ℕ \to I (2 k + 1) \in ℝ^{+}$
64		2cnd	$⊢ k \in ℕ \to 2 \in ℂ$
65		nncn	$⊢ k \in ℕ \to k \in ℂ$
66	64 65	mulcld	$⊢ k \in ℕ \to 2 k \in ℂ$
67		1cnd	$⊢ k \in ℕ \to 1 \in ℂ$
68	66 67	npcand	$⊢ k \in ℕ \to 2 k - 1 + 1 = 2 k$
69	68	fveq2d	$⊢ k \in ℕ \to I (2 k - 1 + 1) = I (2 k)$
70	2 56	wallispilem1	$⊢ k \in ℕ \to I (2 k - 1 + 1) \leq I (2 k - 1)$
71	69 70	eqbrtrrd	$⊢ k \in ℕ \to I (2 k) \leq I (2 k - 1)$
72	50 59 63 71	lediv1dd	$⊢ k \in ℕ \to \frac{I (2 k)}{I (2 k + 1)} \leq \frac{I (2 k - 1)}{I (2 k + 1)}$
73	66 67	addcld	$⊢ k \in ℕ \to 2 k + 1 \in ℂ$
74	10	a1i	$⊢ k \in ℕ \to 2 \neq 0$
75		nnne0	$⊢ k \in ℕ \to k \neq 0$
76	64 65 74 75	mulne0d	$⊢ k \in ℕ \to 2 k \neq 0$
77	73 66 76	divcld	$⊢ k \in ℕ \to \frac{2 k + 1}{2 k} \in ℂ$
78	63	rpcnd	$⊢ k \in ℕ \to I (2 k + 1) \in ℂ$
79	63	rpne0d	$⊢ k \in ℕ \to I (2 k + 1) \neq 0$
80	77 78 79	divcan4d	$⊢ k \in ℕ \to \frac{(\frac{2 k + 1}{2 k}) I (2 k + 1)}{I (2 k + 1)} = \frac{2 k + 1}{2 k}$
81		2re	$⊢ 2 \in ℝ$
82	81	a1i	$⊢ k \in ℕ \to 2 \in ℝ$
83		nnre	$⊢ k \in ℕ \to k \in ℝ$
84	82 83	remulcld	$⊢ k \in ℕ \to 2 k \in ℝ$
85		1red	$⊢ k \in ℕ \to 1 \in ℝ$
86	84 85	readdcld	$⊢ k \in ℕ \to 2 k + 1 \in ℝ$
87	45	nn0ge0d	$⊢ k \in ℕ \to 0 \leq 2$
88		nnge1	$⊢ k \in ℕ \to 1 \leq k$
89	82 83 87 88	lemulge11d	$⊢ k \in ℕ \to 2 \leq 2 k$
90	84	ltp1d	$⊢ k \in ℕ \to 2 k < 2 k + 1$
91	82 84 86 89 90	lelttrd	$⊢ k \in ℕ \to 2 < 2 k + 1$
92	82 86 91	ltled	$⊢ k \in ℕ \to 2 \leq 2 k + 1$
93	45	nn0zd	$⊢ k \in ℕ \to 2 \in ℤ$
94	61	nn0zd	$⊢ k \in ℕ \to 2 k + 1 \in ℤ$
95		eluz	$⊢ (2 \in ℤ \land 2 k + 1 \in ℤ) \to (2 k + 1 \in ℤ_{\geq 2} \leftrightarrow 2 \leq 2 k + 1)$
96	93 94 95	syl2anc	$⊢ k \in ℕ \to (2 k + 1 \in ℤ_{\geq 2} \leftrightarrow 2 \leq 2 k + 1)$
97	92 96	mpbird	$⊢ k \in ℕ \to 2 k + 1 \in ℤ_{\geq 2}$
98	2 97	itgsinexp	$⊢ k \in ℕ \to I (2 k + 1) = (\frac{2 k + 1 - 1}{2 k + 1}) I (2 k + 1 - 2)$
99	66 67	pncand	$⊢ k \in ℕ \to 2 k + 1 - 1 = 2 k$
100	99	oveq1d	$⊢ k \in ℕ \to \frac{2 k + 1 - 1}{2 k + 1} = \frac{2 k}{2 k + 1}$
101		1e2m1	$⊢ 1 = 2 - 1$
102	101	a1i	$⊢ k \in ℕ \to 1 = 2 - 1$
103	102	oveq2d	$⊢ k \in ℕ \to 2 k - 1 = 2 k - (2 - 1)$
104	66 64 67	subsub3d	$⊢ k \in ℕ \to 2 k - (2 - 1) = 2 k + 1 - 2$
105	103 104	eqtr2d	$⊢ k \in ℕ \to 2 k + 1 - 2 = 2 k - 1$
106	105	fveq2d	$⊢ k \in ℕ \to I (2 k + 1 - 2) = I (2 k - 1)$
107	100 106	oveq12d	$⊢ k \in ℕ \to (\frac{2 k + 1 - 1}{2 k + 1}) I (2 k + 1 - 2) = (\frac{2 k}{2 k + 1}) I (2 k - 1)$
108	98 107	eqtrd	$⊢ k \in ℕ \to I (2 k + 1) = (\frac{2 k}{2 k + 1}) I (2 k - 1)$
109	108	oveq2d	$⊢ k \in ℕ \to (\frac{2 k + 1}{2 k}) I (2 k + 1) = (\frac{2 k + 1}{2 k}) (\frac{2 k}{2 k + 1}) I (2 k - 1)$
110	54	peano2nnd	$⊢ k \in ℕ \to 2 k + 1 \in ℕ$
111	110	nnne0d	$⊢ k \in ℕ \to 2 k + 1 \neq 0$
112	66 73 111	divcld	$⊢ k \in ℕ \to \frac{2 k}{2 k + 1} \in ℂ$
113	58	rpcnd	$⊢ k \in ℕ \to I (2 k - 1) \in ℂ$
114	77 112 113	mulassd	$⊢ k \in ℕ \to (\frac{2 k + 1}{2 k}) (\frac{2 k}{2 k + 1}) I (2 k - 1) = (\frac{2 k + 1}{2 k}) (\frac{2 k}{2 k + 1}) I (2 k - 1)$
115	73 66 111 76	divcan6d	$⊢ k \in ℕ \to (\frac{2 k + 1}{2 k}) (\frac{2 k}{2 k + 1}) = 1$
116	115	oveq1d	$⊢ k \in ℕ \to (\frac{2 k + 1}{2 k}) (\frac{2 k}{2 k + 1}) I (2 k - 1) = 1 I (2 k - 1)$
117	113	mullidd	$⊢ k \in ℕ \to 1 I (2 k - 1) = I (2 k - 1)$
118	116 117	eqtrd	$⊢ k \in ℕ \to (\frac{2 k + 1}{2 k}) (\frac{2 k}{2 k + 1}) I (2 k - 1) = I (2 k - 1)$
119	109 114 118	3eqtr2d	$⊢ k \in ℕ \to (\frac{2 k + 1}{2 k}) I (2 k + 1) = I (2 k - 1)$
120	119	oveq1d	$⊢ k \in ℕ \to \frac{(\frac{2 k + 1}{2 k}) I (2 k + 1)}{I (2 k + 1)} = \frac{I (2 k - 1)}{I (2 k + 1)}$
121	80 120	eqtr3d	$⊢ k \in ℕ \to \frac{2 k + 1}{2 k} = \frac{I (2 k - 1)}{I (2 k + 1)}$
122	72 121	breqtrrd	$⊢ k \in ℕ \to \frac{I (2 k)}{I (2 k + 1)} \leq \frac{2 k + 1}{2 k}$
123	49 63	rpdivcld	$⊢ k \in ℕ \to \frac{I (2 k)}{I (2 k + 1)} \in ℝ^{+}$
124		nfcv	$⊢ \underline{Ⅎ} n k$
125		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
126	2 125	nfcxfr	$⊢ \underline{Ⅎ} n I$
127		nfcv	$⊢ \underline{Ⅎ} n 2 k$
128	126 127	nffv	$⊢ \underline{Ⅎ} n I (2 k)$
129		nfcv	$⊢ \underline{Ⅎ} n \div$
130		nfcv	$⊢ \underline{Ⅎ} n (2 k + 1)$
131	126 130	nffv	$⊢ \underline{Ⅎ} n I (2 k + 1)$
132	128 129 131	nfov	$⊢ \underline{Ⅎ} n (\frac{I (2 k)}{I (2 k + 1)})$
133		oveq2	$⊢ n = k \to 2 n = 2 k$
134	133	fveq2d	$⊢ n = k \to I (2 n) = I (2 k)$
135	133	fvoveq1d	$⊢ n = k \to I (2 n + 1) = I (2 k + 1)$
136	134 135	oveq12d	$⊢ n = k \to \frac{I (2 n)}{I (2 n + 1)} = \frac{I (2 k)}{I (2 k + 1)}$
137	124 132 136 3	fvmptf	$⊢ (k \in ℕ \land \frac{I (2 k)}{I (2 k + 1)} \in ℝ^{+}) \to G (k) = \frac{I (2 k)}{I (2 k + 1)}$
138	123 137	mpdan	$⊢ k \in ℕ \to G (k) = \frac{I (2 k)}{I (2 k + 1)}$
139	5	a1i	$⊢ k \in ℕ \to L = (n \in ℕ ⟼ \frac{2 n + 1}{2 n})$
140		simpr	$⊢ (k \in ℕ \land n = k) \to n = k$
141	140	oveq2d	$⊢ (k \in ℕ \land n = k) \to 2 n = 2 k$
142	141	oveq1d	$⊢ (k \in ℕ \land n = k) \to 2 n + 1 = 2 k + 1$
143	142 141	oveq12d	$⊢ (k \in ℕ \land n = k) \to \frac{2 n + 1}{2 n} = \frac{2 k + 1}{2 k}$
144	139 143 53 77	fvmptd	$⊢ k \in ℕ \to L (k) = \frac{2 k + 1}{2 k}$
145	122 138 144	3brtr4d	$⊢ k \in ℕ \to G (k) \leq L (k)$
146	145	adantl	$⊢ (⊤ \land k \in ℕ) \to G (k) \leq L (k)$
147	78 79	dividd	$⊢ k \in ℕ \to \frac{I (2 k + 1)}{I (2 k + 1)} = 1$
148	63	rpred	$⊢ k \in ℕ \to I (2 k + 1) \in ℝ$
149	2 47	wallispilem1	$⊢ k \in ℕ \to I (2 k + 1) \leq I (2 k)$
150	148 50 63 149	lediv1dd	$⊢ k \in ℕ \to \frac{I (2 k + 1)}{I (2 k + 1)} \leq \frac{I (2 k)}{I (2 k + 1)}$
151	147 150	eqbrtrrd	$⊢ k \in ℕ \to 1 \leq \frac{I (2 k)}{I (2 k + 1)}$
152	151 138	breqtrrd	$⊢ k \in ℕ \to 1 \leq G (k)$
153	152	adantl	$⊢ (⊤ \land k \in ℕ) \to 1 \leq G (k)$
154	7 8 13 17 35 44 146 153	climsqz2	$⊢ ⊤ \to G ⇝ 1$
155	154	mptru	$⊢ G ⇝ 1$
156	6 155	eqbrtrri	$⊢ H ⇝ 1$

Metamath Proof Explorer

Theorem wallispilem5

Proof