Step | Hyp | Ref
| Expression |
1 | | 2cnd 12286 |
. . . 4
โข (๐ โ โ โ 2 โ
โ) |
2 | | peano2nn 12220 |
. . . . . 6
โข (๐ โ โ โ (๐ + 1) โ
โ) |
3 | | nnmulcl 12232 |
. . . . . 6
โข ((๐ โ โ โง (๐ + 1) โ โ) โ
(๐ ยท (๐ + 1)) โ
โ) |
4 | 2, 3 | mpdan 685 |
. . . . 5
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ โ) |
5 | 4 | nncnd 12224 |
. . . 4
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ โ) |
6 | 4 | nnne0d 12258 |
. . . 4
โข (๐ โ โ โ (๐ ยท (๐ + 1)) โ 0) |
7 | 1, 5, 6 | divrecd 11989 |
. . 3
โข (๐ โ โ โ (2 /
(๐ ยท (๐ + 1))) = (2 ยท (1 /
(๐ ยท (๐ + 1))))) |
8 | 7 | sumeq2i 15641 |
. 2
โข
ฮฃ๐ โ
โ (2 / (๐ ยท
(๐ + 1))) = ฮฃ๐ โ โ (2 ยท (1 /
(๐ ยท (๐ + 1)))) |
9 | | nnuz 12861 |
. . . . 5
โข โ =
(โคโฅโ1) |
10 | | 1zzd 12589 |
. . . . 5
โข (โค
โ 1 โ โค) |
11 | | id 22 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ = ๐) |
12 | | oveq1 7412 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
13 | 11, 12 | oveq12d 7423 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท (๐ + 1)) = (๐ ยท (๐ + 1))) |
14 | 13 | oveq2d 7421 |
. . . . . . 7
โข (๐ = ๐ โ (1 / (๐ ยท (๐ + 1))) = (1 / (๐ ยท (๐ + 1)))) |
15 | | eqid 2732 |
. . . . . . 7
โข (๐ โ โ โฆ (1 /
(๐ ยท (๐ + 1)))) = (๐ โ โ โฆ (1 / (๐ ยท (๐ + 1)))) |
16 | | ovex 7438 |
. . . . . . 7
โข (1 /
(๐ ยท (๐ + 1))) โ
V |
17 | 14, 15, 16 | fvmpt 6995 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ โ โฆ (1 /
(๐ ยท (๐ + 1))))โ๐) = (1 / (๐ ยท (๐ + 1)))) |
18 | 17 | adantl 482 |
. . . . 5
โข
((โค โง ๐
โ โ) โ ((๐
โ โ โฆ (1 / (๐ ยท (๐ + 1))))โ๐) = (1 / (๐ ยท (๐ + 1)))) |
19 | 4 | nnrecred 12259 |
. . . . . . 7
โข (๐ โ โ โ (1 /
(๐ ยท (๐ + 1))) โ
โ) |
20 | 19 | recnd 11238 |
. . . . . 6
โข (๐ โ โ โ (1 /
(๐ ยท (๐ + 1))) โ
โ) |
21 | 20 | adantl 482 |
. . . . 5
โข
((โค โง ๐
โ โ) โ (1 / (๐ ยท (๐ + 1))) โ โ) |
22 | 15 | trireciplem 15804 |
. . . . . . 7
โข seq1( + ,
(๐ โ โ โฆ
(1 / (๐ ยท (๐ + 1))))) โ
1 |
23 | 22 | a1i 11 |
. . . . . 6
โข (โค
โ seq1( + , (๐ โ
โ โฆ (1 / (๐
ยท (๐ + 1)))))
โ 1) |
24 | | climrel 15432 |
. . . . . . 7
โข Rel
โ |
25 | 24 | releldmi 5945 |
. . . . . 6
โข (seq1( +
, (๐ โ โ โฆ
(1 / (๐ ยท (๐ + 1))))) โ 1 โ seq1(
+ , (๐ โ โ
โฆ (1 / (๐ ยท
(๐ + 1))))) โ dom
โ ) |
26 | 23, 25 | syl 17 |
. . . . 5
โข (โค
โ seq1( + , (๐ โ
โ โฆ (1 / (๐
ยท (๐ + 1))))) โ
dom โ ) |
27 | | 2cnd 12286 |
. . . . 5
โข (โค
โ 2 โ โ) |
28 | 9, 10, 18, 21, 26, 27 | isummulc2 15704 |
. . . 4
โข (โค
โ (2 ยท ฮฃ๐
โ โ (1 / (๐
ยท (๐ + 1)))) =
ฮฃ๐ โ โ (2
ยท (1 / (๐ ยท
(๐ +
1))))) |
29 | 9, 10, 18, 21, 23 | isumclim 15699 |
. . . . 5
โข (โค
โ ฮฃ๐ โ
โ (1 / (๐ ยท
(๐ + 1))) =
1) |
30 | 29 | oveq2d 7421 |
. . . 4
โข (โค
โ (2 ยท ฮฃ๐
โ โ (1 / (๐
ยท (๐ + 1)))) = (2
ยท 1)) |
31 | 28, 30 | eqtr3d 2774 |
. . 3
โข (โค
โ ฮฃ๐ โ
โ (2 ยท (1 / (๐
ยท (๐ + 1)))) = (2
ยท 1)) |
32 | 31 | mptru 1548 |
. 2
โข
ฮฃ๐ โ
โ (2 ยท (1 / (๐
ยท (๐ + 1)))) = (2
ยท 1) |
33 | | 2t1e2 12371 |
. 2
โข (2
ยท 1) = 2 |
34 | 8, 32, 33 | 3eqtri 2764 |
1
โข
ฮฃ๐ โ
โ (2 / (๐ ยท
(๐ + 1))) =
2 |