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 ( ( 𝑀𝑁𝑁𝑀 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 dvdszrcl ( 𝑀𝑁 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2 simpr ( ( 𝑀𝑁𝑁𝑀 ) → 𝑁𝑀 )
3 breq1 ( 𝑁 = 0 → ( 𝑁𝑀 ↔ 0 ∥ 𝑀 ) )
4 0dvds ( 𝑀 ∈ ℤ → ( 0 ∥ 𝑀𝑀 = 0 ) )
5 4 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∥ 𝑀𝑀 = 0 ) )
6 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
7 6 abs00ad ( 𝑀 ∈ ℤ → ( ( abs ‘ 𝑀 ) = 0 ↔ 𝑀 = 0 ) )
8 7 bicomd ( 𝑀 ∈ ℤ → ( 𝑀 = 0 ↔ ( abs ‘ 𝑀 ) = 0 ) )
9 8 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 = 0 ↔ ( abs ‘ 𝑀 ) = 0 ) )
10 5 9 bitrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∥ 𝑀 ↔ ( abs ‘ 𝑀 ) = 0 ) )
11 3 10 sylan9bb ( ( 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁𝑀 ↔ ( abs ‘ 𝑀 ) = 0 ) )
12 fveq2 ( 𝑁 = 0 → ( abs ‘ 𝑁 ) = ( abs ‘ 0 ) )
13 abs0 ( abs ‘ 0 ) = 0
14 12 13 eqtrdi ( 𝑁 = 0 → ( abs ‘ 𝑁 ) = 0 )
15 14 adantr ( ( 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( abs ‘ 𝑁 ) = 0 )
16 15 eqeq2d ( ( 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ↔ ( abs ‘ 𝑀 ) = 0 ) )
17 11 16 bitr4d ( ( 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁𝑀 ↔ ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) )
18 2 17 syl5ib ( ( 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑀𝑁𝑁𝑀 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) )
19 18 expd ( ( 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 → ( 𝑁𝑀 → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
20 simprl ( ( ¬ 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
21 simpr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
22 21 adantl ( ( ¬ 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
23 neqne ( ¬ 𝑁 = 0 → 𝑁 ≠ 0 )
24 23 adantr ( ( ¬ 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ≠ 0 )
25 dvdsleabs2 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀𝑁 → ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) ) )
26 20 22 24 25 syl3anc ( ( ¬ 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 → ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) ) )
27 simpr ( ( 𝑁𝑀𝑀𝑁 ) → 𝑀𝑁 )
28 breq1 ( 𝑀 = 0 → ( 𝑀𝑁 ↔ 0 ∥ 𝑁 ) )
29 0dvds ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁𝑁 = 0 ) )
30 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
31 30 abs00ad ( 𝑁 ∈ ℤ → ( ( abs ‘ 𝑁 ) = 0 ↔ 𝑁 = 0 ) )
32 eqcom ( ( abs ‘ 𝑁 ) = 0 ↔ 0 = ( abs ‘ 𝑁 ) )
33 31 32 bitr3di ( 𝑁 ∈ ℤ → ( 𝑁 = 0 ↔ 0 = ( abs ‘ 𝑁 ) ) )
34 29 33 bitrd ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 0 = ( abs ‘ 𝑁 ) ) )
35 34 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∥ 𝑁 ↔ 0 = ( abs ‘ 𝑁 ) ) )
36 28 35 sylan9bb ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 ↔ 0 = ( abs ‘ 𝑁 ) ) )
37 fveq2 ( 𝑀 = 0 → ( abs ‘ 𝑀 ) = ( abs ‘ 0 ) )
38 37 13 eqtrdi ( 𝑀 = 0 → ( abs ‘ 𝑀 ) = 0 )
39 38 adantr ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( abs ‘ 𝑀 ) = 0 )
40 39 eqeq1d ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ↔ 0 = ( abs ‘ 𝑁 ) ) )
41 36 40 bitr4d ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 ↔ ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) )
42 27 41 syl5ib ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑁𝑀𝑀𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) )
43 42 a1dd ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑁𝑀𝑀𝑁 ) → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
44 43 expcomd ( ( 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 → ( 𝑁𝑀 → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) ) )
45 21 adantl ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
46 simprl ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
47 neqne ( ¬ 𝑀 = 0 → 𝑀 ≠ 0 )
48 47 adantr ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ≠ 0 )
49 dvdsleabs2 ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ( 𝑁𝑀 → ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) ) )
50 45 46 48 49 syl3anc ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁𝑀 → ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) ) )
51 eqcom ( ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ↔ ( abs ‘ 𝑁 ) = ( abs ‘ 𝑀 ) )
52 30 abscld ( 𝑁 ∈ ℤ → ( abs ‘ 𝑁 ) ∈ ℝ )
53 6 abscld ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) ∈ ℝ )
54 letri3 ( ( ( abs ‘ 𝑁 ) ∈ ℝ ∧ ( abs ‘ 𝑀 ) ∈ ℝ ) → ( ( abs ‘ 𝑁 ) = ( abs ‘ 𝑀 ) ↔ ( ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) ∧ ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) ) ) )
55 52 53 54 syl2anr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) = ( abs ‘ 𝑀 ) ↔ ( ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) ∧ ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) ) ) )
56 51 55 syl5bb ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ↔ ( ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) ∧ ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) ) ) )
57 56 biimprd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) ∧ ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) )
58 57 expd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
59 58 adantl ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( abs ‘ 𝑁 ) ≤ ( abs ‘ 𝑀 ) → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
60 50 59 syld ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁𝑀 → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
61 60 a1d ( ( ¬ 𝑀 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 → ( 𝑁𝑀 → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) ) )
62 44 61 pm2.61ian ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁 → ( 𝑁𝑀 → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) ) )
63 62 com34 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁 → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( 𝑁𝑀 → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) ) )
64 63 adantl ( ( ¬ 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 → ( ( abs ‘ 𝑀 ) ≤ ( abs ‘ 𝑁 ) → ( 𝑁𝑀 → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) ) )
65 26 64 mpdd ( ( ¬ 𝑁 = 0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀𝑁 → ( 𝑁𝑀 → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
66 19 65 pm2.61ian ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁 → ( 𝑁𝑀 → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) ) )
67 1 66 mpcom ( 𝑀𝑁 → ( 𝑁𝑀 → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) ) )
68 67 imp ( ( 𝑀𝑁𝑁𝑀 ) → ( abs ‘ 𝑀 ) = ( abs ‘ 𝑁 ) )