Step | Hyp | Ref
| Expression |
1 | | pntsval.1 |
. . 3
โข ๐ = (๐ โ โ โฆ ฮฃ๐ โ
(1...(โโ๐))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ / ๐))))) |
2 | 1 | pntsval 26936 |
. 2
โข (๐ด โ โ โ (๐โ๐ด) = ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ด / ๐))))) |
3 | | elfznn 13477 |
. . . . . . 7
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
4 | 3 | adantl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ) |
5 | | vmacl 26483 |
. . . . . 6
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
6 | 4, 5 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฮโ๐)
โ โ) |
7 | 6 | recnd 11190 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฮโ๐)
โ โ) |
8 | 4 | nnrpd 12962 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ+) |
9 | 8 | relogcld 25994 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (logโ๐) โ
โ) |
10 | 9 | recnd 11190 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (logโ๐) โ
โ) |
11 | | simpl 484 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ๐ด โ
โ) |
12 | 11, 4 | nndivred 12214 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (๐ด / ๐) โ
โ) |
13 | | chpcl 26489 |
. . . . . 6
โข ((๐ด / ๐) โ โ โ (ฯโ(๐ด / ๐)) โ โ) |
14 | 12, 13 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฯโ(๐ด /
๐)) โ
โ) |
15 | 14 | recnd 11190 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฯโ(๐ด /
๐)) โ
โ) |
16 | 7, 10, 15 | adddid 11186 |
. . 3
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
ยท ((logโ๐) +
(ฯโ(๐ด / ๐)))) = (((ฮโ๐) ยท (logโ๐)) + ((ฮโ๐) ยท (ฯโ(๐ด / ๐))))) |
17 | 16 | sumeq2dv 15595 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท ((logโ๐) + (ฯโ(๐ด / ๐)))) = ฮฃ๐ โ (1...(โโ๐ด))(((ฮโ๐) ยท (logโ๐)) + ((ฮโ๐) ยท (ฯโ(๐ด / ๐))))) |
18 | | fveq2 6847 |
. . . . . . 7
โข (๐ = ๐ โ (ฮโ๐) = (ฮโ๐)) |
19 | | oveq2 7370 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ด / ๐) = (๐ด / ๐)) |
20 | 19 | fveq2d 6851 |
. . . . . . 7
โข (๐ = ๐ โ (ฯโ(๐ด / ๐)) = (ฯโ(๐ด / ๐))) |
21 | 18, 20 | oveq12d 7380 |
. . . . . 6
โข (๐ = ๐ โ ((ฮโ๐) ยท (ฯโ(๐ด / ๐))) = ((ฮโ๐) ยท (ฯโ(๐ด / ๐)))) |
22 | 21 | cbvsumv 15588 |
. . . . 5
โข
ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐))) = ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐))) |
23 | | fzfid 13885 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (1...(โโ(๐ด / ๐))) โ Fin) |
24 | | elfznn 13477 |
. . . . . . . . . . . 12
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
25 | 24 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ๐ โ
โ) |
26 | | vmacl 26483 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฮโ๐)
โ โ) |
28 | 27 | recnd 11190 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฮโ๐)
โ โ) |
29 | | elfznn 13477 |
. . . . . . . . . . . 12
โข (๐ โ
(1...(โโ(๐ด /
๐))) โ ๐ โ
โ) |
30 | 29 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ ๐ โ
โ) |
31 | | vmacl 26483 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ
(ฮโ๐) โ
โ) |
33 | 32 | recnd 11190 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ
(ฮโ๐) โ
โ) |
34 | 23, 28, 33 | fsummulc2 15676 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ด /
๐)))(ฮโ๐)) = ฮฃ๐ โ (1...(โโ(๐ด / ๐)))((ฮโ๐) ยท (ฮโ๐))) |
35 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ๐ด โ
โ) |
36 | 35, 25 | nndivred 12214 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (๐ด / ๐) โ
โ) |
37 | | chpval 26487 |
. . . . . . . . . 10
โข ((๐ด / ๐) โ โ โ (ฯโ(๐ด / ๐)) = ฮฃ๐ โ (1...(โโ(๐ด / ๐)))(ฮโ๐)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (ฯโ(๐ด /
๐)) = ฮฃ๐ โ
(1...(โโ(๐ด /
๐)))(ฮโ๐)) |
39 | 38 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
ยท (ฯโ(๐ด /
๐))) =
((ฮโ๐)
ยท ฮฃ๐ โ
(1...(โโ(๐ด /
๐)))(ฮโ๐))) |
40 | 30 | nncnd 12176 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ ๐ โ
โ) |
41 | 24 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ ๐ โ
โ) |
42 | 41 | nncnd 12176 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ ๐ โ
โ) |
43 | 41 | nnne0d 12210 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ ๐ โ 0) |
44 | 40, 42, 43 | divcan3d 11943 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ ((๐ ยท ๐) / ๐) = ๐) |
45 | 44 | fveq2d 6851 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ
(ฮโ((๐
ยท ๐) / ๐)) = (ฮโ๐)) |
46 | 45 | oveq2d 7378 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ
(1...(โโ(๐ด /
๐)))) โ
((ฮโ๐)
ยท (ฮโ((๐ ยท ๐) / ๐))) = ((ฮโ๐) ยท (ฮโ๐))) |
47 | 46 | sumeq2dv 15595 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ฮฃ๐ โ
(1...(โโ(๐ด /
๐)))((ฮโ๐) ยท
(ฮโ((๐
ยท ๐) / ๐))) = ฮฃ๐ โ (1...(โโ(๐ด / ๐)))((ฮโ๐) ยท (ฮโ๐))) |
48 | 34, 39, 47 | 3eqtr4d 2787 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
ยท (ฯโ(๐ด /
๐))) = ฮฃ๐ โ
(1...(โโ(๐ด /
๐)))((ฮโ๐) ยท
(ฮโ((๐
ยท ๐) / ๐)))) |
49 | 48 | sumeq2dv 15595 |
. . . . . 6
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐))) = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ (1...(โโ(๐ด / ๐)))((ฮโ๐) ยท (ฮโ((๐ ยท ๐) / ๐)))) |
50 | | fvoveq1 7385 |
. . . . . . . 8
โข (๐ = (๐ ยท ๐) โ (ฮโ(๐ / ๐)) = (ฮโ((๐ ยท ๐) / ๐))) |
51 | 50 | oveq2d 7378 |
. . . . . . 7
โข (๐ = (๐ ยท ๐) โ ((ฮโ๐) ยท (ฮโ(๐ / ๐))) = ((ฮโ๐) ยท (ฮโ((๐ ยท ๐) / ๐)))) |
52 | | id 22 |
. . . . . . 7
โข (๐ด โ โ โ ๐ด โ
โ) |
53 | | ssrab2 4042 |
. . . . . . . . . . . 12
โข {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} โ โ |
54 | | simpr 486 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) |
55 | 53, 54 | sselid 3947 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ ๐ โ โ) |
56 | 55, 26 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ (ฮโ๐) โ โ) |
57 | | dvdsdivcl 16205 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ (๐ / ๐) โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) |
58 | 4, 57 | sylan 581 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ (๐ / ๐) โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) |
59 | 53, 58 | sselid 3947 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ (๐ / ๐) โ โ) |
60 | | vmacl 26483 |
. . . . . . . . . . 11
โข ((๐ / ๐) โ โ โ
(ฮโ(๐ / ๐)) โ
โ) |
61 | 59, 60 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ (ฮโ(๐ / ๐)) โ โ) |
62 | 56, 61 | remulcld 11192 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ ((ฮโ๐) ยท (ฮโ(๐ / ๐))) โ โ) |
63 | 62 | recnd 11190 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐}) โ ((ฮโ๐) ยท (ฮโ(๐ / ๐))) โ โ) |
64 | 63 | anasss 468 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐})) โ ((ฮโ๐) ยท
(ฮโ(๐ / ๐))) โ
โ) |
65 | 51, 52, 64 | dvdsflsumcom 26553 |
. . . . . 6
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐))) = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ (1...(โโ(๐ด / ๐)))((ฮโ๐) ยท (ฮโ((๐ ยท ๐) / ๐)))) |
66 | 49, 65 | eqtr4d 2780 |
. . . . 5
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐))) = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐)))) |
67 | 22, 66 | eqtrid 2789 |
. . . 4
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐))) = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐)))) |
68 | 67 | oveq2d 7378 |
. . 3
โข (๐ด โ โ โ
(ฮฃ๐ โ
(1...(โโ๐ด))((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐)))) = (ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐))))) |
69 | | fzfid 13885 |
. . . 4
โข (๐ด โ โ โ
(1...(โโ๐ด))
โ Fin) |
70 | 7, 10 | mulcld 11182 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
ยท (logโ๐))
โ โ) |
71 | 7, 15 | mulcld 11182 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ((ฮโ๐)
ยท (ฯโ(๐ด /
๐))) โ
โ) |
72 | 69, 70, 71 | fsumadd 15632 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))(((ฮโ๐) ยท (logโ๐)) + ((ฮโ๐) ยท (ฯโ(๐ด / ๐)))) = (ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (ฯโ(๐ด / ๐))))) |
73 | | fzfid 13885 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ (1...๐) โ
Fin) |
74 | | dvdsssfz1 16207 |
. . . . . . . 8
โข (๐ โ โ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} โ (1...๐)) |
75 | 4, 74 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ {๐ฆ โ โ
โฃ ๐ฆ โฅ ๐} โ (1...๐)) |
76 | 73, 75 | ssfid 9218 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ {๐ฆ โ โ
โฃ ๐ฆ โฅ ๐} โ Fin) |
77 | 76, 62 | fsumrecl 15626 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ฮฃ๐ โ
{๐ฆ โ โ โฃ
๐ฆ โฅ ๐} ((ฮโ๐) ยท
(ฮโ(๐ / ๐))) โ
โ) |
78 | 77 | recnd 11190 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(1...(โโ๐ด)))
โ ฮฃ๐ โ
{๐ฆ โ โ โฃ
๐ฆ โฅ ๐} ((ฮโ๐) ยท
(ฮโ(๐ / ๐))) โ
โ) |
79 | 69, 70, 78 | fsumadd 15632 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))(((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐)))) = (ฮฃ๐ โ (1...(โโ๐ด))((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐))))) |
80 | 68, 72, 79 | 3eqtr4d 2787 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ
(1...(โโ๐ด))(((ฮโ๐) ยท (logโ๐)) + ((ฮโ๐) ยท (ฯโ(๐ด / ๐)))) = ฮฃ๐ โ (1...(โโ๐ด))(((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐))))) |
81 | 2, 17, 80 | 3eqtrd 2781 |
1
โข (๐ด โ โ โ (๐โ๐ด) = ฮฃ๐ โ (1...(โโ๐ด))(((ฮโ๐) ยท (logโ๐)) + ฮฃ๐ โ {๐ฆ โ โ โฃ ๐ฆ โฅ ๐} ((ฮโ๐) ยท (ฮโ(๐ / ๐))))) |