Metamath Proof Explorer

Theorem nzin

Description: The intersection of the set of multiples ofm, mℤ, and those ofn, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m andn. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypotheses nzin.m ⊢φ→M∈ℤ
nzin.n ⊢φ→N∈ℤ
Assertion nzin ⊢φ→∥M∩∥N=∥MlcmN

Proof

Step Hyp Ref Expression
1 nzin.m ⊢φ→M∈ℤ
2 nzin.n ⊢φ→N∈ℤ
3 dvdszrcl ⊢M∥n→M∈ℤ∧n∈ℤ
4 dvdszrcl ⊢N∥n→N∈ℤ∧n∈ℤ
5 3 4 anim12i ⊢M∥n∧N∥n→M∈ℤ∧n∈ℤ∧N∈ℤ∧n∈ℤ
6 anandir ⊢M∈ℤ∧N∈ℤ∧n∈ℤ↔M∈ℤ∧n∈ℤ∧N∈ℤ∧n∈ℤ
7 5 6 sylibr ⊢M∥n∧N∥n→M∈ℤ∧N∈ℤ∧n∈ℤ
8 7 ancomd ⊢M∥n∧N∥n→n∈ℤ∧M∈ℤ∧N∈ℤ
9 lcmdvds ⊢n∈ℤ∧M∈ℤ∧N∈ℤ→M∥n∧N∥n→MlcmN∥n
10 9 3expb ⊢n∈ℤ∧M∈ℤ∧N∈ℤ→M∥n∧N∥n→MlcmN∥n
11 8 10 mpcom ⊢M∥n∧N∥n→MlcmN∥n
12 elin ⊢n∈∥M∩∥N↔n∈∥M∧n∈∥N
13 reldvds ⊢Rel⁡∥
14 elrelimasn ⊢Rel⁡∥→n∈∥M↔M∥n
15 13 14 ax-mp ⊢n∈∥M↔M∥n
16 elrelimasn ⊢Rel⁡∥→n∈∥N↔N∥n
17 13 16 ax-mp ⊢n∈∥N↔N∥n
18 15 17 anbi12i ⊢n∈∥M∧n∈∥N↔M∥n∧N∥n
19 12 18 bitri ⊢n∈∥M∩∥N↔M∥n∧N∥n
20 elrelimasn ⊢Rel⁡∥→n∈∥MlcmN↔MlcmN∥n
21 13 20 ax-mp ⊢n∈∥MlcmN↔MlcmN∥n
22 11 19 21 3imtr4i ⊢n∈∥M∩∥N→n∈∥MlcmN
23 22 ssriv ⊢∥M∩∥N⊆∥MlcmN
24 23 a1i ⊢φ→∥M∩∥N⊆∥MlcmN
25 dvdslcm ⊢M∈ℤ∧N∈ℤ→M∥MlcmN∧N∥MlcmN
26 1 2 25 syl2anc ⊢φ→M∥MlcmN∧N∥MlcmN
27 26 simpld ⊢φ→M∥MlcmN
28 lcmcl ⊢M∈ℤ∧N∈ℤ→MlcmN∈ℕ0
29 1 2 28 syl2anc ⊢φ→MlcmN∈ℕ0
30 29 nn0zd ⊢φ→MlcmN∈ℤ
31 30 1 nzss ⊢φ→∥MlcmN⊆∥M↔M∥MlcmN
32 27 31 mpbird ⊢φ→∥MlcmN⊆∥M
33 26 simprd ⊢φ→N∥MlcmN
34 30 2 nzss ⊢φ→∥MlcmN⊆∥N↔N∥MlcmN
35 33 34 mpbird ⊢φ→∥MlcmN⊆∥N
36 32 35 ssind ⊢φ→∥MlcmN⊆∥M∩∥N
37 24 36 eqssd ⊢φ→∥M∩∥N=∥MlcmN