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 ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) gcd 𝑃 ) = ( 𝑁 gcd ( 𝑀 gcd 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 anass ⊢ ( ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) ∧ 𝑃 = 0 ) ↔ ( 𝑁 = 0 ∧ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) )
2 anass ⊢ ( ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) ↔ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) )
3 2 rabbii ⊢ { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) }
4 3 supeq1i ⊢ sup ( { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) = sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) } , ℝ , < )
5 1 4 ifbieq2i ⊢ if ( ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) ∧ 𝑃 = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) ) = if ( ( 𝑁 = 0 ∧ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) } , ℝ , < ) )
6 gcdcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) ∈ ℕ0 )
7 6 3adant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) ∈ ℕ0 )
8 7 nn0zd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) ∈ ℤ )
9 simp3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑃 ∈ ℤ )
10 gcdval ⊢ ( ( ( 𝑁 gcd 𝑀 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) gcd 𝑃 ) = if ( ( ( 𝑁 gcd 𝑀 ) = 0 ∧ 𝑃 = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) ) )
11 8 9 10 syl2anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) gcd 𝑃 ) = if ( ( ( 𝑁 gcd 𝑀 ) = 0 ∧ 𝑃 = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) ) )
12 gcdeq0 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) = 0 ↔ ( 𝑁 = 0 ∧ 𝑀 = 0 ) ) )
13 12 3adant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) = 0 ↔ ( 𝑁 = 0 ∧ 𝑀 = 0 ) ) )
14 13 anbi1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( 𝑁 gcd 𝑀 ) = 0 ∧ 𝑃 = 0 ) ↔ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) ∧ 𝑃 = 0 ) ) )
15 14 bicomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) ∧ 𝑃 = 0 ) ↔ ( ( 𝑁 gcd 𝑀 ) = 0 ∧ 𝑃 = 0 ) ) )
16 simpr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
17 simpl1 ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℤ )
18 simpl2 ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → 𝑀 ∈ ℤ )
19 dvdsgcdb ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ↔ 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ↔ 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ) )
21 20 anbi1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) ↔ ( 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) ) )
22 21 rabbidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } )
23 22 supeq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → sup ( { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) = sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) )
24 15 23 ifbieq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → if ( ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) ∧ 𝑃 = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) ) = if ( ( ( 𝑁 gcd 𝑀 ) = 0 ∧ 𝑃 = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ ( 𝑁 gcd 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) ) )
25 11 24 eqtr4d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) gcd 𝑃 ) = if ( ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) ∧ 𝑃 = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ 𝑀 ) ∧ 𝑥 ∥ 𝑃 ) } , ℝ , < ) ) )
26 simp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑁 ∈ ℤ )
27 gcdcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑀 gcd 𝑃 ) ∈ ℕ0 )
28 27 3adant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑀 gcd 𝑃 ) ∈ ℕ0 )
29 28 nn0zd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑀 gcd 𝑃 ) ∈ ℤ )
30 gcdval ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 gcd 𝑃 ) ∈ ℤ ) → ( 𝑁 gcd ( 𝑀 gcd 𝑃 ) ) = if ( ( 𝑁 = 0 ∧ ( 𝑀 gcd 𝑃 ) = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) } , ℝ , < ) ) )
31 26 29 30 syl2anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 gcd ( 𝑀 gcd 𝑃 ) ) = if ( ( 𝑁 = 0 ∧ ( 𝑀 gcd 𝑃 ) = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) } , ℝ , < ) ) )
32 gcdeq0 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑀 gcd 𝑃 ) = 0 ↔ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) )
33 32 3adant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑀 gcd 𝑃 ) = 0 ↔ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) )
34 33 anbi2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 = 0 ∧ ( 𝑀 gcd 𝑃 ) = 0 ) ↔ ( 𝑁 = 0 ∧ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) ) )
35 34 bicomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 = 0 ∧ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) ↔ ( 𝑁 = 0 ∧ ( 𝑀 gcd 𝑃 ) = 0 ) ) )
36 simpl3 ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℤ )
37 dvdsgcdb ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ↔ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) )
38 16 18 36 37 syl3anc ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ↔ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) )
39 38 anbi2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) ↔ ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) ) )
40 39 rabbidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) } = { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) } )
41 40 supeq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) } , ℝ , < ) = sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) } , ℝ , < ) )
42 35 41 ifbieq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → if ( ( 𝑁 = 0 ∧ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) } , ℝ , < ) ) = if ( ( 𝑁 = 0 ∧ ( 𝑀 gcd 𝑃 ) = 0 ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ 𝑥 ∥ ( 𝑀 gcd 𝑃 ) ) } , ℝ , < ) ) )
43 31 42 eqtr4d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 gcd ( 𝑀 gcd 𝑃 ) ) = if ( ( 𝑁 = 0 ∧ ( 𝑀 = 0 ∧ 𝑃 = 0 ) ) , 0 , sup ( { 𝑥 ∈ ℤ ∣ ( 𝑥 ∥ 𝑁 ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑃 ) ) } , ℝ , < ) ) )
44 5 25 43 3eqtr4a ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 gcd 𝑀 ) gcd 𝑃 ) = ( 𝑁 gcd ( 𝑀 gcd 𝑃 ) ) )