Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wallispi Structured version   Visualization version   GIF version

Theorem wallispi 40786
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.
StepHypRef Expression
1 nnuz 11912 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11596 . . . 4 (⊤ → 1 ∈ ℤ)
3 wallispi.1 . . . . . . . 8 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4 eqid 2756 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5 eqid 2756 . . . . . . . 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 2756 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7 eqid 2756 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
83, 4, 5, 6, 7wallispilem5 40785 . . . . . . 7 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
98a1i 11 . . . . . 6 (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10 2cnd 11281 . . . . . . 7 (⊤ → 2 ∈ ℂ)
11 picn 24406 . . . . . . . 8 π ∈ ℂ
1211a1i 11 . . . . . . 7 (⊤ → π ∈ ℂ)
13 pire 24405 . . . . . . . . 9 π ∈ ℝ
14 pipos 24407 . . . . . . . . 9 0 < π
1513, 14gt0ne0ii 10752 . . . . . . . 8 π ≠ 0
1615a1i 11 . . . . . . 7 (⊤ → π ≠ 0)
1710, 12, 16divcld 10989 . . . . . 6 (⊤ → (2 / π) ∈ ℂ)
18 nnex 11214 . . . . . . . 8 ℕ ∈ V
1918mptex 6646 . . . . . . 7 (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
2019a1i 11 . . . . . 6 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
2111a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → π ∈ ℂ)
2221halfcld 11465 . . . . . . . . . 10 (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23 elnnuz 11913 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
2423biimpi 206 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
253a1i 11 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
26 oveq2 6817 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
2726oveq1d 6824 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
2826, 27oveq12d 6827 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
2926oveq1d 6824 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
3026, 29oveq12d 6827 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
3128, 30oveq12d 6827 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
3231adantl 473 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (1...𝑛) ∧ 𝑘 = 𝑗) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
33 elfznn 12559 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
34 2cnd 11281 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 2 ∈ ℂ)
35 nncn 11216 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
3634, 35mulcld 10248 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
37 1cnd 10244 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 1 ∈ ℂ)
3836, 37subcld 10580 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
39 1red 10243 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 ∈ ℝ)
40 1t1e1 11363 . . . . . . . . . . . . . . . . . . . . . 22 (1 · 1) = 1
4139, 39remulcld 10258 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
42 2re 11278 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 2 ∈ ℝ)
4443, 39remulcld 10258 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
45 nnre 11215 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
4643, 45remulcld 10258 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
47 1rp 12025 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ+
4847a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 ∈ ℝ+)
49 1lt2 11382 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 < 2
5049a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 < 2)
5139, 43, 48, 50ltmul1dd 12116 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
52 0le2 11299 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 2
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 0 ≤ 2)
54 nnge1 11234 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 ≤ 𝑗)
5539, 45, 43, 53, 54lemul2ad 11152 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
5641, 44, 46, 51, 55ltletrd 10385 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
5740, 56syl5eqbrr 4836 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
5839, 57gtned 10360 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
5936, 37, 58subne0d 10589 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
6036, 38, 59divcld 10989 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
6136, 37addcld 10247 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
62 0red 10229 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 0 ∈ ℝ)
6346, 39readdcld 10257 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
6448rpgt0d 12064 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 0 < 1)
65 2rp 12026 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℝ+
6665a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → 2 ∈ ℝ+)
67 nnrp 12031 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
6866, 67rpmulcld 12077 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
6939, 68ltaddrp2d 12095 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
7062, 39, 63, 64, 69lttrd 10386 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
7162, 70gtned 10360 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
7236, 61, 71divcld 10989 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
7360, 72mulcld 10248 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
7433, 73syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
7525, 32, 33, 74fvmptd 6446 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑛) → (𝐹𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
7665a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
7733nnrpd 12059 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
7876, 77rpmulcld 12077 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
7946, 39resubcld 10646 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
80 1m1e0 11277 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
8139, 46, 39, 57ltsub1dd 10827 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
8280, 81syl5eqbrr 4836 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
8379, 82elrpd 12058 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
8433, 83syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
8578, 84rpdivcld 12078 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
8642a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
8733nnred 11223 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
8886, 87remulcld 10258 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
8976rpge0d 12065 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
9077rpge0d 12065 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
9186, 87, 89, 90mulge0d 10792 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
9288, 91ge0p1rpd 12091 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
9378, 92rpdivcld 12078 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
9485, 93rpmulcld 12077 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
9575, 94eqeltrd 2835 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑛) → (𝐹𝑗) ∈ ℝ+)
9695adantl 473 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹𝑗) ∈ ℝ+)
97 rpmulcl 12044 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℝ+𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
9897adantl 473 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
9924, 96, 98seqcl 13011 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
10099rpcnd 12063 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
10199rpne0d 12066 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
102100, 101reccld 10982 . . . . . . . . . 10 (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
10322, 102mulcld 10248 . . . . . . . . 9 (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
1046, 103fmpti 6542 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
105104a1i 11 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
106105ffvelrnda 6518 . . . . . 6 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
107 fveq2 6348 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
108107eleq1d 2820 . . . . . . . . . . . 12 (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
109108, 99vtoclga 3408 . . . . . . . . . . 11 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
110109rpcnd 12063 . . . . . . . . . 10 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
111109rpne0d 12066 . . . . . . . . . 10 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
11237, 110, 111divrecd 10992 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
11311a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → π ∈ ℂ)
11466rpne0d 12066 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 2 ≠ 0)
11515a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → π ≠ 0)
11634, 113, 114, 115divcan6d 11008 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
117116eqcomd 2762 . . . . . . . . . 10 (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
118117oveq1d 6824 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
11934, 113, 115divcld 10989 . . . . . . . . . 10 (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
120113halfcld 11465 . . . . . . . . . 10 (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
121110, 111reccld 10982 . . . . . . . . . 10 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
122119, 120, 121mulassd 10251 . . . . . . . . 9 (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
123112, 118, 1223eqtrd 2794 . . . . . . . 8 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
124 eqidd 2757 . . . . . . . . 9 (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
125107oveq2d 6825 . . . . . . . . . 10 (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
126125adantl 473 . . . . . . . . 9 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
127 id 22 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
128109rpreccld 12071 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
129124, 126, 127, 128fvmptd 6446 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
130 eqidd 2757 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
131126oveq2d 6825 . . . . . . . . . 10 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132120, 121mulcld 10248 . . . . . . . . . 10 (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
133130, 131, 127, 132fvmptd 6446 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
134133oveq2d 6825 . . . . . . . 8 (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
135123, 129, 1343eqtr4d 2800 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
136135adantl 473 . . . . . 6 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
1371, 2, 9, 17, 20, 106, 136climmulc2 14562 . . . . 5 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
138 2cn 11279 . . . . . . 7 2 ∈ ℂ
139138, 11, 15divcli 10955 . . . . . 6 (2 / π) ∈ ℂ
140139mulid1i 10230 . . . . 5 ((2 / π) · 1) = (2 / π)
141137, 140syl6breq 4841 . . . 4 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
142 2ne0 11301 . . . . . 6 2 ≠ 0
143138, 11, 142, 15divne0i 10961 . . . . 5 (2 / π) ≠ 0
144143a1i 11 . . . 4 (⊤ → (2 / π) ≠ 0)
145129, 121eqeltrd 2835 . . . . . 6 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
146110, 111recne0d 10983 . . . . . . . 8 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
147129, 146eqnetrd 2995 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
148 nelsn 4353 . . . . . . 7 (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
149147, 148syl 17 . . . . . 6 (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
150145, 149eldifd 3722 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
151150adantl 473 . . . 4 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
152110, 111recrecd 10986 . . . . . 6 (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
153124, 126, 127, 121fvmptd 6446 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
154153oveq2d 6825 . . . . . 6 (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
155 wallispi.2 . . . . . . 7 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
156107, 155, 99fvmpt3 6444 . . . . . 6 (𝑗 ∈ ℕ → (𝑊𝑗) = (seq1( · , 𝐹)‘𝑗))
157152, 154, 1563eqtr4rd 2801 . . . . 5 (𝑗 ∈ ℕ → (𝑊𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
158157adantl 473 . . . 4 ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
15918mptex 6646 . . . . . 6 (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
160155, 159eqeltri 2831 . . . . 5 𝑊 ∈ V
161160a1i 11 . . . 4 (⊤ → 𝑊 ∈ V)
1621, 2, 141, 144, 151, 158, 161climrec 40334 . . 3 (⊤ → 𝑊 ⇝ (1 / (2 / π)))
163162trud 1638 . 2 𝑊 ⇝ (1 / (2 / π))
164 recdiv 10919 . . 3 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
165138, 142, 11, 15, 164mp4an 711 . 2 (1 / (2 / π)) = (π / 2)
166163, 165breqtri 4825 1 𝑊 ⇝ (π / 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 383   = wceq 1628  wtru 1629  wcel 2135  wne 2928  Vcvv 3336  cdif 3708  {csn 4317   class class class wbr 4800  cmpt 4877  wf 6041  cfv 6045  (class class class)co 6809  cc 10122  cr 10123  0cc0 10124  1c1 10125   + caddc 10127   · cmul 10129   < clt 10262  cle 10263  cmin 10454   / cdiv 10872  cn 11208  2c2 11258  0cn0 11480  cuz 11875  +crp 12021  (,)cioo 12364  ...cfz 12515  seqcseq 12991  cexp 13050  cli 14410  sincsin 14989  πcpi 14992  citg 23582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-inf2 8707  ax-cc 9445  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201  ax-pre-sup 10202  ax-addf 10203  ax-mulf 10204
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-fal 1634  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-iin 4671  df-disj 4769  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-of 7058  df-ofr 7059  df-om 7227  df-1st 7329  df-2nd 7330  df-supp 7460  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-2o 7726  df-oadd 7729  df-omul 7730  df-er 7907  df-map 8021  df-pm 8022  df-ixp 8071  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-fsupp 8437  df-fi 8478  df-sup 8509  df-inf 8510  df-oi 8576  df-card 8951  df-acn 8954  df-cda 9178  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-8 11273  df-9 11274  df-n0 11481  df-z 11566  df-dec 11682  df-uz 11876  df-q 11978  df-rp 12022  df-xneg 12135  df-xadd 12136  df-xmul 12137  df-ioo 12368  df-ioc 12369  df-ico 12370  df-icc 12371  df-fz 12516  df-fzo 12656  df-fl 12783  df-mod 12859  df-seq 12992  df-exp 13051  df-fac 13251  df-bc 13280  df-hash 13308  df-shft 14002  df-cj 14034  df-re 14035  df-im 14036  df-sqrt 14170  df-abs 14171  df-limsup 14397  df-clim 14414  df-rlim 14415  df-sum 14612  df-ef 14993  df-sin 14995  df-cos 14996  df-pi 14998  df-struct 16057  df-ndx 16058  df-slot 16059  df-base 16061  df-sets 16062  df-ress 16063  df-plusg 16152  df-mulr 16153  df-starv 16154  df-sca 16155  df-vsca 16156  df-ip 16157  df-tset 16158  df-ple 16159  df-ds 16162  df-unif 16163  df-hom 16164  df-cco 16165  df-rest 16281  df-topn 16282  df-0g 16300  df-gsum 16301  df-topgen 16302  df-pt 16303  df-prds 16306  df-xrs 16360  df-qtop 16365  df-imas 16366  df-xps 16368  df-mre 16444  df-mrc 16445  df-acs 16447  df-mgm 17439  df-sgrp 17481  df-mnd 17492  df-submnd 17533  df-mulg 17738  df-cntz 17946  df-cmn 18391  df-psmet 19936  df-xmet 19937  df-met 19938  df-bl 19939  df-mopn 19940  df-fbas 19941  df-fg 19942  df-cnfld 19945  df-top 20897  df-topon 20914  df-topsp 20935  df-bases 20948  df-cld 21021  df-ntr 21022  df-cls 21023  df-nei 21100  df-lp 21138  df-perf 21139  df-cn 21229  df-cnp 21230  df-haus 21317  df-cmp 21388  df-tx 21563  df-hmeo 21756  df-fil 21847  df-fm 21939  df-flim 21940  df-flf 21941  df-xms 22322  df-ms 22323  df-tms 22324  df-cncf 22878  df-ovol 23429  df-vol 23430  df-mbf 23583  df-itg1 23584  df-itg2 23585  df-ibl 23586  df-itg 23587  df-0p 23632  df-limc 23825  df-dv 23826
This theorem is referenced by:  wallispi2  40789
  Copyright terms: Public domain W3C validator