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 ‘ 𝑁 ) )