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 
|- ( ( M || N /\ N || M ) -> ( abs ` M ) = ( abs ` N ) )

Proof

Step Hyp Ref Expression
1 dvdszrcl 
 |-  ( M || N -> ( M e. ZZ /\ N e. ZZ ) )
2 simpr 
 |-  ( ( M || N /\ N || M ) -> N || M )
3 breq1 
 |-  ( N = 0 -> ( N || M <-> 0 || M ) )
4 0dvds 
 |-  ( M e. ZZ -> ( 0 || M <-> M = 0 ) )
5 4 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 || M <-> M = 0 ) )
6 zcn 
 |-  ( M e. ZZ -> M e. CC )
7 6 abs00ad 
 |-  ( M e. ZZ -> ( ( abs ` M ) = 0 <-> M = 0 ) )
8 7 bicomd 
 |-  ( M e. ZZ -> ( M = 0 <-> ( abs ` M ) = 0 ) )
9 8 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M = 0 <-> ( abs ` M ) = 0 ) )
10 5 9 bitrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 || M <-> ( abs ` M ) = 0 ) )
11 3 10 sylan9bb 
 |-  ( ( N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N || M <-> ( abs ` M ) = 0 ) )
12 fveq2 
 |-  ( N = 0 -> ( abs ` N ) = ( abs ` 0 ) )
13 abs0 
 |-  ( abs ` 0 ) = 0
14 12 13 eqtrdi 
 |-  ( N = 0 -> ( abs ` N ) = 0 )
15 14 adantr 
 |-  ( ( N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( abs ` N ) = 0 )
16 15 eqeq2d 
 |-  ( ( N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( abs ` M ) = ( abs ` N ) <-> ( abs ` M ) = 0 ) )
17 11 16 bitr4d 
 |-  ( ( N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N || M <-> ( abs ` M ) = ( abs ` N ) ) )
18 2 17 imbitrid 
 |-  ( ( N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( M || N /\ N || M ) -> ( abs ` M ) = ( abs ` N ) ) )
19 18 expd 
 |-  ( ( N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N -> ( N || M -> ( abs ` M ) = ( abs ` N ) ) ) )
20 simprl 
 |-  ( ( -. N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> M e. ZZ )
21 simpr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
22 21 adantl 
 |-  ( ( -. N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> N e. ZZ )
23 neqne 
 |-  ( -. N = 0 -> N =/= 0 )
24 23 adantr 
 |-  ( ( -. N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> N =/= 0 )
25 dvdsleabs2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> ( abs ` M ) <_ ( abs ` N ) ) )
26 20 22 24 25 syl3anc 
 |-  ( ( -. N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N -> ( abs ` M ) <_ ( abs ` N ) ) )
27 simpr 
 |-  ( ( N || M /\ M || N ) -> M || N )
28 breq1 
 |-  ( M = 0 -> ( M || N <-> 0 || N ) )
29 0dvds 
 |-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
30 zcn 
 |-  ( N e. ZZ -> N e. CC )
31 30 abs00ad 
 |-  ( N e. ZZ -> ( ( abs ` N ) = 0 <-> N = 0 ) )
32 eqcom 
 |-  ( ( abs ` N ) = 0 <-> 0 = ( abs ` N ) )
33 31 32 bitr3di 
 |-  ( N e. ZZ -> ( N = 0 <-> 0 = ( abs ` N ) ) )
34 29 33 bitrd 
 |-  ( N e. ZZ -> ( 0 || N <-> 0 = ( abs ` N ) ) )
35 34 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 || N <-> 0 = ( abs ` N ) ) )
36 28 35 sylan9bb 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N <-> 0 = ( abs ` N ) ) )
37 fveq2 
 |-  ( M = 0 -> ( abs ` M ) = ( abs ` 0 ) )
38 37 13 eqtrdi 
 |-  ( M = 0 -> ( abs ` M ) = 0 )
39 38 adantr 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( abs ` M ) = 0 )
40 39 eqeq1d 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( abs ` M ) = ( abs ` N ) <-> 0 = ( abs ` N ) ) )
41 36 40 bitr4d 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N <-> ( abs ` M ) = ( abs ` N ) ) )
42 27 41 imbitrid 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( N || M /\ M || N ) -> ( abs ` M ) = ( abs ` N ) ) )
43 42 a1dd 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( N || M /\ M || N ) -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) )
44 43 expcomd 
 |-  ( ( M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N -> ( N || M -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) ) )
45 21 adantl 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> N e. ZZ )
46 simprl 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> M e. ZZ )
47 neqne 
 |-  ( -. M = 0 -> M =/= 0 )
48 47 adantr 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> M =/= 0 )
49 dvdsleabs2 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ M =/= 0 ) -> ( N || M -> ( abs ` N ) <_ ( abs ` M ) ) )
50 45 46 48 49 syl3anc 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N || M -> ( abs ` N ) <_ ( abs ` M ) ) )
51 eqcom 
 |-  ( ( abs ` M ) = ( abs ` N ) <-> ( abs ` N ) = ( abs ` M ) )
52 30 abscld 
 |-  ( N e. ZZ -> ( abs ` N ) e. RR )
53 6 abscld 
 |-  ( M e. ZZ -> ( abs ` M ) e. RR )
54 letri3 
 |-  ( ( ( abs ` N ) e. RR /\ ( abs ` M ) e. RR ) -> ( ( abs ` N ) = ( abs ` M ) <-> ( ( abs ` N ) <_ ( abs ` M ) /\ ( abs ` M ) <_ ( abs ` N ) ) ) )
55 52 53 54 syl2anr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` N ) = ( abs ` M ) <-> ( ( abs ` N ) <_ ( abs ` M ) /\ ( abs ` M ) <_ ( abs ` N ) ) ) )
56 51 55 bitrid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) = ( abs ` N ) <-> ( ( abs ` N ) <_ ( abs ` M ) /\ ( abs ` M ) <_ ( abs ` N ) ) ) )
57 56 biimprd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` N ) <_ ( abs ` M ) /\ ( abs ` M ) <_ ( abs ` N ) ) -> ( abs ` M ) = ( abs ` N ) ) )
58 57 expd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` N ) <_ ( abs ` M ) -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) )
59 58 adantl 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( abs ` N ) <_ ( abs ` M ) -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) )
60 50 59 syld 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N || M -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) )
61 60 a1d 
 |-  ( ( -. M = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N -> ( N || M -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) ) )
62 44 61 pm2.61ian 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( N || M -> ( ( abs ` M ) <_ ( abs ` N ) -> ( abs ` M ) = ( abs ` N ) ) ) ) )
63 62 com34 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( ( abs ` M ) <_ ( abs ` N ) -> ( N || M -> ( abs ` M ) = ( abs ` N ) ) ) ) )
64 63 adantl 
 |-  ( ( -. N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N -> ( ( abs ` M ) <_ ( abs ` N ) -> ( N || M -> ( abs ` M ) = ( abs ` N ) ) ) ) )
65 26 64 mpdd 
 |-  ( ( -. N = 0 /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M || N -> ( N || M -> ( abs ` M ) = ( abs ` N ) ) ) )
66 19 65 pm2.61ian 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( N || M -> ( abs ` M ) = ( abs ` N ) ) ) )
67 1 66 mpcom 
 |-  ( M || N -> ( N || M -> ( abs ` M ) = ( abs ` N ) ) )
68 67 imp 
 |-  ( ( M || N /\ N || M ) -> ( abs ` M ) = ( abs ` N ) )