Step | Hyp | Ref
| Expression |
1 | | fveq2 6889 |
. . 3
โข (๐ฅ = 1 โ (seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1)))))โ๐ฅ) = (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) +
1)))))โ1)) |
2 | | oveq2 7414 |
. . . . . 6
โข (๐ฅ = 1 โ (2 ยท ๐ฅ) = (2 ยท
1)) |
3 | 2 | oveq1d 7421 |
. . . . 5
โข (๐ฅ = 1 โ ((2 ยท ๐ฅ) + 1) = ((2 ยท 1) +
1)) |
4 | 3 | oveq2d 7422 |
. . . 4
โข (๐ฅ = 1 โ (1 / ((2 ยท
๐ฅ) + 1)) = (1 / ((2
ยท 1) + 1))) |
5 | | fveq2 6889 |
. . . 4
โข (๐ฅ = 1 โ (seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฅ) =
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ1)) |
6 | 4, 5 | oveq12d 7424 |
. . 3
โข (๐ฅ = 1 โ ((1 / ((2 ยท
๐ฅ) + 1)) ยท (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฅ)) = ((1 / ((2 ยท 1) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ1))) |
7 | 1, 6 | eqeq12d 2749 |
. 2
โข (๐ฅ = 1 โ ((seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1)))))โ๐ฅ) = ((1 / ((2
ยท ๐ฅ) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฅ)) โ (seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1)))))โ1) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ1)))) |
8 | | fveq2 6889 |
. . 3
โข (๐ฅ = ๐ฆ โ (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฅ) = (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฆ)) |
9 | | oveq2 7414 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (2 ยท ๐ฅ) = (2 ยท ๐ฆ)) |
10 | 9 | oveq1d 7421 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((2 ยท ๐ฅ) + 1) = ((2 ยท ๐ฆ) + 1)) |
11 | 10 | oveq2d 7422 |
. . . 4
โข (๐ฅ = ๐ฆ โ (1 / ((2 ยท ๐ฅ) + 1)) = (1 / ((2 ยท ๐ฆ) + 1))) |
12 | | fveq2 6889 |
. . . 4
โข (๐ฅ = ๐ฆ โ (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฅ) =
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ)) |
13 | 11, 12 | oveq12d 7424 |
. . 3
โข (๐ฅ = ๐ฆ โ ((1 / ((2 ยท ๐ฅ) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฅ)) =
((1 / ((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))) |
14 | 8, 13 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ฆ โ ((seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฅ) = ((1 / ((2 ยท ๐ฅ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฅ))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))) |
15 | | fveq2 6889 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฅ) = (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ(๐ฆ + 1))) |
16 | | oveq2 7414 |
. . . . . 6
โข (๐ฅ = (๐ฆ + 1) โ (2 ยท ๐ฅ) = (2 ยท (๐ฆ + 1))) |
17 | 16 | oveq1d 7421 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ ((2 ยท ๐ฅ) + 1) = ((2 ยท (๐ฆ + 1)) + 1)) |
18 | 17 | oveq2d 7422 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (1 / ((2 ยท ๐ฅ) + 1)) = (1 / ((2 ยท
(๐ฆ + 1)) +
1))) |
19 | | fveq2 6889 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฅ) =
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1))) |
20 | 18, 19 | oveq12d 7424 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ ((1 / ((2 ยท ๐ฅ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฅ)) =
((1 / ((2 ยท (๐ฆ + 1))
+ 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ(๐ฆ +
1)))) |
21 | 15, 20 | eqeq12d 2749 |
. 2
โข (๐ฅ = (๐ฆ + 1) โ ((seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฅ) = ((1 / ((2 ยท ๐ฅ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฅ))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ(๐ฆ + 1)) = ((1 / ((2 ยท
(๐ฆ + 1)) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1))))) |
22 | | fveq2 6889 |
. . 3
โข (๐ฅ = ๐ โ (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฅ) = (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐)) |
23 | | oveq2 7414 |
. . . . . 6
โข (๐ฅ = ๐ โ (2 ยท ๐ฅ) = (2 ยท ๐)) |
24 | 23 | oveq1d 7421 |
. . . . 5
โข (๐ฅ = ๐ โ ((2 ยท ๐ฅ) + 1) = ((2 ยท ๐) + 1)) |
25 | 24 | oveq2d 7422 |
. . . 4
โข (๐ฅ = ๐ โ (1 / ((2 ยท ๐ฅ) + 1)) = (1 / ((2 ยท ๐) + 1))) |
26 | | fveq2 6889 |
. . . 4
โข (๐ฅ = ๐ โ (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฅ) =
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐)) |
27 | 25, 26 | oveq12d 7424 |
. . 3
โข (๐ฅ = ๐ โ ((1 / ((2 ยท ๐ฅ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฅ)) =
((1 / ((2 ยท ๐) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐))) |
28 | 22, 27 | eqeq12d 2749 |
. 2
โข (๐ฅ = ๐ โ ((seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฅ) = ((1 / ((2 ยท ๐ฅ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฅ))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐) = ((1 / ((2 ยท ๐) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐)))) |
29 | | 1z 12589 |
. . . 4
โข 1 โ
โค |
30 | | seq1 13976 |
. . . 4
โข (1 โ
โค โ (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ1) =
((๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ1)) |
31 | 29, 30 | ax-mp 5 |
. . 3
โข (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ1) = ((๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) +
1))))โ1) |
32 | | 1nn 12220 |
. . . 4
โข 1 โ
โ |
33 | | oveq2 7414 |
. . . . . . 7
โข (๐ = 1 โ (2 ยท ๐) = (2 ยท
1)) |
34 | 33 | oveq1d 7421 |
. . . . . . 7
โข (๐ = 1 โ ((2 ยท ๐) โ 1) = ((2 ยท 1)
โ 1)) |
35 | 33, 34 | oveq12d 7424 |
. . . . . 6
โข (๐ = 1 โ ((2 ยท ๐) / ((2 ยท ๐) โ 1)) = ((2 ยท 1)
/ ((2 ยท 1) โ 1))) |
36 | 33 | oveq1d 7421 |
. . . . . . 7
โข (๐ = 1 โ ((2 ยท ๐) + 1) = ((2 ยท 1) +
1)) |
37 | 33, 36 | oveq12d 7424 |
. . . . . 6
โข (๐ = 1 โ ((2 ยท ๐) / ((2 ยท ๐) + 1)) = ((2 ยท 1) / ((2
ยท 1) + 1))) |
38 | 35, 37 | oveq12d 7424 |
. . . . 5
โข (๐ = 1 โ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1))) = (((2 ยท
1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2 ยท 1) +
1)))) |
39 | | eqid 2733 |
. . . . 5
โข (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))) = (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))) |
40 | | ovex 7439 |
. . . . 5
โข (((2
ยท 1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2
ยท 1) + 1))) โ V |
41 | 38, 39, 40 | fvmpt 6996 |
. . . 4
โข (1 โ
โ โ ((๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1))))โ1) = (((2
ยท 1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2
ยท 1) + 1)))) |
42 | 32, 41 | ax-mp 5 |
. . 3
โข ((๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1))))โ1) = (((2
ยท 1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2
ยท 1) + 1))) |
43 | | 2t1e2 12372 |
. . . . . . 7
โข (2
ยท 1) = 2 |
44 | 43 | oveq1i 7416 |
. . . . . . . 8
โข ((2
ยท 1) โ 1) = (2 โ 1) |
45 | | 2m1e1 12335 |
. . . . . . . 8
โข (2
โ 1) = 1 |
46 | 44, 45 | eqtri 2761 |
. . . . . . 7
โข ((2
ยท 1) โ 1) = 1 |
47 | 43, 46 | oveq12i 7418 |
. . . . . 6
โข ((2
ยท 1) / ((2 ยท 1) โ 1)) = (2 / 1) |
48 | 43 | oveq1i 7416 |
. . . . . . . 8
โข ((2
ยท 1) + 1) = (2 + 1) |
49 | | 2p1e3 12351 |
. . . . . . . 8
โข (2 + 1) =
3 |
50 | 48, 49 | eqtri 2761 |
. . . . . . 7
โข ((2
ยท 1) + 1) = 3 |
51 | 43, 50 | oveq12i 7418 |
. . . . . 6
โข ((2
ยท 1) / ((2 ยท 1) + 1)) = (2 / 3) |
52 | 47, 51 | oveq12i 7418 |
. . . . 5
โข (((2
ยท 1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2
ยท 1) + 1))) = ((2 / 1) ยท (2 / 3)) |
53 | | 2cn 12284 |
. . . . . 6
โข 2 โ
โ |
54 | | ax-1cn 11165 |
. . . . . 6
โข 1 โ
โ |
55 | | 3cn 12290 |
. . . . . 6
โข 3 โ
โ |
56 | | ax-1ne0 11176 |
. . . . . 6
โข 1 โ
0 |
57 | | 3ne0 12315 |
. . . . . 6
โข 3 โ
0 |
58 | 53, 54, 53, 55, 56, 57 | divmuldivi 11971 |
. . . . 5
โข ((2 / 1)
ยท (2 / 3)) = ((2 ยท 2) / (1 ยท 3)) |
59 | | 2t2e4 12373 |
. . . . . 6
โข (2
ยท 2) = 4 |
60 | 55 | mullidi 11216 |
. . . . . 6
โข (1
ยท 3) = 3 |
61 | 59, 60 | oveq12i 7418 |
. . . . 5
โข ((2
ยท 2) / (1 ยท 3)) = (4 / 3) |
62 | 52, 58, 61 | 3eqtri 2765 |
. . . 4
โข (((2
ยท 1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2
ยท 1) + 1))) = (4 / 3) |
63 | | 4cn 12294 |
. . . . 5
โข 4 โ
โ |
64 | | divrec2 11886 |
. . . . 5
โข ((4
โ โ โง 3 โ โ โง 3 โ 0) โ (4 / 3) = ((1 / 3)
ยท 4)) |
65 | 63, 55, 57, 64 | mp3an 1462 |
. . . 4
โข (4 / 3) =
((1 / 3) ยท 4) |
66 | 50 | eqcomi 2742 |
. . . . . 6
โข 3 = ((2
ยท 1) + 1) |
67 | 66 | oveq2i 7417 |
. . . . 5
โข (1 / 3) =
(1 / ((2 ยท 1) + 1)) |
68 | | seq1 13976 |
. . . . . . . 8
โข (1 โ
โค โ (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ1) = ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ1)) |
69 | 29, 68 | ax-mp 5 |
. . . . . . 7
โข (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ1) = ((๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2)))โ1) |
70 | 33 | oveq1d 7421 |
. . . . . . . . . 10
โข (๐ = 1 โ ((2 ยท ๐)โ4) = ((2 ยท
1)โ4)) |
71 | 33, 34 | oveq12d 7424 |
. . . . . . . . . . 11
โข (๐ = 1 โ ((2 ยท ๐) ยท ((2 ยท ๐) โ 1)) = ((2 ยท 1)
ยท ((2 ยท 1) โ 1))) |
72 | 71 | oveq1d 7421 |
. . . . . . . . . 10
โข (๐ = 1 โ (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2) = (((2
ยท 1) ยท ((2 ยท 1) โ 1))โ2)) |
73 | 70, 72 | oveq12d 7424 |
. . . . . . . . 9
โข (๐ = 1 โ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)) = (((2
ยท 1)โ4) / (((2 ยท 1) ยท ((2 ยท 1) โ
1))โ2))) |
74 | | eqid 2733 |
. . . . . . . . 9
โข (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))) = (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))) |
75 | | ovex 7439 |
. . . . . . . . 9
โข (((2
ยท 1)โ4) / (((2 ยท 1) ยท ((2 ยท 1) โ
1))โ2)) โ V |
76 | 73, 74, 75 | fvmpt 6996 |
. . . . . . . 8
โข (1 โ
โ โ ((๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)))โ1) = (((2
ยท 1)โ4) / (((2 ยท 1) ยท ((2 ยท 1) โ
1))โ2))) |
77 | 32, 76 | ax-mp 5 |
. . . . . . 7
โข ((๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2)))โ1) = (((2 ยท 1)โ4) / (((2 ยท 1) ยท
((2 ยท 1) โ 1))โ2)) |
78 | 43 | oveq1i 7416 |
. . . . . . . . 9
โข ((2
ยท 1)โ4) = (2โ4) |
79 | 43, 46 | oveq12i 7418 |
. . . . . . . . . . 11
โข ((2
ยท 1) ยท ((2 ยท 1) โ 1)) = (2 ยท
1) |
80 | 79, 43 | eqtri 2761 |
. . . . . . . . . 10
โข ((2
ยท 1) ยท ((2 ยท 1) โ 1)) = 2 |
81 | 80 | oveq1i 7416 |
. . . . . . . . 9
โข (((2
ยท 1) ยท ((2 ยท 1) โ 1))โ2) =
(2โ2) |
82 | 78, 81 | oveq12i 7418 |
. . . . . . . 8
โข (((2
ยท 1)โ4) / (((2 ยท 1) ยท ((2 ยท 1) โ
1))โ2)) = ((2โ4) / (2โ2)) |
83 | | 2exp4 17015 |
. . . . . . . . . 10
โข
(2โ4) = ;16 |
84 | | sq2 14158 |
. . . . . . . . . 10
โข
(2โ2) = 4 |
85 | 83, 84 | oveq12i 7418 |
. . . . . . . . 9
โข
((2โ4) / (2โ2)) = (;16 / 4) |
86 | | 4t4e16 12773 |
. . . . . . . . . . 11
โข (4
ยท 4) = ;16 |
87 | 86 | eqcomi 2742 |
. . . . . . . . . 10
โข ;16 = (4 ยท 4) |
88 | 87 | oveq1i 7416 |
. . . . . . . . 9
โข (;16 / 4) = ((4 ยท 4) /
4) |
89 | | 4ne0 12317 |
. . . . . . . . . 10
โข 4 โ
0 |
90 | 63, 63, 89 | divcan3i 11957 |
. . . . . . . . 9
โข ((4
ยท 4) / 4) = 4 |
91 | 85, 88, 90 | 3eqtri 2765 |
. . . . . . . 8
โข
((2โ4) / (2โ2)) = 4 |
92 | 82, 91 | eqtri 2761 |
. . . . . . 7
โข (((2
ยท 1)โ4) / (((2 ยท 1) ยท ((2 ยท 1) โ
1))โ2)) = 4 |
93 | 69, 77, 92 | 3eqtri 2765 |
. . . . . 6
โข (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ1) =
4 |
94 | 93 | eqcomi 2742 |
. . . . 5
โข 4 =
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ1) |
95 | 67, 94 | oveq12i 7418 |
. . . 4
โข ((1 / 3)
ยท 4) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ1)) |
96 | 62, 65, 95 | 3eqtri 2765 |
. . 3
โข (((2
ยท 1) / ((2 ยท 1) โ 1)) ยท ((2 ยท 1) / ((2
ยท 1) + 1))) = ((1 / ((2 ยท 1) + 1)) ยท (seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ1)) |
97 | 31, 42, 96 | 3eqtri 2765 |
. 2
โข (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ1) = ((1 / ((2
ยท 1) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ1)) |
98 | | elnnuz 12863 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
(โคโฅโ1)) |
99 | 98 | biimpi 215 |
. . . . . 6
โข (๐ฆ โ โ โ ๐ฆ โ
(โคโฅโ1)) |
100 | 99 | adantr 482 |
. . . . 5
โข ((๐ฆ โ โ โง (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))
โ ๐ฆ โ
(โคโฅโ1)) |
101 | | seqp1 13978 |
. . . . 5
โข (๐ฆ โ
(โคโฅโ1) โ (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ(๐ฆ + 1)) = ((seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1)))))โ๐ฆ) ยท
((๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ(๐ฆ +
1)))) |
102 | 100, 101 | syl 17 |
. . . 4
โข ((๐ฆ โ โ โง (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ(๐ฆ + 1)) = ((seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1)))))โ๐ฆ) ยท
((๐ โ โ โฆ
(((2 ยท ๐) / ((2
ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ(๐ฆ +
1)))) |
103 | | simpr 486 |
. . . . 5
โข ((๐ฆ โ โ โง (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ))) |
104 | 103 | oveq1d 7421 |
. . . 4
โข ((๐ฆ โ โ โง (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))
โ ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))))โ๐ฆ) ยท ((๐ โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1))))โ(๐ฆ + 1))) = (((1 / ((2 ยท
๐ฆ) + 1)) ยท (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ)) ยท ((๐ โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1))))โ(๐ฆ + 1)))) |
105 | | eqidd 2734 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1)))) = (๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) +
1))))) |
106 | | oveq2 7414 |
. . . . . . . . . . . 12
โข (๐ = (๐ฆ + 1) โ (2 ยท ๐) = (2 ยท (๐ฆ + 1))) |
107 | 106 | oveq1d 7421 |
. . . . . . . . . . . 12
โข (๐ = (๐ฆ + 1) โ ((2 ยท ๐) โ 1) = ((2 ยท (๐ฆ + 1)) โ
1)) |
108 | 106, 107 | oveq12d 7424 |
. . . . . . . . . . 11
โข (๐ = (๐ฆ + 1) โ ((2 ยท ๐) / ((2 ยท ๐) โ 1)) = ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) โ
1))) |
109 | 106 | oveq1d 7421 |
. . . . . . . . . . . 12
โข (๐ = (๐ฆ + 1) โ ((2 ยท ๐) + 1) = ((2 ยท (๐ฆ + 1)) + 1)) |
110 | 106, 109 | oveq12d 7424 |
. . . . . . . . . . 11
โข (๐ = (๐ฆ + 1) โ ((2 ยท ๐) / ((2 ยท ๐) + 1)) = ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) + 1))) |
111 | 108, 110 | oveq12d 7424 |
. . . . . . . . . 10
โข (๐ = (๐ฆ + 1) โ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1))) = (((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) โ 1)) ยท ((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) +
1)))) |
112 | 111 | adantl 483 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1))) = (((2 ยท
(๐ฆ + 1)) / ((2 ยท
(๐ฆ + 1)) โ 1))
ยท ((2 ยท (๐ฆ +
1)) / ((2 ยท (๐ฆ + 1))
+ 1)))) |
113 | | peano2nn 12221 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (๐ฆ + 1) โ
โ) |
114 | | 2rp 12976 |
. . . . . . . . . . . . 13
โข 2 โ
โ+ |
115 | 114 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ 2 โ
โ+) |
116 | | nnre 12216 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
117 | | nnnn0 12476 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ ๐ฆ โ
โ0) |
118 | 117 | nn0ge0d 12532 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ 0 โค
๐ฆ) |
119 | 116, 118 | ge0p1rpd 13043 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (๐ฆ + 1) โ
โ+) |
120 | 115, 119 | rpmulcld 13029 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) โ
โ+) |
121 | | 2re 12283 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ 2 โ
โ) |
123 | | 1red 11212 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ 1 โ
โ) |
124 | 116, 123 | readdcld 11240 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (๐ฆ + 1) โ
โ) |
125 | 122, 124 | remulcld 11241 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) โ
โ) |
126 | 125, 123 | resubcld 11639 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) โ
1) โ โ) |
127 | | 1lt2 12380 |
. . . . . . . . . . . . . . 15
โข 1 <
2 |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ 1 <
2) |
129 | | nnrp 12982 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ๐ฆ โ
โ+) |
130 | 123, 129 | ltaddrp2d 13047 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ 1 <
(๐ฆ + 1)) |
131 | 122, 124,
128, 130 | mulgt1d 12147 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ 1 < (2
ยท (๐ฆ +
1))) |
132 | 123, 125 | posdifd 11798 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (1 <
(2 ยท (๐ฆ + 1)) โ
0 < ((2 ยท (๐ฆ +
1)) โ 1))) |
133 | 131, 132 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ 0 <
((2 ยท (๐ฆ + 1))
โ 1)) |
134 | 126, 133 | elrpd 13010 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) โ
1) โ โ+) |
135 | 120, 134 | rpdivcld 13030 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) โ
1)) โ โ+) |
136 | 115 | rpge0d 13017 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ 0 โค
2) |
137 | | 0le1 11734 |
. . . . . . . . . . . . . . 15
โข 0 โค
1 |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ 0 โค
1) |
139 | 116, 123,
118, 138 | addge0d 11787 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ 0 โค
(๐ฆ + 1)) |
140 | 122, 124,
136, 139 | mulge0d 11788 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ 0 โค (2
ยท (๐ฆ +
1))) |
141 | 125, 140 | ge0p1rpd 13043 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) + 1)
โ โ+) |
142 | 120, 141 | rpdivcld 13030 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) + 1))
โ โ+) |
143 | 135, 142 | rpmulcld 13029 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) โ
1)) ยท ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) + 1))) โ
โ+) |
144 | 105, 112,
113, 143 | fvmptd 7003 |
. . . . . . . 8
โข (๐ฆ โ โ โ ((๐ โ โ โฆ (((2
ยท ๐) / ((2 ยท
๐) โ 1)) ยท ((2
ยท ๐) / ((2 ยท
๐) + 1))))โ(๐ฆ + 1)) = (((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) โ 1)) ยท ((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) +
1)))) |
145 | 144 | oveq2d 7422 |
. . . . . . 7
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((๐ โ โ
โฆ (((2 ยท ๐) /
((2 ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ(๐ฆ + 1))) =
(((1 / ((2 ยท ๐ฆ) +
1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท (((2 ยท (๐ฆ +
1)) / ((2 ยท (๐ฆ + 1))
โ 1)) ยท ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) + 1))))) |
146 | 125 | recnd 11239 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) โ
โ) |
147 | 126 | recnd 11239 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) โ
1) โ โ) |
148 | 141 | rpcnd 13015 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) + 1)
โ โ) |
149 | 133 | gt0ne0d 11775 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) โ
1) โ 0) |
150 | 141 | rpne0d 13018 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) + 1) โ
0) |
151 | 146, 147,
146, 148, 149, 150 | divmuldivd 12028 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) โ
1)) ยท ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) + 1))) = (((2 ยท (๐ฆ + 1)) ยท (2 ยท
(๐ฆ + 1))) / (((2 ยท
(๐ฆ + 1)) โ 1)
ยท ((2 ยท (๐ฆ +
1)) + 1)))) |
152 | 146, 146 | mulcld 11231 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) ยท
(2 ยท (๐ฆ + 1)))
โ โ) |
153 | 152, 147,
148, 149, 150 | divdiv1d 12018 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ((((2
ยท (๐ฆ + 1)) ยท
(2 ยท (๐ฆ + 1))) / ((2
ยท (๐ฆ + 1)) โ
1)) / ((2 ยท (๐ฆ + 1))
+ 1)) = (((2 ยท (๐ฆ +
1)) ยท (2 ยท (๐ฆ
+ 1))) / (((2 ยท (๐ฆ +
1)) โ 1) ยท ((2 ยท (๐ฆ + 1)) + 1)))) |
154 | 146 | sqvald 14105 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ2) =
((2 ยท (๐ฆ + 1))
ยท (2 ยท (๐ฆ +
1)))) |
155 | 154 | eqcomd 2739 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) ยท
(2 ยท (๐ฆ + 1))) = ((2
ยท (๐ฆ +
1))โ2)) |
156 | 155 | oveq1d 7421 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) ยท
(2 ยท (๐ฆ + 1))) / ((2
ยท (๐ฆ + 1)) โ
1)) = (((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))) |
157 | 156 | oveq1d 7421 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ((((2
ยท (๐ฆ + 1)) ยท
(2 ยท (๐ฆ + 1))) / ((2
ยท (๐ฆ + 1)) โ
1)) / ((2 ยท (๐ฆ + 1))
+ 1)) = ((((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1)) / ((2 ยท (๐ฆ + 1)) + 1))) |
158 | 151, 153,
157 | 3eqtr2d 2779 |
. . . . . . . 8
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) / ((2
ยท (๐ฆ + 1)) โ
1)) ยท ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) + 1))) = ((((2 ยท (๐ฆ + 1))โ2) / ((2 ยท
(๐ฆ + 1)) โ 1)) / ((2
ยท (๐ฆ + 1)) +
1))) |
159 | 158 | oveq2d 7422 |
. . . . . . 7
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท (((2 ยท (๐ฆ +
1)) / ((2 ยท (๐ฆ + 1))
โ 1)) ยท ((2 ยท (๐ฆ + 1)) / ((2 ยท (๐ฆ + 1)) + 1)))) = (((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((((2 ยท (๐ฆ
+ 1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1)) / ((2 ยท (๐ฆ + 1)) + 1)))) |
160 | 146 | sqcld 14106 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ2)
โ โ) |
161 | 160, 147,
149 | divcld 11987 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ2) /
((2 ยท (๐ฆ + 1))
โ 1)) โ โ) |
162 | 161, 148,
150 | divrec2d 11991 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ((((2
ยท (๐ฆ + 1))โ2) /
((2 ยท (๐ฆ + 1))
โ 1)) / ((2 ยท (๐ฆ + 1)) + 1)) = ((1 / ((2 ยท (๐ฆ + 1)) + 1)) ยท (((2
ยท (๐ฆ + 1))โ2) /
((2 ยท (๐ฆ + 1))
โ 1)))) |
163 | 162 | oveq2d 7422 |
. . . . . . . 8
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((((2 ยท (๐ฆ
+ 1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1)) / ((2 ยท (๐ฆ + 1)) + 1))) = (((1 / ((2
ยท ๐ฆ) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ)) ยท ((1 / ((2 ยท
(๐ฆ + 1)) + 1)) ยท
(((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))))) |
164 | | 2cnd 12287 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ 2 โ
โ) |
165 | | nncn 12217 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
166 | 164, 165 | mulcld 11231 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ
โ) |
167 | | 1cnd 11206 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ 1 โ
โ) |
168 | 166, 167 | addcld 11230 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) + 1) โ
โ) |
169 | | 2nn 12282 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ 2 โ
โ) |
171 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
172 | 170, 171 | nnmulcld 12262 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (2
ยท ๐ฆ) โ
โ) |
173 | 172 | peano2nnd 12226 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) + 1) โ
โ) |
174 | 173 | nnne0d 12259 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) + 1) โ
0) |
175 | 168, 174 | reccld 11980 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (1 / ((2
ยท ๐ฆ) + 1)) โ
โ) |
176 | | eqidd 2734 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ฅ โ (1...๐ฆ)) โ (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))) = (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2)))) |
177 | | oveq2 7414 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ฅ โ (2 ยท ๐) = (2 ยท ๐ฅ)) |
178 | 177 | oveq1d 7421 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ ((2 ยท ๐)โ4) = ((2 ยท ๐ฅ)โ4)) |
179 | 177 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ฅ โ ((2 ยท ๐) โ 1) = ((2 ยท ๐ฅ) โ 1)) |
180 | 177, 179 | oveq12d 7424 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ฅ โ ((2 ยท ๐) ยท ((2 ยท ๐) โ 1)) = ((2 ยท ๐ฅ) ยท ((2 ยท ๐ฅ) โ 1))) |
181 | 180 | oveq1d 7421 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฅ โ (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2) = (((2 ยท ๐ฅ) ยท ((2 ยท ๐ฅ) โ
1))โ2)) |
182 | 178, 181 | oveq12d 7424 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฅ โ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)) = (((2 ยท ๐ฅ)โ4) / (((2 ยท ๐ฅ) ยท ((2 ยท ๐ฅ) โ
1))โ2))) |
183 | 182 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ โง ๐ฅ โ (1...๐ฆ)) โง ๐ = ๐ฅ) โ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)) = (((2 ยท ๐ฅ)โ4) / (((2 ยท ๐ฅ) ยท ((2 ยท ๐ฅ) โ
1))โ2))) |
184 | | elfznn 13527 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ (1...๐ฆ) โ ๐ฅ โ โ) |
185 | 184 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ฅ โ (1...๐ฆ)) โ ๐ฅ โ โ) |
186 | 169 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ 2 โ
โ) |
187 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
188 | 186, 187 | nnmulcld 12262 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
โ) |
189 | | 4nn0 12488 |
. . . . . . . . . . . . . . . . . . 19
โข 4 โ
โ0 |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ 4 โ
โ0) |
191 | 188, 190 | nnexpcld 14205 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ)โ4) โ
โ) |
192 | 191 | nncnd 12225 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ)โ4) โ
โ) |
193 | | 2cnd 12287 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ 2 โ
โ) |
194 | | nncn 12217 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
195 | 193, 194 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
โ) |
196 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ 1 โ
โ) |
197 | 195, 196 | subcld 11568 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ) โ 1)
โ โ) |
198 | 195, 197 | mulcld 11231 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ) ยท ((2
ยท ๐ฅ) โ 1))
โ โ) |
199 | 198 | sqcld 14106 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โ โ (((2
ยท ๐ฅ) ยท ((2
ยท ๐ฅ) โ
1))โ2) โ โ) |
200 | 186 | nnne0d 12259 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ 2 โ
0) |
201 | | nnne0 12243 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ ๐ฅ โ 0) |
202 | 193, 194,
200, 201 | mulne0d 11863 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
0) |
203 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ โ โ 1 โ
โ) |
204 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ 2 โ
โ) |
205 | 204, 203 | remulcld 11241 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โ โ (2
ยท 1) โ โ) |
206 | | nnre 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
207 | 204, 206 | remulcld 11241 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
โ) |
208 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ (2
ยท 1) = 2) |
209 | 127, 208 | breqtrrid 5186 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โ โ 1 < (2
ยท 1)) |
210 | | 0le2 12311 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 โค
2 |
211 | 210 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ 0 โค
2) |
212 | | nnge1 12237 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ โ โ 1 โค
๐ฅ) |
213 | 203, 206,
204, 211, 212 | lemul2ad 12151 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โ โ (2
ยท 1) โค (2 ยท ๐ฅ)) |
214 | 203, 205,
207, 209, 213 | ltletrd 11371 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ โ โ 1 < (2
ยท ๐ฅ)) |
215 | 203, 214 | gtned 11346 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ โ โ (2
ยท ๐ฅ) โ
1) |
216 | 195, 196,
215 | subne0d 11577 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ) โ 1) โ
0) |
217 | 195, 197,
202, 216 | mulne0d 11863 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ ((2
ยท ๐ฅ) ยท ((2
ยท ๐ฅ) โ 1))
โ 0) |
218 | | 2z 12591 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โค |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ 2 โ
โค) |
220 | 198, 217,
219 | expne0d 14114 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ โ โ (((2
ยท ๐ฅ) ยท ((2
ยท ๐ฅ) โ
1))โ2) โ 0) |
221 | 192, 199,
220 | divcld 11987 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ (((2
ยท ๐ฅ)โ4) / (((2
ยท ๐ฅ) ยท ((2
ยท ๐ฅ) โ
1))โ2)) โ โ) |
222 | 184, 221 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ (1...๐ฆ) โ (((2 ยท ๐ฅ)โ4) / (((2 ยท ๐ฅ) ยท ((2 ยท ๐ฅ) โ 1))โ2)) โ
โ) |
223 | 222 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ฅ โ (1...๐ฆ)) โ (((2 ยท ๐ฅ)โ4) / (((2 ยท ๐ฅ) ยท ((2 ยท ๐ฅ) โ 1))โ2)) โ
โ) |
224 | 176, 183,
185, 223 | fvmptd 7003 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ฅ โ (1...๐ฆ)) โ ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ๐ฅ) =
(((2 ยท ๐ฅ)โ4) /
(((2 ยท ๐ฅ) ยท
((2 ยท ๐ฅ) โ
1))โ2))) |
225 | 224, 223 | eqeltrd 2834 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ฅ โ (1...๐ฆ)) โ ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ๐ฅ)
โ โ) |
226 | | mulcl 11191 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ค โ โ) โ (๐ฅ ยท ๐ค) โ โ) |
227 | 226 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง (๐ฅ โ โ โง ๐ค โ โ)) โ (๐ฅ ยท ๐ค) โ โ) |
228 | 99, 225, 227 | seqcl 13985 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) โ
โ) |
229 | 175, 228 | mulcld 11231 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ((1 / ((2
ยท ๐ฆ) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ)) โ
โ) |
230 | 148, 150 | reccld 11980 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (1 / ((2
ยท (๐ฆ + 1)) + 1))
โ โ) |
231 | 229, 230,
161 | mul12d 11420 |
. . . . . . . 8
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((1 / ((2 ยท (๐ฆ + 1)) + 1)) ยท (((2 ยท (๐ฆ + 1))โ2) / ((2 ยท
(๐ฆ + 1)) โ 1)))) =
((1 / ((2 ยท (๐ฆ + 1))
+ 1)) ยท (((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท (((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))))) |
232 | 175, 228 | mulcomd 11232 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((1 / ((2
ยท ๐ฆ) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ)) = ((seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (1 / ((2 ยท ๐ฆ) + 1)))) |
233 | 232 | oveq1d 7421 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท (((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))) = (((seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (1 / ((2 ยท ๐ฆ) + 1))) ยท (((2 ยท (๐ฆ + 1))โ2) / ((2 ยท
(๐ฆ + 1)) โ
1)))) |
234 | 228, 175,
161 | mulassd 11234 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) ยท (1 / ((2 ยท
๐ฆ) + 1))) ยท (((2
ยท (๐ฆ + 1))โ2) /
((2 ยท (๐ฆ + 1))
โ 1))) = ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท ((1 / ((2 ยท ๐ฆ) + 1)) ยท (((2 ยท (๐ฆ + 1))โ2) / ((2 ยท
(๐ฆ + 1)) โ
1))))) |
235 | 167, 168,
160, 147, 174, 149 | divmuldivd 12028 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((1 / ((2
ยท ๐ฆ) + 1)) ยท
(((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))) = ((1 ยท ((2
ยท (๐ฆ + 1))โ2))
/ (((2 ยท ๐ฆ) + 1)
ยท ((2 ยท (๐ฆ +
1)) โ 1)))) |
236 | 160 | mullidd 11229 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (1
ยท ((2 ยท (๐ฆ +
1))โ2)) = ((2 ยท (๐ฆ + 1))โ2)) |
237 | 164, 165,
167 | adddid 11235 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) = ((2
ยท ๐ฆ) + (2 ยท
1))) |
238 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ โ (2
ยท 1) = 2) |
239 | 238 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) + (2 ยท
1)) = ((2 ยท ๐ฆ) +
2)) |
240 | 237, 239 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) = ((2
ยท ๐ฆ) +
2)) |
241 | 240 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) โ
1) = (((2 ยท ๐ฆ) + 2)
โ 1)) |
242 | 166, 164,
167 | addsubassd 11588 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (((2
ยท ๐ฆ) + 2) โ 1)
= ((2 ยท ๐ฆ) + (2
โ 1))) |
243 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ (2
โ 1) = 1) |
244 | 243 | oveq2d 7422 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) + (2 โ
1)) = ((2 ยท ๐ฆ) +
1)) |
245 | 241, 242,
244 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) โ
1) = ((2 ยท ๐ฆ) +
1)) |
246 | 245 | oveq2d 7422 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (((2
ยท ๐ฆ) + 1) ยท
((2 ยท (๐ฆ + 1))
โ 1)) = (((2 ยท ๐ฆ) + 1) ยท ((2 ยท ๐ฆ) + 1))) |
247 | 168 | sqvald 14105 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (((2
ยท ๐ฆ) + 1)โ2) =
(((2 ยท ๐ฆ) + 1)
ยท ((2 ยท ๐ฆ) +
1))) |
248 | 246, 247 | eqtr4d 2776 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (((2
ยท ๐ฆ) + 1) ยท
((2 ยท (๐ฆ + 1))
โ 1)) = (((2 ยท ๐ฆ) + 1)โ2)) |
249 | 236, 248 | oveq12d 7424 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((1
ยท ((2 ยท (๐ฆ +
1))โ2)) / (((2 ยท ๐ฆ) + 1) ยท ((2 ยท (๐ฆ + 1)) โ 1))) = (((2
ยท (๐ฆ + 1))โ2) /
(((2 ยท ๐ฆ) +
1)โ2))) |
250 | | 2p2e4 12344 |
. . . . . . . . . . . . . . . . . 18
โข (2 + 2) =
4 |
251 | 53, 53, 250 | mvlladdi 11475 |
. . . . . . . . . . . . . . . . 17
โข 2 = (4
โ 2) |
252 | 251 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ 2 = (4
โ 2)) |
253 | 252 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ2) =
((2 ยท (๐ฆ +
1))โ(4 โ 2))) |
254 | 120 | rpne0d 13018 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) โ
0) |
255 | 218 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ 2 โ
โค) |
256 | | 4z 12593 |
. . . . . . . . . . . . . . . . 17
โข 4 โ
โค |
257 | 256 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ 4 โ
โค) |
258 | 146, 254,
255, 257 | expsubd 14119 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ(4
โ 2)) = (((2 ยท (๐ฆ + 1))โ4) / ((2 ยท (๐ฆ +
1))โ2))) |
259 | 253, 258 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ2) =
(((2 ยท (๐ฆ +
1))โ4) / ((2 ยท (๐ฆ + 1))โ2))) |
260 | 245 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ ((2
ยท ๐ฆ) + 1) = ((2
ยท (๐ฆ + 1)) โ
1)) |
261 | 260 | oveq1d 7421 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (((2
ยท ๐ฆ) + 1)โ2) =
(((2 ยท (๐ฆ + 1))
โ 1)โ2)) |
262 | 259, 261 | oveq12d 7424 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ2) /
(((2 ยท ๐ฆ) +
1)โ2)) = ((((2 ยท (๐ฆ + 1))โ4) / ((2 ยท (๐ฆ + 1))โ2)) / (((2 ยท
(๐ฆ + 1)) โ
1)โ2))) |
263 | 146, 254,
257 | expclzd 14113 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ4)
โ โ) |
264 | 147 | sqcld 14106 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) โ
1)โ2) โ โ) |
265 | 165, 167 | addcld 11230 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (๐ฆ + 1) โ
โ) |
266 | 170 | nnne0d 12259 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ 2 โ
0) |
267 | 113 | nnne0d 12259 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ โ (๐ฆ + 1) โ 0) |
268 | 164, 265,
266, 267 | mulne0d 11863 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ (2
ยท (๐ฆ + 1)) โ
0) |
269 | 146, 268,
255 | expne0d 14114 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1))โ2)
โ 0) |
270 | 147, 149,
255 | expne0d 14114 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) โ
1)โ2) โ 0) |
271 | 263, 160,
264, 269, 270 | divdiv1d 12018 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ((((2
ยท (๐ฆ + 1))โ4) /
((2 ยท (๐ฆ +
1))โ2)) / (((2 ยท (๐ฆ + 1)) โ 1)โ2)) = (((2 ยท
(๐ฆ + 1))โ4) / (((2
ยท (๐ฆ + 1))โ2)
ยท (((2 ยท (๐ฆ +
1)) โ 1)โ2)))) |
272 | 146, 147 | sqmuld 14120 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1))โ2) = (((2 ยท (๐ฆ + 1))โ2) ยท (((2 ยท (๐ฆ + 1)) โ
1)โ2))) |
273 | 272 | eqcomd 2739 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ2)
ยท (((2 ยท (๐ฆ +
1)) โ 1)โ2)) = (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ
1))โ2)) |
274 | 273 | oveq2d 7422 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ4) /
(((2 ยท (๐ฆ +
1))โ2) ยท (((2 ยท (๐ฆ + 1)) โ 1)โ2))) = (((2 ยท
(๐ฆ + 1))โ4) / (((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1))โ2))) |
275 | 262, 271,
274 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ2) /
(((2 ยท ๐ฆ) +
1)โ2)) = (((2 ยท (๐ฆ + 1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท
(๐ฆ + 1)) โ
1))โ2))) |
276 | 235, 249,
275 | 3eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ((1 / ((2
ยท ๐ฆ) + 1)) ยท
(((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))) = (((2 ยท (๐ฆ + 1))โ4) / (((2 ยท
(๐ฆ + 1)) ยท ((2
ยท (๐ฆ + 1)) โ
1))โ2))) |
277 | 276 | oveq2d 7422 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) ยท ((1 / ((2 ยท
๐ฆ) + 1)) ยท (((2
ยท (๐ฆ + 1))โ2) /
((2 ยท (๐ฆ + 1))
โ 1)))) = ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (((2 ยท (๐ฆ +
1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ
1))โ2)))) |
278 | 233, 234,
277 | 3eqtrd 2777 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท (((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1))) = ((seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (((2 ยท (๐ฆ +
1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ
1))โ2)))) |
279 | 278 | oveq2d 7422 |
. . . . . . . 8
โข (๐ฆ โ โ โ ((1 / ((2
ยท (๐ฆ + 1)) + 1))
ยท (((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท (((2 ยท (๐ฆ +
1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1)))) = ((1 / ((2 ยท
(๐ฆ + 1)) + 1)) ยท
((seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) ยท (((2 ยท (๐ฆ + 1))โ4) / (((2 ยท
(๐ฆ + 1)) ยท ((2
ยท (๐ฆ + 1)) โ
1))โ2))))) |
280 | 163, 231,
279 | 3eqtrd 2777 |
. . . . . . 7
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((((2 ยท (๐ฆ
+ 1))โ2) / ((2 ยท (๐ฆ + 1)) โ 1)) / ((2 ยท (๐ฆ + 1)) + 1))) = ((1 / ((2
ยท (๐ฆ + 1)) + 1))
ยท ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (((2 ยท (๐ฆ +
1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ
1))โ2))))) |
281 | 145, 159,
280 | 3eqtrd 2777 |
. . . . . 6
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((๐ โ โ
โฆ (((2 ยท ๐) /
((2 ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ(๐ฆ + 1))) = ((1
/ ((2 ยท (๐ฆ + 1)) +
1)) ยท ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (((2 ยท (๐ฆ +
1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ
1))โ2))))) |
282 | | eqidd 2734 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))) = (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)))) |
283 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ ๐ = (๐ฆ + 1)) |
284 | 283 | oveq2d 7422 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ (2 ยท ๐) = (2 ยท (๐ฆ + 1))) |
285 | 284 | oveq1d 7421 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ ((2 ยท ๐)โ4) = ((2 ยท (๐ฆ + 1))โ4)) |
286 | 284 | oveq1d 7421 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ ((2 ยท ๐) โ 1) = ((2 ยท (๐ฆ + 1)) โ
1)) |
287 | 284, 286 | oveq12d 7424 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ ((2 ยท ๐) ยท ((2 ยท ๐) โ 1)) = ((2 ยท (๐ฆ + 1)) ยท ((2 ยท
(๐ฆ + 1)) โ
1))) |
288 | 287 | oveq1d 7421 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2) = (((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1))โ2)) |
289 | 285, 288 | oveq12d 7424 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ = (๐ฆ + 1)) โ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)) = (((2
ยท (๐ฆ + 1))โ4) /
(((2 ยท (๐ฆ + 1))
ยท ((2 ยท (๐ฆ +
1)) โ 1))โ2))) |
290 | 146, 147 | mulcld 11231 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1)) โ โ) |
291 | 290 | sqcld 14106 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1))โ2) โ โ) |
292 | 146, 147,
254, 149 | mulne0d 11863 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1)) โ 0) |
293 | 290, 292,
255 | expne0d 14114 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1)) ยท
((2 ยท (๐ฆ + 1))
โ 1))โ2) โ 0) |
294 | 263, 291,
293 | divcld 11987 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ4) /
(((2 ยท (๐ฆ + 1))
ยท ((2 ยท (๐ฆ +
1)) โ 1))โ2)) โ โ) |
295 | 282, 289,
113, 294 | fvmptd 7003 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ((๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2)))โ(๐ฆ +
1)) = (((2 ยท (๐ฆ +
1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ
1))โ2))) |
296 | 295 | eqcomd 2739 |
. . . . . . . 8
โข (๐ฆ โ โ โ (((2
ยท (๐ฆ + 1))โ4) /
(((2 ยท (๐ฆ + 1))
ยท ((2 ยท (๐ฆ +
1)) โ 1))โ2)) = ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ(๐ฆ +
1))) |
297 | 296 | oveq2d 7422 |
. . . . . . 7
โข (๐ฆ โ โ โ ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) ยท (((2 ยท (๐ฆ + 1))โ4) / (((2 ยท
(๐ฆ + 1)) ยท ((2
ยท (๐ฆ + 1)) โ
1))โ2))) = ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท ((๐ โ โ
โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)))โ(๐ฆ + 1)))) |
298 | 297 | oveq2d 7422 |
. . . . . 6
โข (๐ฆ โ โ โ ((1 / ((2
ยท (๐ฆ + 1)) + 1))
ยท ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท (((2 ยท (๐ฆ +
1))โ4) / (((2 ยท (๐ฆ + 1)) ยท ((2 ยท (๐ฆ + 1)) โ 1))โ2)))) =
((1 / ((2 ยท (๐ฆ + 1))
+ 1)) ยท ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท ((๐ โ โ
โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)))โ(๐ฆ + 1))))) |
299 | | seqp1 13978 |
. . . . . . . . 9
โข (๐ฆ โ
(โคโฅโ1) โ (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ(๐ฆ +
1)) = ((seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) ยท ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ(๐ฆ +
1)))) |
300 | 99, 299 | syl 17 |
. . . . . . . 8
โข (๐ฆ โ โ โ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1)) = ((seq1( ยท ,
(๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท ((๐ โ โ
โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)))โ(๐ฆ + 1)))) |
301 | 300 | eqcomd 2739 |
. . . . . . 7
โข (๐ฆ โ โ โ ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ๐ฆ) ยท ((๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2)))โ(๐ฆ +
1))) = (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1))) |
302 | 301 | oveq2d 7422 |
. . . . . 6
โข (๐ฆ โ โ โ ((1 / ((2
ยท (๐ฆ + 1)) + 1))
ยท ((seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ)
ยท ((๐ โ โ
โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2)))โ(๐ฆ + 1)))) = ((1 / ((2 ยท
(๐ฆ + 1)) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1)))) |
303 | 281, 298,
302 | 3eqtrd 2777 |
. . . . 5
โข (๐ฆ โ โ โ (((1 /
((2 ยท ๐ฆ) + 1))
ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((๐ โ โ
โฆ (((2 ยท ๐) /
((2 ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ(๐ฆ + 1))) = ((1
/ ((2 ยท (๐ฆ + 1)) +
1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ(๐ฆ +
1)))) |
304 | 303 | adantr 482 |
. . . 4
โข ((๐ฆ โ โ โง (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))
โ (((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2
ยท ๐)โ4) / (((2
ยท ๐) ยท ((2
ยท ๐) โ
1))โ2))))โ๐ฆ))
ยท ((๐ โ โ
โฆ (((2 ยท ๐) /
((2 ยท ๐) โ 1))
ยท ((2 ยท ๐) /
((2 ยท ๐) +
1))))โ(๐ฆ + 1))) = ((1
/ ((2 ยท (๐ฆ + 1)) +
1)) ยท (seq1( ยท , (๐ โ โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ
1))โ2))))โ(๐ฆ +
1)))) |
305 | 102, 104,
304 | 3eqtrd 2777 |
. . 3
โข ((๐ฆ โ โ โง (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ)))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ(๐ฆ + 1)) = ((1 / ((2 ยท
(๐ฆ + 1)) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1)))) |
306 | 305 | ex 414 |
. 2
โข (๐ฆ โ โ โ ((seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐ฆ) = ((1 / ((2 ยท ๐ฆ) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐ฆ))
โ (seq1( ยท , (๐
โ โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ(๐ฆ + 1)) = ((1 / ((2 ยท
(๐ฆ + 1)) + 1)) ยท
(seq1( ยท , (๐ โ
โ โฆ (((2 ยท ๐)โ4) / (((2 ยท ๐) ยท ((2 ยท ๐) โ 1))โ2))))โ(๐ฆ + 1))))) |
307 | 7, 14, 21, 28, 97, 306 | nnind 12227 |
1
โข (๐ โ โ โ (seq1(
ยท , (๐ โ
โ โฆ (((2 ยท ๐) / ((2 ยท ๐) โ 1)) ยท ((2 ยท ๐) / ((2 ยท ๐) + 1)))))โ๐) = ((1 / ((2 ยท ๐) + 1)) ยท (seq1( ยท
, (๐ โ โ โฆ
(((2 ยท ๐)โ4) /
(((2 ยท ๐) ยท
((2 ยท ๐) โ
1))โ2))))โ๐))) |