Theorem wallispi 42404

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 12282	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12014	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		wallispi.1	. . . . . . . 8 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4		eqid 2821	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5		eqid 2821	. . . . . . . 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 2821	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7		eqid 2821	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
8	3, 4, 5, 6, 7	wallispilem5 42403	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
9	8	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10		2cnd 11716	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℂ)
11		picn 25045	. . . . . . . 8 ⊢ π ∈ ℂ
12	11	a1i 11	. . . . . . 7 ⊢ (⊤ → π ∈ ℂ)
13		pire 25044	. . . . . . . . 9 ⊢ π ∈ ℝ
14		pipos 25046	. . . . . . . . 9 ⊢ 0 < π
15	13, 14	gt0ne0ii 11176	. . . . . . . 8 ⊢ π ≠ 0
16	15	a1i 11	. . . . . . 7 ⊢ (⊤ → π ≠ 0)
17	10, 12, 16	divcld 11416	. . . . . 6 ⊢ (⊤ → (2 / π) ∈ ℂ)
18		nnex 11644	. . . . . . . 8 ⊢ ℕ ∈ V
19	18	mptex 6986	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
20	19	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
21	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → π ∈ ℂ)
22	21	halfcld 11883	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23		elnnuz 12283	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ≥‘1))
24	23	biimpi 218	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ≥‘1))
25		oveq2 7164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
26	25	oveq1d 7171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
27	25, 26	oveq12d 7174	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
28	25	oveq1d 7171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
29	25, 28	oveq12d 7174	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
30	27, 29	oveq12d 7174	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
31		elfznn 12937	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
32		2cnd 11716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℂ)
33		nncn 11646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
34	32, 33	mulcld 10661	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
35		1cnd 10636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℂ)
36	34, 35	subcld 10997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
37		1red 10642	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ)
38		1t1e1 11800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 · 1) = 1
39	37, 37	remulcld 10671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
40		2re 11712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ)
42	41, 37	remulcld 10671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
43		nnre 11645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
44	41, 43	remulcld 10671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
45		1rp 12394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ+
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ+)
47		1lt2 11809	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 < 2
48	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 < 2)
49	37, 41, 46, 48	ltmul1dd 12487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
50		0le2 11740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ≤ 2
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 0 ≤ 2)
52		nnge1 11666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ≤ 𝑗)
53	37, 43, 41, 51, 52	lemul2ad 11580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
54	39, 42, 44, 49, 53	ltletrd 10800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
55	38, 54	eqbrtrrid 5102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
56	37, 55	gtned 10775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
57	34, 35, 56	subne0d 11006	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
58	34, 36, 57	divcld 11416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
59	34, 35	addcld 10660	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
60		0red 10644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 ∈ ℝ)
61	44, 37	readdcld 10670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
62	46	rpgt0d 12435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 0 < 1)
63		2rp 12395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ+
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ+)
65		nnrp 12401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
66	64, 65	rpmulcld 12448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
67	37, 66	ltaddrp2d 12466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
68	60, 37, 61, 62, 67	lttrd 10801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
69	60, 68	gtned 10775	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
70	34, 59, 69	divcld 11416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
71	58, 70	mulcld 10661	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
72	31, 71	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
73	3, 30, 31, 72	fvmptd3 6791	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
74	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
75	31	nnrpd 12430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
76	74, 75	rpmulcld 12448	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
77	44, 37	resubcld 11068	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
78		1m1e0 11710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
79	37, 44, 37, 55	ltsub1dd 11252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
80	78, 79	eqbrtrrid 5102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
81	77, 80	elrpd 12429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
82	31, 81	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
83	76, 82	rpdivcld 12449	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
84	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
85	31	nnred 11653	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
86	84, 85	remulcld 10671	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
87	74	rpge0d 12436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
88	75	rpge0d 12436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
89	84, 85, 87, 88	mulge0d 11217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
90	86, 89	ge0p1rpd 12462	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
91	76, 90	rpdivcld 12449	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
92	83, 91	rpmulcld 12448	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
93	73, 92	eqeltrd 2913	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) ∈ ℝ+)
94	93	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹‘𝑗) ∈ ℝ+)
95		rpmulcl 12413	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
96	95	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
97	24, 94, 96	seqcl 13391	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
98	97	rpcnd 12434	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
99	97	rpne0d 12437	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
100	98, 99	reccld 11409	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
101	22, 100	mulcld 10661	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
102	6, 101	fmpti 6876	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
103	102	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
104	103	ffvelrnda 6851	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
105		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
106	105	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
107	106, 97	vtoclga 3574	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
108	107	rpcnd 12434	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
109	107	rpne0d 12437	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
110	35, 108, 109	divrecd 11419	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
111	11	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ∈ ℂ)
112	64	rpne0d 12437	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 2 ≠ 0)
113	15	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ≠ 0)
114	32, 111, 112, 113	divcan6d 11435	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
115	114	eqcomd 2827	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
116	115	oveq1d 7171	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
117	32, 111, 113	divcld 11416	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
118	111	halfcld 11883	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
119	108, 109	reccld 11409	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
120	117, 118, 119	mulassd 10664	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
121	110, 116, 120	3eqtrd 2860	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
122		eqidd 2822	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
123	105	oveq2d 7172	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
124	123	adantl 484	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
125		id 22	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
126	107	rpreccld 12442	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
127	122, 124, 125, 126	fvmptd 6775	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
128		eqidd 2822	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
129	124	oveq2d 7172	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
130	118, 119	mulcld 10661	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
131	128, 129, 125, 130	fvmptd 6775	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132	131	oveq2d 7172	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
133	121, 127, 132	3eqtr4d 2866	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
134	133	adantl 484	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
135	1, 2, 9, 17, 20, 104, 134	climmulc2 14993	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
136		2cn 11713	. . . . . . 7 ⊢ 2 ∈ ℂ
137	136, 11, 15	divcli 11382	. . . . . 6 ⊢ (2 / π) ∈ ℂ
138	137	mulid1i 10645	. . . . 5 ⊢ ((2 / π) · 1) = (2 / π)
139	135, 138	breqtrdi 5107	. . . 4 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
140		2ne0 11742	. . . . . 6 ⊢ 2 ≠ 0
141	136, 11, 140, 15	divne0i 11388	. . . . 5 ⊢ (2 / π) ≠ 0
142	141	a1i 11	. . . 4 ⊢ (⊤ → (2 / π) ≠ 0)
143	127, 119	eqeltrd 2913	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
144	108, 109	recne0d 11410	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
145	127, 144	eqnetrd 3083	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
146		nelsn 4605	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
147	145, 146	syl 17	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
148	143, 147	eldifd 3947	. . . . 5 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
149	148	adantl 484	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
150	108, 109	recrecd 11413	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
151	122, 124, 125, 119	fvmptd 6775	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
152	151	oveq2d 7172	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
153		wallispi.2	. . . . . . 7 ⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
154	105, 153, 97	fvmpt3 6772	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (seq1( · , 𝐹)‘𝑗))
155	150, 152, 154	3eqtr4rd 2867	. . . . 5 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
156	155	adantl 484	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
157	18	mptex 6986	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
158	153, 157	eqeltri 2909	. . . . 5 ⊢ 𝑊 ∈ V
159	158	a1i 11	. . . 4 ⊢ (⊤ → 𝑊 ∈ V)
160	1, 2, 139, 142, 149, 156, 159	climrec 41933	. . 3 ⊢ (⊤ → 𝑊 ⇝ (1 / (2 / π)))
161	160	mptru 1544	. 2 ⊢ 𝑊 ⇝ (1 / (2 / π))
162		recdiv 11346	. . 3 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
163	136, 140, 11, 15, 162	mp4an 691	. 2 ⊢ (1 / (2 / π)) = (π / 2)
164	161, 163	breqtri 5091	1 ⊢ 𝑊 ⇝ (π / 2)

