# Metamath Proof Explorer

## Theorem gcdass

Description: Associative law for gcd operator. Theorem 1.4(b) in ApostolNT p. 16. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion gcdass
`|- ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) gcd P ) = ( N gcd ( M gcd P ) ) )`

### Proof

Step Hyp Ref Expression
1 anass
` |-  ( ( ( N = 0 /\ M = 0 ) /\ P = 0 ) <-> ( N = 0 /\ ( M = 0 /\ P = 0 ) ) )`
2 anass
` |-  ( ( ( x || N /\ x || M ) /\ x || P ) <-> ( x || N /\ ( x || M /\ x || P ) ) )`
3 2 rabbii
` |-  { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } = { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) }`
4 3 supeq1i
` |-  sup ( { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } , RR , < ) = sup ( { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) } , RR , < )`
5 1 4 ifbieq2i
` |-  if ( ( ( N = 0 /\ M = 0 ) /\ P = 0 ) , 0 , sup ( { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } , RR , < ) ) = if ( ( N = 0 /\ ( M = 0 /\ P = 0 ) ) , 0 , sup ( { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) } , RR , < ) )`
6 gcdcl
` |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N gcd M ) e. NN0 )`
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N gcd M ) e. NN0 )`
8 7 nn0zd
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N gcd M ) e. ZZ )`
9 simp3
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> P e. ZZ )`
10 gcdval
` |-  ( ( ( N gcd M ) e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) gcd P ) = if ( ( ( N gcd M ) = 0 /\ P = 0 ) , 0 , sup ( { x e. ZZ | ( x || ( N gcd M ) /\ x || P ) } , RR , < ) ) )`
11 8 9 10 syl2anc
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) gcd P ) = if ( ( ( N gcd M ) = 0 /\ P = 0 ) , 0 , sup ( { x e. ZZ | ( x || ( N gcd M ) /\ x || P ) } , RR , < ) ) )`
12 gcdeq0
` |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N gcd M ) = 0 <-> ( N = 0 /\ M = 0 ) ) )`
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) = 0 <-> ( N = 0 /\ M = 0 ) ) )`
14 13 anbi1d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( ( N gcd M ) = 0 /\ P = 0 ) <-> ( ( N = 0 /\ M = 0 ) /\ P = 0 ) ) )`
15 14 bicomd
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( ( N = 0 /\ M = 0 ) /\ P = 0 ) <-> ( ( N gcd M ) = 0 /\ P = 0 ) ) )`
16 simpr
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> x e. ZZ )`
17 simpl1
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> N e. ZZ )`
18 simpl2
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> M e. ZZ )`
19 dvdsgcdb
` |-  ( ( x e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( ( x || N /\ x || M ) <-> x || ( N gcd M ) ) )`
20 16 17 18 19 syl3anc
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> ( ( x || N /\ x || M ) <-> x || ( N gcd M ) ) )`
21 20 anbi1d
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> ( ( ( x || N /\ x || M ) /\ x || P ) <-> ( x || ( N gcd M ) /\ x || P ) ) )`
22 21 rabbidva
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } = { x e. ZZ | ( x || ( N gcd M ) /\ x || P ) } )`
23 22 supeq1d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> sup ( { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } , RR , < ) = sup ( { x e. ZZ | ( x || ( N gcd M ) /\ x || P ) } , RR , < ) )`
24 15 23 ifbieq2d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> if ( ( ( N = 0 /\ M = 0 ) /\ P = 0 ) , 0 , sup ( { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } , RR , < ) ) = if ( ( ( N gcd M ) = 0 /\ P = 0 ) , 0 , sup ( { x e. ZZ | ( x || ( N gcd M ) /\ x || P ) } , RR , < ) ) )`
25 11 24 eqtr4d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) gcd P ) = if ( ( ( N = 0 /\ M = 0 ) /\ P = 0 ) , 0 , sup ( { x e. ZZ | ( ( x || N /\ x || M ) /\ x || P ) } , RR , < ) ) )`
26 simp1
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> N e. ZZ )`
27 gcdcl
` |-  ( ( M e. ZZ /\ P e. ZZ ) -> ( M gcd P ) e. NN0 )`
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( M gcd P ) e. NN0 )`
29 28 nn0zd
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( M gcd P ) e. ZZ )`
30 gcdval
` |-  ( ( N e. ZZ /\ ( M gcd P ) e. ZZ ) -> ( N gcd ( M gcd P ) ) = if ( ( N = 0 /\ ( M gcd P ) = 0 ) , 0 , sup ( { x e. ZZ | ( x || N /\ x || ( M gcd P ) ) } , RR , < ) ) )`
31 26 29 30 syl2anc
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N gcd ( M gcd P ) ) = if ( ( N = 0 /\ ( M gcd P ) = 0 ) , 0 , sup ( { x e. ZZ | ( x || N /\ x || ( M gcd P ) ) } , RR , < ) ) )`
32 gcdeq0
` |-  ( ( M e. ZZ /\ P e. ZZ ) -> ( ( M gcd P ) = 0 <-> ( M = 0 /\ P = 0 ) ) )`
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( M gcd P ) = 0 <-> ( M = 0 /\ P = 0 ) ) )`
34 33 anbi2d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N = 0 /\ ( M gcd P ) = 0 ) <-> ( N = 0 /\ ( M = 0 /\ P = 0 ) ) ) )`
35 34 bicomd
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N = 0 /\ ( M = 0 /\ P = 0 ) ) <-> ( N = 0 /\ ( M gcd P ) = 0 ) ) )`
36 simpl3
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> P e. ZZ )`
37 dvdsgcdb
` |-  ( ( x e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( x || M /\ x || P ) <-> x || ( M gcd P ) ) )`
38 16 18 36 37 syl3anc
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> ( ( x || M /\ x || P ) <-> x || ( M gcd P ) ) )`
39 38 anbi2d
` |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. ZZ ) -> ( ( x || N /\ ( x || M /\ x || P ) ) <-> ( x || N /\ x || ( M gcd P ) ) ) )`
40 39 rabbidva
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) } = { x e. ZZ | ( x || N /\ x || ( M gcd P ) ) } )`
41 40 supeq1d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> sup ( { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) } , RR , < ) = sup ( { x e. ZZ | ( x || N /\ x || ( M gcd P ) ) } , RR , < ) )`
42 35 41 ifbieq2d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> if ( ( N = 0 /\ ( M = 0 /\ P = 0 ) ) , 0 , sup ( { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) } , RR , < ) ) = if ( ( N = 0 /\ ( M gcd P ) = 0 ) , 0 , sup ( { x e. ZZ | ( x || N /\ x || ( M gcd P ) ) } , RR , < ) ) )`
43 31 42 eqtr4d
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N gcd ( M gcd P ) ) = if ( ( N = 0 /\ ( M = 0 /\ P = 0 ) ) , 0 , sup ( { x e. ZZ | ( x || N /\ ( x || M /\ x || P ) ) } , RR , < ) ) )`
44 5 25 43 3eqtr4a
` |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) gcd P ) = ( N gcd ( M gcd P ) ) )`