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 )
7 6 3adant3 
 |-  ( ( 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 ) ) )
13 12 3adant3 
 |-  ( ( 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 )
28 27 3adant1 
 |-  ( ( 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 ) ) )
33 32 3adant1 
 |-  ( ( 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 ) ) )