Metamath Proof Explorer

Theorem wallispilem5

Description: The sequence H converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses wallispilem5.1 ⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
wallispilem5.2 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
wallispilem5.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) )
wallispilem5.4 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
wallispilem5.5 ⊢ 𝐿 = ( 𝑛 ∈ ℕ ↦ ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · 𝑛 ) ) )
Assertion wallispilem5 𝐻 ⇝ 1

Proof

Step Hyp Ref Expression
1 wallispilem5.1 ⊢ 𝐹 = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
2 wallispilem5.2 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
3 wallispilem5.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) )
4 wallispilem5.4 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( π / 2 ) · ( 1 / ( seq 1 ( · , 𝐹 ) ‘ 𝑛 ) ) ) )
5 wallispilem5.5 ⊢ 𝐿 = ( 𝑛 ∈ ℕ ↦ ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · 𝑛 ) ) )
6 1 2 3 4 wallispilem4 ⊢ 𝐺 = 𝐻
7 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
8 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
9 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
10 2ne0 ⊢ 2 ≠ 0
11 10 a1i ⊢ ( ⊤ → 2 ≠ 0 )
12 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
13 5 9 11 12 clim1fr1 ⊢ ( ⊤ → 𝐿 ⇝ 1 )
14 nnex ⊢ ℕ ∈ V
15 14 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ V
16 3 15 eqeltri ⊢ 𝐺 ∈ V
17 16 a1i ⊢ ( ⊤ → 𝐺 ∈ V )
18 2nn0 ⊢ 2 ∈ ℕ0
19 18 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ0 )
20 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
21 19 20 nn0mulcld ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℕ0 )
22 1nn0 ⊢ 1 ∈ ℕ0
23 22 a1i ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℕ0 )
24 21 23 nn0addcld ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 )
25 24 nn0red ⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ )
26 21 nn0red ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℝ )
27 2cnd ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ )
28 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
29 10 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ≠ 0 )
30 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
31 27 28 29 30 mulne0d ⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ≠ 0 )
32 25 26 31 redivcld ⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · 𝑛 ) ) ∈ ℝ )
33 5 32 fmpti ⊢ 𝐿 : ℕ ⟶ ℝ
34 33 a1i ⊢ ( ⊤ → 𝐿 : ℕ ⟶ ℝ )
35 34 ffvelcdmda ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐿 ‘ 𝑘 ) ∈ ℝ )
36 2 wallispilem3 ⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( 𝐼 ‘ ( 2 · 𝑛 ) ) ∈ ℝ+ )
37 21 36 syl ⊢ ( 𝑛 ∈ ℕ → ( 𝐼 ‘ ( 2 · 𝑛 ) ) ∈ ℝ+ )
38 37 rpred ⊢ ( 𝑛 ∈ ℕ → ( 𝐼 ‘ ( 2 · 𝑛 ) ) ∈ ℝ )
39 2 wallispilem3 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 → ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ+ )
40 24 39 syl ⊢ ( 𝑛 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ+ )
41 38 40 rerpdivcld ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℝ )
42 3 41 fmpti ⊢ 𝐺 : ℕ ⟶ ℝ
43 42 a1i ⊢ ( ⊤ → 𝐺 : ℕ ⟶ ℝ )
44 43 ffvelcdmda ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
45 18 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℕ0 )
46 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
47 45 46 nn0mulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℕ0 )
48 2 wallispilem3 ⊢ ( ( 2 · 𝑘 ) ∈ ℕ0 → ( 𝐼 ‘ ( 2 · 𝑘 ) ) ∈ ℝ+ )
49 47 48 syl ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( 2 · 𝑘 ) ) ∈ ℝ+ )
50 49 rpred ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( 2 · 𝑘 ) ) ∈ ℝ )
51 2nn ⊢ 2 ∈ ℕ
52 51 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℕ )
53 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
54 52 53 nnmulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℕ )
55 nnm1nn0 ⊢ ( ( 2 · 𝑘 ) ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ0 )
56 54 55 syl ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ0 )
57 2 wallispilem3 ⊢ ( ( ( 2 · 𝑘 ) − 1 ) ∈ ℕ0 → ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ∈ ℝ+ )
58 56 57 syl ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ∈ ℝ+ )
59 58 rpred ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ∈ ℝ )
60 22 a1i ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℕ0 )
61 47 60 nn0addcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 )
62 2 wallispilem3 ⊢ ( ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ+ )
63 61 62 syl ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ+ )
64 2cnd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℂ )
65 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
66 64 65 mulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℂ )
67 1cnd ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℂ )
68 66 67 npcand ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) = ( 2 · 𝑘 ) )
69 68 fveq2d ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) ) = ( 𝐼 ‘ ( 2 · 𝑘 ) ) )
70 2 56 wallispilem1 ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( ( 2 · 𝑘 ) − 1 ) + 1 ) ) ≤ ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
71 69 70 eqbrtrrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( 2 · 𝑘 ) ) ≤ ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
72 50 59 63 71 lediv1dd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ≤ ( ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
73 66 67 addcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
74 10 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ≠ 0 )
75 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
76 64 65 74 75 mulne0d ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ≠ 0 )
77 73 66 76 divcld ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) ∈ ℂ )
78 63 rpcnd ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
79 63 rpne0d ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ≠ 0 )
80 77 78 79 divcan4d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) )
81 2re ⊢ 2 ∈ ℝ
82 81 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ )
83 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
84 82 83 remulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ )
85 1red ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℝ )
86 84 85 readdcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℝ )
87 45 nn0ge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 2 )
88 nnge1 ⊢ ( 𝑘 ∈ ℕ → 1 ≤ 𝑘 )
89 82 83 87 88 lemulge11d ⊢ ( 𝑘 ∈ ℕ → 2 ≤ ( 2 · 𝑘 ) )
90 84 ltp1d ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) < ( ( 2 · 𝑘 ) + 1 ) )
91 82 84 86 89 90 lelttrd ⊢ ( 𝑘 ∈ ℕ → 2 < ( ( 2 · 𝑘 ) + 1 ) )
92 82 86 91 ltled ⊢ ( 𝑘 ∈ ℕ → 2 ≤ ( ( 2 · 𝑘 ) + 1 ) )
93 45 nn0zd ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℤ )
94 61 nn0zd ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℤ )
95 eluz ⊢ ( ( 2 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) ∈ ℤ ) → ( ( ( 2 · 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ 2 ≤ ( ( 2 · 𝑘 ) + 1 ) ) )
96 93 94 95 syl2anc ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ 2 ≤ ( ( 2 · 𝑘 ) + 1 ) ) )
97 92 96 mpbird ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
98 2 97 itgsinexp ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑘 ) + 1 ) − 2 ) ) ) )
99 66 67 pncand ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) = ( 2 · 𝑘 ) )
100 99 oveq1d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) / ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) )
101 1e2m1 ⊢ 1 = ( 2 − 1 )
102 101 a1i ⊢ ( 𝑘 ∈ ℕ → 1 = ( 2 − 1 ) )
103 102 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 𝑘 ) − ( 2 − 1 ) ) )
104 66 64 67 subsub3d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) − ( 2 − 1 ) ) = ( ( ( 2 · 𝑘 ) + 1 ) − 2 ) )
105 103 104 eqtr2d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) + 1 ) − 2 ) = ( ( 2 · 𝑘 ) − 1 ) )
106 105 fveq2d ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( ( 2 · 𝑘 ) + 1 ) − 2 ) ) = ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
107 100 106 oveq12d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝐼 ‘ ( ( ( 2 · 𝑘 ) + 1 ) − 2 ) ) ) = ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )
108 98 107 eqtrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )
109 108 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) )
110 54 peano2nnd ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ )
111 110 nnne0d ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 1 ) ≠ 0 )
112 66 73 111 divcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
113 58 rpcnd ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ∈ ℂ )
114 77 112 113 mulassd ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) ) )
115 73 66 111 76 divcan6d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = 1 )
116 115 oveq1d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 1 · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) )
117 113 mullidd ⊢ ( 𝑘 ∈ ℕ → ( 1 · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
118 116 117 eqtrd ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) ) = ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
119 109 114 118 3eqtr2d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) )
120 119 oveq1d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) · ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
121 80 120 eqtr3d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) = ( ( 𝐼 ‘ ( ( 2 · 𝑘 ) − 1 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
122 72 121 breqtrrd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ≤ ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) )
123 49 63 rpdivcld ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ∈ ℝ+ )
124 nfcv ⊢ Ⅎ 𝑛 𝑘
125 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
126 2 125 nfcxfr ⊢ Ⅎ 𝑛 𝐼
127 nfcv ⊢ Ⅎ 𝑛 ( 2 · 𝑘 )
128 126 127 nffv ⊢ Ⅎ 𝑛 ( 𝐼 ‘ ( 2 · 𝑘 ) )
129 nfcv ⊢ Ⅎ 𝑛 /
130 nfcv ⊢ Ⅎ 𝑛 ( ( 2 · 𝑘 ) + 1 )
131 126 130 nffv ⊢ Ⅎ 𝑛 ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) )
132 128 129 131 nfov ⊢ Ⅎ 𝑛 ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) )
133 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
134 133 fveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝐼 ‘ ( 2 · 𝑛 ) ) = ( 𝐼 ‘ ( 2 · 𝑘 ) ) )
135 133 fvoveq1d ⊢ ( 𝑛 = 𝑘 → ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) = ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) )
136 134 135 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐼 ‘ ( 2 · 𝑛 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
137 124 132 136 3 fvmptf ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ∈ ℝ+ ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
138 123 137 mpdan ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
139 5 a1i ⊢ ( 𝑘 ∈ ℕ → 𝐿 = ( 𝑛 ∈ ℕ ↦ ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · 𝑛 ) ) ) )
140 simpr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → 𝑛 = 𝑘 )
141 140 oveq2d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
142 141 oveq1d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) )
143 142 141 oveq12d ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 = 𝑘 ) → ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · 𝑛 ) ) = ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) )
144 139 143 53 77 fvmptd ⊢ ( 𝑘 ∈ ℕ → ( 𝐿 ‘ 𝑘 ) = ( ( ( 2 · 𝑘 ) + 1 ) / ( 2 · 𝑘 ) ) )
145 122 138 144 3brtr4d ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐿 ‘ 𝑘 ) )
146 145 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐿 ‘ 𝑘 ) )
147 78 79 dividd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = 1 )
148 63 rpred ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ )
149 2 47 wallispilem1 ⊢ ( 𝑘 ∈ ℕ → ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ≤ ( 𝐼 ‘ ( 2 · 𝑘 ) ) )
150 148 50 63 149 lediv1dd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ≤ ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
151 147 150 eqbrtrrd ⊢ ( 𝑘 ∈ ℕ → 1 ≤ ( ( 𝐼 ‘ ( 2 · 𝑘 ) ) / ( 𝐼 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
152 151 138 breqtrrd ⊢ ( 𝑘 ∈ ℕ → 1 ≤ ( 𝐺 ‘ 𝑘 ) )
153 152 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 1 ≤ ( 𝐺 ‘ 𝑘 ) )
154 7 8 13 17 35 44 146 153 climsqz2 ⊢ ( ⊤ → 𝐺 ⇝ 1 )
155 154 mptru ⊢ 𝐺 ⇝ 1
156 6 155 eqbrtrri ⊢ 𝐻 ⇝ 1