Metamath Proof Explorer


Theorem lcmass

Description: Associative law for lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmass NMPNlcmMlcmP=NlcmMlcmP

Proof

Step Hyp Ref Expression
1 orass N=0M=0P=0N=0M=0P=0
2 anass NxMxPxNxMxPx
3 2 rabbii x|NxMxPx=x|NxMxPx
4 3 infeq1i supx|NxMxPx<=supx|NxMxPx<
5 1 4 ifbieq2i ifN=0M=0P=00supx|NxMxPx<=ifN=0M=0P=00supx|NxMxPx<
6 lcmcl NMNlcmM0
7 6 3adant3 NMPNlcmM0
8 7 nn0zd NMPNlcmM
9 simp3 NMPP
10 lcmval NlcmMPNlcmMlcmP=ifNlcmM=0P=00supx|NlcmMxPx<
11 8 9 10 syl2anc NMPNlcmMlcmP=ifNlcmM=0P=00supx|NlcmMxPx<
12 lcmeq0 NMNlcmM=0N=0M=0
13 12 3adant3 NMPNlcmM=0N=0M=0
14 13 orbi1d NMPNlcmM=0P=0N=0M=0P=0
15 14 bicomd NMPN=0M=0P=0NlcmM=0P=0
16 nnz xx
17 16 adantl NMPxx
18 simp1 NMPN
19 18 adantr NMPxN
20 simpl2 NMPxM
21 lcmdvdsb xNMNxMxNlcmMx
22 17 19 20 21 syl3anc NMPxNxMxNlcmMx
23 22 anbi1d NMPxNxMxPxNlcmMxPx
24 23 rabbidva NMPx|NxMxPx=x|NlcmMxPx
25 24 infeq1d NMPsupx|NxMxPx<=supx|NlcmMxPx<
26 15 25 ifbieq2d NMPifN=0M=0P=00supx|NxMxPx<=ifNlcmM=0P=00supx|NlcmMxPx<
27 11 26 eqtr4d NMPNlcmMlcmP=ifN=0M=0P=00supx|NxMxPx<
28 lcmcl MPMlcmP0
29 28 3adant1 NMPMlcmP0
30 29 nn0zd NMPMlcmP
31 lcmval NMlcmPNlcmMlcmP=ifN=0MlcmP=00supx|NxMlcmPx<
32 18 30 31 syl2anc NMPNlcmMlcmP=ifN=0MlcmP=00supx|NxMlcmPx<
33 lcmeq0 MPMlcmP=0M=0P=0
34 33 3adant1 NMPMlcmP=0M=0P=0
35 34 orbi2d NMPN=0MlcmP=0N=0M=0P=0
36 35 bicomd NMPN=0M=0P=0N=0MlcmP=0
37 9 adantr NMPxP
38 lcmdvdsb xMPMxPxMlcmPx
39 17 20 37 38 syl3anc NMPxMxPxMlcmPx
40 39 anbi2d NMPxNxMxPxNxMlcmPx
41 40 rabbidva NMPx|NxMxPx=x|NxMlcmPx
42 41 infeq1d NMPsupx|NxMxPx<=supx|NxMlcmPx<
43 36 42 ifbieq2d NMPifN=0M=0P=00supx|NxMxPx<=ifN=0MlcmP=00supx|NxMlcmPx<
44 32 43 eqtr4d NMPNlcmMlcmP=ifN=0M=0P=00supx|NxMxPx<
45 5 27 44 3eqtr4a NMPNlcmMlcmP=NlcmMlcmP