Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . 4
โข (๐ โ โ โ
(1...๐) โ
Fin) |
2 | | dvdsssfz1 16207 |
. . . 4
โข (๐ โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
3 | 1, 2 | ssfid 9218 |
. . 3
โข (๐ โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ Fin) |
4 | | fzfid 13885 |
. . . . 5
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (1...๐) โ Fin) |
5 | | elrabi 3644 |
. . . . . . 7
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ๐ โ โ) |
6 | 5 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ โ โ) |
7 | | dvdsssfz1 16207 |
. . . . . 6
โข (๐ โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
8 | 6, 7 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
9 | 4, 8 | ssfid 9218 |
. . . 4
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ Fin) |
10 | | elrabi 3644 |
. . . . . . . . 9
โข (๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ๐ข โ โ) |
11 | 10 | ad2antll 728 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ๐ข โ โ) |
12 | | vmacl 26483 |
. . . . . . . 8
โข (๐ข โ โ โ
(ฮโ๐ข) โ
โ) |
13 | 11, 12 | syl 17 |
. . . . . . 7
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ (ฮโ๐ข) โ โ) |
14 | | breq1 5113 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ข โ (๐ฅ โฅ ๐ โ ๐ข โฅ ๐)) |
15 | 14 | elrab 3650 |
. . . . . . . . . . 11
โข (๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (๐ข โ โ โง ๐ข โฅ ๐)) |
16 | 15 | simprbi 498 |
. . . . . . . . . 10
โข (๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ๐ข โฅ ๐) |
17 | 16 | ad2antll 728 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ๐ข โฅ ๐) |
18 | 5 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ๐ โ โ) |
19 | | nndivdvds 16152 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ข โ โ) โ (๐ข โฅ ๐ โ (๐ / ๐ข) โ โ)) |
20 | 18, 11, 19 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ (๐ข โฅ ๐ โ (๐ / ๐ข) โ โ)) |
21 | 17, 20 | mpbid 231 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ (๐ / ๐ข) โ โ) |
22 | | vmacl 26483 |
. . . . . . . 8
โข ((๐ / ๐ข) โ โ โ
(ฮโ(๐ / ๐ข)) โ
โ) |
23 | 21, 22 | syl 17 |
. . . . . . 7
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ (ฮโ(๐ / ๐ข)) โ โ) |
24 | 13, 23 | remulcld 11192 |
. . . . . 6
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ((ฮโ๐ข) ยท
(ฮโ(๐ / ๐ข))) โ
โ) |
25 | 24 | recnd 11190 |
. . . . 5
โข ((๐ โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ((ฮโ๐ข) ยท
(ฮโ(๐ / ๐ข))) โ
โ) |
26 | 25 | anassrs 469 |
. . . 4
โข (((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) โ โ) |
27 | 9, 26 | fsumcl 15625 |
. . 3
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) โ โ) |
28 | | vmacl 26483 |
. . . . . 6
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
29 | 6, 28 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (ฮโ๐) โ โ) |
30 | 6 | nnrpd 12962 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ โ โ+) |
31 | 30 | relogcld 25994 |
. . . . 5
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (logโ๐) โ โ) |
32 | 29, 31 | remulcld 11192 |
. . . 4
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐) ยท (logโ๐)) โ
โ) |
33 | 32 | recnd 11190 |
. . 3
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐) ยท (logโ๐)) โ
โ) |
34 | 3, 27, 33 | fsumadd 15632 |
. 2
โข (๐ โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) + ((ฮโ๐) ยท (logโ๐))) = (ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) + ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)))) |
35 | | id 22 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
36 | | fvoveq1 7385 |
. . . . . 6
โข (๐ = (๐ข ยท ๐) โ (ฮโ(๐ / ๐ข)) = (ฮโ((๐ข ยท ๐) / ๐ข))) |
37 | 36 | oveq2d 7378 |
. . . . 5
โข (๐ = (๐ข ยท ๐) โ ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) = ((ฮโ๐ข) ยท (ฮโ((๐ข ยท ๐) / ๐ข)))) |
38 | 35, 37, 25 | fsumdvdscom 26550 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) = ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} ((ฮโ๐ข) ยท (ฮโ((๐ข ยท ๐) / ๐ข)))) |
39 | | ssrab2 4042 |
. . . . . . . . . . . . 13
โข {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} โ โ |
40 | | simpr 486 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) |
41 | 39, 40 | sselid 3947 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ ๐ โ โ) |
42 | 41 | nncnd 12176 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ ๐ โ โ) |
43 | | ssrab2 4042 |
. . . . . . . . . . . . . 14
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ โ |
44 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
45 | 43, 44 | sselid 3947 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ โ) |
46 | 45 | nncnd 12176 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ โ) |
47 | 46 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ ๐ข โ โ) |
48 | 45 | nnne0d 12210 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ 0) |
49 | 48 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ ๐ข โ 0) |
50 | 42, 47, 49 | divcan3d 11943 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ ((๐ข ยท ๐) / ๐ข) = ๐) |
51 | 50 | fveq2d 6851 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ (ฮโ((๐ข ยท ๐) / ๐ข)) = (ฮโ๐)) |
52 | 51 | sumeq2dv 15595 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ((๐ข ยท ๐) / ๐ข)) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ๐)) |
53 | | dvdsdivcl 16205 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ข) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
54 | 43, 53 | sselid 3947 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ข) โ โ) |
55 | | vmasum 26580 |
. . . . . . . . 9
โข ((๐ / ๐ข) โ โ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ๐) = (logโ(๐ / ๐ข))) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ๐) = (logโ(๐ / ๐ข))) |
57 | | nnrp 12933 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ+) |
58 | 57 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ โ
โ+) |
59 | 45 | nnrpd 12962 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ โ+) |
60 | 58, 59 | relogdivd 25997 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (logโ(๐ / ๐ข)) = ((logโ๐) โ (logโ๐ข))) |
61 | 52, 56, 60 | 3eqtrd 2781 |
. . . . . . 7
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ((๐ข ยท ๐) / ๐ข)) = ((logโ๐) โ (logโ๐ข))) |
62 | 61 | oveq2d 7378 |
. . . . . 6
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐ข) ยท ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ((๐ข ยท ๐) / ๐ข))) = ((ฮโ๐ข) ยท ((logโ๐) โ (logโ๐ข)))) |
63 | | fzfid 13885 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (1...(๐ / ๐ข)) โ Fin) |
64 | | dvdsssfz1 16207 |
. . . . . . . . 9
โข ((๐ / ๐ข) โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} โ (1...(๐ / ๐ข))) |
65 | 54, 64 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} โ (1...(๐ / ๐ข))) |
66 | 63, 65 | ssfid 9218 |
. . . . . . 7
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} โ Fin) |
67 | 45, 12 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (ฮโ๐ข) โ โ) |
68 | 67 | recnd 11190 |
. . . . . . 7
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (ฮโ๐ข) โ โ) |
69 | | vmacl 26483 |
. . . . . . . . . 10
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
70 | 41, 69 | syl 17 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ (ฮโ๐) โ โ) |
71 | 70 | recnd 11190 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ (ฮโ๐) โ โ) |
72 | 51, 71 | eqeltrd 2838 |
. . . . . . 7
โข (((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)}) โ (ฮโ((๐ข ยท ๐) / ๐ข)) โ โ) |
73 | 66, 68, 72 | fsummulc2 15676 |
. . . . . 6
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐ข) ยท ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} (ฮโ((๐ข ยท ๐) / ๐ข))) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} ((ฮโ๐ข) ยท (ฮโ((๐ข ยท ๐) / ๐ข)))) |
74 | | relogcl 25947 |
. . . . . . . . 9
โข (๐ โ โ+
โ (logโ๐) โ
โ) |
75 | 74 | recnd 11190 |
. . . . . . . 8
โข (๐ โ โ+
โ (logโ๐) โ
โ) |
76 | 58, 75 | syl 17 |
. . . . . . 7
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (logโ๐) โ โ) |
77 | 59 | relogcld 25994 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (logโ๐ข) โ โ) |
78 | 77 | recnd 11190 |
. . . . . . 7
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (logโ๐ข) โ โ) |
79 | 68, 76, 78 | subdid 11618 |
. . . . . 6
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐ข) ยท ((logโ๐) โ (logโ๐ข))) = (((ฮโ๐ข) ยท (logโ๐)) โ
((ฮโ๐ข)
ยท (logโ๐ข)))) |
80 | 62, 73, 79 | 3eqtr3d 2785 |
. . . . 5
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} ((ฮโ๐ข) ยท (ฮโ((๐ข ยท ๐) / ๐ข))) = (((ฮโ๐ข) ยท (logโ๐)) โ ((ฮโ๐ข) ยท (logโ๐ข)))) |
81 | 80 | sumeq2dv 15595 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ข)} ((ฮโ๐ข) ยท (ฮโ((๐ข ยท ๐) / ๐ข))) = ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (((ฮโ๐ข) ยท (logโ๐)) โ ((ฮโ๐ข) ยท (logโ๐ข)))) |
82 | 68, 76 | mulcld 11182 |
. . . . . 6
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐ข) ยท (logโ๐)) โ
โ) |
83 | 68, 78 | mulcld 11182 |
. . . . . 6
โข ((๐ โ โ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((ฮโ๐ข) ยท (logโ๐ข)) โ
โ) |
84 | 3, 82, 83 | fsumsub 15680 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (((ฮโ๐ข) ยท (logโ๐)) โ ((ฮโ๐ข) ยท (logโ๐ข))) = (ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐)) โ ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐ข)))) |
85 | 57, 75 | syl 17 |
. . . . . . . 8
โข (๐ โ โ โ
(logโ๐) โ
โ) |
86 | 85 | sqvald 14055 |
. . . . . . 7
โข (๐ โ โ โ
((logโ๐)โ2) =
((logโ๐) ยท
(logโ๐))) |
87 | | vmasum 26580 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐ข) = (logโ๐)) |
88 | 87 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ โ โ
(ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐ข) ยท (logโ๐)) = ((logโ๐) ยท (logโ๐))) |
89 | 3, 85, 68 | fsummulc1 15677 |
. . . . . . 7
โข (๐ โ โ โ
(ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮโ๐ข) ยท (logโ๐)) = ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐))) |
90 | 86, 88, 89 | 3eqtr2rd 2784 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐)) = ((logโ๐)โ2)) |
91 | | fveq2 6847 |
. . . . . . . . 9
โข (๐ข = ๐ โ (ฮโ๐ข) = (ฮโ๐)) |
92 | | fveq2 6847 |
. . . . . . . . 9
โข (๐ข = ๐ โ (logโ๐ข) = (logโ๐)) |
93 | 91, 92 | oveq12d 7380 |
. . . . . . . 8
โข (๐ข = ๐ โ ((ฮโ๐ข) ยท (logโ๐ข)) = ((ฮโ๐) ยท (logโ๐))) |
94 | 93 | cbvsumv 15588 |
. . . . . . 7
โข
ฮฃ๐ข โ
{๐ฅ โ โ โฃ
๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐ข)) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)) |
95 | 94 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐ข)) = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐))) |
96 | 90, 95 | oveq12d 7380 |
. . . . 5
โข (๐ โ โ โ
(ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐)) โ ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (logโ๐ข))) = (((logโ๐)โ2) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)))) |
97 | 84, 96 | eqtrd 2777 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (((ฮโ๐ข) ยท (logโ๐)) โ ((ฮโ๐ข) ยท (logโ๐ข))) = (((logโ๐)โ2) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)))) |
98 | 38, 81, 97 | 3eqtrd 2781 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) = (((logโ๐)โ2) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)))) |
99 | 98 | oveq1d 7377 |
. 2
โข (๐ โ โ โ
(ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) + ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐))) = ((((logโ๐)โ2) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐))) + ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)))) |
100 | 85 | sqcld 14056 |
. . 3
โข (๐ โ โ โ
((logโ๐)โ2)
โ โ) |
101 | 3, 33 | fsumcl 15625 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐)) โ โ) |
102 | 100, 101 | npcand 11523 |
. 2
โข (๐ โ โ โ
((((logโ๐)โ2)
โ ฮฃ๐ โ
{๐ฅ โ โ โฃ
๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐))) + ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐) ยท (logโ๐))) = ((logโ๐)โ2)) |
103 | 34, 99, 102 | 3eqtrd 2781 |
1
โข (๐ โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} (ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} ((ฮโ๐ข) ยท (ฮโ(๐ / ๐ข))) + ((ฮโ๐) ยท (logโ๐))) = ((logโ๐)โ2)) |