Theorem wallispi 43611

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 12621	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12351	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		wallispi.1	. . . . . . . 8 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4		eqid 2738	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5		eqid 2738	. . . . . . . 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 2738	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7		eqid 2738	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
8	3, 4, 5, 6, 7	wallispilem5 43610	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
9	8	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10		2cnd 12051	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℂ)
11		picn 25616	. . . . . . . 8 ⊢ π ∈ ℂ
12	11	a1i 11	. . . . . . 7 ⊢ (⊤ → π ∈ ℂ)
13		pire 25615	. . . . . . . . 9 ⊢ π ∈ ℝ
14		pipos 25617	. . . . . . . . 9 ⊢ 0 < π
15	13, 14	gt0ne0ii 11511	. . . . . . . 8 ⊢ π ≠ 0
16	15	a1i 11	. . . . . . 7 ⊢ (⊤ → π ≠ 0)
17	10, 12, 16	divcld 11751	. . . . . 6 ⊢ (⊤ → (2 / π) ∈ ℂ)
18		nnex 11979	. . . . . . . 8 ⊢ ℕ ∈ V
19	18	mptex 7099	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
20	19	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
21	11	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → π ∈ ℂ)
22	21	halfcld 12218	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23		elnnuz 12622	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ≥‘1))
24	23	biimpi 215	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ≥‘1))
25		oveq2 7283	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
26	25	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
27	25, 26	oveq12d 7293	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
28	25	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
29	25, 28	oveq12d 7293	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
30	27, 29	oveq12d 7293	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
31		elfznn 13285	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
32		2cnd 12051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℂ)
33		nncn 11981	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
34	32, 33	mulcld 10995	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
35		1cnd 10970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℂ)
36	34, 35	subcld 11332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
37		1red 10976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ)
38		1t1e1 12135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 · 1) = 1
39	37, 37	remulcld 11005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
40		2re 12047	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ)
42	41, 37	remulcld 11005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
43		nnre 11980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
44	41, 43	remulcld 11005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
45		1rp 12734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ+
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ∈ ℝ+)
47		1lt2 12144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 < 2
48	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 < 2)
49	37, 41, 46, 48	ltmul1dd 12827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
50		0le2 12075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ≤ 2
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 0 ≤ 2)
52		nnge1 12001	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ ℕ → 1 ≤ 𝑗)
53	37, 43, 41, 51, 52	lemul2ad 11915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
54	39, 42, 44, 49, 53	ltletrd 11135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
55	38, 54	eqbrtrrid 5110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
56	37, 55	gtned 11110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
57	34, 35, 56	subne0d 11341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
58	34, 36, 57	divcld 11751	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
59	34, 35	addcld 10994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
60		0red 10978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 ∈ ℝ)
61	44, 37	readdcld 11004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
62	46	rpgt0d 12775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 0 < 1)
63		2rp 12735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ+
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 2 ∈ ℝ+)
65		nnrp 12741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
66	64, 65	rpmulcld 12788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
67	37, 66	ltaddrp2d 12806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
68	60, 37, 61, 62, 67	lttrd 11136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
69	60, 68	gtned 11110	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
70	34, 59, 69	divcld 11751	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
71	58, 70	mulcld 10995	. . . . . . . . . . . . . . . . 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 6898	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
74	63	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
75	31	nnrpd 12770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
76	74, 75	rpmulcld 12788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
77	44, 37	resubcld 11403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
78		1m1e0 12045	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
79	37, 44, 37, 55	ltsub1dd 11587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
80	78, 79	eqbrtrrid 5110	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
81	77, 80	elrpd 12769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
82	31, 81	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
83	76, 82	rpdivcld 12789	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
84	40	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
85	31	nnred 11988	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
86	84, 85	remulcld 11005	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
87	74	rpge0d 12776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
88	75	rpge0d 12776	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
89	84, 85, 87, 88	mulge0d 11552	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
90	86, 89	ge0p1rpd 12802	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
91	76, 90	rpdivcld 12789	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
92	83, 91	rpmulcld 12788	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
93	73, 92	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑛) → (𝐹‘𝑗) ∈ ℝ+)
94	93	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹‘𝑗) ∈ ℝ+)
95		rpmulcl 12753	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
96	95	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
97	24, 94, 96	seqcl 13743	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
98	97	rpcnd 12774	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
99	97	rpne0d 12777	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
100	98, 99	reccld 11744	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
101	22, 100	mulcld 10995	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
102	6, 101	fmpti 6986	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
103	102	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
104	103	ffvelrnda 6961	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
105		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
106	105	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
107	106, 97	vtoclga 3513	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
108	107	rpcnd 12774	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
109	107	rpne0d 12777	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
110	35, 108, 109	divrecd 11754	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
111	11	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ∈ ℂ)
112	64	rpne0d 12777	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 2 ≠ 0)
113	15	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → π ≠ 0)
114	32, 111, 112, 113	divcan6d 11770	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
115	114	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
116	115	oveq1d 7290	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
117	32, 111, 113	divcld 11751	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
118	111	halfcld 12218	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
119	108, 109	reccld 11744	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
120	117, 118, 119	mulassd 10998	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
121	110, 116, 120	3eqtrd 2782	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
122		eqidd 2739	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
123	105	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
124	123	adantl 482	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
125		id 22	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
126	107	rpreccld 12782	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
127	122, 124, 125, 126	fvmptd 6882	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
128		eqidd 2739	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
129	124	oveq2d 7291	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
130	118, 119	mulcld 10995	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
131	128, 129, 125, 130	fvmptd 6882	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132	131	oveq2d 7291	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
133	121, 127, 132	3eqtr4d 2788	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
134	133	adantl 482	. . . . . 6 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
135	1, 2, 9, 17, 20, 104, 134	climmulc2 15346	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
136		2cn 12048	. . . . . . 7 ⊢ 2 ∈ ℂ
137	136, 11, 15	divcli 11717	. . . . . 6 ⊢ (2 / π) ∈ ℂ
138	137	mulid1i 10979	. . . . 5 ⊢ ((2 / π) · 1) = (2 / π)
139	135, 138	breqtrdi 5115	. . . 4 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
140		2ne0 12077	. . . . . 6 ⊢ 2 ≠ 0
141	136, 11, 140, 15	divne0i 11723	. . . . 5 ⊢ (2 / π) ≠ 0
142	141	a1i 11	. . . 4 ⊢ (⊤ → (2 / π) ≠ 0)
143	127, 119	eqeltrd 2839	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
144	108, 109	recne0d 11745	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
145	127, 144	eqnetrd 3011	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
146		nelsn 4601	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
147	145, 146	syl 17	. . . . . 6 ⊢ (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
148	143, 147	eldifd 3898	. . . . 5 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
149	148	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
150	108, 109	recrecd 11748	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
151	122, 124, 125, 119	fvmptd 6882	. . . . . . 7 ⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
152	151	oveq2d 7291	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
153		wallispi.2	. . . . . . 7 ⊢ 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
154	105, 153, 97	fvmpt3 6879	. . . . . 6 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (seq1( · , 𝐹)‘𝑗))
155	150, 152, 154	3eqtr4rd 2789	. . . . 5 ⊢ (𝑗 ∈ ℕ → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
156	155	adantl 482	. . . 4 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊‘𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
157	18	mptex 7099	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
158	153, 157	eqeltri 2835	. . . . 5 ⊢ 𝑊 ∈ V
159	158	a1i 11	. . . 4 ⊢ (⊤ → 𝑊 ∈ V)
160	1, 2, 139, 142, 149, 156, 159	climrec 43144	. . 3 ⊢ (⊤ → 𝑊 ⇝ (1 / (2 / π)))
161	160	mptru 1546	. 2 ⊢ 𝑊 ⇝ (1 / (2 / π))
162		recdiv 11681	. . 3 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
163	136, 140, 11, 15, 162	mp4an 690	. 2 ⊢ (1 / (2 / π)) = (π / 2)
164	161, 163	breqtri 5099	1 ⊢ 𝑊 ⇝ (π / 2)

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1539  ⊤wtru 1540   ∈ wcel 2106   ≠ wne 2943  Vcvv 3432   ∖ cdif 3884  {csn 4561   class class class wbr 5074   ↦ cmpt 5157  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275  ℂcc 10869  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009   ≤ cle 11010   − cmin 11205   / cdiv 11632  ℕcn 11973  2c2 12028  ℕ₀cn0 12233  ℤ_≥cuz 12582  ℝ⁺crp 12730  (,)cioo 13079  ...cfz 13239  seqcseq 13721  ↑cexp 13782   ⇝ cli 15193  sincsin 15773  πcpi 15776  ∫citg 24782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cc 10191  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-symdif 4176  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-disj 5040  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-ofr 7534  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-oadd 8301  df-omul 8302  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-dju 9659  df-card 9697  df-acn 9700  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ioc 13084  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-mod 13590  df-seq 13722  df-exp 13783  df-fac 13988  df-bc 14017  df-hash 14045  df-shft 14778  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-limsup 15180  df-clim 15197  df-rlim 15198  df-sum 15398  df-ef 15777  df-sin 15779  df-cos 15780  df-pi 15782  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-hom 16986  df-cco 16987  df-rest 17133  df-topn 17134  df-0g 17152  df-gsum 17153  df-topgen 17154  df-pt 17155  df-prds 17158  df-xrs 17213  df-qtop 17218  df-imas 17219  df-xps 17221  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-fbas 20594  df-fg 20595  df-cnfld 20598  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-cld 22170  df-ntr 22171  df-cls 22172  df-nei 22249  df-lp 22287  df-perf 22288  df-cn 22378  df-cnp 22379  df-haus 22466  df-cmp 22538  df-tx 22713  df-hmeo 22906  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-xms 23473  df-ms 23474  df-tms 23475  df-cncf 24041  df-ovol 24628  df-vol 24629  df-mbf 24783  df-itg1 24784  df-itg2 24785  df-ibl 24786  df-itg 24787  df-0p 24834  df-limc 25030  df-dv 25031

This theorem is referenced by:  wallispi2  43614