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

Theorem wallispilem5 43285
Description: The sequence 𝐻 converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Hypotheses
Ref Expression
wallispilem5.1 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
wallispilem5.2 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
wallispilem5.3 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
wallispilem5.4 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
wallispilem5.5 𝐿 = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
Assertion
Ref Expression
wallispilem5 𝐻 ⇝ 1
Distinct variable groups:   𝑘,𝑛,𝑥   𝑥,𝐹   𝑘,𝐺   𝑘,𝐿
Allowed substitution hints:   𝐹(𝑘,𝑛)   𝐺(𝑥,𝑛)   𝐻(𝑥,𝑘,𝑛)   𝐼(𝑥,𝑘,𝑛)   𝐿(𝑥,𝑛)

Proof of Theorem wallispilem5
StepHypRef Expression
1 wallispilem5.1 . . 3 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
2 wallispilem5.2 . . 3 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
3 wallispilem5.3 . . 3 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
4 wallispilem5.4 . . 3 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
51, 2, 3, 4wallispilem4 43284 . 2 𝐺 = 𝐻
6 nnuz 12477 . . . 4 ℕ = (ℤ‘1)
7 1zzd 12208 . . . 4 (⊤ → 1 ∈ ℤ)
8 wallispilem5.5 . . . . 5 𝐿 = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛)))
9 2cnd 11908 . . . . 5 (⊤ → 2 ∈ ℂ)
10 2ne0 11934 . . . . . 6 2 ≠ 0
1110a1i 11 . . . . 5 (⊤ → 2 ≠ 0)
12 1cnd 10828 . . . . 5 (⊤ → 1 ∈ ℂ)
138, 9, 11, 12clim1fr1 42817 . . . 4 (⊤ → 𝐿 ⇝ 1)
14 nnex 11836 . . . . . . 7 ℕ ∈ V
1514mptex 7039 . . . . . 6 (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) ∈ V
163, 15eqeltri 2834 . . . . 5 𝐺 ∈ V
1716a1i 11 . . . 4 (⊤ → 𝐺 ∈ V)
18 2nn0 12107 . . . . . . . . . . . 12 2 ∈ ℕ0
1918a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 2 ∈ ℕ0)
20 nnnn0 12097 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
2119, 20nn0mulcld 12155 . . . . . . . . . 10 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ0)
22 1nn0 12106 . . . . . . . . . . 11 1 ∈ ℕ0
2322a1i 11 . . . . . . . . . 10 (𝑛 ∈ ℕ → 1 ∈ ℕ0)
2421, 23nn0addcld 12154 . . . . . . . . 9 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ0)
2524nn0red 12151 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ)
2621nn0red 12151 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℝ)
27 2cnd 11908 . . . . . . . . 9 (𝑛 ∈ ℕ → 2 ∈ ℂ)
28 nncn 11838 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
2910a1i 11 . . . . . . . . 9 (𝑛 ∈ ℕ → 2 ≠ 0)
30 nnne0 11864 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
3127, 28, 29, 30mulne0d 11484 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ≠ 0)
3225, 26, 31redivcld 11660 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (2 · 𝑛)) ∈ ℝ)
338, 32fmpti 6929 . . . . . 6 𝐿:ℕ⟶ℝ
3433a1i 11 . . . . 5 (⊤ → 𝐿:ℕ⟶ℝ)
3534ffvelrnda 6904 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿𝑘) ∈ ℝ)
362wallispilem3 43283 . . . . . . . . . 10 ((2 · 𝑛) ∈ ℕ0 → (𝐼‘(2 · 𝑛)) ∈ ℝ+)
3721, 36syl 17 . . . . . . . . 9 (𝑛 ∈ ℕ → (𝐼‘(2 · 𝑛)) ∈ ℝ+)
3837rpred 12628 . . . . . . . 8 (𝑛 ∈ ℕ → (𝐼‘(2 · 𝑛)) ∈ ℝ)
392wallispilem3 43283 . . . . . . . . 9 (((2 · 𝑛) + 1) ∈ ℕ0 → (𝐼‘((2 · 𝑛) + 1)) ∈ ℝ+)
4024, 39syl 17 . . . . . . . 8 (𝑛 ∈ ℕ → (𝐼‘((2 · 𝑛) + 1)) ∈ ℝ+)
4138, 40rerpdivcld 12659 . . . . . . 7 (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) ∈ ℝ)
423, 41fmpti 6929 . . . . . 6 𝐺:ℕ⟶ℝ
4342a1i 11 . . . . 5 (⊤ → 𝐺:ℕ⟶ℝ)
4443ffvelrnda 6904 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
4518a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 2 ∈ ℕ0)
46 nnnn0 12097 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
4745, 46nn0mulcld 12155 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ0)
482wallispilem3 43283 . . . . . . . . . 10 ((2 · 𝑘) ∈ ℕ0 → (𝐼‘(2 · 𝑘)) ∈ ℝ+)
4947, 48syl 17 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐼‘(2 · 𝑘)) ∈ ℝ+)
5049rpred 12628 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐼‘(2 · 𝑘)) ∈ ℝ)
51 2nn 11903 . . . . . . . . . . . . 13 2 ∈ ℕ
5251a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℕ)
53 id 22 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
5452, 53nnmulcld 11883 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
55 nnm1nn0 12131 . . . . . . . . . . 11 ((2 · 𝑘) ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ0)
5654, 55syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) ∈ ℕ0)
572wallispilem3 43283 . . . . . . . . . 10 (((2 · 𝑘) − 1) ∈ ℕ0 → (𝐼‘((2 · 𝑘) − 1)) ∈ ℝ+)
5856, 57syl 17 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) − 1)) ∈ ℝ+)
5958rpred 12628 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) − 1)) ∈ ℝ)
6022a1i 11 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ∈ ℕ0)
6147, 60nn0addcld 12154 . . . . . . . . 9 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℕ0)
622wallispilem3 43283 . . . . . . . . 9 (((2 · 𝑘) + 1) ∈ ℕ0 → (𝐼‘((2 · 𝑘) + 1)) ∈ ℝ+)
6361, 62syl 17 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) ∈ ℝ+)
64 2cnd 11908 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℂ)
65 nncn 11838 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
6664, 65mulcld 10853 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
67 1cnd 10828 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 1 ∈ ℂ)
6866, 67npcand 11193 . . . . . . . . . 10 (𝑘 ∈ ℕ → (((2 · 𝑘) − 1) + 1) = (2 · 𝑘))
6968fveq2d 6721 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐼‘(((2 · 𝑘) − 1) + 1)) = (𝐼‘(2 · 𝑘)))
702, 56wallispilem1 43281 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐼‘(((2 · 𝑘) − 1) + 1)) ≤ (𝐼‘((2 · 𝑘) − 1)))
7169, 70eqbrtrrd 5077 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐼‘(2 · 𝑘)) ≤ (𝐼‘((2 · 𝑘) − 1)))
7250, 59, 63, 71lediv1dd 12686 . . . . . . 7 (𝑘 ∈ ℕ → ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))) ≤ ((𝐼‘((2 · 𝑘) − 1)) / (𝐼‘((2 · 𝑘) + 1))))
7366, 67addcld 10852 . . . . . . . . . 10 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
7410a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 2 ≠ 0)
75 nnne0 11864 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
7664, 65, 74, 75mulne0d 11484 . . . . . . . . . 10 (𝑘 ∈ ℕ → (2 · 𝑘) ≠ 0)
7773, 66, 76divcld 11608 . . . . . . . . 9 (𝑘 ∈ ℕ → (((2 · 𝑘) + 1) / (2 · 𝑘)) ∈ ℂ)
7863rpcnd 12630 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) ∈ ℂ)
7963rpne0d 12633 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) ≠ 0)
8077, 78, 79divcan4d 11614 . . . . . . . 8 (𝑘 ∈ ℕ → (((((2 · 𝑘) + 1) / (2 · 𝑘)) · (𝐼‘((2 · 𝑘) + 1))) / (𝐼‘((2 · 𝑘) + 1))) = (((2 · 𝑘) + 1) / (2 · 𝑘)))
81 2re 11904 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
8281a1i 11 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → 2 ∈ ℝ)
83 nnre 11837 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
8482, 83remulcld 10863 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
85 1red 10834 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 1 ∈ ℝ)
8684, 85readdcld 10862 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
8745nn0ge0d 12153 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 0 ≤ 2)
88 nnge1 11858 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
8982, 83, 87, 88lemulge11d 11769 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 2 ≤ (2 · 𝑘))
9084ltp1d 11762 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
9182, 84, 86, 89, 90lelttrd 10990 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → 2 < ((2 · 𝑘) + 1))
9282, 86, 91ltled 10980 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 2 ≤ ((2 · 𝑘) + 1))
9345nn0zd 12280 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → 2 ∈ ℤ)
9461nn0zd 12280 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℤ)
95 eluz 12452 . . . . . . . . . . . . . . 15 ((2 ∈ ℤ ∧ ((2 · 𝑘) + 1) ∈ ℤ) → (((2 · 𝑘) + 1) ∈ (ℤ‘2) ↔ 2 ≤ ((2 · 𝑘) + 1)))
9693, 94, 95syl2anc 587 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (((2 · 𝑘) + 1) ∈ (ℤ‘2) ↔ 2 ≤ ((2 · 𝑘) + 1)))
9792, 96mpbird 260 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ (ℤ‘2))
982, 97itgsinexp 43171 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) = (((((2 · 𝑘) + 1) − 1) / ((2 · 𝑘) + 1)) · (𝐼‘(((2 · 𝑘) + 1) − 2))))
9966, 67pncand 11190 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
10099oveq1d 7228 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → ((((2 · 𝑘) + 1) − 1) / ((2 · 𝑘) + 1)) = ((2 · 𝑘) / ((2 · 𝑘) + 1)))
101 1e2m1 11957 . . . . . . . . . . . . . . . . 17 1 = (2 − 1)
102101a1i 11 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 1 = (2 − 1))
103102oveq2d 7229 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → ((2 · 𝑘) − 1) = ((2 · 𝑘) − (2 − 1)))
10466, 64, 67subsub3d 11219 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → ((2 · 𝑘) − (2 − 1)) = (((2 · 𝑘) + 1) − 2))
105103, 104eqtr2d 2778 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (((2 · 𝑘) + 1) − 2) = ((2 · 𝑘) − 1))
106105fveq2d 6721 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐼‘(((2 · 𝑘) + 1) − 2)) = (𝐼‘((2 · 𝑘) − 1)))
107100, 106oveq12d 7231 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (((((2 · 𝑘) + 1) − 1) / ((2 · 𝑘) + 1)) · (𝐼‘(((2 · 𝑘) + 1) − 2))) = (((2 · 𝑘) / ((2 · 𝑘) + 1)) · (𝐼‘((2 · 𝑘) − 1))))
10898, 107eqtrd 2777 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) = (((2 · 𝑘) / ((2 · 𝑘) + 1)) · (𝐼‘((2 · 𝑘) − 1))))
109108oveq2d 7229 . . . . . . . . . 10 (𝑘 ∈ ℕ → ((((2 · 𝑘) + 1) / (2 · 𝑘)) · (𝐼‘((2 · 𝑘) + 1))) = ((((2 · 𝑘) + 1) / (2 · 𝑘)) · (((2 · 𝑘) / ((2 · 𝑘) + 1)) · (𝐼‘((2 · 𝑘) − 1)))))
11054peano2nnd 11847 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℕ)
111110nnne0d 11880 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
11266, 73, 111divcld 11608 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((2 · 𝑘) / ((2 · 𝑘) + 1)) ∈ ℂ)
11358rpcnd 12630 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) − 1)) ∈ ℂ)
11477, 112, 113mulassd 10856 . . . . . . . . . 10 (𝑘 ∈ ℕ → (((((2 · 𝑘) + 1) / (2 · 𝑘)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) · (𝐼‘((2 · 𝑘) − 1))) = ((((2 · 𝑘) + 1) / (2 · 𝑘)) · (((2 · 𝑘) / ((2 · 𝑘) + 1)) · (𝐼‘((2 · 𝑘) − 1)))))
11573, 66, 111, 76divcan6d 11627 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((((2 · 𝑘) + 1) / (2 · 𝑘)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = 1)
116115oveq1d 7228 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (((((2 · 𝑘) + 1) / (2 · 𝑘)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) · (𝐼‘((2 · 𝑘) − 1))) = (1 · (𝐼‘((2 · 𝑘) − 1))))
117113mulid2d 10851 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 · (𝐼‘((2 · 𝑘) − 1))) = (𝐼‘((2 · 𝑘) − 1)))
118116, 117eqtrd 2777 . . . . . . . . . 10 (𝑘 ∈ ℕ → (((((2 · 𝑘) + 1) / (2 · 𝑘)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) · (𝐼‘((2 · 𝑘) − 1))) = (𝐼‘((2 · 𝑘) − 1)))
119109, 114, 1183eqtr2d 2783 . . . . . . . . 9 (𝑘 ∈ ℕ → ((((2 · 𝑘) + 1) / (2 · 𝑘)) · (𝐼‘((2 · 𝑘) + 1))) = (𝐼‘((2 · 𝑘) − 1)))
120119oveq1d 7228 . . . . . . . 8 (𝑘 ∈ ℕ → (((((2 · 𝑘) + 1) / (2 · 𝑘)) · (𝐼‘((2 · 𝑘) + 1))) / (𝐼‘((2 · 𝑘) + 1))) = ((𝐼‘((2 · 𝑘) − 1)) / (𝐼‘((2 · 𝑘) + 1))))
12180, 120eqtr3d 2779 . . . . . . 7 (𝑘 ∈ ℕ → (((2 · 𝑘) + 1) / (2 · 𝑘)) = ((𝐼‘((2 · 𝑘) − 1)) / (𝐼‘((2 · 𝑘) + 1))))
12272, 121breqtrrd 5081 . . . . . 6 (𝑘 ∈ ℕ → ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))) ≤ (((2 · 𝑘) + 1) / (2 · 𝑘)))
12349, 63rpdivcld 12645 . . . . . . 7 (𝑘 ∈ ℕ → ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))) ∈ ℝ+)
124 nfcv 2904 . . . . . . . 8 𝑛𝑘
125 nfmpt1 5153 . . . . . . . . . . 11 𝑛(𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑥)↑𝑛) d𝑥)
1262, 125nfcxfr 2902 . . . . . . . . . 10 𝑛𝐼
127 nfcv 2904 . . . . . . . . . 10 𝑛(2 · 𝑘)
128126, 127nffv 6727 . . . . . . . . 9 𝑛(𝐼‘(2 · 𝑘))
129 nfcv 2904 . . . . . . . . 9 𝑛 /
130 nfcv 2904 . . . . . . . . . 10 𝑛((2 · 𝑘) + 1)
131126, 130nffv 6727 . . . . . . . . 9 𝑛(𝐼‘((2 · 𝑘) + 1))
132128, 129, 131nfov 7243 . . . . . . . 8 𝑛((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1)))
133 oveq2 7221 . . . . . . . . . 10 (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
134133fveq2d 6721 . . . . . . . . 9 (𝑛 = 𝑘 → (𝐼‘(2 · 𝑛)) = (𝐼‘(2 · 𝑘)))
135133fvoveq1d 7235 . . . . . . . . 9 (𝑛 = 𝑘 → (𝐼‘((2 · 𝑛) + 1)) = (𝐼‘((2 · 𝑘) + 1)))
136134, 135oveq12d 7231 . . . . . . . 8 (𝑛 = 𝑘 → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))))
137124, 132, 136, 3fvmptf 6839 . . . . . . 7 ((𝑘 ∈ ℕ ∧ ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))) ∈ ℝ+) → (𝐺𝑘) = ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))))
138123, 137mpdan 687 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) = ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))))
1398a1i 11 . . . . . . 7 (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (((2 · 𝑛) + 1) / (2 · 𝑛))))
140 simpr 488 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
141140oveq2d 7229 . . . . . . . . 9 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
142141oveq1d 7228 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
143142, 141oveq12d 7231 . . . . . . 7 ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (((2 · 𝑛) + 1) / (2 · 𝑛)) = (((2 · 𝑘) + 1) / (2 · 𝑘)))
144139, 143, 53, 77fvmptd 6825 . . . . . 6 (𝑘 ∈ ℕ → (𝐿𝑘) = (((2 · 𝑘) + 1) / (2 · 𝑘)))
145122, 138, 1443brtr4d 5085 . . . . 5 (𝑘 ∈ ℕ → (𝐺𝑘) ≤ (𝐿𝑘))
146145adantl 485 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐿𝑘))
14778, 79dividd 11606 . . . . . . 7 (𝑘 ∈ ℕ → ((𝐼‘((2 · 𝑘) + 1)) / (𝐼‘((2 · 𝑘) + 1))) = 1)
14863rpred 12628 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) ∈ ℝ)
1492, 47wallispilem1 43281 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐼‘((2 · 𝑘) + 1)) ≤ (𝐼‘(2 · 𝑘)))
150148, 50, 63, 149lediv1dd 12686 . . . . . . 7 (𝑘 ∈ ℕ → ((𝐼‘((2 · 𝑘) + 1)) / (𝐼‘((2 · 𝑘) + 1))) ≤ ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))))
151147, 150eqbrtrrd 5077 . . . . . 6 (𝑘 ∈ ℕ → 1 ≤ ((𝐼‘(2 · 𝑘)) / (𝐼‘((2 · 𝑘) + 1))))
152151, 138breqtrrd 5081 . . . . 5 (𝑘 ∈ ℕ → 1 ≤ (𝐺𝑘))
153152adantl 485 . . . 4 ((⊤ ∧ 𝑘 ∈ ℕ) → 1 ≤ (𝐺𝑘))
1546, 7, 13, 17, 35, 44, 146, 153climsqz2 15203 . . 3 (⊤ → 𝐺 ⇝ 1)
155154mptru 1550 . 2 𝐺 ⇝ 1
1565, 155eqbrtrri 5076 1 𝐻 ⇝ 1
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1543  wtru 1544  wcel 2110  wne 2940  Vcvv 3408   class class class wbr 5053  cmpt 5135  wf 6376  cfv 6380  (class class class)co 7213  cc 10727  cr 10728  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  cle 10868  cmin 11062   / cdiv 11489  cn 11830  2c2 11885  0cn0 12090  cz 12176  cuz 12438  +crp 12586  (,)cioo 12935  seqcseq 13574  cexp 13635  cli 15045  sincsin 15625  πcpi 15628  citg 24515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cc 10049  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807  ax-addf 10808  ax-mulf 10809
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-symdif 4157  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-disj 5019  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-ofr 7470  df-om 7645  df-1st 7761  df-2nd 7762  df-supp 7904  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-oadd 8206  df-omul 8207  df-er 8391  df-map 8510  df-pm 8511  df-ixp 8579  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fsupp 8986  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-dju 9517  df-card 9555  df-acn 9558  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-z 12177  df-dec 12294  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ioc 12940  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-mod 13443  df-seq 13575  df-exp 13636  df-fac 13840  df-bc 13869  df-hash 13897  df-shft 14630  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-limsup 15032  df-clim 15049  df-rlim 15050  df-sum 15250  df-ef 15629  df-sin 15631  df-cos 15632  df-pi 15634  df-struct 16700  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-ress 16785  df-plusg 16815  df-mulr 16816  df-starv 16817  df-sca 16818  df-vsca 16819  df-ip 16820  df-tset 16821  df-ple 16822  df-ds 16824  df-unif 16825  df-hom 16826  df-cco 16827  df-rest 16927  df-topn 16928  df-0g 16946  df-gsum 16947  df-topgen 16948  df-pt 16949  df-prds 16952  df-xrs 17007  df-qtop 17012  df-imas 17013  df-xps 17015  df-mre 17089  df-mrc 17090  df-acs 17092  df-mgm 18114  df-sgrp 18163  df-mnd 18174  df-submnd 18219  df-mulg 18489  df-cntz 18711  df-cmn 19172  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-fbas 20360  df-fg 20361  df-cnfld 20364  df-top 21791  df-topon 21808  df-topsp 21830  df-bases 21843  df-cld 21916  df-ntr 21917  df-cls 21918  df-nei 21995  df-lp 22033  df-perf 22034  df-cn 22124  df-cnp 22125  df-haus 22212  df-cmp 22284  df-tx 22459  df-hmeo 22652  df-fil 22743  df-fm 22835  df-flim 22836  df-flf 22837  df-xms 23218  df-ms 23219  df-tms 23220  df-cncf 23775  df-ovol 24361  df-vol 24362  df-mbf 24516  df-itg1 24517  df-itg2 24518  df-ibl 24519  df-itg 24520  df-0p 24567  df-limc 24763  df-dv 24764
This theorem is referenced by:  wallispi  43286
  Copyright terms: Public domain W3C validator