This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lcmcllem

Description: Lemma for lcmn0cl and dvdslcm . (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmcllem 
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } )

Proof

Step Hyp Ref Expression
1 lcmn0val 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
2 ssrab2 
 |-  { n e. NN | ( M || n /\ N || n ) } C_ NN
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 sseqtri 
 |-  { n e. NN | ( M || n /\ N || n ) } C_ ( ZZ>= ` 1 )
5 zmulcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
6 5 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M x. N ) e. ZZ )
7 zcn 
 |-  ( M e. ZZ -> M e. CC )
8 zcn 
 |-  ( N e. ZZ -> N e. CC )
9 7 8 anim12i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. CC /\ N e. CC ) )
10 ioran 
 |-  ( -. ( M = 0 \/ N = 0 ) <-> ( -. M = 0 /\ -. N = 0 ) )
11 df-ne 
 |-  ( M =/= 0 <-> -. M = 0 )
12 df-ne 
 |-  ( N =/= 0 <-> -. N = 0 )
13 11 12 anbi12i 
 |-  ( ( M =/= 0 /\ N =/= 0 ) <-> ( -. M = 0 /\ -. N = 0 ) )
14 10 13 sylbb2 
 |-  ( -. ( M = 0 \/ N = 0 ) -> ( M =/= 0 /\ N =/= 0 ) )
15 mulne0 
 |-  ( ( ( M e. CC /\ M =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) ) -> ( M x. N ) =/= 0 )
16 15 an4s 
 |-  ( ( ( M e. CC /\ N e. CC ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( M x. N ) =/= 0 )
17 9 14 16 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M x. N ) =/= 0 )
18 nnabscl 
 |-  ( ( ( M x. N ) e. ZZ /\ ( M x. N ) =/= 0 ) -> ( abs ` ( M x. N ) ) e. NN )
19 6 17 18 syl2anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( abs ` ( M x. N ) ) e. NN )
20 dvdsmul1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M x. N ) )
21 dvdsabsb 
 |-  ( ( M e. ZZ /\ ( M x. N ) e. ZZ ) -> ( M || ( M x. N ) <-> M || ( abs ` ( M x. N ) ) ) )
22 5 21 syldan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M x. N ) <-> M || ( abs ` ( M x. N ) ) ) )
23 20 22 mpbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M || ( abs ` ( M x. N ) ) )
24 dvdsmul2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )
25 dvdsabsb 
 |-  ( ( N e. ZZ /\ ( M x. N ) e. ZZ ) -> ( N || ( M x. N ) <-> N || ( abs ` ( M x. N ) ) ) )
26 5 25 sylan2 
 |-  ( ( N e. ZZ /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( N || ( M x. N ) <-> N || ( abs ` ( M x. N ) ) ) )
27 26 anabss7 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N || ( M x. N ) <-> N || ( abs ` ( M x. N ) ) ) )
28 24 27 mpbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N || ( abs ` ( M x. N ) ) )
29 23 28 jca 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( abs ` ( M x. N ) ) /\ N || ( abs ` ( M x. N ) ) ) )
30 29 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M || ( abs ` ( M x. N ) ) /\ N || ( abs ` ( M x. N ) ) ) )
31 breq2 
 |-  ( n = ( abs ` ( M x. N ) ) -> ( M || n <-> M || ( abs ` ( M x. N ) ) ) )
32 breq2 
 |-  ( n = ( abs ` ( M x. N ) ) -> ( N || n <-> N || ( abs ` ( M x. N ) ) ) )
33 31 32 anbi12d 
 |-  ( n = ( abs ` ( M x. N ) ) -> ( ( M || n /\ N || n ) <-> ( M || ( abs ` ( M x. N ) ) /\ N || ( abs ` ( M x. N ) ) ) ) )
34 33 rspcev 
 |-  ( ( ( abs ` ( M x. N ) ) e. NN /\ ( M || ( abs ` ( M x. N ) ) /\ N || ( abs ` ( M x. N ) ) ) ) -> E. n e. NN ( M || n /\ N || n ) )
35 19 30 34 syl2anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> E. n e. NN ( M || n /\ N || n ) )
36 rabn0 
 |-  ( { n e. NN | ( M || n /\ N || n ) } =/= (/) <-> E. n e. NN ( M || n /\ N || n ) )
37 35 36 sylibr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> { n e. NN | ( M || n /\ N || n ) } =/= (/) )
38 infssuzcl 
 |-  ( ( { n e. NN | ( M || n /\ N || n ) } C_ ( ZZ>= ` 1 ) /\ { n e. NN | ( M || n /\ N || n ) } =/= (/) ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) e. { n e. NN | ( M || n /\ N || n ) } )
39 4 37 38 sylancr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) e. { n e. NN | ( M || n /\ N || n ) } )
40 1 39 eqeltrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } )