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 
|- ( ph -> M e. ZZ )
nzin.n 
|- ( ph -> N e. ZZ )
Assertion nzin 
|- ( ph -> ( ( || " { M } ) i^i ( || " { N } ) ) = ( || " { ( M lcm N ) } ) )

Proof

Step Hyp Ref Expression
1 nzin.m 
 |-  ( ph -> M e. ZZ )
2 nzin.n 
 |-  ( ph -> N e. ZZ )
3 dvdszrcl 
 |-  ( M || n -> ( M e. ZZ /\ n e. ZZ ) )
4 dvdszrcl 
 |-  ( N || n -> ( N e. ZZ /\ n e. ZZ ) )
5 3 4 anim12i 
 |-  ( ( M || n /\ N || n ) -> ( ( M e. ZZ /\ n e. ZZ ) /\ ( N e. ZZ /\ n e. ZZ ) ) )
6 anandir 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ n e. ZZ ) <-> ( ( M e. ZZ /\ n e. ZZ ) /\ ( N e. ZZ /\ n e. ZZ ) ) )
7 5 6 sylibr 
 |-  ( ( M || n /\ N || n ) -> ( ( M e. ZZ /\ N e. ZZ ) /\ n e. ZZ ) )
8 7 ancomd 
 |-  ( ( M || n /\ N || n ) -> ( n e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) )
9 lcmdvds 
 |-  ( ( n e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || n /\ N || n ) -> ( M lcm N ) || n ) )
10 9 3expb 
 |-  ( ( n e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( M || n /\ N || n ) -> ( M lcm N ) || n ) )
11 8 10 mpcom 
 |-  ( ( M || n /\ N || n ) -> ( M lcm N ) || n )
12 elin 
 |-  ( n e. ( ( || " { M } ) i^i ( || " { N } ) ) <-> ( n e. ( || " { M } ) /\ n e. ( || " { N } ) ) )
13 reldvds 
 |-  Rel ||
14 elrelimasn 
 |-  ( Rel || -> ( n e. ( || " { M } ) <-> M || n ) )
15 13 14 ax-mp 
 |-  ( n e. ( || " { M } ) <-> M || n )
16 elrelimasn 
 |-  ( Rel || -> ( n e. ( || " { N } ) <-> N || n ) )
17 13 16 ax-mp 
 |-  ( n e. ( || " { N } ) <-> N || n )
18 15 17 anbi12i 
 |-  ( ( n e. ( || " { M } ) /\ n e. ( || " { N } ) ) <-> ( M || n /\ N || n ) )
19 12 18 bitri 
 |-  ( n e. ( ( || " { M } ) i^i ( || " { N } ) ) <-> ( M || n /\ N || n ) )
20 elrelimasn 
 |-  ( Rel || -> ( n e. ( || " { ( M lcm N ) } ) <-> ( M lcm N ) || n ) )
21 13 20 ax-mp 
 |-  ( n e. ( || " { ( M lcm N ) } ) <-> ( M lcm N ) || n )
22 11 19 21 3imtr4i 
 |-  ( n e. ( ( || " { M } ) i^i ( || " { N } ) ) -> n e. ( || " { ( M lcm N ) } ) )
23 22 ssriv 
 |-  ( ( || " { M } ) i^i ( || " { N } ) ) C_ ( || " { ( M lcm N ) } )
24 23 a1i 
 |-  ( ph -> ( ( || " { M } ) i^i ( || " { N } ) ) C_ ( || " { ( M lcm N ) } ) )
25 dvdslcm 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
26 1 2 25 syl2anc 
 |-  ( ph -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
27 26 simpld 
 |-  ( ph -> M || ( M lcm N ) )
28 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
29 1 2 28 syl2anc 
 |-  ( ph -> ( M lcm N ) e. NN0 )
30 29 nn0zd 
 |-  ( ph -> ( M lcm N ) e. ZZ )
31 30 1 nzss 
 |-  ( ph -> ( ( || " { ( M lcm N ) } ) C_ ( || " { M } ) <-> M || ( M lcm N ) ) )
32 27 31 mpbird 
 |-  ( ph -> ( || " { ( M lcm N ) } ) C_ ( || " { M } ) )
33 26 simprd 
 |-  ( ph -> N || ( M lcm N ) )
34 30 2 nzss 
 |-  ( ph -> ( ( || " { ( M lcm N ) } ) C_ ( || " { N } ) <-> N || ( M lcm N ) ) )
35 33 34 mpbird 
 |-  ( ph -> ( || " { ( M lcm N ) } ) C_ ( || " { N } ) )
36 32 35 ssind 
 |-  ( ph -> ( || " { ( M lcm N ) } ) C_ ( ( || " { M } ) i^i ( || " { N } ) ) )
37 24 36 eqssd 
 |-  ( ph -> ( ( || " { M } ) i^i ( || " { N } ) ) = ( || " { ( M lcm N ) } ) )