Step | Hyp | Ref
| Expression |
1 | | breq1 5109 |
. . . 4
โข (๐ฅ = ๐ โ (๐ฅ โฅ ๐ โ ๐ โฅ ๐)) |
2 | | elrabi 3640 |
. . . . 5
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ ๐ โ โ) |
3 | 2 | ad2antll 728 |
. . . 4
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โ) |
4 | 3 | nnzd 12527 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โค) |
5 | | fsumdvdsdiag.1 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
6 | 5 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โ) |
7 | | simprl 770 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
8 | | dvdsdivcl 16199 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
9 | 6, 7, 8 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
10 | | elrabi 3640 |
. . . . . . 7
โข ((๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (๐ / ๐) โ โ) |
11 | 9, 10 | syl 17 |
. . . . . 6
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โ โ) |
12 | 11 | nnzd 12527 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โ โค) |
13 | 6 | nnzd 12527 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โค) |
14 | | breq1 5109 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฅ โฅ (๐ / ๐) โ ๐ โฅ (๐ / ๐))) |
15 | 14 | elrab 3646 |
. . . . . . 7
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ (๐ โ โ โง ๐ โฅ (๐ / ๐))) |
16 | 15 | simprbi 498 |
. . . . . 6
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)} โ ๐ โฅ (๐ / ๐)) |
17 | 16 | ad2antll 728 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โฅ (๐ / ๐)) |
18 | | breq1 5109 |
. . . . . . . 8
โข (๐ฅ = (๐ / ๐) โ (๐ฅ โฅ ๐ โ (๐ / ๐) โฅ ๐)) |
19 | 18 | elrab 3646 |
. . . . . . 7
โข ((๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ((๐ / ๐) โ โ โง (๐ / ๐) โฅ ๐)) |
20 | 19 | simprbi 498 |
. . . . . 6
โข ((๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (๐ / ๐) โฅ ๐) |
21 | 9, 20 | syl 17 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โฅ ๐) |
22 | 4, 12, 13, 17, 21 | dvdstrd 16178 |
. . . 4
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โฅ ๐) |
23 | 1, 3, 22 | elrabd 3648 |
. . 3
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
24 | | breq1 5109 |
. . . 4
โข (๐ฅ = ๐ โ (๐ฅ โฅ (๐ / ๐) โ ๐ โฅ (๐ / ๐))) |
25 | | elrabi 3640 |
. . . . 5
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ ๐ โ โ) |
26 | 25 | ad2antrl 727 |
. . . 4
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โ) |
27 | 26 | nnzd 12527 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โค) |
28 | 26 | nnne0d 12204 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ 0) |
29 | | dvdsmulcr 16169 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ / ๐) โ โค โง (๐ โ โค โง ๐ โ 0)) โ ((๐ ยท ๐) โฅ ((๐ / ๐) ยท ๐) โ ๐ โฅ (๐ / ๐))) |
30 | 4, 12, 27, 28, 29 | syl112anc 1375 |
. . . . . . 7
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ((๐ ยท ๐) โฅ ((๐ / ๐) ยท ๐) โ ๐ โฅ (๐ / ๐))) |
31 | 17, 30 | mpbird 257 |
. . . . . 6
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ ยท ๐) โฅ ((๐ / ๐) ยท ๐)) |
32 | 6 | nncnd 12170 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โ) |
33 | 26 | nncnd 12170 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โ) |
34 | 32, 33, 28 | divcan1d 11933 |
. . . . . . 7
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ((๐ / ๐) ยท ๐) = ๐) |
35 | 3 | nncnd 12170 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ โ) |
36 | 3 | nnne0d 12204 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ 0) |
37 | 32, 35, 36 | divcan2d 11934 |
. . . . . . 7
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ ยท (๐ / ๐)) = ๐) |
38 | 34, 37 | eqtr4d 2780 |
. . . . . 6
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ((๐ / ๐) ยท ๐) = (๐ ยท (๐ / ๐))) |
39 | 31, 38 | breqtrd 5132 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ ยท ๐) โฅ (๐ ยท (๐ / ๐))) |
40 | | ssrab2 4038 |
. . . . . . . 8
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ โ |
41 | | dvdsdivcl 16199 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
42 | 6, 23, 41 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
43 | 40, 42 | sselid 3943 |
. . . . . . 7
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โ โ) |
44 | 43 | nnzd 12527 |
. . . . . 6
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ / ๐) โ โค) |
45 | | dvdscmulr 16168 |
. . . . . 6
โข ((๐ โ โค โง (๐ / ๐) โ โค โง (๐ โ โค โง ๐ โ 0)) โ ((๐ ยท ๐) โฅ (๐ ยท (๐ / ๐)) โ ๐ โฅ (๐ / ๐))) |
46 | 27, 44, 4, 36, 45 | syl112anc 1375 |
. . . . 5
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ((๐ ยท ๐) โฅ (๐ ยท (๐ / ๐)) โ ๐ โฅ (๐ / ๐))) |
47 | 39, 46 | mpbid 231 |
. . . 4
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โฅ (๐ / ๐)) |
48 | 24, 26, 47 | elrabd 3648 |
. . 3
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) |
49 | 23, 48 | jca 513 |
. 2
โข ((๐ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) โ (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)})) |
50 | 49 | ex 414 |
1
โข (๐ โ ((๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}) โ (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ (๐ / ๐)}))) |