Theorem wallispi 46041

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 12812	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12540	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		wallispi.1	. . . . . . . 8 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4		eqid 2729	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5		eqid 2729	. . . . . . . 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 2729	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7		eqid 2729	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
8	3, 4, 5, 6, 7	wallispilem5 46040	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
9	8	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10		2cnd 12240	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℂ)
11		picn 26343	. . . . . . . 8 ⊢ π ∈ ℂ
12	11	a1i 11	. . . . . . 7 ⊢ (⊤ → π ∈ ℂ)
13		pire 26342	. . . . . . . . 9 ⊢ π ∈ ℝ
14		pipos 26344	. . . . . . . . 9 ⊢ 0 < π
15	13, 14	gt0ne0ii 11690	. . . . . . . 8 ⊢ π ≠ 0
16	15	a1i 11	. . . . . . 7 ⊢ (⊤ → π ≠ 0)
17	10, 12, 16	divcld 11934	. . . . . 6 ⊢ (⊤ → (2 / π) ∈ ℂ)
18		nnex 12168	. . . . . . . 8 ⊢ ℕ ∈ V
19	18	mptex 7179	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
20	19	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
21	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → π ∈ ℂ)
22	21	halfcld 12403	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23		elnnuz 12813	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ≥‘1))
24	23	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ≥‘1))
25		oveq2 7377	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
26	25	oveq1d 7384	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
27	25, 26	oveq12d 7387	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
28	25	oveq1d 7384	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
29	25, 28	oveq12d 7387	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
30	27, 29	oveq12d 7387	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
31		elfznn 13490	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
32		2cnd 12240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℂ)
33		nncn 12170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
34	32, 33	mulcld 11170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
35		1cnd 11145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℂ)
36	34, 35	subcld 11509	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
37		1red 11151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ)
38		1t1e1 12319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 · 1) = 1
39	37, 37	remulcld 11180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
40		2re 12236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ)
42	41, 37	remulcld 11180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
43		nnre 12169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
44	41, 43	remulcld 11180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
45		1rp 12931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ+
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ+)
47		1lt2 12328	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 < 2
48	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 < 2)
49	37, 41, 46, 48	ltmul1dd 13026	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
50		0le2 12264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ≤ 2
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 0 ≤ 2)
52		nnge1 12190	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ≤ 𝑗)
53	37, 43, 41, 51, 52	lemul2ad 12099	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
54	39, 42, 44, 49, 53	ltletrd 11310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
55	38, 54	eqbrtrrid 5138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
56	37, 55	gtned 11285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
57	34, 35, 56	subne0d 11518	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
58	34, 36, 57	divcld 11934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
59	34, 35	addcld 11169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
60		0red 11153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 ∈ ℝ)
61	44, 37	readdcld 11179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
62	46	rpgt0d 12974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 0 < 1)
63		2rp 12932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ+
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ+)
65		nnrp 12939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
66	64, 65	rpmulcld 12987	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
67	37, 66	ltaddrp2d 13005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
68	60, 37, 61, 62, 67	lttrd 11311	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
69	60, 68	gtned 11285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
70	34, 59, 69	divcld 11934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
71	58, 70	mulcld 11170	. . . . . . . . . . . . . . . . 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 6973	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
74	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
75	31	nnrpd 12969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
76	74, 75	rpmulcld 12987	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
77	44, 37	resubcld 11582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
78		1m1e0 12234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
79	37, 44, 37, 55	ltsub1dd 11766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
80	78, 79	eqbrtrrid 5138	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
81	77, 80	elrpd 12968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
82	31, 81	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
83	76, 82	rpdivcld 12988	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
84	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
85	31	nnred 12177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
86	84, 85	remulcld 11180	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
87	74	rpge0d 12975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
88	75	rpge0d 12975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
89	84, 85, 87, 88	mulge0d 11731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
90	86, 89	ge0p1rpd 13001	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
91	76, 90	rpdivcld 12988	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
92	83, 91	rpmulcld 12987	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
93	73, 92	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) ∈ ℝ+)
94	93	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹‘𝑗) ∈ ℝ+)
95		rpmulcl 12952	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
96	95	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
97	24, 94, 96	seqcl 13963	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
98	97	rpcnd 12973	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
99	97	rpne0d 12976	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
100	98, 99	reccld 11927	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
101	22, 100	mulcld 11170	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
102	6, 101	fmpti 7066	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
103	102	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
104	103	ffvelcdmda 7038	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
105		fveq2 6840	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
106	105	eleq1d 2813	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
107	106, 97	vtoclga 3540	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
108	107	rpcnd 12973	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
109	107	rpne0d 12976	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
110	35, 108, 109	divrecd 11937	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
111	11	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ∈ ℂ)
112	64	rpne0d 12976	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 2 ≠ 0)
113	15	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ≠ 0)
114	32, 111, 112, 113	divcan6d 11953	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
115	114	eqcomd 2735	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
116	115	oveq1d 7384	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
117	32, 111, 113	divcld 11934	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
118	111	halfcld 12403	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
119	108, 109	reccld 11927	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
120	117, 118, 119	mulassd 11173	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
121	110, 116, 120	3eqtrd 2768	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
122		eqidd 2730	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
123	105	oveq2d 7385	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
124	123	adantl 481	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
125		id 22	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
126	107	rpreccld 12981	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
127	122, 124, 125, 126	fvmptd 6957	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
128		eqidd 2730	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
129	124	oveq2d 7385	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
130	118, 119	mulcld 11170	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
131	128, 129, 125, 130	fvmptd 6957	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132	131	oveq2d 7385	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
133	121, 127, 132	3eqtr4d 2774	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
134	133	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
135	1, 2, 9, 17, 20, 104, 134	climmulc2 15579	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
136		2cn 12237	. . . . . . 7 ⊢ 2 ∈ ℂ
137	136, 11, 15	divcli 11900	. . . . . 6 ⊢ (2 / π) ∈ ℂ
138	137	mulridi 11154	. . . . 5 ⊢ ((2 / π) · 1) = (2 / π)
139	135, 138	breqtrdi 5143	. . . 4 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
140		2ne0 12266	. . . . . 6 ⊢ 2 ≠ 0
141	136, 11, 140, 15	divne0i 11906	. . . . 5 ⊢ (2 / π) ≠ 0
142	141	a1i 11	. . . 4 ⊢ (⊤ → (2 / π) ≠ 0)
143	127, 119	eqeltrd 2828	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
144	108, 109	recne0d 11928	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
145	127, 144	eqnetrd 2992	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
146		nelsn 4626	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
147	145, 146	syl 17	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
148	143, 147	eldifd 3922	. . . . 5 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
149	148	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
150	108, 109	recrecd 11931	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
151	122, 124, 125, 119	fvmptd 6957	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
152	151	oveq2d 7385	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
153		wallispi.2	. . . . . . 7 ⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
154	105, 153, 97	fvmpt3 6954	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (seq1( · , 𝐹)‘𝑗))
155	150, 152, 154	3eqtr4rd 2775	. . . . 5 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
156	155	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
157	18	mptex 7179	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
158	153, 157	eqeltri 2824	. . . . 5 ⊢ 𝑊 ∈ V
159	158	a1i 11	. . . 4 ⊢ (⊤ → 𝑊 ∈ V)
160	1, 2, 139, 142, 149, 156, 159	climrec 45574	. . 3 ⊢ (⊤ → 𝑊 ⇝ (1 / (2 / π)))
161	160	mptru 1547	. 2 ⊢ 𝑊 ⇝ (1 / (2 / π))
162		recdiv 11864	. . 3 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
163	136, 140, 11, 15, 162	mp4an 693	. 2 ⊢ (1 / (2 / π)) = (π / 2)
164	161, 163	breqtri 5127	1 ⊢ 𝑊 ⇝ (π / 2)

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109   ≠ wne 2925  Vcvv 3444   ∖ cdif 3908  {csn 4585   class class class wbr 5102   ↦ cmpt 5183  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   · cmul 11049   < clt 11184   ≤ cle 11185   − cmin 11381   / cdiv 11811  ℕcn 12162  2c2 12217  ℕ₀cn0 12418  ℤ_≥cuz 12769  ℝ⁺crp 12927  (,)cioo 13282  ...cfz 13444  seqcseq 13942  ↑cexp 14002   ⇝ cli 15426  sincsin 16005  πcpi 16008  ∫citg 25495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cc 10364  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122  ax-addf 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-symdif 4212  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-disj 5070  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-ofr 7634  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-oadd 8415  df-omul 8416  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-fi 9338  df-sup 9369  df-inf 9370  df-oi 9439  df-dju 9830  df-card 9868  df-acn 9871  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-q 12884  df-rp 12928  df-xneg 13048  df-xadd 13049  df-xmul 13050  df-ioo 13286  df-ioc 13287  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-fl 13730  df-mod 13808  df-seq 13943  df-exp 14003  df-fac 14215  df-bc 14244  df-hash 14272  df-shft 15009  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-limsup 15413  df-clim 15430  df-rlim 15431  df-sum 15629  df-ef 16009  df-sin 16011  df-cos 16012  df-pi 16014  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17361  df-topn 17362  df-0g 17380  df-gsum 17381  df-topgen 17382  df-pt 17383  df-prds 17386  df-xrs 17441  df-qtop 17446  df-imas 17447  df-xps 17449  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18543  df-sgrp 18622  df-mnd 18638  df-submnd 18687  df-mulg 18976  df-cntz 19225  df-cmn 19688  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22757  df-topon 22774  df-topsp 22796  df-bases 22809  df-cld 22882  df-ntr 22883  df-cls 22884  df-nei 22961  df-lp 22999  df-perf 23000  df-cn 23090  df-cnp 23091  df-haus 23178  df-cmp 23250  df-tx 23425  df-hmeo 23618  df-fil 23709  df-fm 23801  df-flim 23802  df-flf 23803  df-xms 24184  df-ms 24185  df-tms 24186  df-cncf 24747  df-ovol 25341  df-vol 25342  df-mbf 25496  df-itg1 25497  df-itg2 25498  df-ibl 25499  df-itg 25500  df-0p 25547  df-limc 25743  df-dv 25744

This theorem is referenced by:  wallispi2  46044