Metamath Proof Explorer

Theorem gcddiv

Description: Division law for GCD. (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→AgcdBC=ACgcdBC

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∈ℤ→agcdb∈ℕ0
13 12 nn0cnd ⊢a∈ℤ∧b∈ℤ→agcdb∈ℂ
14 13 3adant3 ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→agcdb∈ℂ
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∈ℕ→agcdb⁢CC=agcdb
20 nnnn0 ⊢C∈ℕ→C∈ℕ0
21 mulgcdr ⊢a∈ℤ∧b∈ℤ∧C∈ℕ0→a⁢Cgcdb⁢C=agcdb⁢C
22 20 21 syl3an3 ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢Cgcdb⁢C=agcdb⁢C
23 22 oveq1d ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢Cgcdb⁢CC=agcdb⁢CC
24 zcn ⊢a∈ℤ→a∈ℂ
25 24 3ad2ant1 ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a∈ℂ
26 25 16 18 divcan4d ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢CC=a
27 zcn ⊢b∈ℤ→b∈ℂ
28 27 3ad2ant2 ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→b∈ℂ
29 28 16 18 divcan4d ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→b⁢CC=b
30 26 29 oveq12d ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢CCgcdb⁢CC=agcdb
31 19 23 30 3eqtr4d ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢Cgcdb⁢CC=a⁢CCgcdb⁢CC
32 oveq12 ⊢a⁢C=A∧b⁢C=B→a⁢Cgcdb⁢C=AgcdB
33 32 oveq1d ⊢a⁢C=A∧b⁢C=B→a⁢Cgcdb⁢CC=AgcdBC
34 oveq1 ⊢a⁢C=A→a⁢CC=AC
35 oveq1 ⊢b⁢C=B→b⁢CC=BC
36 34 35 oveqan12d ⊢a⁢C=A∧b⁢C=B→a⁢CCgcdb⁢CC=ACgcdBC
37 33 36 eqeq12d ⊢a⁢C=A∧b⁢C=B→a⁢Cgcdb⁢CC=a⁢CCgcdb⁢CC↔AgcdBC=ACgcdBC
38 31 37 syl5ibcom ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢C=A∧b⁢C=B→AgcdBC=ACgcdBC
39 38 3expa ⊢a∈ℤ∧b∈ℤ∧C∈ℕ→a⁢C=A∧b⁢C=B→AgcdBC=ACgcdBC
40 39 expcom ⊢C∈ℕ→a∈ℤ∧b∈ℤ→a⁢C=A∧b⁢C=B→AgcdBC=ACgcdBC
41 40 rexlimdvv ⊢C∈ℕ→∃a∈ℤ∃b∈ℤa⁢C=A∧b⁢C=B→AgcdBC=ACgcdBC
42 41 3ad2ant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℕ→∃a∈ℤ∃b∈ℤa⁢C=A∧b⁢C=B→AgcdBC=ACgcdBC
43 11 42 sylbid ⊢A∈ℤ∧B∈ℤ∧C∈ℕ→C∥A∧C∥B→AgcdBC=ACgcdBC
44 43 imp ⊢A∈ℤ∧B∈ℤ∧C∈ℕ∧C∥A∧C∥B→AgcdBC=ACgcdBC