Description: If two integers divide each other, they must be equal, up to a difference in sign. Theorem 1.1(j) in ApostolNT p. 14. (Contributed by Mario Carneiro, 30-May-2014) (Revised by AV, 7-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsabseq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdszrcl | |
|
2 | simpr | |
|
3 | breq1 | |
|
4 | 0dvds | |
|
5 | 4 | adantr | |
6 | zcn | |
|
7 | 6 | abs00ad | |
8 | 7 | bicomd | |
9 | 8 | adantr | |
10 | 5 9 | bitrd | |
11 | 3 10 | sylan9bb | |
12 | fveq2 | |
|
13 | abs0 | |
|
14 | 12 13 | eqtrdi | |
15 | 14 | adantr | |
16 | 15 | eqeq2d | |
17 | 11 16 | bitr4d | |
18 | 2 17 | syl5ib | |
19 | 18 | expd | |
20 | simprl | |
|
21 | simpr | |
|
22 | 21 | adantl | |
23 | neqne | |
|
24 | 23 | adantr | |
25 | dvdsleabs2 | |
|
26 | 20 22 24 25 | syl3anc | |
27 | simpr | |
|
28 | breq1 | |
|
29 | 0dvds | |
|
30 | zcn | |
|
31 | 30 | abs00ad | |
32 | eqcom | |
|
33 | 31 32 | bitr3di | |
34 | 29 33 | bitrd | |
35 | 34 | adantl | |
36 | 28 35 | sylan9bb | |
37 | fveq2 | |
|
38 | 37 13 | eqtrdi | |
39 | 38 | adantr | |
40 | 39 | eqeq1d | |
41 | 36 40 | bitr4d | |
42 | 27 41 | syl5ib | |
43 | 42 | a1dd | |
44 | 43 | expcomd | |
45 | 21 | adantl | |
46 | simprl | |
|
47 | neqne | |
|
48 | 47 | adantr | |
49 | dvdsleabs2 | |
|
50 | 45 46 48 49 | syl3anc | |
51 | eqcom | |
|
52 | 30 | abscld | |
53 | 6 | abscld | |
54 | letri3 | |
|
55 | 52 53 54 | syl2anr | |
56 | 51 55 | syl5bb | |
57 | 56 | biimprd | |
58 | 57 | expd | |
59 | 58 | adantl | |
60 | 50 59 | syld | |
61 | 60 | a1d | |
62 | 44 61 | pm2.61ian | |
63 | 62 | com34 | |
64 | 63 | adantl | |
65 | 26 64 | mpdd | |
66 | 19 65 | pm2.61ian | |
67 | 1 66 | mpcom | |
68 | 67 | imp | |