Metamath Proof Explorer

Theorem gcddiv

Description: Division law for the gcd operator. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion gcddiv ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ ∧ C ∥ A ∧ C ∥ B → A gcd B C = A C gcd B C

Proof

Step Hyp Ref Expression
1 nnz ⊢ C ∈ ℕ → C ∈ ℤ
2 1 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → C ∈ ℤ
3 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → A ∈ ℤ
4 divides ⊢ C ∈ ℤ ∧ A ∈ ℤ → C ∥ A ↔ ∃ a ∈ ℤ a ⁢ C = A
5 2 3 4 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → C ∥ A ↔ ∃ a ∈ ℤ a ⁢ C = A
6 simp2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → B ∈ ℤ
7 divides ⊢ C ∈ ℤ ∧ B ∈ ℤ → C ∥ B ↔ ∃ b ∈ ℤ b ⁢ C = B
8 2 6 7 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → C ∥ B ↔ ∃ b ∈ ℤ b ⁢ C = B
9 5 8 anbi12d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → C ∥ A ∧ C ∥ B ↔ ∃ a ∈ ℤ a ⁢ C = A ∧ ∃ b ∈ ℤ b ⁢ C = B
10 reeanv ⊢ ∃ a ∈ ℤ ∃ b ∈ ℤ a ⁢ C = A ∧ b ⁢ C = B ↔ ∃ a ∈ ℤ a ⁢ C = A ∧ ∃ b ∈ ℤ b ⁢ C = B
11 9 10 bitr4di ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → C ∥ A ∧ C ∥ B ↔ ∃ a ∈ ℤ ∃ b ∈ ℤ a ⁢ C = A ∧ b ⁢ C = B
12 gcdcl ⊢ a ∈ ℤ ∧ b ∈ ℤ → a gcd b ∈ ℕ 0
13 12 nn0cnd ⊢ a ∈ ℤ ∧ b ∈ ℤ → a gcd b ∈ ℂ
14 13 3adant3 ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a gcd b ∈ ℂ
15 nncn ⊢ C ∈ ℕ → C ∈ ℂ
16 15 3ad2ant3 ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → C ∈ ℂ
17 nnne0 ⊢ C ∈ ℕ → C ≠ 0
18 17 3ad2ant3 ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → C ≠ 0
19 14 16 18 divcan4d ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a gcd b ⁢ C C = a gcd b
20 nnnn0 ⊢ C ∈ ℕ → C ∈ ℕ 0
21 mulgcdr ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ 0 → a ⁢ C gcd b ⁢ C = a gcd b ⁢ C
22 20 21 syl3an3 ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C gcd b ⁢ C = a gcd b ⁢ C
23 22 oveq1d ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C gcd b ⁢ C C = a gcd b ⁢ C C
24 zcn ⊢ a ∈ ℤ → a ∈ ℂ
25 24 3ad2ant1 ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ∈ ℂ
26 25 16 18 divcan4d ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C C = a
27 zcn ⊢ b ∈ ℤ → b ∈ ℂ
28 27 3ad2ant2 ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → b ∈ ℂ
29 28 16 18 divcan4d ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → b ⁢ C C = b
30 26 29 oveq12d ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C C gcd b ⁢ C C = a gcd b
31 19 23 30 3eqtr4d ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C gcd b ⁢ C C = a ⁢ C C gcd b ⁢ C C
32 oveq12 ⊢ a ⁢ C = A ∧ b ⁢ C = B → a ⁢ C gcd b ⁢ C = A gcd B
33 32 oveq1d ⊢ a ⁢ C = A ∧ b ⁢ C = B → a ⁢ C gcd b ⁢ C C = A gcd B C
34 oveq1 ⊢ a ⁢ C = A → a ⁢ C C = A C
35 oveq1 ⊢ b ⁢ C = B → b ⁢ C C = B C
36 34 35 oveqan12d ⊢ a ⁢ C = A ∧ b ⁢ C = B → a ⁢ C C gcd b ⁢ C C = A C gcd B C
37 33 36 eqeq12d ⊢ a ⁢ C = A ∧ b ⁢ C = B → a ⁢ C gcd b ⁢ C C = a ⁢ C C gcd b ⁢ C C ↔ A gcd B C = A C gcd B C
38 31 37 syl5ibcom ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C = A ∧ b ⁢ C = B → A gcd B C = A C gcd B C
39 38 3expa ⊢ a ∈ ℤ ∧ b ∈ ℤ ∧ C ∈ ℕ → a ⁢ C = A ∧ b ⁢ C = B → A gcd B C = A C gcd B C
40 39 expcom ⊢ C ∈ ℕ → a ∈ ℤ ∧ b ∈ ℤ → a ⁢ C = A ∧ b ⁢ C = B → A gcd B C = A C gcd B C
41 40 rexlimdvv ⊢ C ∈ ℕ → ∃ a ∈ ℤ ∃ b ∈ ℤ a ⁢ C = A ∧ b ⁢ C = B → A gcd B C = A C gcd B C
42 41 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → ∃ a ∈ ℤ ∃ b ∈ ℤ a ⁢ C = A ∧ b ⁢ C = B → A gcd B C = A C gcd B C
43 11 42 sylbid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ → C ∥ A ∧ C ∥ B → A gcd B C = A C gcd B C
44 43 imp ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ ∧ C ∥ A ∧ C ∥ B → A gcd B C = A C gcd B C