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 bitr4di 
 |-  ( ( 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 ) ) )