Step | Hyp | Ref
| Expression |
1 | | nfcv 2908 |
. . 3
โข
โฒ๐ขฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด |
2 | | nfcv 2908 |
. . . 4
โข
โฒ๐{๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข} |
3 | | nfcsb1v 3885 |
. . . 4
โข
โฒ๐โฆ๐ข / ๐โฆ๐ด |
4 | 2, 3 | nfsum 15582 |
. . 3
โข
โฒ๐ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด |
5 | | breq2 5114 |
. . . . 5
โข (๐ = ๐ข โ (๐ฅ โฅ ๐ โ ๐ฅ โฅ ๐ข)) |
6 | 5 | rabbidv 3418 |
. . . 4
โข (๐ = ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} = {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}) |
7 | | csbeq1a 3874 |
. . . . 5
โข (๐ = ๐ข โ ๐ด = โฆ๐ข / ๐โฆ๐ด) |
8 | 7 | adantr 482 |
. . . 4
โข ((๐ = ๐ข โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ด = โฆ๐ข / ๐โฆ๐ด) |
9 | 6, 8 | sumeq12dv 15598 |
. . 3
โข (๐ = ๐ข โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด) |
10 | 1, 4, 9 | cbvsumi 15589 |
. 2
โข
ฮฃ๐ โ
{๐ฅ โ โ โฃ
๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด = ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด |
11 | | breq2 5114 |
. . . . . 6
โข (๐ข = (๐ / ๐ฃ) โ (๐ฅ โฅ ๐ข โ ๐ฅ โฅ (๐ / ๐ฃ))) |
12 | 11 | rabbidv 3418 |
. . . . 5
โข (๐ข = (๐ / ๐ฃ) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข} = {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}) |
13 | | csbeq1 3863 |
. . . . . 6
โข (๐ข = (๐ / ๐ฃ) โ โฆ๐ข / ๐โฆ๐ด = โฆ(๐ / ๐ฃ) / ๐โฆ๐ด) |
14 | 13 | adantr 482 |
. . . . 5
โข ((๐ข = (๐ / ๐ฃ) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}) โ โฆ๐ข / ๐โฆ๐ด = โฆ(๐ / ๐ฃ) / ๐โฆ๐ด) |
15 | 12, 14 | sumeq12dv 15598 |
. . . 4
โข (๐ข = (๐ / ๐ฃ) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด) |
16 | | fzfid 13885 |
. . . . 5
โข (๐ โ (1...๐) โ Fin) |
17 | | fsumdvdscom.1 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
18 | | dvdsssfz1 16207 |
. . . . . 6
โข (๐ โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
19 | 17, 18 | syl 17 |
. . . . 5
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
20 | 16, 19 | ssfid 9218 |
. . . 4
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ Fin) |
21 | | eqid 2737 |
. . . . . 6
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} = {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} |
22 | | eqid 2737 |
. . . . . 6
โข (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โฆ (๐ / ๐ง)) = (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โฆ (๐ / ๐ง)) |
23 | 21, 22 | dvdsflip 16206 |
. . . . 5
โข (๐ โ โ โ (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โฆ (๐ / ๐ง)):{๐ฅ โ โ โฃ ๐ฅ โฅ ๐}โ1-1-ontoโ{๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
24 | 17, 23 | syl 17 |
. . . 4
โข (๐ โ (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โฆ (๐ / ๐ง)):{๐ฅ โ โ โฃ ๐ฅ โฅ ๐}โ1-1-ontoโ{๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
25 | | oveq2 7370 |
. . . . . 6
โข (๐ง = ๐ฃ โ (๐ / ๐ง) = (๐ / ๐ฃ)) |
26 | | ovex 7395 |
. . . . . 6
โข (๐ / ๐ง) โ V |
27 | 25, 22, 26 | fvmpt3i 6958 |
. . . . 5
โข (๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ((๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โฆ (๐ / ๐ง))โ๐ฃ) = (๐ / ๐ฃ)) |
28 | 27 | adantl 483 |
. . . 4
โข ((๐ โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ((๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โฆ (๐ / ๐ง))โ๐ฃ) = (๐ / ๐ฃ)) |
29 | | fzfid 13885 |
. . . . . 6
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (1...๐ข) โ Fin) |
30 | | ssrab2 4042 |
. . . . . . . 8
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ โ |
31 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
32 | 30, 31 | sselid 3947 |
. . . . . . 7
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ข โ โ) |
33 | | dvdsssfz1 16207 |
. . . . . . 7
โข (๐ข โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข} โ (1...๐ข)) |
34 | 32, 33 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข} โ (1...๐ข)) |
35 | 29, 34 | ssfid 9218 |
. . . . 5
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข} โ Fin) |
36 | | fsumdvdscom.3 |
. . . . . . . . 9
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ๐ด โ โ) |
37 | 36 | ralrimivva 3198 |
. . . . . . . 8
โข (๐ โ โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด โ โ) |
38 | | nfv 1918 |
. . . . . . . . 9
โข
โฒ๐ขโ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด โ โ |
39 | 3 | nfel1 2924 |
. . . . . . . . . 10
โข
โฒ๐โฆ๐ข / ๐โฆ๐ด โ โ |
40 | 2, 39 | nfralw 3297 |
. . . . . . . . 9
โข
โฒ๐โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ |
41 | 7 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = ๐ข โ (๐ด โ โ โ โฆ๐ข / ๐โฆ๐ด โ โ)) |
42 | 6, 41 | raleqbidv 3322 |
. . . . . . . . 9
โข (๐ = ๐ข โ (โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด โ โ โ โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ)) |
43 | 38, 40, 42 | cbvralw 3292 |
. . . . . . . 8
โข
(โ๐ โ
{๐ฅ โ โ โฃ
๐ฅ โฅ ๐}โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด โ โ โ โ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ) |
44 | 37, 43 | sylib 217 |
. . . . . . 7
โข (๐ โ โ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ) |
45 | 44 | r19.21bi 3237 |
. . . . . 6
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ) |
46 | 45 | r19.21bi 3237 |
. . . . 5
โข (((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}) โ โฆ๐ข / ๐โฆ๐ด โ โ) |
47 | 35, 46 | fsumcl 15625 |
. . . 4
โข ((๐ โง ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ) |
48 | 15, 20, 24, 28, 47 | fsumf1o 15615 |
. . 3
โข (๐ โ ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด = ฮฃ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด) |
49 | 13 | eleq1d 2823 |
. . . . . . . 8
โข (๐ข = (๐ / ๐ฃ) โ (โฆ๐ข / ๐โฆ๐ด โ โ โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ)) |
50 | 12, 49 | raleqbidv 3322 |
. . . . . . 7
โข (๐ข = (๐ / ๐ฃ) โ (โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ โ โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ)) |
51 | 44 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ โ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด โ โ) |
52 | | dvdsdivcl 16205 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ฃ) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
53 | 17, 52 | sylan 581 |
. . . . . . 7
โข ((๐ โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ฃ) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
54 | 50, 51, 53 | rspcdva 3585 |
. . . . . 6
โข ((๐ โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ โ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ) |
55 | 54 | r19.21bi 3237 |
. . . . 5
โข (((๐ โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}) โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ) |
56 | 55 | anasss 468 |
. . . 4
โข ((๐ โง (๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)})) โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ) |
57 | 17, 56 | fsumdvdsdiag 26549 |
. . 3
โข (๐ โ ฮฃ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด) |
58 | | oveq2 7370 |
. . . . . . 7
โข (๐ฃ = ((๐ / ๐) / ๐) โ (๐ / ๐ฃ) = (๐ / ((๐ / ๐) / ๐))) |
59 | 58 | csbeq1d 3864 |
. . . . . 6
โข (๐ฃ = ((๐ / ๐) / ๐) โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด = โฆ(๐ / ((๐ / ๐) / ๐)) / ๐โฆ๐ด) |
60 | | fzfid 13885 |
. . . . . . 7
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (1...(๐ / ๐)) โ Fin) |
61 | | dvdsdivcl 16205 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
62 | 30, 61 | sselid 3947 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐) โ โ) |
63 | 17, 62 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐) โ โ) |
64 | | dvdsssfz1 16207 |
. . . . . . . 8
โข ((๐ / ๐) โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ (1...(๐ / ๐))) |
65 | 63, 64 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ (1...(๐ / ๐))) |
66 | 60, 65 | ssfid 9218 |
. . . . . 6
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ Fin) |
67 | | eqid 2737 |
. . . . . . . 8
โข {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} = {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} |
68 | | eqid 2737 |
. . . . . . . 8
โข (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โฆ ((๐ / ๐) / ๐ง)) = (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โฆ ((๐ / ๐) / ๐ง)) |
69 | 67, 68 | dvdsflip 16206 |
. . . . . . 7
โข ((๐ / ๐) โ โ โ (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โฆ ((๐ / ๐) / ๐ง)):{๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โ1-1-ontoโ{๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) |
70 | 63, 69 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โฆ ((๐ / ๐) / ๐ง)):{๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โ1-1-ontoโ{๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) |
71 | | oveq2 7370 |
. . . . . . . 8
โข (๐ง = ๐ โ ((๐ / ๐) / ๐ง) = ((๐ / ๐) / ๐)) |
72 | | ovex 7395 |
. . . . . . . 8
โข ((๐ / ๐) / ๐ง) โ V |
73 | 71, 68, 72 | fvmpt3i 6958 |
. . . . . . 7
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ ((๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โฆ ((๐ / ๐) / ๐ง))โ๐) = ((๐ / ๐) / ๐)) |
74 | 73 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ ((๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โฆ ((๐ / ๐) / ๐ง))โ๐) = ((๐ / ๐) / ๐)) |
75 | 17 | fsumdvdsdiaglem 26548 |
. . . . . . . 8
โข (๐ โ ((๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}))) |
76 | 56 | ex 414 |
. . . . . . . 8
โข (๐ โ ((๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐ฃ)}) โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ)) |
77 | 75, 76 | syld 47 |
. . . . . . 7
โข (๐ โ ((๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ)) |
78 | 77 | impl 457 |
. . . . . 6
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ โฆ(๐ / ๐ฃ) / ๐โฆ๐ด โ โ) |
79 | 59, 66, 70, 74, 78 | fsumf1o 15615 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โฆ(๐ / ((๐ / ๐) / ๐)) / ๐โฆ๐ด) |
80 | | ovexd 7397 |
. . . . . . 7
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ / ((๐ / ๐) / ๐)) โ V) |
81 | | nncn 12168 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
82 | | nnne0 12194 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ 0) |
83 | 81, 82 | jca 513 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ โ โ โง ๐ โ 0)) |
84 | 17, 83 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ โ โง ๐ โ 0)) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ โ โ โง ๐ โ 0)) |
86 | 85 | simpld 496 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ ๐ โ โ) |
87 | | elrabi 3644 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ๐ โ โ) |
88 | 87 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ๐ โ โ) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ ๐ โ โ) |
90 | | nncn 12168 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
91 | | nnne0 12194 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ 0) |
92 | 90, 91 | jca 513 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ โ โ โง ๐ โ 0)) |
93 | 89, 92 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ โ โ โง ๐ โ 0)) |
94 | | elrabi 3644 |
. . . . . . . . . . . . . . 15
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ ๐ โ โ) |
95 | 94 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ ๐ โ โ) |
96 | | nncn 12168 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
97 | | nnne0 12194 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ 0) |
98 | 96, 97 | jca 513 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ โ โ โง ๐ โ 0)) |
99 | 95, 98 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ โ โ โง ๐ โ 0)) |
100 | | divdiv1 11873 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ 0) โง (๐ โ โ โง ๐ โ 0)) โ ((๐ / ๐) / ๐) = (๐ / (๐ ยท ๐))) |
101 | 86, 93, 99, 100 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ ((๐ / ๐) / ๐) = (๐ / (๐ ยท ๐))) |
102 | 101 | oveq2d 7378 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ / ((๐ / ๐) / ๐)) = (๐ / (๐ / (๐ ยท ๐)))) |
103 | | nnmulcl 12184 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
104 | 88, 94, 103 | syl2an 597 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ ยท ๐) โ โ) |
105 | | nncn 12168 |
. . . . . . . . . . . . . 14
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ โ) |
106 | | nnne0 12194 |
. . . . . . . . . . . . . 14
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ 0) |
107 | 105, 106 | jca 513 |
. . . . . . . . . . . . 13
โข ((๐ ยท ๐) โ โ โ ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โ 0)) |
108 | 104, 107 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โ 0)) |
109 | | ddcan 11876 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ 0) โง ((๐ ยท ๐) โ โ โง (๐ ยท ๐) โ 0)) โ (๐ / (๐ / (๐ ยท ๐))) = (๐ ยท ๐)) |
110 | 85, 108, 109 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ / (๐ / (๐ ยท ๐))) = (๐ ยท ๐)) |
111 | 102, 110 | eqtrd 2777 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ / ((๐ / ๐) / ๐)) = (๐ ยท ๐)) |
112 | 111 | eqeq2d 2748 |
. . . . . . . . 9
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ = (๐ / ((๐ / ๐) / ๐)) โ ๐ = (๐ ยท ๐))) |
113 | 112 | biimpa 478 |
. . . . . . . 8
โข ((((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โง ๐ = (๐ / ((๐ / ๐) / ๐))) โ ๐ = (๐ ยท ๐)) |
114 | | fsumdvdscom.2 |
. . . . . . . 8
โข (๐ = (๐ ยท ๐) โ ๐ด = ๐ต) |
115 | 113, 114 | syl 17 |
. . . . . . 7
โข ((((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โง ๐ = (๐ / ((๐ / ๐) / ๐))) โ ๐ด = ๐ต) |
116 | 80, 115 | csbied 3898 |
. . . . . 6
โข (((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ โฆ(๐ / ((๐ / ๐) / ๐)) / ๐โฆ๐ด = ๐ต) |
117 | 116 | sumeq2dv 15595 |
. . . . 5
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โฆ(๐ / ((๐ / ๐) / ๐)) / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}๐ต) |
118 | 79, 117 | eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ ฮฃ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}๐ต) |
119 | 118 | sumeq2dv 15595 |
. . 3
โข (๐ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ฃ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}โฆ(๐ / ๐ฃ) / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}๐ต) |
120 | 48, 57, 119 | 3eqtrd 2781 |
. 2
โข (๐ โ ฮฃ๐ข โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ข}โฆ๐ข / ๐โฆ๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}๐ต) |
121 | 10, 120 | eqtrid 2789 |
1
โข (๐ โ ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ด = ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}๐ต) |