Step | Hyp | Ref
| Expression |
1 | | dvdsflip.f |
. 2
โข ๐น = (๐ฆ โ ๐ด โฆ (๐ / ๐ฆ)) |
2 | | dvdsflip.a |
. . . . 5
โข ๐ด = {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} |
3 | 2 | eleq2i 2830 |
. . . 4
โข (๐ฆ โ ๐ด โ ๐ฆ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
4 | | dvdsdivcl 16133 |
. . . 4
โข ((๐ โ โ โง ๐ฆ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ฆ) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
5 | 3, 4 | sylan2b 595 |
. . 3
โข ((๐ โ โ โง ๐ฆ โ ๐ด) โ (๐ / ๐ฆ) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
6 | 5, 2 | eleqtrrdi 2850 |
. 2
โข ((๐ โ โ โง ๐ฆ โ ๐ด) โ (๐ / ๐ฆ) โ ๐ด) |
7 | 2 | eleq2i 2830 |
. . . 4
โข (๐ง โ ๐ด โ ๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
8 | | dvdsdivcl 16133 |
. . . 4
โข ((๐ โ โ โง ๐ง โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ง) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
9 | 7, 8 | sylan2b 595 |
. . 3
โข ((๐ โ โ โง ๐ง โ ๐ด) โ (๐ / ๐ง) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) |
10 | 9, 2 | eleqtrrdi 2850 |
. 2
โข ((๐ โ โ โง ๐ง โ ๐ด) โ (๐ / ๐ง) โ ๐ด) |
11 | 2 | ssrab3 4039 |
. . . . . 6
โข ๐ด โ
โ |
12 | 11 | sseli 3939 |
. . . . 5
โข (๐ฆ โ ๐ด โ ๐ฆ โ โ) |
13 | 11 | sseli 3939 |
. . . . 5
โข (๐ง โ ๐ด โ ๐ง โ โ) |
14 | 12, 13 | anim12i 614 |
. . . 4
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ด) โ (๐ฆ โ โ โง ๐ง โ โ)) |
15 | | nncn 12095 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
16 | 15 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ๐ โ
โ) |
17 | | nncn 12095 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
18 | 17 | ad2antrl 727 |
. . . . . 6
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ๐ฆ โ
โ) |
19 | | nncn 12095 |
. . . . . . 7
โข (๐ง โ โ โ ๐ง โ
โ) |
20 | 19 | ad2antll 728 |
. . . . . 6
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ๐ง โ
โ) |
21 | | nnne0 12121 |
. . . . . . 7
โข (๐ง โ โ โ ๐ง โ 0) |
22 | 21 | ad2antll 728 |
. . . . . 6
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ๐ง โ 0) |
23 | 16, 18, 20, 22 | divmul3d 11899 |
. . . . 5
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐ / ๐ง) = ๐ฆ โ ๐ = (๐ฆ ยท ๐ง))) |
24 | | nnne0 12121 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ 0) |
25 | 24 | ad2antrl 727 |
. . . . . 6
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ๐ฆ โ 0) |
26 | 16, 20, 18, 25 | divmul2d 11898 |
. . . . 5
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐ / ๐ฆ) = ๐ง โ ๐ = (๐ฆ ยท ๐ง))) |
27 | 23, 26 | bitr4d 282 |
. . . 4
โข ((๐ โ โ โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐ / ๐ง) = ๐ฆ โ (๐ / ๐ฆ) = ๐ง)) |
28 | 14, 27 | sylan2 594 |
. . 3
โข ((๐ โ โ โง (๐ฆ โ ๐ด โง ๐ง โ ๐ด)) โ ((๐ / ๐ง) = ๐ฆ โ (๐ / ๐ฆ) = ๐ง)) |
29 | | eqcom 2745 |
. . 3
โข (๐ฆ = (๐ / ๐ง) โ (๐ / ๐ง) = ๐ฆ) |
30 | | eqcom 2745 |
. . 3
โข (๐ง = (๐ / ๐ฆ) โ (๐ / ๐ฆ) = ๐ง) |
31 | 28, 29, 30 | 3bitr4g 314 |
. 2
โข ((๐ โ โ โง (๐ฆ โ ๐ด โง ๐ง โ ๐ด)) โ (๐ฆ = (๐ / ๐ง) โ ๐ง = (๐ / ๐ฆ))) |
32 | 1, 6, 10, 31 | f1o2d 7598 |
1
โข (๐ โ โ โ ๐น:๐ดโ1-1-ontoโ๐ด) |