# 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 e. ZZ /\ B e. ZZ /\ C e. NN ) /\ ( C || A /\ C || B ) ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) )`

### Proof

Step Hyp Ref Expression
1 nnz
` |-  ( C e. NN -> C e. ZZ )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> C e. ZZ )`
3 simp1
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> A e. ZZ )`
4 divides
` |-  ( ( C e. ZZ /\ A e. ZZ ) -> ( C || A <-> E. a e. ZZ ( a x. C ) = A ) )`
5 2 3 4 syl2anc
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C || A <-> E. a e. ZZ ( a x. C ) = A ) )`
6 simp2
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> B e. ZZ )`
7 divides
` |-  ( ( C e. ZZ /\ B e. ZZ ) -> ( C || B <-> E. b e. ZZ ( b x. C ) = B ) )`
8 2 6 7 syl2anc
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( C || B <-> E. b e. ZZ ( b x. C ) = B ) )`
9 5 8 anbi12d
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( ( C || A /\ C || B ) <-> ( E. a e. ZZ ( a x. C ) = A /\ E. b e. ZZ ( b x. C ) = B ) ) )`
10 reeanv
` |-  ( E. a e. ZZ E. b e. ZZ ( ( a x. C ) = A /\ ( b x. C ) = B ) <-> ( E. a e. ZZ ( a x. C ) = A /\ E. b e. ZZ ( b x. C ) = B ) )`
11 9 10 syl6bbr
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( ( C || A /\ C || B ) <-> E. a e. ZZ E. b e. ZZ ( ( a x. C ) = A /\ ( b x. C ) = B ) ) )`
12 gcdcl
` |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a gcd b ) e. NN0 )`
13 12 nn0cnd
` |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a gcd b ) e. CC )`
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( a gcd b ) e. CC )`
15 nncn
` |-  ( C e. NN -> C e. CC )`
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> C e. CC )`
17 nnne0
` |-  ( C e. NN -> C =/= 0 )`
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> C =/= 0 )`
19 14 16 18 divcan4d
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( ( a gcd b ) x. C ) / C ) = ( a gcd b ) )`
20 nnnn0
` |-  ( C e. NN -> C e. NN0 )`
21 mulgcdr
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN0 ) -> ( ( a x. C ) gcd ( b x. C ) ) = ( ( a gcd b ) x. C ) )`
22 20 21 syl3an3
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( a x. C ) gcd ( b x. C ) ) = ( ( a gcd b ) x. C ) )`
23 22 oveq1d
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( ( a x. C ) gcd ( b x. C ) ) / C ) = ( ( ( a gcd b ) x. C ) / C ) )`
24 zcn
` |-  ( a e. ZZ -> a e. CC )`
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> a e. CC )`
26 25 16 18 divcan4d
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( a x. C ) / C ) = a )`
27 zcn
` |-  ( b e. ZZ -> b e. CC )`
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> b e. CC )`
29 28 16 18 divcan4d
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( b x. C ) / C ) = b )`
30 26 29 oveq12d
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( ( a x. C ) / C ) gcd ( ( b x. C ) / C ) ) = ( a gcd b ) )`
31 19 23 30 3eqtr4d
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( ( a x. C ) gcd ( b x. C ) ) / C ) = ( ( ( a x. C ) / C ) gcd ( ( b x. C ) / C ) ) )`
32 oveq12
` |-  ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( a x. C ) gcd ( b x. C ) ) = ( A gcd B ) )`
33 32 oveq1d
` |-  ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( ( a x. C ) gcd ( b x. C ) ) / C ) = ( ( A gcd B ) / C ) )`
34 oveq1
` |-  ( ( a x. C ) = A -> ( ( a x. C ) / C ) = ( A / C ) )`
35 oveq1
` |-  ( ( b x. C ) = B -> ( ( b x. C ) / C ) = ( B / C ) )`
36 34 35 oveqan12d
` |-  ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( ( a x. C ) / C ) gcd ( ( b x. C ) / C ) ) = ( ( A / C ) gcd ( B / C ) ) )`
37 33 36 eqeq12d
` |-  ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( ( ( a x. C ) gcd ( b x. C ) ) / C ) = ( ( ( a x. C ) / C ) gcd ( ( b x. C ) / C ) ) <-> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )`
38 31 37 syl5ibcom
` |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )`
39 38 3expa
` |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ C e. NN ) -> ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )`
40 39 expcom
` |-  ( C e. NN -> ( ( a e. ZZ /\ b e. ZZ ) -> ( ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) ) )`
41 40 rexlimdvv
` |-  ( C e. NN -> ( E. a e. ZZ E. b e. ZZ ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( E. a e. ZZ E. b e. ZZ ( ( a x. C ) = A /\ ( b x. C ) = B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )`
` |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( ( C || A /\ C || B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )`
` |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ ( C || A /\ C || B ) ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) )`