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 44721
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 12861 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12589 . . . 4 (⊤ → 1 ∈ ℤ)
3 wallispi.1 . . . . . . . 8 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4 eqid 2733 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5 eqid 2733 . . . . . . . 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 2733 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7 eqid 2733 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
83, 4, 5, 6, 7wallispilem5 44720 . . . . . . 7 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
98a1i 11 . . . . . 6 (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10 2cnd 12286 . . . . . . 7 (⊤ → 2 ∈ ℂ)
11 picn 25951 . . . . . . . 8 π ∈ ℂ
1211a1i 11 . . . . . . 7 (⊤ → π ∈ ℂ)
13 pire 25950 . . . . . . . . 9 π ∈ ℝ
14 pipos 25952 . . . . . . . . 9 0 < π
1513, 14gt0ne0ii 11746 . . . . . . . 8 π ≠ 0
1615a1i 11 . . . . . . 7 (⊤ → π ≠ 0)
1710, 12, 16divcld 11986 . . . . . 6 (⊤ → (2 / π) ∈ ℂ)
18 nnex 12214 . . . . . . . 8 ℕ ∈ V
1918mptex 7220 . . . . . . 7 (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
2019a1i 11 . . . . . 6 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
2111a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → π ∈ ℂ)
2221halfcld 12453 . . . . . . . . . 10 (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23 elnnuz 12862 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
2423biimpi 215 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
25 oveq2 7412 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
2625oveq1d 7419 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
2725, 26oveq12d 7422 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
2825oveq1d 7419 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
2925, 28oveq12d 7422 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
3027, 29oveq12d 7422 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
31 elfznn 13526 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
32 2cnd 12286 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 2 ∈ ℂ)
33 nncn 12216 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
3432, 33mulcld 11230 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
35 1cnd 11205 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 1 ∈ ℂ)
3634, 35subcld 11567 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
37 1red 11211 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 ∈ ℝ)
38 1t1e1 12370 . . . . . . . . . . . . . . . . . . . . . 22 (1 · 1) = 1
3937, 37remulcld 11240 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
40 2re 12282 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
4140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 2 ∈ ℝ)
4241, 37remulcld 11240 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
43 nnre 12215 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
4441, 43remulcld 11240 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
45 1rp 12974 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ+
4645a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 ∈ ℝ+)
47 1lt2 12379 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 < 2
4847a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 < 2)
4937, 41, 46, 48ltmul1dd 13067 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
50 0le2 12310 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 2
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 0 ≤ 2)
52 nnge1 12236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 ≤ 𝑗)
5337, 43, 41, 51, 52lemul2ad 12150 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
5439, 42, 44, 49, 53ltletrd 11370 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
5538, 54eqbrtrrid 5183 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
5637, 55gtned 11345 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
5734, 35, 56subne0d 11576 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
5834, 36, 57divcld 11986 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
5934, 35addcld 11229 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
60 0red 11213 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 0 ∈ ℝ)
6144, 37readdcld 11239 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
6246rpgt0d 13015 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 0 < 1)
63 2rp 12975 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℝ+
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → 2 ∈ ℝ+)
65 nnrp 12981 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
6664, 65rpmulcld 13028 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
6737, 66ltaddrp2d 13046 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
6860, 37, 61, 62, 67lttrd 11371 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
6960, 68gtned 11345 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
7034, 59, 69divcld 11986 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
7158, 70mulcld 11230 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
7231, 71syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
733, 30, 31, 72fvmptd3 7017 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑛) → (𝐹𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
7463a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
7531nnrpd 13010 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
7674, 75rpmulcld 13028 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
7744, 37resubcld 11638 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
78 1m1e0 12280 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
7937, 44, 37, 55ltsub1dd 11822 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
8078, 79eqbrtrrid 5183 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
8177, 80elrpd 13009 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
8231, 81syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
8376, 82rpdivcld 13029 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
8440a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
8531nnred 12223 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
8684, 85remulcld 11240 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
8774rpge0d 13016 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
8875rpge0d 13016 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
8984, 85, 87, 88mulge0d 11787 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
9086, 89ge0p1rpd 13042 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
9176, 90rpdivcld 13029 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
9283, 91rpmulcld 13028 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
9373, 92eqeltrd 2834 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑛) → (𝐹𝑗) ∈ ℝ+)
9493adantl 483 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹𝑗) ∈ ℝ+)
95 rpmulcl 12993 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℝ+𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
9695adantl 483 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
9724, 94, 96seqcl 13984 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
9897rpcnd 13014 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
9997rpne0d 13017 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
10098, 99reccld 11979 . . . . . . . . . 10 (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
10122, 100mulcld 11230 . . . . . . . . 9 (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
1026, 101fmpti 7107 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
103102a1i 11 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
104103ffvelcdmda 7082 . . . . . 6 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
105 fveq2 6888 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
106105eleq1d 2819 . . . . . . . . . . . 12 (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
107106, 97vtoclga 3565 . . . . . . . . . . 11 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
108107rpcnd 13014 . . . . . . . . . 10 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
109107rpne0d 13017 . . . . . . . . . 10 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
11035, 108, 109divrecd 11989 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
11111a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → π ∈ ℂ)
11264rpne0d 13017 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 2 ≠ 0)
11315a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → π ≠ 0)
11432, 111, 112, 113divcan6d 12005 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
115114eqcomd 2739 . . . . . . . . . 10 (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
116115oveq1d 7419 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
11732, 111, 113divcld 11986 . . . . . . . . . 10 (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
118111halfcld 12453 . . . . . . . . . 10 (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
119108, 109reccld 11979 . . . . . . . . . 10 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
120117, 118, 119mulassd 11233 . . . . . . . . 9 (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
121110, 116, 1203eqtrd 2777 . . . . . . . 8 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
122 eqidd 2734 . . . . . . . . 9 (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
123105oveq2d 7420 . . . . . . . . . 10 (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
124123adantl 483 . . . . . . . . 9 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
125 id 22 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
126107rpreccld 13022 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
127122, 124, 125, 126fvmptd 7001 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
128 eqidd 2734 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
129124oveq2d 7420 . . . . . . . . . 10 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
130118, 119mulcld 11230 . . . . . . . . . 10 (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
131128, 129, 125, 130fvmptd 7001 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132131oveq2d 7420 . . . . . . . 8 (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
133121, 127, 1323eqtr4d 2783 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
134133adantl 483 . . . . . 6 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
1351, 2, 9, 17, 20, 104, 134climmulc2 15577 . . . . 5 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
136 2cn 12283 . . . . . . 7 2 ∈ ℂ
137136, 11, 15divcli 11952 . . . . . 6 (2 / π) ∈ ℂ
138137mulridi 11214 . . . . 5 ((2 / π) · 1) = (2 / π)
139135, 138breqtrdi 5188 . . . 4 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
140 2ne0 12312 . . . . . 6 2 ≠ 0
141136, 11, 140, 15divne0i 11958 . . . . 5 (2 / π) ≠ 0
142141a1i 11 . . . 4 (⊤ → (2 / π) ≠ 0)
143127, 119eqeltrd 2834 . . . . . 6 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
144108, 109recne0d 11980 . . . . . . . 8 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
145127, 144eqnetrd 3009 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
146 nelsn 4667 . . . . . . 7 (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
147145, 146syl 17 . . . . . 6 (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
148143, 147eldifd 3958 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
149148adantl 483 . . . 4 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
150108, 109recrecd 11983 . . . . . 6 (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
151122, 124, 125, 119fvmptd 7001 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
152151oveq2d 7420 . . . . . 6 (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
153 wallispi.2 . . . . . . 7 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
154105, 153, 97fvmpt3 6998 . . . . . 6 (𝑗 ∈ ℕ → (𝑊𝑗) = (seq1( · , 𝐹)‘𝑗))
155150, 152, 1543eqtr4rd 2784 . . . . 5 (𝑗 ∈ ℕ → (𝑊𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
156155adantl 483 . . . 4 ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
15718mptex 7220 . . . . . 6 (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
158153, 157eqeltri 2830 . . . . 5 𝑊 ∈ V
159158a1i 11 . . . 4 (⊤ → 𝑊 ∈ V)
1601, 2, 139, 142, 149, 156, 159climrec 44254 . . 3 (⊤ → 𝑊 ⇝ (1 / (2 / π)))
161160mptru 1549 . 2 𝑊 ⇝ (1 / (2 / π))
162 recdiv 11916 . . 3 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
163136, 140, 11, 15, 162mp4an 692 . 2 (1 / (2 / π)) = (π / 2)
164161, 163breqtri 5172 1 𝑊 ⇝ (π / 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397   = wceq 1542  wtru 1543  wcel 2107  wne 2941  Vcvv 3475  cdif 3944  {csn 4627   class class class wbr 5147  cmpt 5230  wf 6536  cfv 6540  (class class class)co 7404  cc 11104  cr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244  cle 11245  cmin 11440   / cdiv 11867  cn 12208  2c2 12263  0cn0 12468  cuz 12818  +crp 12970  (,)cioo 13320  ...cfz 13480  seqcseq 13962  cexp 14023  cli 15424  sincsin 16003  πcpi 16006  citg 25117
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cc 10426  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-symdif 4241  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-ofr 7666  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-omul 8466  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19643  df-psmet 20921  df-xmet 20922  df-met 20923  df-bl 20924  df-mopn 20925  df-fbas 20926  df-fg 20927  df-cnfld 20930  df-top 22378  df-topon 22395  df-topsp 22417  df-bases 22431  df-cld 22505  df-ntr 22506  df-cls 22507  df-nei 22584  df-lp 22622  df-perf 22623  df-cn 22713  df-cnp 22714  df-haus 22801  df-cmp 22873  df-tx 23048  df-hmeo 23241  df-fil 23332  df-fm 23424  df-flim 23425  df-flf 23426  df-xms 23808  df-ms 23809  df-tms 23810  df-cncf 24376  df-ovol 24963  df-vol 24964  df-mbf 25118  df-itg1 25119  df-itg2 25120  df-ibl 25121  df-itg 25122  df-0p 25169  df-limc 25365  df-dv 25366
This theorem is referenced by:  wallispi2  44724
  Copyright terms: Public domain W3C validator