Syntax hints:  ¬ wn 3   ∧ wa 398   = wceq 1537  ⊤wtru 1538   ∈ wcel 2114   ≠ wne 3016  Vcvv 3494   ∖ cdif 3933  {csn 4567   class class class wbr 5066   ↦ cmpt 5146  ⟶wf 6351  ‘cfv 6355  (class class class)co 7156  ℂcc 10535  ℝcr 10536  0cc0 10537  1c1 10538   + caddc 10540   · cmul 10542   < clt 10675   ≤ cle 10676   − cmin 10870   / cdiv 11297  ℕcn 11638  2c2 11693  ℕ₀cn0 11898  ℤ_≥cuz 12244  ℝ⁺crp 12390  (,)cioo 12739  ...cfz 12893  seqcseq 13370  ↑cexp 13430   ⇝ cli 14841  sincsin 15417  πcpi 15420  ∫citg 24219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104  ax-cc 9857  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615  ax-addf 10616  ax-mulf 10617

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-symdif 4219  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-iin 4922  df-disj 5032  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7409  df-ofr 7410  df-om 7581  df-1st 7689  df-2nd 7690  df-supp 7831  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-2o 8103  df-oadd 8106  df-omul 8107  df-er 8289  df-map 8408  df-pm 8409  df-ixp 8462  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-fsupp 8834  df-fi 8875  df-sup 8906  df-inf 8907  df-oi 8974  df-dju 9330  df-card 9368  df-acn 9371  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11639  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707  df-9 11708  df-n0 11899  df-z 11983  df-dec 12100  df-uz 12245  df-q 12350  df-rp 12391  df-xneg 12508  df-xadd 12509  df-xmul 12510  df-ioo 12743  df-ioc 12744  df-ico 12745  df-icc 12746  df-fz 12894  df-fzo 13035  df-fl 13163  df-mod 13239  df-seq 13371  df-exp 13431  df-fac 13635  df-bc 13664  df-hash 13692  df-shft 14426  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-limsup 14828  df-clim 14845  df-rlim 14846  df-sum 15043  df-ef 15421  df-sin 15423  df-cos 15424  df-pi 15426  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-0g 16715  df-gsum 16716  df-topgen 16717  df-pt 16718  df-prds 16721  df-xrs 16775  df-qtop 16780  df-imas 16781  df-xps 16783  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-submnd 17957  df-mulg 18225  df-cntz 18447  df-cmn 18908  df-psmet 20537  df-xmet 20538  df-met 20539  df-bl 20540  df-mopn 20541  df-fbas 20542  df-fg 20543  df-cnfld 20546  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cld 21627  df-ntr 21628  df-cls 21629  df-nei 21706  df-lp 21744  df-perf 21745  df-cn 21835  df-cnp 21836  df-haus 21923  df-cmp 21995  df-tx 22170  df-hmeo 22363  df-fil 22454  df-fm 22546  df-flim 22547  df-flf 22548  df-xms 22930  df-ms 22931  df-tms 22932  df-cncf 23486  df-ovol 24065  df-vol 24066  df-mbf 24220  df-itg1 24221  df-itg2 24222  df-ibl 24223  df-itg 24224  df-0p 24271  df-limc 24464  df-dv 24465

This theorem is referenced by:  wallispi2  42407