Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 1 → (2 · 𝑥) = (2 ·
1)) |
2 | 1 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1))) |
3 | 1 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 1 → ((2 · 𝑥) + 1) = ((2 · 1) +
1)) |
4 | 3 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) +
1))) |
5 | 2, 4 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) +
1)))) |
6 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 1 → (seq1( · ,
𝐹)‘𝑥) = (seq1( · , 𝐹)‘1)) |
7 | 6 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 1 → (1 / (seq1( ·
, 𝐹)‘𝑥)) = (1 / (seq1( · ,
𝐹)‘1))) |
8 | 7 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 1 → ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘1)))) |
9 | 5, 8 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2)
· (1 / (seq1( · , 𝐹)‘1))))) |
10 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
11 | 10 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦))) |
12 | 10 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((2 · 𝑥) + 1) = ((2 · 𝑦) + 1)) |
13 | 12 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1))) |
14 | 11, 13 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) |
15 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦)) |
16 | 15 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦))) |
17 | 16 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘𝑦)))) |
18 | 14, 17 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦))))) |
19 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1))) |
20 | 19 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1)))) |
21 | 19 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((2 · 𝑥) + 1) = ((2 · (𝑦 + 1)) + 1)) |
22 | 21 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1))) |
23 | 20, 22 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1)))) |
24 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1))) |
25 | 24 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) |
26 | 25 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘(𝑦 + 1))))) |
27 | 23, 26 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘(𝑦 + 1)))))) |
28 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛)) |
29 | 28 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛))) |
30 | 28 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((2 · 𝑥) + 1) = ((2 · 𝑛) + 1)) |
31 | 30 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1))) |
32 | 29, 31 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) |
33 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛)) |
34 | 33 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛))) |
35 | 34 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘𝑛)))) |
36 | 32, 35 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑛))))) |
37 | | 2t1e2 11176 |
. . . . . . 7
⊢ (2
· 1) = 2 |
38 | 37 | fveq2i 6194 |
. . . . . 6
⊢ (𝐼‘(2 · 1)) = (𝐼‘2) |
39 | 37 | oveq1i 6660 |
. . . . . . . 8
⊢ ((2
· 1) + 1) = (2 + 1) |
40 | | 2p1e3 11151 |
. . . . . . . 8
⊢ (2 + 1) =
3 |
41 | 39, 40 | eqtri 2644 |
. . . . . . 7
⊢ ((2
· 1) + 1) = 3 |
42 | 41 | fveq2i 6194 |
. . . . . 6
⊢ (𝐼‘((2 · 1) + 1)) =
(𝐼‘3) |
43 | 38, 42 | oveq12i 6662 |
. . . . 5
⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) =
((𝐼‘2) / (𝐼‘3)) |
44 | | 2z 11409 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
45 | | uzid 11702 |
. . . . . . . . 9
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
⊢ 2 ∈
(ℤ≥‘2) |
47 | | wallispilem4.2 |
. . . . . . . . . 10
⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦
∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧) |
48 | 47 | wallispilem2 40283 |
. . . . . . . . 9
⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈
(ℤ≥‘2) → (𝐼‘2) = (((2 − 1) / 2) ·
(𝐼‘(2 −
2))))) |
49 | 48 | simp3i 1072 |
. . . . . . . 8
⊢ (2 ∈
(ℤ≥‘2) → (𝐼‘2) = (((2 − 1) / 2) ·
(𝐼‘(2 −
2)))) |
50 | 46, 49 | ax-mp 5 |
. . . . . . 7
⊢ (𝐼‘2) = (((2 − 1) / 2)
· (𝐼‘(2
− 2))) |
51 | | 2m1e1 11135 |
. . . . . . . . 9
⊢ (2
− 1) = 1 |
52 | 51 | oveq1i 6660 |
. . . . . . . 8
⊢ ((2
− 1) / 2) = (1 / 2) |
53 | | 2cn 11091 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
54 | 53 | subidi 10352 |
. . . . . . . . . 10
⊢ (2
− 2) = 0 |
55 | 54 | fveq2i 6194 |
. . . . . . . . 9
⊢ (𝐼‘(2 − 2)) = (𝐼‘0) |
56 | 48 | simp1i 1070 |
. . . . . . . . 9
⊢ (𝐼‘0) =
π |
57 | 55, 56 | eqtri 2644 |
. . . . . . . 8
⊢ (𝐼‘(2 − 2)) =
π |
58 | 52, 57 | oveq12i 6662 |
. . . . . . 7
⊢ (((2
− 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) ·
π) |
59 | | ax-1cn 9994 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
60 | | 2cnne0 11242 |
. . . . . . . . 9
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
61 | | picn 24211 |
. . . . . . . . 9
⊢ π
∈ ℂ |
62 | | div32 10705 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈
ℂ) → ((1 / 2) · π) = (1 · (π /
2))) |
63 | 59, 60, 61, 62 | mp3an 1424 |
. . . . . . . 8
⊢ ((1 / 2)
· π) = (1 · (π / 2)) |
64 | | 2ne0 11113 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
65 | 61, 53, 64 | divcli 10767 |
. . . . . . . . 9
⊢ (π /
2) ∈ ℂ |
66 | 65 | mulid2i 10043 |
. . . . . . . 8
⊢ (1
· (π / 2)) = (π / 2) |
67 | 63, 66 | eqtri 2644 |
. . . . . . 7
⊢ ((1 / 2)
· π) = (π / 2) |
68 | 50, 58, 67 | 3eqtri 2648 |
. . . . . 6
⊢ (𝐼‘2) = (π /
2) |
69 | | 3z 11410 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
70 | | 2re 11090 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
71 | | 3re 11094 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
72 | | 2lt3 11195 |
. . . . . . . . . 10
⊢ 2 <
3 |
73 | 70, 71, 72 | ltleii 10160 |
. . . . . . . . 9
⊢ 2 ≤
3 |
74 | | eluz2 11693 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈
ℤ ∧ 2 ≤ 3)) |
75 | 44, 69, 73, 74 | mpbir3an 1244 |
. . . . . . . 8
⊢ 3 ∈
(ℤ≥‘2) |
76 | 47 | wallispilem2 40283 |
. . . . . . . . 9
⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈
(ℤ≥‘2) → (𝐼‘3) = (((3 − 1) / 3) ·
(𝐼‘(3 −
2))))) |
77 | 76 | simp3i 1072 |
. . . . . . . 8
⊢ (3 ∈
(ℤ≥‘2) → (𝐼‘3) = (((3 − 1) / 3) ·
(𝐼‘(3 −
2)))) |
78 | 75, 77 | ax-mp 5 |
. . . . . . 7
⊢ (𝐼‘3) = (((3 − 1) / 3)
· (𝐼‘(3
− 2))) |
79 | | 3m1e2 11137 |
. . . . . . . . . 10
⊢ (3
− 1) = 2 |
80 | 79 | eqcomi 2631 |
. . . . . . . . 9
⊢ 2 = (3
− 1) |
81 | 80 | oveq1i 6660 |
. . . . . . . 8
⊢ (2 / 3) =
((3 − 1) / 3) |
82 | | 3cn 11095 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
83 | 82, 53, 59, 40 | subaddrii 10370 |
. . . . . . . . . 10
⊢ (3
− 2) = 1 |
84 | 83 | fveq2i 6194 |
. . . . . . . . 9
⊢ (𝐼‘(3 − 2)) = (𝐼‘1) |
85 | 48 | simp2i 1071 |
. . . . . . . . 9
⊢ (𝐼‘1) = 2 |
86 | 84, 85 | eqtr2i 2645 |
. . . . . . . 8
⊢ 2 =
(𝐼‘(3 −
2)) |
87 | 81, 86 | oveq12i 6662 |
. . . . . . 7
⊢ ((2 / 3)
· 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2))) |
88 | | 3ne0 11115 |
. . . . . . . . 9
⊢ 3 ≠
0 |
89 | 53, 82, 88 | divcli 10767 |
. . . . . . . 8
⊢ (2 / 3)
∈ ℂ |
90 | 89, 53 | mulcomi 10046 |
. . . . . . 7
⊢ ((2 / 3)
· 2) = (2 · (2 / 3)) |
91 | 78, 87, 90 | 3eqtr2i 2650 |
. . . . . 6
⊢ (𝐼‘3) = (2 · (2 /
3)) |
92 | 68, 91 | oveq12i 6662 |
. . . . 5
⊢ ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 /
3))) |
93 | | 1z 11407 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
94 | | seq1 12814 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1)) |
95 | 93, 94 | ax-mp 5 |
. . . . . . . 8
⊢ (seq1(
· , 𝐹)‘1) =
(𝐹‘1) |
96 | | 1nn 11031 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
97 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (2 · 𝑘) = (2 ·
1)) |
98 | 97, 37 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (2 · 𝑘) = 2) |
99 | 97 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1)
− 1)) |
100 | 37 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢ ((2
· 1) − 1) = (2 − 1) |
101 | 100, 51 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ ((2
· 1) − 1) = 1 |
102 | 99, 101 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) =
1) |
103 | 98, 102 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 /
1)) |
104 | 53 | div1i 10753 |
. . . . . . . . . . . 12
⊢ (2 / 1) =
2 |
105 | 103, 104 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) =
2) |
106 | 98 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 +
1)) |
107 | 106, 40 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = 3) |
108 | 98, 107 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 /
3)) |
109 | 105, 108 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1))) = (2 · (2
/ 3))) |
110 | | wallispilem4.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1)))) |
111 | | ovex 6678 |
. . . . . . . . . 10
⊢ (2
· (2 / 3)) ∈ V |
112 | 109, 110,
111 | fvmpt 6282 |
. . . . . . . . 9
⊢ (1 ∈
ℕ → (𝐹‘1)
= (2 · (2 / 3))) |
113 | 96, 112 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐹‘1) = (2 · (2 /
3)) |
114 | 95, 113 | eqtr2i 2645 |
. . . . . . 7
⊢ (2
· (2 / 3)) = (seq1( · , 𝐹)‘1) |
115 | 114 | oveq2i 6661 |
. . . . . 6
⊢ ((π /
2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1)) |
116 | 53, 89 | mulcli 10045 |
. . . . . . . . 9
⊢ (2
· (2 / 3)) ∈ ℂ |
117 | 113, 116 | eqeltri 2697 |
. . . . . . . 8
⊢ (𝐹‘1) ∈
ℂ |
118 | 95, 117 | eqeltri 2697 |
. . . . . . 7
⊢ (seq1(
· , 𝐹)‘1)
∈ ℂ |
119 | 53, 82, 64, 88 | divne0i 10773 |
. . . . . . . . 9
⊢ (2 / 3)
≠ 0 |
120 | 53, 89, 64, 119 | mulne0i 10670 |
. . . . . . . 8
⊢ (2
· (2 / 3)) ≠ 0 |
121 | 114, 120 | eqnetrri 2865 |
. . . . . . 7
⊢ (seq1(
· , 𝐹)‘1) ≠
0 |
122 | 65, 118, 121 | divreci 10770 |
. . . . . 6
⊢ ((π /
2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘1))) |
123 | 115, 122 | eqtri 2644 |
. . . . 5
⊢ ((π /
2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))) |
124 | 43, 92, 123 | 3eqtri 2648 |
. . . 4
⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) =
((π / 2) · (1 / (seq1( · , 𝐹)‘1))) |
125 | | oveq2 6658 |
. . . . . . 7
⊢ (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))))) |
126 | 125 | adantl 482 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦)))) → (((((2 ·
𝑦) + 1) / (2 ·
(𝑦 + 1))) / ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))))) |
127 | | 2cnd 11093 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 2 ∈
ℂ) |
128 | | nncn 11028 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
129 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 1 ∈
ℂ) |
130 | 127, 128,
129 | adddid 10064 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) = ((2
· 𝑦) + (2 ·
1))) |
131 | 127 | mulid1d 10057 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (2
· 1) = 2) |
132 | 131 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (2 ·
1)) = ((2 · 𝑦) +
2)) |
133 | 130, 132 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) = ((2
· 𝑦) +
2)) |
134 | 133 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) = (((2 · 𝑦) + 2)
− 1)) |
135 | 127, 128 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℂ) |
136 | 135, 127,
129 | addsubassd 10412 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 2) − 1)
= ((2 · 𝑦) + (2
− 1))) |
137 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
− 1) = 1) |
138 | 137 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (2 −
1)) = ((2 · 𝑦) +
1)) |
139 | 134, 136,
138 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) = ((2 · 𝑦) +
1)) |
140 | 139 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) −
1) / (2 · (𝑦 + 1)))
= (((2 · 𝑦) + 1) /
(2 · (𝑦 +
1)))) |
141 | 140 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((((2
· (𝑦 + 1)) −
1) / (2 · (𝑦 + 1)))
· (𝐼‘(2
· 𝑦))) = ((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) ·
(𝐼‘(2 · 𝑦)))) |
142 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (3
− 1) = 2) |
143 | 142 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (3 −
1)) = ((2 · 𝑦) +
2)) |
144 | 82 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 3 ∈
ℂ) |
145 | 135, 144,
129 | addsubassd 10412 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 3) − 1)
= ((2 · 𝑦) + (3
− 1))) |
146 | 143, 145,
133 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 3) − 1)
= (2 · (𝑦 +
1))) |
147 | 146 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((((2
· 𝑦) + 3) − 1)
/ ((2 · 𝑦) + 3)) =
((2 · (𝑦 + 1)) / ((2
· 𝑦) +
3))) |
148 | 147 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (((((2
· 𝑦) + 3) − 1)
/ ((2 · 𝑦) + 3))
· (𝐼‘(((2
· 𝑦) + 3) −
2))) = (((2 · (𝑦 +
1)) / ((2 · 𝑦) + 3))
· (𝐼‘(((2
· 𝑦) + 3) −
2)))) |
149 | 141, 148 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (((((2
· (𝑦 + 1)) −
1) / (2 · (𝑦 + 1)))
· (𝐼‘(2
· 𝑦))) / (((((2
· 𝑦) + 3) − 1)
/ ((2 · 𝑦) + 3))
· (𝐼‘(((2
· 𝑦) + 3) −
2)))) = (((((2 · 𝑦)
+ 1) / (2 · (𝑦 +
1))) · (𝐼‘(2
· 𝑦))) / (((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3)) ·
(𝐼‘(((2 ·
𝑦) + 3) −
2))))) |
150 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 2 ∈
ℤ) |
151 | | nnz 11399 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
152 | 151 | peano2zd 11485 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℤ) |
153 | 150, 152 | zmulcld 11488 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
ℤ) |
154 | 70 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 2 ∈
ℝ) |
155 | | nnre 11027 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
156 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 1 ∈
ℝ) |
157 | 155, 156 | readdcld 10069 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℝ) |
158 | | 0le2 11111 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
2 |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 0 ≤
2) |
160 | | nnnn0 11299 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
161 | 160 | nn0ge0d 11354 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 0 ≤
𝑦) |
162 | 156, 155 | addge02d 10616 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (0 ≤
𝑦 ↔ 1 ≤ (𝑦 + 1))) |
163 | 161, 162 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 1 ≤
(𝑦 + 1)) |
164 | 154, 157,
159, 163 | lemulge11d 10961 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 2 ≤ (2
· (𝑦 +
1))) |
165 | 44 | eluz1i 11695 |
. . . . . . . . . . . . 13
⊢ ((2
· (𝑦 + 1)) ∈
(ℤ≥‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2
· (𝑦 +
1)))) |
166 | 153, 164,
165 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
(ℤ≥‘2)) |
167 | 47, 166 | itgsinexp 40170 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 ·
(𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) −
2)))) |
168 | 133 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
2) = (((2 · 𝑦) + 2)
− 2)) |
169 | 135, 127 | pncand 10393 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 2) − 2)
= (2 · 𝑦)) |
170 | 168, 169 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
2) = (2 · 𝑦)) |
171 | 170 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦))) |
172 | 171 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((((2
· (𝑦 + 1)) −
1) / (2 · (𝑦 + 1)))
· (𝐼‘((2
· (𝑦 + 1)) −
2))) = ((((2 · (𝑦 +
1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦)))) |
173 | 167, 172 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 ·
(𝑦 + 1))) · (𝐼‘(2 · 𝑦)))) |
174 | 133 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) + 1) =
(((2 · 𝑦) + 2) +
1)) |
175 | 135, 127,
129 | addassd 10062 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 2) + 1) = ((2
· 𝑦) + (2 +
1))) |
176 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2 + 1) =
3) |
177 | 176 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (2 + 1)) =
((2 · 𝑦) +
3)) |
178 | 174, 175,
177 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) + 1) =
((2 · 𝑦) +
3)) |
179 | 178 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3))) |
180 | 150, 151 | zmulcld 11488 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℤ) |
181 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 3 ∈
ℤ) |
182 | 180, 181 | zaddcld 11486 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 3) ∈
ℤ) |
183 | 154, 155 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℝ) |
184 | 71 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 3 ∈
ℝ) |
185 | 183, 184 | readdcld 10069 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 3) ∈
ℝ) |
186 | | nnge1 11046 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 1 ≤
𝑦) |
187 | 154, 155,
159, 186 | lemulge11d 10961 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 2 ≤ (2
· 𝑦)) |
188 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
189 | | 3pos 11114 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
3 |
190 | 188, 71, 189 | ltleii 10160 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
3 |
191 | 183, 184 | addge01d 10615 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (0 ≤ 3
↔ (2 · 𝑦) ≤
((2 · 𝑦) +
3))) |
192 | 190, 191 | mpbii 223 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ≤ ((2
· 𝑦) +
3)) |
193 | 154, 183,
185, 187, 192 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 2 ≤
((2 · 𝑦) +
3)) |
194 | 44 | eluz1i 11695 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑦) + 3) ∈
(ℤ≥‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2
· 𝑦) +
3))) |
195 | 182, 193,
194 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 3) ∈
(ℤ≥‘2)) |
196 | 47, 195 | itgsinexp 40170 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 ·
𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) −
2)))) |
197 | 179, 196 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 ·
𝑦) + 3) − 1) / ((2
· 𝑦) + 3)) ·
(𝐼‘(((2 ·
𝑦) + 3) −
2)))) |
198 | 173, 197 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 ·
(𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 ·
𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) −
2))))) |
199 | 135, 129 | addcld 10059 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
ℂ) |
200 | 128, 129 | addcld 10059 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℂ) |
201 | 127, 200 | mulcld 10060 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
ℂ) |
202 | 64 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 2 ≠
0) |
203 | | peano2nn 11032 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ) |
204 | 203 | nnne0d 11065 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0) |
205 | 127, 200,
202, 204 | mulne0d 10679 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ≠
0) |
206 | 199, 201,
205 | divcld 10801 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) ∈
ℂ) |
207 | | 2nn0 11309 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
208 | 207 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 2 ∈
ℕ0) |
209 | 208, 160 | nn0mulcld 11356 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℕ0) |
210 | 47 | wallispilem3 40284 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑦) ∈
ℕ0 → (𝐼‘(2 · 𝑦)) ∈
ℝ+) |
211 | 210 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((2
· 𝑦) ∈
ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℂ) |
212 | 209, 211 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈
ℂ) |
213 | 135, 144 | addcld 10059 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 3) ∈
ℂ) |
214 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 0 ∈
ℝ) |
215 | | 2pos 11112 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
216 | 215 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 0 <
2) |
217 | | nngt0 11049 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
218 | 154, 155,
216, 217 | mulgt0d 10192 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 0 < (2
· 𝑦)) |
219 | 184, 189 | jctir 561 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (3 ∈
ℝ ∧ 0 < 3)) |
220 | | elrp 11834 |
. . . . . . . . . . . . . . . 16
⊢ (3 ∈
ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3)) |
221 | 219, 220 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 3 ∈
ℝ+) |
222 | 183, 221 | ltaddrpd 11905 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) < ((2
· 𝑦) +
3)) |
223 | 214, 183,
185, 218, 222 | lttrd 10198 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 0 <
((2 · 𝑦) +
3)) |
224 | 223 | gt0ne0d 10592 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 3) ≠
0) |
225 | 201, 213,
224 | divcld 10801 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3)) ∈
ℂ) |
226 | 201, 213,
205, 224 | divne0d 10817 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3)) ≠
0) |
227 | 182, 150 | zsubcld 11487 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 3) − 2)
∈ ℤ) |
228 | 185, 154 | subge0d 10617 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (0 ≤
(((2 · 𝑦) + 3)
− 2) ↔ 2 ≤ ((2 · 𝑦) + 3))) |
229 | 193, 228 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 0 ≤
(((2 · 𝑦) + 3)
− 2)) |
230 | | elnn0z 11390 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑦) + 3) − 2)
∈ ℕ0 ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤
(((2 · 𝑦) + 3)
− 2))) |
231 | 227, 229,
230 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 3) − 2)
∈ ℕ0) |
232 | 47 | wallispilem3 40284 |
. . . . . . . . . . . . 13
⊢ ((((2
· 𝑦) + 3) − 2)
∈ ℕ0 → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈
ℝ+) |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈
ℝ+) |
234 | 233 | rpcnne0d 11881 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈
ℂ ∧ (𝐼‘(((2
· 𝑦) + 3) −
2)) ≠ 0)) |
235 | 225, 226,
234 | jca31 557 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3)) ∈
ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧
(𝐼‘(((2 ·
𝑦) + 3) − 2)) ≠
0))) |
236 | | divmuldiv 10725 |
. . . . . . . . . 10
⊢ ((((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) ∈
ℂ ∧ (𝐼‘(2
· 𝑦)) ∈
ℂ) ∧ ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) + 3)) ≠ 0) ∧
((𝐼‘(((2 ·
𝑦) + 3) − 2)) ∈
ℂ ∧ (𝐼‘(((2
· 𝑦) + 3) −
2)) ≠ 0))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) −
2))))) |
237 | 206, 212,
235, 236 | syl21anc 1325 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) / ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3))) ·
((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) −
2))))) |
238 | 149, 198,
237 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))))) |
239 | 135, 144,
127 | addsubassd 10412 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 3) − 2)
= ((2 · 𝑦) + (3
− 2))) |
240 | 83 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (3
− 2) = 1) |
241 | 240 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (3 −
2)) = ((2 · 𝑦) +
1)) |
242 | 239, 241 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 3) − 2)
= ((2 · 𝑦) +
1)) |
243 | 242 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1))) |
244 | 243 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) |
245 | 244 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) / ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3))) ·
((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))) |
246 | 238, 245 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))) |
247 | 246 | adantr 481 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))) |
248 | | elnnuz 11724 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈
(ℤ≥‘1)) |
249 | 248 | biimpi 206 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
(ℤ≥‘1)) |
250 | | seqp1 12816 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈
(ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1)))) |
251 | 249, 250 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (seq1(
· , 𝐹)‘(𝑦 + 1)) = ((seq1( · ,
𝐹)‘𝑦) · (𝐹‘(𝑦 + 1)))) |
252 | 110 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) +
1))))) |
253 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1))) |
254 | 253 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) −
1)) |
255 | 253, 254 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) −
1))) |
256 | 253 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1)) |
257 | 253, 256 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) |
258 | 255, 257 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) +
1)))) |
259 | 258 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) + 1))) = (((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) − 1))
· ((2 · (𝑦 +
1)) / ((2 · (𝑦 + 1))
+ 1)))) |
260 | 154, 157 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
ℝ) |
261 | 260, 156 | resubcld 10458 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) ∈ ℝ) |
262 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
2 |
263 | 262 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 1 <
2) |
264 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) |
265 | 156, 264 | ltaddrp2d 11906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 1 <
(𝑦 + 1)) |
266 | 154, 157,
263, 265 | mulgt1d 10960 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 1 < (2
· (𝑦 +
1))) |
267 | 156, 266 | gtned 10172 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ≠
1) |
268 | 201, 129,
267 | subne0d 10401 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) −
1) ≠ 0) |
269 | 260, 261,
268 | redivcld 10853 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) −
1)) ∈ ℝ) |
270 | 178, 185 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) + 1)
∈ ℝ) |
271 | 178, 224 | eqnetrd 2861 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) + 1) ≠
0) |
272 | 260, 270,
271 | redivcld 10853 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) + 1))
∈ ℝ) |
273 | 269, 272 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) −
1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈
ℝ) |
274 | 252, 259,
203, 273 | fvmptd 6288 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) +
1)))) |
275 | 274 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((seq1(
· , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) +
1))))) |
276 | 251, 275 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (seq1(
· , 𝐹)‘(𝑦 + 1)) = ((seq1( · ,
𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) +
1))))) |
277 | 276 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) +
1)))))) |
278 | 277 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1(
· , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) +
1))))))) |
279 | 139 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) −
1)) = ((2 · (𝑦 + 1))
/ ((2 · 𝑦) +
1))) |
280 | 178 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) + 1)) =
((2 · (𝑦 + 1)) / ((2
· 𝑦) +
3))) |
281 | 279, 280 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) −
1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) + 3)))) |
282 | 281 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((seq1(
· , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2
· (𝑦 + 1)) / ((2
· (𝑦 + 1)) + 1)))) =
((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) |
283 | 282 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (1 /
((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) + 1))))) = (1 /
((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) |
284 | 283 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) + 1)))))) = ((π
/ 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))) |
285 | | elfznn 12370 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ) |
286 | 285 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ) |
287 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℕ → 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2
· 𝑘) / ((2 ·
𝑘) +
1))))) |
288 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤)) |
289 | 288 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1)) |
290 | 288, 289 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1))) |
291 | 288 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1)) |
292 | 288, 291 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1))) |
293 | 290, 292 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2
· 𝑤) / ((2 ·
𝑤) + 1)))) |
294 | 293 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℕ ∧ 𝑘 = 𝑤) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2
· 𝑤) / ((2 ·
𝑤) + 1)))) |
295 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℕ) |
296 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ+ |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℕ → 2 ∈
ℝ+) |
298 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℝ+) |
299 | 297, 298 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ℕ → (2
· 𝑤) ∈
ℝ+) |
300 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℕ → 2 ∈
ℝ) |
301 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℝ) |
302 | 300, 301 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℕ → (2
· 𝑤) ∈
ℝ) |
303 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℕ → 1 ∈
ℝ) |
304 | 302, 303 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℕ → ((2
· 𝑤) − 1)
∈ ℝ) |
305 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℕ → 1 ≤
𝑤) |
306 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℂ) |
307 | 306 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ∈ ℕ → (1
· 𝑤) = 𝑤) |
308 | 303, 300,
298 | ltmul1d 11913 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 ∈ ℕ → (1 < 2
↔ (1 · 𝑤) <
(2 · 𝑤))) |
309 | 262, 308 | mpbii 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ∈ ℕ → (1
· 𝑤) < (2
· 𝑤)) |
310 | 307, 309 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤)) |
311 | 303, 301,
302, 305, 310 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℕ → 1 < (2
· 𝑤)) |
312 | 303, 302 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℕ → (1 <
(2 · 𝑤) ↔ 0
< ((2 · 𝑤)
− 1))) |
313 | 311, 312 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℕ → 0 <
((2 · 𝑤) −
1)) |
314 | 304, 313 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ℕ → ((2
· 𝑤) − 1)
∈ ℝ+) |
315 | 299, 314 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ℕ → ((2
· 𝑤) / ((2 ·
𝑤) − 1)) ∈
ℝ+) |
316 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℕ → 0 ≤
2) |
317 | 298 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℕ → 0 ≤
𝑤) |
318 | 300, 301,
316, 317 | mulge0d 10604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℕ → 0 ≤ (2
· 𝑤)) |
319 | 302, 318 | ge0p1rpd 11902 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ℕ → ((2
· 𝑤) + 1) ∈
ℝ+) |
320 | 299, 319 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ ℕ → ((2
· 𝑤) / ((2 ·
𝑤) + 1)) ∈
ℝ+) |
321 | 315, 320 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℕ → (((2
· 𝑤) / ((2 ·
𝑤) − 1)) · ((2
· 𝑤) / ((2 ·
𝑤) + 1))) ∈
ℝ+) |
322 | 287, 294,
295, 321 | fvmptd 6288 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1)))) |
323 | 322, 321 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) ∈
ℝ+) |
324 | 286, 323 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹‘𝑤) ∈
ℝ+) |
325 | | rpmulcl 11855 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ+
∧ 𝑧 ∈
ℝ+) → (𝑤 · 𝑧) ∈
ℝ+) |
326 | 325 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ+
∧ 𝑧 ∈
ℝ+)) → (𝑤 · 𝑧) ∈
ℝ+) |
327 | 249, 324,
326 | seqcl 12821 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (seq1(
· , 𝐹)‘𝑦) ∈
ℝ+) |
328 | 327 | rpcnne0d 11881 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((seq1(
· , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1(
· , 𝐹)‘𝑦) ≠ 0)) |
329 | 296 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 2 ∈
ℝ+) |
330 | 155, 161 | ge0p1rpd 11902 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℝ+) |
331 | 329, 330 | rpmulcld 11888 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
ℝ+) |
332 | 154, 155,
159, 161 | mulge0d 10604 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 0 ≤ (2
· 𝑦)) |
333 | 183, 332 | ge0p1rpd 11902 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
ℝ+) |
334 | 331, 333 | rpdivcld 11889 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 1)) ∈
ℝ+) |
335 | 329, 264 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℝ+) |
336 | 335, 221 | rpaddcld 11887 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 3) ∈
ℝ+) |
337 | 331, 336 | rpdivcld 11889 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3)) ∈
ℝ+) |
338 | 334, 337 | rpmulcld 11888 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) / ((2
· 𝑦) + 1)) ·
((2 · (𝑦 + 1)) / ((2
· 𝑦) + 3))) ∈
ℝ+) |
339 | 338 | rpcnne0d 11881 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((((2
· (𝑦 + 1)) / ((2
· 𝑦) + 1)) ·
((2 · (𝑦 + 1)) / ((2
· 𝑦) + 3))) ∈
ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠
0)) |
340 | | divdiv1 10736 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · ,
𝐹)‘𝑦) ≠ 0) ∧ ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) + 3))) ∈ ℂ
∧ (((2 · (𝑦 +
1)) / ((2 · 𝑦) + 1))
· ((2 · (𝑦 +
1)) / ((2 · 𝑦) +
3))) ≠ 0)) → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1(
· , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) +
3)))))) |
341 | 129, 328,
339, 340 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((1 /
(seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1(
· , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) +
3)))))) |
342 | 341 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (1 /
((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1(
· , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) +
3))))) |
343 | 342 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = ((π / 2)
· ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) |
344 | 65 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (π /
2) ∈ ℂ) |
345 | 327 | rpcnd 11874 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (seq1(
· , 𝐹)‘𝑦) ∈
ℂ) |
346 | 327 | rpne0d 11877 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (seq1(
· , 𝐹)‘𝑦) ≠ 0) |
347 | 345, 346 | reccld 10794 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (1 /
(seq1( · , 𝐹)‘𝑦)) ∈ ℂ) |
348 | 338 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) / ((2
· 𝑦) + 1)) ·
((2 · (𝑦 + 1)) / ((2
· 𝑦) + 3))) ∈
ℂ) |
349 | 338 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) / ((2
· 𝑦) + 1)) ·
((2 · (𝑦 + 1)) / ((2
· 𝑦) + 3))) ≠
0) |
350 | 344, 347,
348, 349 | divassd 10836 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = ((π / 2) ·
((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) |
351 | 139, 268 | eqnetrrd 2862 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ≠
0) |
352 | 201, 199,
201, 213, 351, 224 | divmuldivd 10842 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) / ((2
· 𝑦) + 1)) ·
((2 · (𝑦 + 1)) / ((2
· 𝑦) + 3))) = (((2
· (𝑦 + 1)) ·
(2 · (𝑦 + 1))) /
(((2 · 𝑦) + 1)
· ((2 · 𝑦) +
3)))) |
353 | 352 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 ·
𝑦) +
3))))) |
354 | 344, 347 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ) |
355 | 201, 201 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
(2 · (𝑦 + 1)))
∈ ℂ) |
356 | 199, 213 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) ·
((2 · 𝑦) + 3))
∈ ℂ) |
357 | 201, 201,
205, 205 | mulne0d 10679 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
(2 · (𝑦 + 1))) ≠
0) |
358 | 199, 213,
351, 224 | mulne0d 10679 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) ·
((2 · 𝑦) + 3)) ≠
0) |
359 | 354, 355,
356, 357, 358 | divdiv2d 10833 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 ·
𝑦) + 3)))) = ((((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 ·
(𝑦 +
1))))) |
360 | 354, 356,
355, 357 | divassd 10836 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((((π
/ 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 ·
(𝑦 + 1)))) = (((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 ·
𝑦) + 3)) / ((2 ·
(𝑦 + 1)) · (2
· (𝑦 +
1)))))) |
361 | 359, 360 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 ·
𝑦) + 3)))) = (((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 ·
𝑦) + 3)) / ((2 ·
(𝑦 + 1)) · (2
· (𝑦 +
1)))))) |
362 | 199, 201,
201, 213, 205, 224, 205 | divdivdivd 10848 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) / ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3))) = ((((2
· 𝑦) + 1) ·
((2 · 𝑦) + 3)) / ((2
· (𝑦 + 1)) ·
(2 · (𝑦 +
1))))) |
363 | 362 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((((2
· 𝑦) + 1) ·
((2 · 𝑦) + 3)) / ((2
· (𝑦 + 1)) ·
(2 · (𝑦 + 1)))) =
((((2 · 𝑦) + 1) / (2
· (𝑦 + 1))) / ((2
· (𝑦 + 1)) / ((2
· 𝑦) +
3)))) |
364 | 363 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 ·
𝑦) + 3)) / ((2 ·
(𝑦 + 1)) · (2
· (𝑦 + 1))))) =
(((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) |
365 | 353, 361,
364 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) |
366 | 343, 350,
365 | 3eqtr2d 2662 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = (((π / 2)
· (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) |
367 | 61 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → π
∈ ℂ) |
368 | 367 | halfcld 11277 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (π /
2) ∈ ℂ) |
369 | 368, 347 | mulcld 10060 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ) |
370 | 206, 225,
226 | divcld 10801 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) / ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3))) ∈
ℂ) |
371 | 369, 370 | mulcomd 10061 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((((2 ·
𝑦) + 1) / (2 ·
(𝑦 + 1))) / ((2 ·
(𝑦 + 1)) / ((2 ·
𝑦) + 3))) · ((π /
2) · (1 / (seq1( · , 𝐹)‘𝑦))))) |
372 | 284, 366,
371 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 ·
(𝑦 + 1)) / ((2 ·
(𝑦 + 1)) + 1)))))) = (((((2
· 𝑦) + 1) / (2
· (𝑦 + 1))) / ((2
· (𝑦 + 1)) / ((2
· 𝑦) + 3))) ·
((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))) |
373 | 278, 372 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → ((π /
2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 /
(seq1( · , 𝐹)‘𝑦))))) |
374 | 373 | adantr 481 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦)))) → ((π / 2) ·
(1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 /
(seq1( · , 𝐹)‘𝑦))))) |
375 | 126, 247,
374 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘(𝑦 + 1))))) |
376 | 375 | ex 450 |
. . . 4
⊢ (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 /
(seq1( · , 𝐹)‘(𝑦 + 1)))))) |
377 | 9, 18, 27, 36, 124, 376 | nnind 11038 |
. . 3
⊢ (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1(
· , 𝐹)‘𝑛)))) |
378 | 377 | mpteq2ia 4740 |
. 2
⊢ (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛)))) |
379 | | wallispilem4.3 |
. 2
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) |
380 | | wallispilem4.4 |
. 2
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) ·
(1 / (seq1( · , 𝐹)‘𝑛)))) |
381 | 378, 379,
380 | 3eqtr4i 2654 |
1
⊢ 𝐺 = 𝐻 |