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 )
2 1 3ad2ant3
 |-  ( ( 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 )
14 13 3adant3
 |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> ( a gcd b ) e. CC )
15 nncn
 |-  ( C e. NN -> C e. CC )
16 15 3ad2ant3
 |-  ( ( a e. ZZ /\ b e. ZZ /\ C e. NN ) -> C e. CC )
17 nnne0
 |-  ( C e. NN -> C =/= 0 )
18 17 3ad2ant3
 |-  ( ( 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 )
25 24 3ad2ant1
 |-  ( ( 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 )
28 27 3ad2ant2
 |-  ( ( 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 ) ) ) )
42 41 3ad2ant3
 |-  ( ( 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 ) ) ) )
43 11 42 sylbid
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) -> ( ( C || A /\ C || B ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) ) )
44 43 imp
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ ( C || A /\ C || B ) ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) )