Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = 1 β (2 Β· π₯) = (2 Β·
1)) |
2 | 1 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = 1 β (πΌβ(2 Β· π₯)) = (πΌβ(2 Β· 1))) |
3 | 1 | fvoveq1d 7380 |
. . . . . 6
β’ (π₯ = 1 β (πΌβ((2 Β· π₯) + 1)) = (πΌβ((2 Β· 1) +
1))) |
4 | 2, 3 | oveq12d 7376 |
. . . . 5
β’ (π₯ = 1 β ((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((πΌβ(2 Β· 1)) / (πΌβ((2 Β· 1) +
1)))) |
5 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = 1 β (seq1( Β· ,
πΉ)βπ₯) = (seq1( Β· , πΉ)β1)) |
6 | 5 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = 1 β (1 / (seq1( Β·
, πΉ)βπ₯)) = (1 / (seq1( Β· ,
πΉ)β1))) |
7 | 6 | oveq2d 7374 |
. . . . 5
β’ (π₯ = 1 β ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ₯))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)β1)))) |
8 | 4, 7 | eqeq12d 2749 |
. . . 4
β’ (π₯ = 1 β (((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) β ((πΌβ(2 Β· 1)) / (πΌβ((2 Β· 1) + 1))) = ((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)β1))))) |
9 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π¦ β (2 Β· π₯) = (2 Β· π¦)) |
10 | 9 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π¦ β (πΌβ(2 Β· π₯)) = (πΌβ(2 Β· π¦))) |
11 | 9 | fvoveq1d 7380 |
. . . . . 6
β’ (π₯ = π¦ β (πΌβ((2 Β· π₯) + 1)) = (πΌβ((2 Β· π¦) + 1))) |
12 | 10, 11 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π¦ β ((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1)))) |
13 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = π¦ β (seq1( Β· , πΉ)βπ₯) = (seq1( Β· , πΉ)βπ¦)) |
14 | 13 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = π¦ β (1 / (seq1( Β· , πΉ)βπ₯)) = (1 / (seq1( Β· , πΉ)βπ¦))) |
15 | 14 | oveq2d 7374 |
. . . . 5
β’ (π₯ = π¦ β ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)βπ¦)))) |
16 | 12, 15 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π¦ β (((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) β ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ¦))))) |
17 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β (2 Β· π₯) = (2 Β· (π¦ + 1))) |
18 | 17 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β (πΌβ(2 Β· π₯)) = (πΌβ(2 Β· (π¦ + 1)))) |
19 | 17 | fvoveq1d 7380 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β (πΌβ((2 Β· π₯) + 1)) = (πΌβ((2 Β· (π¦ + 1)) + 1))) |
20 | 18, 19 | oveq12d 7376 |
. . . . 5
β’ (π₯ = (π¦ + 1) β ((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1)))) |
21 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β (seq1( Β· , πΉ)βπ₯) = (seq1( Β· , πΉ)β(π¦ + 1))) |
22 | 21 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β (1 / (seq1( Β· , πΉ)βπ₯)) = (1 / (seq1( Β· , πΉ)β(π¦ + 1)))) |
23 | 22 | oveq2d 7374 |
. . . . 5
β’ (π₯ = (π¦ + 1) β ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)β(π¦ + 1))))) |
24 | 20, 23 | eqeq12d 2749 |
. . . 4
β’ (π₯ = (π¦ + 1) β (((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)β(π¦ + 1)))))) |
25 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π β (2 Β· π₯) = (2 Β· π)) |
26 | 25 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΌβ(2 Β· π₯)) = (πΌβ(2 Β· π))) |
27 | 25 | fvoveq1d 7380 |
. . . . . 6
β’ (π₯ = π β (πΌβ((2 Β· π₯) + 1)) = (πΌβ((2 Β· π) + 1))) |
28 | 26, 27 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π β ((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
29 | | fveq2 6843 |
. . . . . . 7
β’ (π₯ = π β (seq1( Β· , πΉ)βπ₯) = (seq1( Β· , πΉ)βπ)) |
30 | 29 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = π β (1 / (seq1( Β· , πΉ)βπ₯)) = (1 / (seq1( Β· , πΉ)βπ))) |
31 | 30 | oveq2d 7374 |
. . . . 5
β’ (π₯ = π β ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)βπ)))) |
32 | 28, 31 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β (((πΌβ(2 Β· π₯)) / (πΌβ((2 Β· π₯) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ₯))) β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ))))) |
33 | | 2t1e2 12321 |
. . . . . . 7
β’ (2
Β· 1) = 2 |
34 | 33 | fveq2i 6846 |
. . . . . 6
β’ (πΌβ(2 Β· 1)) = (πΌβ2) |
35 | 33 | oveq1i 7368 |
. . . . . . . 8
β’ ((2
Β· 1) + 1) = (2 + 1) |
36 | | 2p1e3 12300 |
. . . . . . . 8
β’ (2 + 1) =
3 |
37 | 35, 36 | eqtri 2761 |
. . . . . . 7
β’ ((2
Β· 1) + 1) = 3 |
38 | 37 | fveq2i 6846 |
. . . . . 6
β’ (πΌβ((2 Β· 1) + 1)) =
(πΌβ3) |
39 | 34, 38 | oveq12i 7370 |
. . . . 5
β’ ((πΌβ(2 Β· 1)) / (πΌβ((2 Β· 1) + 1))) =
((πΌβ2) / (πΌβ3)) |
40 | | 2z 12540 |
. . . . . . . . 9
β’ 2 β
β€ |
41 | | uzid 12783 |
. . . . . . . . 9
β’ (2 β
β€ β 2 β (β€β₯β2)) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . 8
β’ 2 β
(β€β₯β2) |
43 | | wallispilem4.2 |
. . . . . . . . . 10
β’ πΌ = (π β β0 β¦
β«(0(,)Ο)((sinβπ§)βπ) dπ§) |
44 | 43 | wallispilem2 44393 |
. . . . . . . . 9
β’ ((πΌβ0) = Ο β§ (πΌβ1) = 2 β§ (2 β
(β€β₯β2) β (πΌβ2) = (((2 β 1) / 2) Β·
(πΌβ(2 β
2))))) |
45 | 44 | simp3i 1142 |
. . . . . . . 8
β’ (2 β
(β€β₯β2) β (πΌβ2) = (((2 β 1) / 2) Β·
(πΌβ(2 β
2)))) |
46 | 42, 45 | ax-mp 5 |
. . . . . . 7
β’ (πΌβ2) = (((2 β 1) / 2)
Β· (πΌβ(2
β 2))) |
47 | | 2m1e1 12284 |
. . . . . . . . 9
β’ (2
β 1) = 1 |
48 | 47 | oveq1i 7368 |
. . . . . . . 8
β’ ((2
β 1) / 2) = (1 / 2) |
49 | | 2cn 12233 |
. . . . . . . . . . 11
β’ 2 β
β |
50 | 49 | subidi 11477 |
. . . . . . . . . 10
β’ (2
β 2) = 0 |
51 | 50 | fveq2i 6846 |
. . . . . . . . 9
β’ (πΌβ(2 β 2)) = (πΌβ0) |
52 | 44 | simp1i 1140 |
. . . . . . . . 9
β’ (πΌβ0) =
Ο |
53 | 51, 52 | eqtri 2761 |
. . . . . . . 8
β’ (πΌβ(2 β 2)) =
Ο |
54 | 48, 53 | oveq12i 7370 |
. . . . . . 7
β’ (((2
β 1) / 2) Β· (πΌβ(2 β 2))) = ((1 / 2) Β·
Ο) |
55 | | ax-1cn 11114 |
. . . . . . . . 9
β’ 1 β
β |
56 | | 2cnne0 12368 |
. . . . . . . . 9
β’ (2 β
β β§ 2 β 0) |
57 | | picn 25832 |
. . . . . . . . 9
β’ Ο
β β |
58 | | div32 11838 |
. . . . . . . . 9
β’ ((1
β β β§ (2 β β β§ 2 β 0) β§ Ο β
β) β ((1 / 2) Β· Ο) = (1 Β· (Ο /
2))) |
59 | 55, 56, 57, 58 | mp3an 1462 |
. . . . . . . 8
β’ ((1 / 2)
Β· Ο) = (1 Β· (Ο / 2)) |
60 | | 2ne0 12262 |
. . . . . . . . . 10
β’ 2 β
0 |
61 | 57, 49, 60 | divcli 11902 |
. . . . . . . . 9
β’ (Ο /
2) β β |
62 | 61 | mulid2i 11165 |
. . . . . . . 8
β’ (1
Β· (Ο / 2)) = (Ο / 2) |
63 | 59, 62 | eqtri 2761 |
. . . . . . 7
β’ ((1 / 2)
Β· Ο) = (Ο / 2) |
64 | 46, 54, 63 | 3eqtri 2765 |
. . . . . 6
β’ (πΌβ2) = (Ο /
2) |
65 | | 3z 12541 |
. . . . . . . . 9
β’ 3 β
β€ |
66 | | 2re 12232 |
. . . . . . . . . 10
β’ 2 β
β |
67 | | 3re 12238 |
. . . . . . . . . 10
β’ 3 β
β |
68 | | 2lt3 12330 |
. . . . . . . . . 10
β’ 2 <
3 |
69 | 66, 67, 68 | ltleii 11283 |
. . . . . . . . 9
β’ 2 β€
3 |
70 | | eluz2 12774 |
. . . . . . . . 9
β’ (3 β
(β€β₯β2) β (2 β β€ β§ 3 β
β€ β§ 2 β€ 3)) |
71 | 40, 65, 69, 70 | mpbir3an 1342 |
. . . . . . . 8
β’ 3 β
(β€β₯β2) |
72 | 43 | wallispilem2 44393 |
. . . . . . . . 9
β’ ((πΌβ0) = Ο β§ (πΌβ1) = 2 β§ (3 β
(β€β₯β2) β (πΌβ3) = (((3 β 1) / 3) Β·
(πΌβ(3 β
2))))) |
73 | 72 | simp3i 1142 |
. . . . . . . 8
β’ (3 β
(β€β₯β2) β (πΌβ3) = (((3 β 1) / 3) Β·
(πΌβ(3 β
2)))) |
74 | 71, 73 | ax-mp 5 |
. . . . . . 7
β’ (πΌβ3) = (((3 β 1) / 3)
Β· (πΌβ(3
β 2))) |
75 | | 3m1e2 12286 |
. . . . . . . . . 10
β’ (3
β 1) = 2 |
76 | 75 | eqcomi 2742 |
. . . . . . . . 9
β’ 2 = (3
β 1) |
77 | 76 | oveq1i 7368 |
. . . . . . . 8
β’ (2 / 3) =
((3 β 1) / 3) |
78 | | 3cn 12239 |
. . . . . . . . . . 11
β’ 3 β
β |
79 | 78, 49, 55, 36 | subaddrii 11495 |
. . . . . . . . . 10
β’ (3
β 2) = 1 |
80 | 79 | fveq2i 6846 |
. . . . . . . . 9
β’ (πΌβ(3 β 2)) = (πΌβ1) |
81 | 44 | simp2i 1141 |
. . . . . . . . 9
β’ (πΌβ1) = 2 |
82 | 80, 81 | eqtr2i 2762 |
. . . . . . . 8
β’ 2 =
(πΌβ(3 β
2)) |
83 | 77, 82 | oveq12i 7370 |
. . . . . . 7
β’ ((2 / 3)
Β· 2) = (((3 β 1) / 3) Β· (πΌβ(3 β 2))) |
84 | | 3ne0 12264 |
. . . . . . . . 9
β’ 3 β
0 |
85 | 49, 78, 84 | divcli 11902 |
. . . . . . . 8
β’ (2 / 3)
β β |
86 | 85, 49 | mulcomi 11168 |
. . . . . . 7
β’ ((2 / 3)
Β· 2) = (2 Β· (2 / 3)) |
87 | 74, 83, 86 | 3eqtr2i 2767 |
. . . . . 6
β’ (πΌβ3) = (2 Β· (2 /
3)) |
88 | 64, 87 | oveq12i 7370 |
. . . . 5
β’ ((πΌβ2) / (πΌβ3)) = ((Ο / 2) / (2 Β· (2 /
3))) |
89 | | 1z 12538 |
. . . . . . . . 9
β’ 1 β
β€ |
90 | | seq1 13925 |
. . . . . . . . 9
β’ (1 β
β€ β (seq1( Β· , πΉ)β1) = (πΉβ1)) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . 8
β’ (seq1(
Β· , πΉ)β1) =
(πΉβ1) |
92 | | 1nn 12169 |
. . . . . . . . 9
β’ 1 β
β |
93 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (2 Β· π) = (2 Β·
1)) |
94 | 93, 33 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π = 1 β (2 Β· π) = 2) |
95 | 93 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ((2 Β· π) β 1) = ((2 Β· 1)
β 1)) |
96 | 33 | oveq1i 7368 |
. . . . . . . . . . . . . . 15
β’ ((2
Β· 1) β 1) = (2 β 1) |
97 | 96, 47 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’ ((2
Β· 1) β 1) = 1 |
98 | 95, 97 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π = 1 β ((2 Β· π) β 1) =
1) |
99 | 94, 98 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = 1 β ((2 Β· π) / ((2 Β· π) β 1)) = (2 /
1)) |
100 | 49 | div1i 11888 |
. . . . . . . . . . . 12
β’ (2 / 1) =
2 |
101 | 99, 100 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π = 1 β ((2 Β· π) / ((2 Β· π) β 1)) =
2) |
102 | 94 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π = 1 β ((2 Β· π) + 1) = (2 +
1)) |
103 | 102, 36 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π = 1 β ((2 Β· π) + 1) = 3) |
104 | 94, 103 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (π = 1 β ((2 Β· π) / ((2 Β· π) + 1)) = (2 /
3)) |
105 | 101, 104 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π = 1 β (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2
Β· π) / ((2 Β·
π) + 1))) = (2 Β· (2
/ 3))) |
106 | | wallispilem4.1 |
. . . . . . . . . 10
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2
Β· π) / ((2 Β·
π) + 1)))) |
107 | | ovex 7391 |
. . . . . . . . . 10
β’ (2
Β· (2 / 3)) β V |
108 | 105, 106,
107 | fvmpt 6949 |
. . . . . . . . 9
β’ (1 β
β β (πΉβ1)
= (2 Β· (2 / 3))) |
109 | 92, 108 | ax-mp 5 |
. . . . . . . 8
β’ (πΉβ1) = (2 Β· (2 /
3)) |
110 | 91, 109 | eqtr2i 2762 |
. . . . . . 7
β’ (2
Β· (2 / 3)) = (seq1( Β· , πΉ)β1) |
111 | 110 | oveq2i 7369 |
. . . . . 6
β’ ((Ο /
2) / (2 Β· (2 / 3))) = ((Ο / 2) / (seq1( Β· , πΉ)β1)) |
112 | 49, 85 | mulcli 11167 |
. . . . . . . . 9
β’ (2
Β· (2 / 3)) β β |
113 | 109, 112 | eqeltri 2830 |
. . . . . . . 8
β’ (πΉβ1) β
β |
114 | 91, 113 | eqeltri 2830 |
. . . . . . 7
β’ (seq1(
Β· , πΉ)β1)
β β |
115 | 49, 78, 60, 84 | divne0i 11908 |
. . . . . . . . 9
β’ (2 / 3)
β 0 |
116 | 49, 85, 60, 115 | mulne0i 11803 |
. . . . . . . 8
β’ (2
Β· (2 / 3)) β 0 |
117 | 110, 116 | eqnetrri 3012 |
. . . . . . 7
β’ (seq1(
Β· , πΉ)β1) β
0 |
118 | 61, 114, 117 | divreci 11905 |
. . . . . 6
β’ ((Ο /
2) / (seq1( Β· , πΉ)β1)) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)β1))) |
119 | 111, 118 | eqtri 2761 |
. . . . 5
β’ ((Ο /
2) / (2 Β· (2 / 3))) = ((Ο / 2) Β· (1 / (seq1( Β· , πΉ)β1))) |
120 | 39, 88, 119 | 3eqtri 2765 |
. . . 4
β’ ((πΌβ(2 Β· 1)) / (πΌβ((2 Β· 1) + 1))) =
((Ο / 2) Β· (1 / (seq1( Β· , πΉ)β1))) |
121 | | oveq2 7366 |
. . . . . . 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( Β· , πΉ)βπ¦))))) |
122 | 121 | adantl 483 |
. . . . . 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( Β· , πΉ)βπ¦))))) |
123 | | 2cnd 12236 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β 2 β
β) |
124 | | nncn 12166 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β π¦ β
β) |
125 | 55 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β 1 β
β) |
126 | 123, 124,
125 | adddid 11184 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (2
Β· (π¦ + 1)) = ((2
Β· π¦) + (2 Β·
1))) |
127 | 123 | mulid1d 11177 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β (2
Β· 1) = 2) |
128 | 127 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· π¦) + (2 Β·
1)) = ((2 Β· π¦) +
2)) |
129 | 126, 128 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
Β· (π¦ + 1)) = ((2
Β· π¦) +
2)) |
130 | 129 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) β
1) = (((2 Β· π¦) + 2)
β 1)) |
131 | 123, 124 | mulcld 11180 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
Β· π¦) β
β) |
132 | 131, 123,
125 | addsubassd 11537 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· π¦) + 2) β 1)
= ((2 Β· π¦) + (2
β 1))) |
133 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
β 1) = 1) |
134 | 133 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· π¦) + (2 β
1)) = ((2 Β· π¦) +
1)) |
135 | 130, 132,
134 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((2
Β· (π¦ + 1)) β
1) = ((2 Β· π¦) +
1)) |
136 | 135 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π¦ β β β (((2
Β· (π¦ + 1)) β
1) / (2 Β· (π¦ + 1)))
= (((2 Β· π¦) + 1) /
(2 Β· (π¦ +
1)))) |
137 | 136 | oveq1d 7373 |
. . . . . . . . . 10
β’ (π¦ β β β ((((2
Β· (π¦ + 1)) β
1) / (2 Β· (π¦ + 1)))
Β· (πΌβ(2
Β· π¦))) = ((((2
Β· π¦) + 1) / (2
Β· (π¦ + 1))) Β·
(πΌβ(2 Β· π¦)))) |
138 | 75 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (3
β 1) = 2) |
139 | 138 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· π¦) + (3 β
1)) = ((2 Β· π¦) +
2)) |
140 | 78 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 3 β
β) |
141 | 131, 140,
125 | addsubassd 11537 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· π¦) + 3) β 1)
= ((2 Β· π¦) + (3
β 1))) |
142 | 139, 141,
129 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ (π¦ β β β (((2
Β· π¦) + 3) β 1)
= (2 Β· (π¦ +
1))) |
143 | 142 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π¦ β β β ((((2
Β· π¦) + 3) β 1)
/ ((2 Β· π¦) + 3)) =
((2 Β· (π¦ + 1)) / ((2
Β· π¦) +
3))) |
144 | 143 | oveq1d 7373 |
. . . . . . . . . 10
β’ (π¦ β β β (((((2
Β· π¦) + 3) β 1)
/ ((2 Β· π¦) + 3))
Β· (πΌβ(((2
Β· π¦) + 3) β
2))) = (((2 Β· (π¦ +
1)) / ((2 Β· π¦) + 3))
Β· (πΌβ(((2
Β· π¦) + 3) β
2)))) |
145 | 137, 144 | oveq12d 7376 |
. . . . . . . . 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))))) |
146 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 2 β
β€) |
147 | | nnz 12525 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β π¦ β
β€) |
148 | 147 | peano2zd 12615 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (π¦ + 1) β
β€) |
149 | 146, 148 | zmulcld 12618 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
β€) |
150 | 66 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 2 β
β) |
151 | | nnre 12165 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β π¦ β
β) |
152 | | 1red 11161 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 1 β
β) |
153 | 151, 152 | readdcld 11189 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (π¦ + 1) β
β) |
154 | | 0le2 12260 |
. . . . . . . . . . . . . . 15
β’ 0 β€
2 |
155 | 154 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 0 β€
2) |
156 | | nnnn0 12425 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β π¦ β
β0) |
157 | 156 | nn0ge0d 12481 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 0 β€
π¦) |
158 | 152, 151 | addge02d 11749 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (0 β€
π¦ β 1 β€ (π¦ + 1))) |
159 | 157, 158 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 1 β€
(π¦ + 1)) |
160 | 150, 153,
155, 159 | lemulge11d 12097 |
. . . . . . . . . . . . 13
β’ (π¦ β β β 2 β€ (2
Β· (π¦ +
1))) |
161 | 40 | eluz1i 12776 |
. . . . . . . . . . . . 13
β’ ((2
Β· (π¦ + 1)) β
(β€β₯β2) β ((2 Β· (π¦ + 1)) β β€ β§ 2 β€ (2
Β· (π¦ +
1)))) |
162 | 149, 160,
161 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
(β€β₯β2)) |
163 | 43, 162 | itgsinexp 44282 |
. . . . . . . . . . 11
β’ (π¦ β β β (πΌβ(2 Β· (π¦ + 1))) = ((((2 Β· (π¦ + 1)) β 1) / (2 Β·
(π¦ + 1))) Β· (πΌβ((2 Β· (π¦ + 1)) β
2)))) |
164 | 129 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β ((2
Β· (π¦ + 1)) β
2) = (((2 Β· π¦) + 2)
β 2)) |
165 | 131, 123 | pncand 11518 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (((2
Β· π¦) + 2) β 2)
= (2 Β· π¦)) |
166 | 164, 165 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) β
2) = (2 Β· π¦)) |
167 | 166 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π¦ β β β (πΌβ((2 Β· (π¦ + 1)) β 2)) = (πΌβ(2 Β· π¦))) |
168 | 167 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π¦ β β β ((((2
Β· (π¦ + 1)) β
1) / (2 Β· (π¦ + 1)))
Β· (πΌβ((2
Β· (π¦ + 1)) β
2))) = ((((2 Β· (π¦ +
1)) β 1) / (2 Β· (π¦ + 1))) Β· (πΌβ(2 Β· π¦)))) |
169 | 163, 168 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π¦ β β β (πΌβ(2 Β· (π¦ + 1))) = ((((2 Β· (π¦ + 1)) β 1) / (2 Β·
(π¦ + 1))) Β· (πΌβ(2 Β· π¦)))) |
170 | 129 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) + 1) =
(((2 Β· π¦) + 2) +
1)) |
171 | 131, 123,
125 | addassd 11182 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· π¦) + 2) + 1) = ((2
Β· π¦) + (2 +
1))) |
172 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2 + 1) =
3) |
173 | 172 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· π¦) + (2 + 1)) =
((2 Β· π¦) +
3)) |
174 | 170, 171,
173 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((2
Β· (π¦ + 1)) + 1) =
((2 Β· π¦) +
3)) |
175 | 174 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π¦ β β β (πΌβ((2 Β· (π¦ + 1)) + 1)) = (πΌβ((2 Β· π¦) + 3))) |
176 | 146, 147 | zmulcld 12618 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
Β· π¦) β
β€) |
177 | 65 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 3 β
β€) |
178 | 176, 177 | zaddcld 12616 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· π¦) + 3) β
β€) |
179 | 150, 151 | remulcld 11190 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
Β· π¦) β
β) |
180 | 67 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 3 β
β) |
181 | 179, 180 | readdcld 11189 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β ((2
Β· π¦) + 3) β
β) |
182 | | nnge1 12186 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 1 β€
π¦) |
183 | 150, 151,
155, 182 | lemulge11d 12097 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 2 β€ (2
Β· π¦)) |
184 | | 0re 11162 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
185 | | 3pos 12263 |
. . . . . . . . . . . . . . . 16
β’ 0 <
3 |
186 | 184, 67, 185 | ltleii 11283 |
. . . . . . . . . . . . . . 15
β’ 0 β€
3 |
187 | 179, 180 | addge01d 11748 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (0 β€ 3
β (2 Β· π¦) β€
((2 Β· π¦) +
3))) |
188 | 186, 187 | mpbii 232 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
Β· π¦) β€ ((2
Β· π¦) +
3)) |
189 | 150, 179,
181, 183, 188 | letrd 11317 |
. . . . . . . . . . . . 13
β’ (π¦ β β β 2 β€
((2 Β· π¦) +
3)) |
190 | 40 | eluz1i 12776 |
. . . . . . . . . . . . 13
β’ (((2
Β· π¦) + 3) β
(β€β₯β2) β (((2 Β· π¦) + 3) β β€ β§ 2 β€ ((2
Β· π¦) +
3))) |
191 | 178, 189,
190 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((2
Β· π¦) + 3) β
(β€β₯β2)) |
192 | 43, 191 | itgsinexp 44282 |
. . . . . . . . . . 11
β’ (π¦ β β β (πΌβ((2 Β· π¦) + 3)) = (((((2 Β· π¦) + 3) β 1) / ((2 Β·
π¦) + 3)) Β· (πΌβ(((2 Β· π¦) + 3) β
2)))) |
193 | 175, 192 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π¦ β β β (πΌβ((2 Β· (π¦ + 1)) + 1)) = (((((2 Β·
π¦) + 3) β 1) / ((2
Β· π¦) + 3)) Β·
(πΌβ(((2 Β·
π¦) + 3) β
2)))) |
194 | 169, 193 | oveq12d 7376 |
. . . . . . . . 9
β’ (π¦ β β β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = (((((2 Β· (π¦ + 1)) β 1) / (2 Β·
(π¦ + 1))) Β· (πΌβ(2 Β· π¦))) / (((((2 Β· π¦) + 3) β 1) / ((2 Β·
π¦) + 3)) Β· (πΌβ(((2 Β· π¦) + 3) β
2))))) |
195 | 131, 125 | addcld 11179 |
. . . . . . . . . . 11
β’ (π¦ β β β ((2
Β· π¦) + 1) β
β) |
196 | 124, 125 | addcld 11179 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ + 1) β
β) |
197 | 123, 196 | mulcld 11180 |
. . . . . . . . . . 11
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
β) |
198 | 60 | a1i 11 |
. . . . . . . . . . . 12
β’ (π¦ β β β 2 β
0) |
199 | | peano2nn 12170 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ + 1) β
β) |
200 | 199 | nnne0d 12208 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ + 1) β 0) |
201 | 123, 196,
198, 200 | mulne0d 11812 |
. . . . . . . . . . 11
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
0) |
202 | 195, 197,
201 | divcld 11936 |
. . . . . . . . . 10
β’ (π¦ β β β (((2
Β· π¦) + 1) / (2
Β· (π¦ + 1))) β
β) |
203 | | 2nn0 12435 |
. . . . . . . . . . . . 13
β’ 2 β
β0 |
204 | 203 | a1i 11 |
. . . . . . . . . . . 12
β’ (π¦ β β β 2 β
β0) |
205 | 204, 156 | nn0mulcld 12483 |
. . . . . . . . . . 11
β’ (π¦ β β β (2
Β· π¦) β
β0) |
206 | 43 | wallispilem3 44394 |
. . . . . . . . . . . 12
β’ ((2
Β· π¦) β
β0 β (πΌβ(2 Β· π¦)) β
β+) |
207 | 206 | rpcnd 12964 |
. . . . . . . . . . 11
β’ ((2
Β· π¦) β
β0 β (πΌβ(2 Β· π¦)) β β) |
208 | 205, 207 | syl 17 |
. . . . . . . . . 10
β’ (π¦ β β β (πΌβ(2 Β· π¦)) β
β) |
209 | 131, 140 | addcld 11179 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((2
Β· π¦) + 3) β
β) |
210 | | 0red 11163 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 0 β
β) |
211 | | 2pos 12261 |
. . . . . . . . . . . . . . . 16
β’ 0 <
2 |
212 | 211 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 0 <
2) |
213 | | nngt0 12189 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 0 <
π¦) |
214 | 150, 151,
212, 213 | mulgt0d 11315 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 0 < (2
Β· π¦)) |
215 | 180, 185 | jctir 522 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β (3 β
β β§ 0 < 3)) |
216 | | elrp 12922 |
. . . . . . . . . . . . . . . 16
β’ (3 β
β+ β (3 β β β§ 0 < 3)) |
217 | 215, 216 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β 3 β
β+) |
218 | 179, 217 | ltaddrpd 12995 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (2
Β· π¦) < ((2
Β· π¦) +
3)) |
219 | 210, 179,
181, 214, 218 | lttrd 11321 |
. . . . . . . . . . . . 13
β’ (π¦ β β β 0 <
((2 Β· π¦) +
3)) |
220 | 219 | gt0ne0d 11724 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((2
Β· π¦) + 3) β
0) |
221 | 197, 209,
220 | divcld 11936 |
. . . . . . . . . . 11
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3)) β
β) |
222 | 197, 209,
201, 220 | divne0d 11952 |
. . . . . . . . . . 11
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3)) β
0) |
223 | 178, 146 | zsubcld 12617 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (((2
Β· π¦) + 3) β 2)
β β€) |
224 | 181, 150 | subge0d 11750 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (0 β€
(((2 Β· π¦) + 3)
β 2) β 2 β€ ((2 Β· π¦) + 3))) |
225 | 189, 224 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β 0 β€
(((2 Β· π¦) + 3)
β 2)) |
226 | | elnn0z 12517 |
. . . . . . . . . . . . . 14
β’ ((((2
Β· π¦) + 3) β 2)
β β0 β ((((2 Β· π¦) + 3) β 2) β β€ β§ 0 β€
(((2 Β· π¦) + 3)
β 2))) |
227 | 223, 225,
226 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· π¦) + 3) β 2)
β β0) |
228 | 43 | wallispilem3 44394 |
. . . . . . . . . . . . 13
β’ ((((2
Β· π¦) + 3) β 2)
β β0 β (πΌβ(((2 Β· π¦) + 3) β 2)) β
β+) |
229 | 227, 228 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β β β (πΌβ(((2 Β· π¦) + 3) β 2)) β
β+) |
230 | 229 | rpcnne0d 12971 |
. . . . . . . . . . 11
β’ (π¦ β β β ((πΌβ(((2 Β· π¦) + 3) β 2)) β
β β§ (πΌβ(((2
Β· π¦) + 3) β
2)) β 0)) |
231 | 221, 222,
230 | jca31 516 |
. . . . . . . . . 10
β’ (π¦ β β β ((((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3)) β
β β§ ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)) β 0) β§ ((πΌβ(((2 Β· π¦) + 3) β 2)) β β β§
(πΌβ(((2 Β·
π¦) + 3) β 2)) β
0))) |
232 | | divmuldiv 11860 |
. . . . . . . . . 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))))) |
233 | 202, 208,
231, 232 | syl21anc 837 |
. . . . . . . . 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))))) |
234 | 145, 194,
233 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (π¦ β β β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = (((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) Β· ((πΌβ(2 Β· π¦)) / (πΌβ(((2 Β· π¦) + 3) β 2))))) |
235 | 131, 140,
123 | addsubassd 11537 |
. . . . . . . . . . . 12
β’ (π¦ β β β (((2
Β· π¦) + 3) β 2)
= ((2 Β· π¦) + (3
β 2))) |
236 | 79 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (3
β 2) = 1) |
237 | 236 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((2
Β· π¦) + (3 β
2)) = ((2 Β· π¦) +
1)) |
238 | 235, 237 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π¦ β β β (((2
Β· π¦) + 3) β 2)
= ((2 Β· π¦) +
1)) |
239 | 238 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π¦ β β β (πΌβ(((2 Β· π¦) + 3) β 2)) = (πΌβ((2 Β· π¦) + 1))) |
240 | 239 | oveq2d 7374 |
. . . . . . . . 9
β’ (π¦ β β β ((πΌβ(2 Β· π¦)) / (πΌβ(((2 Β· π¦) + 3) β 2))) = ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1)))) |
241 | 240 | oveq2d 7374 |
. . . . . . . 8
β’ (π¦ β β β (((((2
Β· π¦) + 1) / (2
Β· (π¦ + 1))) / ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) Β·
((πΌβ(2 Β· π¦)) / (πΌβ(((2 Β· π¦) + 3) β 2)))) = (((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) Β· ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))))) |
242 | 234, 241 | eqtrd 2773 |
. . . . . . 7
β’ (π¦ β β β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = (((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) Β· ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))))) |
243 | 242 | adantr 482 |
. . . . . 6
β’ ((π¦ β β β§ ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ¦)))) β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = (((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) Β· ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))))) |
244 | | elnnuz 12812 |
. . . . . . . . . . . . 13
β’ (π¦ β β β π¦ β
(β€β₯β1)) |
245 | 244 | biimpi 215 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ β
(β€β₯β1)) |
246 | | seqp1 13927 |
. . . . . . . . . . . 12
β’ (π¦ β
(β€β₯β1) β (seq1( Β· , πΉ)β(π¦ + 1)) = ((seq1( Β· , πΉ)βπ¦) Β· (πΉβ(π¦ + 1)))) |
247 | 245, 246 | syl 17 |
. . . . . . . . . . 11
β’ (π¦ β β β (seq1(
Β· , πΉ)β(π¦ + 1)) = ((seq1( Β· ,
πΉ)βπ¦) Β· (πΉβ(π¦ + 1)))) |
248 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π = (π¦ + 1) β (2 Β· π) = (2 Β· (π¦ + 1))) |
249 | 248 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π = (π¦ + 1) β ((2 Β· π) β 1) = ((2 Β· (π¦ + 1)) β
1)) |
250 | 248, 249 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π = (π¦ + 1) β ((2 Β· π) / ((2 Β· π) β 1)) = ((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β
1))) |
251 | 248 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π = (π¦ + 1) β ((2 Β· π) + 1) = ((2 Β· (π¦ + 1)) + 1)) |
252 | 248, 251 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π = (π¦ + 1) β ((2 Β· π) / ((2 Β· π) + 1)) = ((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) + 1))) |
253 | 250, 252 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π = (π¦ + 1) β (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1))) = (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) +
1)))) |
254 | 150, 153 | remulcld 11190 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
β) |
255 | 254, 152 | resubcld 11588 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· (π¦ + 1)) β
1) β β) |
256 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 <
2 |
257 | 256 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β β β 1 <
2) |
258 | | nnrp 12931 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β β β π¦ β
β+) |
259 | 152, 258 | ltaddrp2d 12996 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β β β 1 <
(π¦ + 1)) |
260 | 150, 153,
257, 259 | mulgt1d 12096 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β 1 < (2
Β· (π¦ +
1))) |
261 | 152, 260 | gtned 11295 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
1) |
262 | 197, 125,
261 | subne0d 11526 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· (π¦ + 1)) β
1) β 0) |
263 | 254, 255,
262 | redivcld 11988 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) β
1)) β β) |
264 | 174, 181 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· (π¦ + 1)) + 1)
β β) |
265 | 174, 220 | eqnetrd 3008 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· (π¦ + 1)) + 1) β
0) |
266 | 254, 264,
265 | redivcld 11988 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) + 1))
β β) |
267 | 263, 266 | remulcld 11190 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) β
1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) + 1))) β
β) |
268 | 106, 253,
199, 267 | fvmptd3 6972 |
. . . . . . . . . . . 12
β’ (π¦ β β β (πΉβ(π¦ + 1)) = (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
(π¦ + 1)) +
1)))) |
269 | 268 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π¦ β β β ((seq1(
Β· , πΉ)βπ¦) Β· (πΉβ(π¦ + 1))) = ((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
(π¦ + 1)) +
1))))) |
270 | 247, 269 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π¦ β β β (seq1(
Β· , πΉ)β(π¦ + 1)) = ((seq1( Β· ,
πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
(π¦ + 1)) +
1))))) |
271 | 270 | oveq2d 7374 |
. . . . . . . . 9
β’ (π¦ β β β (1 /
(seq1( Β· , πΉ)β(π¦ + 1))) = (1 / ((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
(π¦ + 1)) +
1)))))) |
272 | 271 | oveq2d 7374 |
. . . . . . . 8
β’ (π¦ β β β ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)β(π¦ + 1)))) = ((Ο / 2) Β· (1 / ((seq1(
Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) +
1))))))) |
273 | 135 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) β
1)) = ((2 Β· (π¦ + 1))
/ ((2 Β· π¦) +
1))) |
274 | 174 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) + 1)) =
((2 Β· (π¦ + 1)) / ((2
Β· π¦) +
3))) |
275 | 273, 274 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π¦ β β β (((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) β
1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) + 1))) = (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
π¦) + 3)))) |
276 | 275 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π¦ β β β ((seq1(
Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2
Β· (π¦ + 1)) / ((2
Β· (π¦ + 1)) + 1)))) =
((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))))) |
277 | 276 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π¦ β β β (1 /
((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· (π¦ + 1)) β 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
(π¦ + 1)) + 1))))) = (1 /
((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))))) |
278 | 277 | oveq2d 7374 |
. . . . . . . . 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))))))) |
279 | | elfznn 13476 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β (1...π¦) β π€ β β) |
280 | 279 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β β β§ π€ β (1...π¦)) β π€ β β) |
281 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π€ β (2 Β· π) = (2 Β· π€)) |
282 | 281 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π€ β ((2 Β· π) β 1) = ((2 Β· π€) β 1)) |
283 | 281, 282 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π€ β ((2 Β· π) / ((2 Β· π) β 1)) = ((2 Β· π€) / ((2 Β· π€) β 1))) |
284 | 281 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π€ β ((2 Β· π) + 1) = ((2 Β· π€) + 1)) |
285 | 281, 284 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π€ β ((2 Β· π) / ((2 Β· π) + 1)) = ((2 Β· π€) / ((2 Β· π€) + 1))) |
286 | 283, 285 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π€ β (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2 Β· π) / ((2 Β· π) + 1))) = (((2 Β· π€) / ((2 Β· π€) β 1)) Β· ((2
Β· π€) / ((2 Β·
π€) + 1)))) |
287 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β β β π€ β
β) |
288 | | 2rp 12925 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β+ |
289 | 288 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β β β 2 β
β+) |
290 | | nnrp 12931 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β β β π€ β
β+) |
291 | 289, 290 | rpmulcld 12978 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β β β (2
Β· π€) β
β+) |
292 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β β β 2 β
β) |
293 | | nnre 12165 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β β β π€ β
β) |
294 | 292, 293 | remulcld 11190 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β β β (2
Β· π€) β
β) |
295 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β β β 1 β
β) |
296 | 294, 295 | resubcld 11588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β β β ((2
Β· π€) β 1)
β β) |
297 | | nnge1 12186 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β β β 1 β€
π€) |
298 | | nncn 12166 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ β β β π€ β
β) |
299 | 298 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β β β (1
Β· π€) = π€) |
300 | 295, 292,
290 | ltmul1d 13003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ β β β (1 < 2
β (1 Β· π€) <
(2 Β· π€))) |
301 | 256, 300 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β β β (1
Β· π€) < (2
Β· π€)) |
302 | 299, 301 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β β β π€ < (2 Β· π€)) |
303 | 295, 293,
294, 297, 302 | lelttrd 11318 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β β β 1 < (2
Β· π€)) |
304 | 295, 294 | posdifd 11747 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β β β (1 <
(2 Β· π€) β 0
< ((2 Β· π€)
β 1))) |
305 | 303, 304 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β β β 0 <
((2 Β· π€) β
1)) |
306 | 296, 305 | elrpd 12959 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β β β ((2
Β· π€) β 1)
β β+) |
307 | 291, 306 | rpdivcld 12979 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β β β ((2
Β· π€) / ((2 Β·
π€) β 1)) β
β+) |
308 | 154 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β β β 0 β€
2) |
309 | 290 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β β β 0 β€
π€) |
310 | 292, 293,
308, 309 | mulge0d 11737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β β β 0 β€ (2
Β· π€)) |
311 | 294, 310 | ge0p1rpd 12992 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β β β ((2
Β· π€) + 1) β
β+) |
312 | 291, 311 | rpdivcld 12979 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β β β ((2
Β· π€) / ((2 Β·
π€) + 1)) β
β+) |
313 | 307, 312 | rpmulcld 12978 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β β β (((2
Β· π€) / ((2 Β·
π€) β 1)) Β· ((2
Β· π€) / ((2 Β·
π€) + 1))) β
β+) |
314 | 106, 286,
287, 313 | fvmptd3 6972 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β β β (πΉβπ€) = (((2 Β· π€) / ((2 Β· π€) β 1)) Β· ((2 Β· π€) / ((2 Β· π€) + 1)))) |
315 | 314, 313 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’ (π€ β β β (πΉβπ€) β
β+) |
316 | 280, 315 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π€ β (1...π¦)) β (πΉβπ€) β
β+) |
317 | | rpmulcl 12943 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β β+
β§ π§ β
β+) β (π€ Β· π§) β
β+) |
318 | 317 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ (π€ β β+
β§ π§ β
β+)) β (π€ Β· π§) β
β+) |
319 | 245, 316,
318 | seqcl 13934 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (seq1(
Β· , πΉ)βπ¦) β
β+) |
320 | 319 | rpcnne0d 12971 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((seq1(
Β· , πΉ)βπ¦) β β β§ (seq1(
Β· , πΉ)βπ¦) β 0)) |
321 | 288 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β 2 β
β+) |
322 | 151, 157 | ge0p1rpd 12992 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β (π¦ + 1) β
β+) |
323 | 321, 322 | rpmulcld 12978 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β (2
Β· (π¦ + 1)) β
β+) |
324 | 150, 151,
155, 157 | mulge0d 11737 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β 0 β€ (2
Β· π¦)) |
325 | 179, 324 | ge0p1rpd 12992 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β ((2
Β· π¦) + 1) β
β+) |
326 | 323, 325 | rpdivcld 12979 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 1)) β
β+) |
327 | 321, 258 | rpmulcld 12978 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β (2
Β· π¦) β
β+) |
328 | 327, 217 | rpaddcld 12977 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β ((2
Β· π¦) + 3) β
β+) |
329 | 323, 328 | rpdivcld 12979 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3)) β
β+) |
330 | 326, 329 | rpmulcld 12978 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 1)) Β·
((2 Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) β
β+) |
331 | 330 | rpcnne0d 12971 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 1)) Β·
((2 Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) β
β β§ (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) β
0)) |
332 | | divdiv1 11871 |
. . . . . . . . . . . . 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)))))) |
333 | 125, 320,
331, 332 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((1 /
(seq1( Β· , πΉ)βπ¦)) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))) = (1 / ((seq1(
Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
π¦) +
3)))))) |
334 | 333 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π¦ β β β (1 /
((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))))) = ((1 / (seq1(
Β· , πΉ)βπ¦)) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β·
(π¦ + 1)) / ((2 Β·
π¦) +
3))))) |
335 | 334 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π¦ β β β ((Ο /
2) Β· (1 / ((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))))) = ((Ο / 2)
Β· ((1 / (seq1( Β· , πΉ)βπ¦)) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))))) |
336 | 61 | a1i 11 |
. . . . . . . . . . 11
β’ (π¦ β β β (Ο /
2) β β) |
337 | 319 | rpcnd 12964 |
. . . . . . . . . . . 12
β’ (π¦ β β β (seq1(
Β· , πΉ)βπ¦) β
β) |
338 | 319 | rpne0d 12967 |
. . . . . . . . . . . 12
β’ (π¦ β β β (seq1(
Β· , πΉ)βπ¦) β 0) |
339 | 337, 338 | reccld 11929 |
. . . . . . . . . . 11
β’ (π¦ β β β (1 /
(seq1( Β· , πΉ)βπ¦)) β β) |
340 | 330 | rpcnd 12964 |
. . . . . . . . . . 11
β’ (π¦ β β β (((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 1)) Β·
((2 Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) β
β) |
341 | 330 | rpne0d 12967 |
. . . . . . . . . . 11
β’ (π¦ β β β (((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 1)) Β·
((2 Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) β
0) |
342 | 336, 339,
340, 341 | divassd 11971 |
. . . . . . . . . 10
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))) = ((Ο / 2) Β·
((1 / (seq1( Β· , πΉ)βπ¦)) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))))) |
343 | 135, 262 | eqnetrrd 3009 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· π¦) + 1) β
0) |
344 | 197, 195,
197, 209, 343, 220 | divmuldivd 11977 |
. . . . . . . . . . . 12
β’ (π¦ β β β (((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 1)) Β·
((2 Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) = (((2
Β· (π¦ + 1)) Β·
(2 Β· (π¦ + 1))) /
(((2 Β· π¦) + 1)
Β· ((2 Β· π¦) +
3)))) |
345 | 344 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))) = (((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ¦))) / (((2 Β· (π¦ + 1)) Β· (2 Β· (π¦ + 1))) / (((2 Β· π¦) + 1) Β· ((2 Β·
π¦) +
3))))) |
346 | 336, 339 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) β β) |
347 | 197, 197 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) Β·
(2 Β· (π¦ + 1)))
β β) |
348 | 195, 209 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· π¦) + 1) Β·
((2 Β· π¦) + 3))
β β) |
349 | 197, 197,
201, 201 | mulne0d 11812 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((2
Β· (π¦ + 1)) Β·
(2 Β· (π¦ + 1))) β
0) |
350 | 195, 209,
343, 220 | mulne0d 11812 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (((2
Β· π¦) + 1) Β·
((2 Β· π¦) + 3)) β
0) |
351 | 346, 347,
348, 349, 350 | divdiv2d 11968 |
. . . . . . . . . . . 12
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) / (((2 Β· (π¦ + 1)) Β· (2 Β· (π¦ + 1))) / (((2 Β· π¦) + 1) Β· ((2 Β·
π¦) + 3)))) = ((((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· (((2 Β· π¦) + 1) Β· ((2 Β· π¦) + 3))) / ((2 Β· (π¦ + 1)) Β· (2 Β·
(π¦ +
1))))) |
352 | 346, 348,
347, 349 | divassd 11971 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((((Ο
/ 2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· (((2 Β· π¦) + 1) Β· ((2 Β· π¦) + 3))) / ((2 Β· (π¦ + 1)) Β· (2 Β·
(π¦ + 1)))) = (((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) Β· ((2 Β·
π¦) + 3)) / ((2 Β·
(π¦ + 1)) Β· (2
Β· (π¦ +
1)))))) |
353 | 351, 352 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) / (((2 Β· (π¦ + 1)) Β· (2 Β· (π¦ + 1))) / (((2 Β· π¦) + 1) Β· ((2 Β·
π¦) + 3)))) = (((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) Β· ((2 Β·
π¦) + 3)) / ((2 Β·
(π¦ + 1)) Β· (2
Β· (π¦ +
1)))))) |
354 | 195, 197,
197, 209, 201, 220, 201 | divdivdivd 11983 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((((2
Β· π¦) + 1) / (2
Β· (π¦ + 1))) / ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) = ((((2
Β· π¦) + 1) Β·
((2 Β· π¦) + 3)) / ((2
Β· (π¦ + 1)) Β·
(2 Β· (π¦ +
1))))) |
355 | 354 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π¦ β β β ((((2
Β· π¦) + 1) Β·
((2 Β· π¦) + 3)) / ((2
Β· (π¦ + 1)) Β·
(2 Β· (π¦ + 1)))) =
((((2 Β· π¦) + 1) / (2
Β· (π¦ + 1))) / ((2
Β· (π¦ + 1)) / ((2
Β· π¦) +
3)))) |
356 | 355 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) Β· ((2 Β·
π¦) + 3)) / ((2 Β·
(π¦ + 1)) Β· (2
Β· (π¦ + 1))))) =
(((Ο / 2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))))) |
357 | 345, 353,
356 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) / (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))) = (((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))))) |
358 | 335, 342,
357 | 3eqtr2d 2779 |
. . . . . . . . 9
β’ (π¦ β β β ((Ο /
2) Β· (1 / ((seq1( Β· , πΉ)βπ¦) Β· (((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 1)) Β· ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))))) = (((Ο / 2)
Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))))) |
359 | 57 | a1i 11 |
. . . . . . . . . . . 12
β’ (π¦ β β β Ο
β β) |
360 | 359 | halfcld 12403 |
. . . . . . . . . . 11
β’ (π¦ β β β (Ο /
2) β β) |
361 | 360, 339 | mulcld 11180 |
. . . . . . . . . 10
β’ (π¦ β β β ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) β β) |
362 | 202, 221,
222 | divcld 11936 |
. . . . . . . . . 10
β’ (π¦ β β β ((((2
Β· π¦) + 1) / (2
Β· (π¦ + 1))) / ((2
Β· (π¦ + 1)) / ((2
Β· π¦) + 3))) β
β) |
363 | 361, 362 | mulcomd 11181 |
. . . . . . . . 9
β’ (π¦ β β β (((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))) Β· ((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3)))) = (((((2 Β·
π¦) + 1) / (2 Β·
(π¦ + 1))) / ((2 Β·
(π¦ + 1)) / ((2 Β·
π¦) + 3))) Β· ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)βπ¦))))) |
364 | 278, 358,
363 | 3eqtrd 2777 |
. . . . . . . 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( Β· , πΉ)βπ¦))))) |
365 | 272, 364 | eqtrd 2773 |
. . . . . . 7
β’ (π¦ β β β ((Ο /
2) Β· (1 / (seq1( Β· , πΉ)β(π¦ + 1)))) = (((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) Β· ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)βπ¦))))) |
366 | 365 | adantr 482 |
. . . . . 6
β’ ((π¦ β β β§ ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ¦)))) β ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)β(π¦ + 1)))) = (((((2 Β· π¦) + 1) / (2 Β· (π¦ + 1))) / ((2 Β· (π¦ + 1)) / ((2 Β· π¦) + 3))) Β· ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)βπ¦))))) |
367 | 122, 243,
366 | 3eqtr4d 2783 |
. . . . 5
β’ ((π¦ β β β§ ((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ¦)))) β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)β(π¦ + 1))))) |
368 | 367 | ex 414 |
. . . 4
β’ (π¦ β β β (((πΌβ(2 Β· π¦)) / (πΌβ((2 Β· π¦) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ¦))) β ((πΌβ(2 Β· (π¦ + 1))) / (πΌβ((2 Β· (π¦ + 1)) + 1))) = ((Ο / 2) Β· (1 /
(seq1( Β· , πΉ)β(π¦ + 1)))))) |
369 | 8, 16, 24, 32, 120, 368 | nnind 12176 |
. . 3
β’ (π β β β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) = ((Ο / 2) Β· (1 / (seq1(
Β· , πΉ)βπ)))) |
370 | 369 | mpteq2ia 5209 |
. 2
β’ (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) = (π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ)))) |
371 | | wallispilem4.3 |
. 2
β’ πΊ = (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
372 | | wallispilem4.4 |
. 2
β’ π» = (π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ)))) |
373 | 370, 371,
372 | 3eqtr4i 2771 |
1
β’ πΊ = π» |