Metamath Proof Explorer


Theorem dvdsabseq

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 MNNMM=N

Proof

Step Hyp Ref Expression
1 dvdszrcl MNMN
2 simpr MNNMNM
3 breq1 N=0NM0M
4 0dvds M0MM=0
5 4 adantr MN0MM=0
6 zcn MM
7 6 abs00ad MM=0M=0
8 7 bicomd MM=0M=0
9 8 adantr MNM=0M=0
10 5 9 bitrd MN0MM=0
11 3 10 sylan9bb N=0MNNMM=0
12 fveq2 N=0N=0
13 abs0 0=0
14 12 13 eqtrdi N=0N=0
15 14 adantr N=0MNN=0
16 15 eqeq2d N=0MNM=NM=0
17 11 16 bitr4d N=0MNNMM=N
18 2 17 syl5ib N=0MNMNNMM=N
19 18 expd N=0MNMNNMM=N
20 simprl ¬N=0MNM
21 simpr MNN
22 21 adantl ¬N=0MNN
23 neqne ¬N=0N0
24 23 adantr ¬N=0MNN0
25 dvdsleabs2 MNN0MNMN
26 20 22 24 25 syl3anc ¬N=0MNMNMN
27 simpr NMMNMN
28 breq1 M=0MN0N
29 0dvds N0NN=0
30 zcn NN
31 30 abs00ad NN=0N=0
32 eqcom N=00=N
33 31 32 bitr3di NN=00=N
34 29 33 bitrd N0N0=N
35 34 adantl MN0N0=N
36 28 35 sylan9bb M=0MNMN0=N
37 fveq2 M=0M=0
38 37 13 eqtrdi M=0M=0
39 38 adantr M=0MNM=0
40 39 eqeq1d M=0MNM=N0=N
41 36 40 bitr4d M=0MNMNM=N
42 27 41 syl5ib M=0MNNMMNM=N
43 42 a1dd M=0MNNMMNMNM=N
44 43 expcomd M=0MNMNNMMNM=N
45 21 adantl ¬M=0MNN
46 simprl ¬M=0MNM
47 neqne ¬M=0M0
48 47 adantr ¬M=0MNM0
49 dvdsleabs2 NMM0NMNM
50 45 46 48 49 syl3anc ¬M=0MNNMNM
51 eqcom M=NN=M
52 30 abscld NN
53 6 abscld MM
54 letri3 NMN=MNMMN
55 52 53 54 syl2anr MNN=MNMMN
56 51 55 syl5bb MNM=NNMMN
57 56 biimprd MNNMMNM=N
58 57 expd MNNMMNM=N
59 58 adantl ¬M=0MNNMMNM=N
60 50 59 syld ¬M=0MNNMMNM=N
61 60 a1d ¬M=0MNMNNMMNM=N
62 44 61 pm2.61ian MNMNNMMNM=N
63 62 com34 MNMNMNNMM=N
64 63 adantl ¬N=0MNMNMNNMM=N
65 26 64 mpdd ¬N=0MNMNNMM=N
66 19 65 pm2.61ian MNMNNMM=N
67 1 66 mpcom MNNMM=N
68 67 imp MNNMM=N