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 42240
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 12275 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12007 . . . 4 (⊤ → 1 ∈ ℤ)
3 wallispi.1 . . . . . . . 8 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
4 eqid 2826 . . . . . . . 8 (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥) = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
5 eqid 2826 . . . . . . . 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 2826 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
7 eqid 2826 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))) = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
83, 4, 5, 6, 7wallispilem5 42239 . . . . . . 7 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1
98a1i 11 . . . . . 6 (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) ⇝ 1)
10 2cnd 11709 . . . . . . 7 (⊤ → 2 ∈ ℂ)
11 picn 24979 . . . . . . . 8 π ∈ ℂ
1211a1i 11 . . . . . . 7 (⊤ → π ∈ ℂ)
13 pire 24978 . . . . . . . . 9 π ∈ ℝ
14 pipos 24980 . . . . . . . . 9 0 < π
1513, 14gt0ne0ii 11170 . . . . . . . 8 π ≠ 0
1615a1i 11 . . . . . . 7 (⊤ → π ≠ 0)
1710, 12, 16divcld 11410 . . . . . 6 (⊤ → (2 / π) ∈ ℂ)
18 nnex 11638 . . . . . . . 8 ℕ ∈ V
1918mptex 6983 . . . . . . 7 (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V
2019a1i 11 . . . . . 6 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ∈ V)
2111a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → π ∈ ℂ)
2221halfcld 11876 . . . . . . . . . 10 (𝑛 ∈ ℕ → (π / 2) ∈ ℂ)
23 elnnuz 12276 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘1))
2423biimpi 217 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
25 oveq2 7158 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
2625oveq1d 7165 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((2 · 𝑘) − 1) = ((2 · 𝑗) − 1))
2725, 26oveq12d 7168 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑗) / ((2 · 𝑗) − 1)))
2825oveq1d 7165 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1))
2925, 28oveq12d 7168 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑗) / ((2 · 𝑗) + 1)))
3027, 29oveq12d 7168 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
31 elfznn 12931 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℕ)
32 2cnd 11709 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 2 ∈ ℂ)
33 nncn 11640 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
3432, 33mulcld 10655 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℂ)
35 1cnd 10630 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 1 ∈ ℂ)
3634, 35subcld 10991 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℂ)
37 1red 10636 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 ∈ ℝ)
38 1t1e1 11793 . . . . . . . . . . . . . . . . . . . . . 22 (1 · 1) = 1
3937, 37remulcld 10665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (1 · 1) ∈ ℝ)
40 2re 11705 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
4140a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 2 ∈ ℝ)
4241, 37remulcld 10665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 1) ∈ ℝ)
43 nnre 11639 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
4441, 43remulcld 10665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ)
45 1rp 12388 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ+
4645a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 ∈ ℝ+)
47 1lt2 11802 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 < 2
4847a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 < 2)
4937, 41, 46, 48ltmul1dd 12481 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (1 · 1) < (2 · 1))
50 0le2 11733 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 2
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 0 ≤ 2)
52 nnge1 11659 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ ℕ → 1 ≤ 𝑗)
5337, 43, 41, 51, 52lemul2ad 11574 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → (2 · 1) ≤ (2 · 𝑗))
5439, 42, 44, 49, 53ltletrd 10794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ → (1 · 1) < (2 · 𝑗))
5538, 54eqbrtrrid 5099 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 < (2 · 𝑗))
5637, 55gtned 10769 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (2 · 𝑗) ≠ 1)
5734, 35, 56subne0d 11000 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ≠ 0)
5834, 36, 57divcld 11410 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℂ)
5934, 35addcld 10654 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℂ)
60 0red 10638 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 0 ∈ ℝ)
6144, 37readdcld 10664 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ∈ ℝ)
6246rpgt0d 12429 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 0 < 1)
63 2rp 12389 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℝ+
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → 2 ∈ ℝ+)
65 nnrp 12395 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
6664, 65rpmulcld 12442 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℕ → (2 · 𝑗) ∈ ℝ+)
6737, 66ltaddrp2d 12460 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℕ → 1 < ((2 · 𝑗) + 1))
6860, 37, 61, 62, 67lttrd 10795 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) + 1))
6960, 68gtned 10769 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) + 1) ≠ 0)
7034, 59, 69divcld 11410 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℂ)
7158, 70mulcld 10655 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℕ → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
7231, 71syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℂ)
733, 30, 31, 72fvmptd3 6789 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑛) → (𝐹𝑗) = (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))))
7463a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ+)
7531nnrpd 12424 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ+)
7674, 75rpmulcld 12442 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ+)
7744, 37resubcld 11062 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ)
78 1m1e0 11703 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
7937, 44, 37, 55ltsub1dd 11246 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℕ → (1 − 1) < ((2 · 𝑗) − 1))
8078, 79eqbrtrrid 5099 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ → 0 < ((2 · 𝑗) − 1))
8177, 80elrpd 12423 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ → ((2 · 𝑗) − 1) ∈ ℝ+)
8231, 81syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) − 1) ∈ ℝ+)
8376, 82rpdivcld 12443 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) − 1)) ∈ ℝ+)
8440a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 2 ∈ ℝ)
8531nnred 11647 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 𝑗 ∈ ℝ)
8684, 85remulcld 10665 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → (2 · 𝑗) ∈ ℝ)
8774rpge0d 12430 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 0 ≤ 2)
8875rpge0d 12430 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑛) → 0 ≤ 𝑗)
8984, 85, 87, 88mulge0d 11211 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (1...𝑛) → 0 ≤ (2 · 𝑗))
9086, 89ge0p1rpd 12456 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) + 1) ∈ ℝ+)
9176, 90rpdivcld 12443 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑛) → ((2 · 𝑗) / ((2 · 𝑗) + 1)) ∈ ℝ+)
9283, 91rpmulcld 12442 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑛) → (((2 · 𝑗) / ((2 · 𝑗) − 1)) · ((2 · 𝑗) / ((2 · 𝑗) + 1))) ∈ ℝ+)
9373, 92eqeltrd 2918 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑛) → (𝐹𝑗) ∈ ℝ+)
9493adantl 482 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...𝑛)) → (𝐹𝑗) ∈ ℝ+)
95 rpmulcl 12407 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℝ+𝑤 ∈ ℝ+) → (𝑗 · 𝑤) ∈ ℝ+)
9695adantl 482 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ (𝑗 ∈ ℝ+𝑤 ∈ ℝ+)) → (𝑗 · 𝑤) ∈ ℝ+)
9724, 94, 96seqcl 13385 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℝ+)
9897rpcnd 12428 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ∈ ℂ)
9997rpne0d 12431 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (seq1( · , 𝐹)‘𝑛) ≠ 0)
10098, 99reccld 11403 . . . . . . . . . 10 (𝑛 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑛)) ∈ ℂ)
10122, 100mulcld 10655 . . . . . . . . 9 (𝑛 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) ∈ ℂ)
1026, 101fmpti 6874 . . . . . . . 8 (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ
103102a1i 11 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))):ℕ⟶ℂ)
104103ffvelrnda 6849 . . . . . 6 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) ∈ ℂ)
105 fveq2 6669 . . . . . . . . . . . . 13 (𝑛 = 𝑗 → (seq1( · , 𝐹)‘𝑛) = (seq1( · , 𝐹)‘𝑗))
106105eleq1d 2902 . . . . . . . . . . . 12 (𝑛 = 𝑗 → ((seq1( · , 𝐹)‘𝑛) ∈ ℝ+ ↔ (seq1( · , 𝐹)‘𝑗) ∈ ℝ+))
107106, 97vtoclga 3579 . . . . . . . . . . 11 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℝ+)
108107rpcnd 12428 . . . . . . . . . 10 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ∈ ℂ)
109107rpne0d 12431 . . . . . . . . . 10 (𝑗 ∈ ℕ → (seq1( · , 𝐹)‘𝑗) ≠ 0)
11035, 108, 109divrecd 11413 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = (1 · (1 / (seq1( · , 𝐹)‘𝑗))))
11111a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → π ∈ ℂ)
11264rpne0d 12431 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 2 ≠ 0)
11315a1i 11 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → π ≠ 0)
11432, 111, 112, 113divcan6d 11429 . . . . . . . . . . 11 (𝑗 ∈ ℕ → ((2 / π) · (π / 2)) = 1)
115114eqcomd 2832 . . . . . . . . . 10 (𝑗 ∈ ℕ → 1 = ((2 / π) · (π / 2)))
116115oveq1d 7165 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 · (1 / (seq1( · , 𝐹)‘𝑗))) = (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))))
11732, 111, 113divcld 11410 . . . . . . . . . 10 (𝑗 ∈ ℕ → (2 / π) ∈ ℂ)
118111halfcld 11876 . . . . . . . . . 10 (𝑗 ∈ ℕ → (π / 2) ∈ ℂ)
119108, 109reccld 11403 . . . . . . . . . 10 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℂ)
120117, 118, 119mulassd 10658 . . . . . . . . 9 (𝑗 ∈ ℕ → (((2 / π) · (π / 2)) · (1 / (seq1( · , 𝐹)‘𝑗))) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
121110, 116, 1203eqtrd 2865 . . . . . . . 8 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
122 eqidd 2827 . . . . . . . . 9 (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))))
123105oveq2d 7166 . . . . . . . . . 10 (𝑛 = 𝑗 → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
124123adantl 482 . . . . . . . . 9 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (seq1( · , 𝐹)‘𝑛)) = (1 / (seq1( · , 𝐹)‘𝑗)))
125 id 22 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
126107rpreccld 12436 . . . . . . . . 9 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ∈ ℝ+)
127122, 124, 125, 126fvmptd 6773 . . . . . . . 8 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
128 eqidd 2827 . . . . . . . . . 10 (𝑗 ∈ ℕ → (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
129124oveq2d 7166 . . . . . . . . . 10 ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
130118, 119mulcld 10655 . . . . . . . . . 10 (𝑗 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))) ∈ ℂ)
131128, 129, 125, 130fvmptd 6773 . . . . . . . . 9 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗))))
132131oveq2d 7166 . . . . . . . 8 (𝑗 ∈ ℕ → ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)) = ((2 / π) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑗)))))
133121, 127, 1323eqtr4d 2871 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
134133adantl 482 . . . . . 6 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = ((2 / π) · ((𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))‘𝑗)))
1351, 2, 9, 17, 20, 104, 134climmulc2 14988 . . . . 5 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ ((2 / π) · 1))
136 2cn 11706 . . . . . . 7 2 ∈ ℂ
137136, 11, 15divcli 11376 . . . . . 6 (2 / π) ∈ ℂ
138137mulid1i 10639 . . . . 5 ((2 / π) · 1) = (2 / π)
139135, 138breqtrdi 5104 . . . 4 (⊤ → (𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛))) ⇝ (2 / π))
140 2ne0 11735 . . . . . 6 2 ≠ 0
141136, 11, 140, 15divne0i 11382 . . . . 5 (2 / π) ≠ 0
142141a1i 11 . . . 4 (⊤ → (2 / π) ≠ 0)
143127, 119eqeltrd 2918 . . . . . 6 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ ℂ)
144108, 109recne0d 11404 . . . . . . . 8 (𝑗 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑗)) ≠ 0)
145127, 144eqnetrd 3088 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0)
146 nelsn 4602 . . . . . . 7 (((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ≠ 0 → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
147145, 146syl 17 . . . . . 6 (𝑗 ∈ ℕ → ¬ ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ {0})
148143, 147eldifd 3951 . . . . 5 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
149148adantl 482 . . . 4 ((⊤ ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) ∈ (ℂ ∖ {0}))
150108, 109recrecd 11407 . . . . . 6 (𝑗 ∈ ℕ → (1 / (1 / (seq1( · , 𝐹)‘𝑗))) = (seq1( · , 𝐹)‘𝑗))
151122, 124, 125, 119fvmptd 6773 . . . . . . 7 (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗) = (1 / (seq1( · , 𝐹)‘𝑗)))
152151oveq2d 7166 . . . . . 6 (𝑗 ∈ ℕ → (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)) = (1 / (1 / (seq1( · , 𝐹)‘𝑗))))
153 wallispi.2 . . . . . . 7 𝑊 = (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛))
154105, 153, 97fvmpt3 6771 . . . . . 6 (𝑗 ∈ ℕ → (𝑊𝑗) = (seq1( · , 𝐹)‘𝑗))
155150, 152, 1543eqtr4rd 2872 . . . . 5 (𝑗 ∈ ℕ → (𝑊𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
156155adantl 482 . . . 4 ((⊤ ∧ 𝑗 ∈ ℕ) → (𝑊𝑗) = (1 / ((𝑛 ∈ ℕ ↦ (1 / (seq1( · , 𝐹)‘𝑛)))‘𝑗)))
15718mptex 6983 . . . . . 6 (𝑛 ∈ ℕ ↦ (seq1( · , 𝐹)‘𝑛)) ∈ V
158153, 157eqeltri 2914 . . . . 5 𝑊 ∈ V
159158a1i 11 . . . 4 (⊤ → 𝑊 ∈ V)
1601, 2, 139, 142, 149, 156, 159climrec 41768 . . 3 (⊤ → 𝑊 ⇝ (1 / (2 / π)))
161160mptru 1537 . 2 𝑊 ⇝ (1 / (2 / π))
162 recdiv 11340 . . 3 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (1 / (2 / π)) = (π / 2))
163136, 140, 11, 15, 162mp4an 689 . 2 (1 / (2 / π)) = (π / 2)
164161, 163breqtri 5088 1 𝑊 ⇝ (π / 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 396   = wceq 1530  wtru 1531  wcel 2107  wne 3021  Vcvv 3500  cdif 3937  {csn 4564   class class class wbr 5063  cmpt 5143  wf 6350  cfv 6354  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536   < clt 10669  cle 10670  cmin 10864   / cdiv 11291  cn 11632  2c2 11686  0cn0 11891  cuz 12237  +crp 12384  (,)cioo 12733  ...cfz 12887  seqcseq 13364  cexp 13424  cli 14836  sincsin 15412  πcpi 15415  citg 24153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098  ax-cc 9851  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-symdif 4223  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-disj 5029  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-ofr 7404  df-om 7574  df-1st 7685  df-2nd 7686  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8284  df-map 8403  df-pm 8404  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-fi 8869  df-sup 8900  df-inf 8901  df-oi 8968  df-dju 9324  df-card 9362  df-acn 9365  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-q 12343  df-rp 12385  df-xneg 12502  df-xadd 12503  df-xmul 12504  df-ioo 12737  df-ioc 12738  df-ico 12739  df-icc 12740  df-fz 12888  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13425  df-fac 13629  df-bc 13658  df-hash 13686  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-ef 15416  df-sin 15418  df-cos 15419  df-pi 15421  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18170  df-cntz 18392  df-cmn 18844  df-psmet 20472  df-xmet 20473  df-met 20474  df-bl 20475  df-mopn 20476  df-fbas 20477  df-fg 20478  df-cnfld 20481  df-top 21437  df-topon 21454  df-topsp 21476  df-bases 21489  df-cld 21562  df-ntr 21563  df-cls 21564  df-nei 21641  df-lp 21679  df-perf 21680  df-cn 21770  df-cnp 21771  df-haus 21858  df-cmp 21930  df-tx 22105  df-hmeo 22298  df-fil 22389  df-fm 22481  df-flim 22482  df-flf 22483  df-xms 22864  df-ms 22865  df-tms 22866  df-cncf 23420  df-ovol 23999  df-vol 24000  df-mbf 24154  df-itg1 24155  df-itg2 24156  df-ibl 24157  df-itg 24158  df-0p 24205  df-limc 24398  df-dv 24399
This theorem is referenced by:  wallispi2  42243
  Copyright terms: Public domain W3C validator