Description: Associative law for lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | lcmass | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orass | |
|
2 | anass | |
|
3 | 2 | rabbii | |
4 | 3 | infeq1i | |
5 | 1 4 | ifbieq2i | |
6 | lcmcl | |
|
7 | 6 | 3adant3 | |
8 | 7 | nn0zd | |
9 | simp3 | |
|
10 | lcmval | |
|
11 | 8 9 10 | syl2anc | |
12 | lcmeq0 | |
|
13 | 12 | 3adant3 | |
14 | 13 | orbi1d | |
15 | 14 | bicomd | |
16 | nnz | |
|
17 | 16 | adantl | |
18 | simp1 | |
|
19 | 18 | adantr | |
20 | simpl2 | |
|
21 | lcmdvdsb | |
|
22 | 17 19 20 21 | syl3anc | |
23 | 22 | anbi1d | |
24 | 23 | rabbidva | |
25 | 24 | infeq1d | |
26 | 15 25 | ifbieq2d | |
27 | 11 26 | eqtr4d | |
28 | lcmcl | |
|
29 | 28 | 3adant1 | |
30 | 29 | nn0zd | |
31 | lcmval | |
|
32 | 18 30 31 | syl2anc | |
33 | lcmeq0 | |
|
34 | 33 | 3adant1 | |
35 | 34 | orbi2d | |
36 | 35 | bicomd | |
37 | 9 | adantr | |
38 | lcmdvdsb | |
|
39 | 17 20 37 38 | syl3anc | |
40 | 39 | anbi2d | |
41 | 40 | rabbidva | |
42 | 41 | infeq1d | |
43 | 36 42 | ifbieq2d | |
44 | 32 43 | eqtr4d | |
45 | 5 27 44 | 3eqtr4a | |