Theorem wallispi 47174

Description: Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

Ref	Expression
wallispi.1	⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
wallispi.2	⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))

Assertion

Ref	Expression
wallispi	⊢ 𝑊 ⇝ (π / 2)

Distinct variable groups:   𝑘,𝑛   𝑛,𝐹

Allowed substitution hints:   𝐹(𝑘)   𝑊(𝑘, 𝑛)

Proof of Theorem wallispi

Dummy variables 𝑗 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 13008	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12731	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		wallispi.1	. . . . . . . 8 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (((𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘(2 · 𝑛)) / ((𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ (((𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘(2 · 𝑛)) / ((𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)‘((2 · 𝑛) + 1))))
6		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
8	3, 4, 5, 6, 7	wallispilem5 47173	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
9	8	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10		2cnd 12425	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℂ)
11		picn 26791	. . . . . . . 8 ⊢ π ∈ ℂ
12	11	a1i 11	. . . . . . 7 ⊢ (⊤ → π ∈ ℂ)
13		pire 26789	. . . . . . . . 9 ⊢ π ∈ ℝ
14		pipos 26793	. . . . . . . . 9 ⊢ 0 < π
15	13, 14	gt0ne0ii 11856	. . . . . . . 8 ⊢ π ≠ 0
16	15	a1i 11	. . . . . . 7 ⊢ (⊤ → π ≠ 0)
17	10, 12, 16	divcld 12097	. . . . . 6 ⊢ (⊤ → (2 / π) ∈ ℂ)
18		nnex 12345	. . . . . . . 8 ⊢ ℕ ∈ V
19	18	mptex 7230	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
20	19	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
21	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → π ∈ ℂ)
22	21	halfcld 12595	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23		elnnuz 13009	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ≥‘1))
24	23	biimpi 219	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ≥‘1))
25		oveq2 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
26	25	oveq1d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
27	25, 26	oveq12d 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
28	25	oveq1d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
29	25, 28	oveq12d 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
30	27, 29	oveq12d 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
31		elfznn 13691	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
32		2cnd 12425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℂ)
33		nncn 12347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
34	32, 33	mulcld 11333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
35		1cnd 11306	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℂ)
36	34, 35	subcld 11673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
37		1red 11313	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ)
38		1t1e1 12508	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 · 1) = 1
39	37, 37	remulcld 11343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
40		2re 12421	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ)
42	41, 37	remulcld 11343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
43		nnre 12346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
44	41, 43	remulcld 11343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
45		1rp 13128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ+
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ+)
47		1lt2 12519	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 < 2
48	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 < 2)
49	37, 41, 46, 48	ltmul1dd 13223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
50		0le2 12449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ≤ 2
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 0 ≤ 2)
52		nnge1 12370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ≤ 𝑗)
53	37, 43, 41, 51, 52	lemul2ad 12261	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
54	39, 42, 44, 49, 53	ltletrd 11474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
55	38, 54	eqbrtrrid 5140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
56	37, 55	gtned 11449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
57	34, 35, 56	subne0d 11683	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
58	34, 36, 57	divcld 12097	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
59	34, 35	addcld 11332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
60		0red 11315	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 ∈ ℝ)
61	44, 37	readdcld 11342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
62	46	rpgt0d 13171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 0 < 1)
63		2rp 13129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ+
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ+)
65		nnrp 13136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
66	64, 65	rpmulcld 13184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
67	37, 66	ltaddrp2d 13202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
68	60, 37, 61, 62, 67	lttrd 11475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
69	60, 68	gtned 11449	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
70	34, 59, 69	divcld 12097	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
71	58, 70	mulcld 11333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
72	31, 71	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
73	3, 30, 31, 72	fvmptd3 7018	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
74	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
75	31	nnrpd 13166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
76	74, 75	rpmulcld 13184	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
77	44, 37	resubcld 11748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
78		1m1e0 12419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
79	37, 44, 37, 55	ltsub1dd 11932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
80	78, 79	eqbrtrrid 5140	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
81	77, 80	elrpd 13165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
82	31, 81	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
83	76, 82	rpdivcld 13185	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
84	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
85	31	nnred 12354	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
86	84, 85	remulcld 11343	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
87	74	rpge0d 13172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
88	75	rpge0d 13172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
89	84, 85, 87, 88	mulge0d 11897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
90	86, 89	ge0p1rpd 13198	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
91	76, 90	rpdivcld 13185	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
92	83, 91	rpmulcld 13184	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
93	73, 92	eqeltrd 2860	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) ∈ ℝ+)
94	93	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹‘𝑗) ∈ ℝ+)
95		rpmulcl 13149	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
96	95	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
97	24, 94, 96	seqcl 14169	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
98	97	rpcnd 13170	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
99	97	rpne0d 13173	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
100	98, 99	reccld 12090	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
101	22, 100	mulcld 11333	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
102	6, 101	fmpti 7113	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
103	102	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
104	103	ffvelcdmda 7085	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
105		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
106	105	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
107	106, 97	vtoclga 3536	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
108	107	rpcnd 13170	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
109	107	rpne0d 13173	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
110	35, 108, 109	divrecd 12100	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
111	11	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ∈ ℂ)
112	64	rpne0d 13173	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 2 ≠ 0)
113	15	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ≠ 0)
114	32, 111, 112, 113	divcan6d 12116	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
115	114	eqcomd 2766	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
116	115	oveq1d 7436	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
117	32, 111, 113	divcld 12097	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
118	111	halfcld 12595	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
119	108, 109	reccld 12090	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
120	117, 118, 119	mulassd 11336	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
121	110, 116, 120	3eqtrd 2799	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
122		eqidd 2761	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
123	105	oveq2d 7437	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
124	123	adantl 487	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
125		id 23	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
126	107	rpreccld 13178	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
127	122, 124, 125, 126	fvmptd 7002	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
128		eqidd 2761	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
129	124	oveq2d 7437	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
130	118, 119	mulcld 11333	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
131	128, 129, 125, 130	fvmptd 7002	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132	131	oveq2d 7437	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
133	121, 127, 132	3eqtr4d 2805	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
134	133	adantl 487	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
135	1, 2, 9, 17, 20, 104, 134	climmulc2 15810	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
136		2cn 12422	. . . . . . 7 ⊢ 2 ∈ ℂ
137	136, 11, 15	divcli 12063	. . . . . 6 ⊢ (2 / π) ∈ ℂ
138	137	mulridi 11317	. . . . 5 ⊢ ((2 / π) · 1) = (2 / π)
139	135, 138	breqtrdi 5145	. . . 4 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
140		2ne0 12453	. . . . . 6 ⊢ 2 ≠ 0
141	136, 11, 140, 15	divne0i 12069	. . . . 5 ⊢ (2 / π) ≠ 0
142	141	a1i 11	. . . 4 ⊢ (⊤ → (2 / π) ≠ 0)
143	127, 119	eqeltrd 2860	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
144	108, 109	recne0d 12091	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
145	127, 144	eqnetrd 3022	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
146		nelsn 4623	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
147	145, 146	syl 18	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
148	143, 147	eldifd 4050	. . . . 5 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
149	148	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
150	108, 109	recrecd 12094	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
151	122, 124, 125, 119	fvmptd 7002	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
152	151	oveq2d 7437	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
153		wallispi.2	. . . . . . 7 ⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
154	105, 153, 97	fvmpt3 6999	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (seq1( · , 𝐹)‘𝑗))
155	150, 152, 154	3eqtr4rd 2806	. . . . 5 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
156	155	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
157	18	mptex 7230	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
158	153, 157	eqeltri 2856	. . . . 5 ⊢ 𝑊 ∈ V
159	158	a1i 11	. . . 4 ⊢ (⊤ → 𝑊 ∈ V)
160	1, 2, 139, 142, 149, 156, 159	climrec 46709	. . 3 ⊢ (⊤ → 𝑊 ⇝ (1 / (2 / π)))
161	160	mptru 1576	. 2 ⊢ 𝑊 ⇝ (1 / (2 / π))
162		recdiv 12027	. . 3 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
163	136, 140, 11, 15, 162	mp4an 706	. 2 ⊢ (1 / (2 / π)) = (π / 2)
164	161, 163	breqtri 5129	1 ⊢ 𝑊 ⇝ (π / 2)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1569  ⊤wtru 1570   ∈ wcel 2144   ≠ wne 2955  Vcvv 3450   ∖ cdif 4045  {csn 4584   class class class wbr 5102   ↦ cmpt 5185  ⟶wf 6535  ‘cfv 6539  (class class class)co 7421  ℂcc 11202  ℝcr 11203  0cc0 11204  1c1 11205   + caddc 11207   · cmul 11209   < clt 11347   ≤ cle 11348   − cmin 11545   / cdiv 11977  ℕcn 12339  2c2 12401  ℕ₀cn0 12610  ℤ_≥cuz 12969  ℝ⁺crp 13124  (,)cioo 13480  ...cfz 13643  seqcseq 14148  ↑cexp 14208   ⇝ cli 15657  sincsin 16235  πcpi 16238  ∫citg 25945

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-inf2 9646  ax-cc 10517  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281  ax-pre-sup 11282  ax-addf 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-symdif 4198  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-disj 5070  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-of 7694  df-ofr 7695  df-om 7879  df-1st 8002  df-2nd 8003  df-supp 8181  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-1o 8480  df-2o 8481  df-oadd 8484  df-omul 8485  df-er 8721  df-map 8853  df-pm 8854  df-ixp 8930  df-en 8978  df-dom 8979  df-sdom 8980  df-fin 8981  df-fsupp 9358  df-fi 9407  df-sup 9438  df-inf 9439  df-oi 9508  df-dju 9986  df-card 10024  df-acn 10027  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-div 11978  df-nn 12340  df-2 12409  df-3 12410  df-4 12411  df-5 12412  df-6 12413  df-7 12414  df-8 12415  df-9 12416  df-n0 12611  df-z 12698  df-dec 12819  df-uz 12970  df-q 13080  df-rp 13125  df-xneg 13245  df-xadd 13246  df-xmul 13247  df-ioo 13484  df-ioc 13485  df-ico 13486  df-icc 13487  df-fz 13644  df-fzo 13793  df-fl 13936  df-mod 14014  df-seq 14149  df-exp 14209  df-fac 14422  df-bc 14451  df-hash 14479  df-shft 15226  df-cj 15272  df-re 15273  df-im 15274  df-sqrt 15408  df-abs 15409  df-limsup 15644  df-clim 15661  df-rlim 15662  df-sum 15860  df-ef 16239  df-sin 16241  df-cos 16242  df-pi 16244  df-struct 17331  df-sets 17348  df-slot 17366  df-ndx 17378  df-base 17394  df-ress 17415  df-plusg 17447  df-mulr 17448  df-starv 17449  df-sca 17450  df-vsca 17451  df-ip 17452  df-tset 17453  df-ple 17454  df-ds 17456  df-unif 17457  df-hom 17458  df-cco 17459  df-rest 17599  df-topn 17600  df-0g 17618  df-gsum 17619  df-topgen 17620  df-pt 17621  df-prds 17624  df-xrs 17680  df-qtop 17685  df-imas 17686  df-xps 17688  df-mre 17762  df-mrc 17763  df-acs 17765  df-mgm 18822  df-sgrp 18914  df-mnd 18930  df-submnd 18985  df-mulg 19284  df-cntz 19537  df-cmn 20002  df-psmet 21676  df-xmet 21677  df-met 21678  df-bl 21679  df-mopn 21680  df-fbas 21681  df-fg 21682  df-cnfld 21685  df-top 23218  df-topon 23235  df-topsp 23257  df-bases 23270  df-cld 23343  df-ntr 23344  df-cls 23345  df-nei 23422  df-lp 23460  df-perf 23461  df-cn 23551  df-cnp 23552  df-haus 23639  df-cmp 23711  df-tx 23887  df-hmeo 24080  df-fil 24171  df-fm 24263  df-flim 24264  df-flf 24265  df-xms 24645  df-ms 24646  df-tms 24647  df-cncf 25205  df-ovol 25791  df-vol 25792  df-mbf 25946  df-itg1 25947  df-itg2 25948  df-ibl 25949  df-itg 25950  df-0p 25997  df-limc 26192  df-dv 26193

This theorem is used by:  wallispi2  47177