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 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