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 → M = N

Proof

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