This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgcddvds

Description: One half of rpmulgcd2 , which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion mulgcddvds 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
2 simp2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
3 simp3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
4 2 3 zmulcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
5 1 4 gcdcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) e. NN0 )
6 5 nn0zd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) e. ZZ )
7 dvds0 
 |-  ( ( K gcd ( M x. N ) ) e. ZZ -> ( K gcd ( M x. N ) ) || 0 )
8 6 7 syl 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || 0 )
9 8 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) = 0 ) -> ( K gcd ( M x. N ) ) || 0 )
10 oveq2 
 |-  ( ( K gcd N ) = 0 -> ( ( K gcd M ) x. ( K gcd N ) ) = ( ( K gcd M ) x. 0 ) )
11 1 2 gcdcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd M ) e. NN0 )
12 11 nn0cnd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd M ) e. CC )
13 12 mul01d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd M ) x. 0 ) = 0 )
14 10 13 sylan9eqr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) = 0 ) -> ( ( K gcd M ) x. ( K gcd N ) ) = 0 )
15 9 14 breqtrrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) = 0 ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )
16 6 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd ( M x. N ) ) e. ZZ )
17 16 zcnd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd ( M x. N ) ) e. CC )
18 1 3 gcdcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) e. NN0 )
19 18 nn0zd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) e. ZZ )
20 19 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd N ) e. ZZ )
21 20 zcnd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd N ) e. CC )
22 simpr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd N ) =/= 0 )
23 17 21 22 divcan1d 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) = ( K gcd ( M x. N ) ) )
24 gcddvds 
 |-  ( ( K e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( K gcd ( M x. N ) ) || K /\ ( K gcd ( M x. N ) ) || ( M x. N ) ) )
25 1 4 24 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd ( M x. N ) ) || K /\ ( K gcd ( M x. N ) ) || ( M x. N ) ) )
26 25 simpld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || K )
27 6 1 19 26 dvdsmultr1d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( K x. ( K gcd N ) ) )
28 27 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd ( M x. N ) ) || ( K x. ( K gcd N ) ) )
29 23 28 eqbrtrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( K x. ( K gcd N ) ) )
30 gcddvds 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( ( K gcd N ) || K /\ ( K gcd N ) || N ) )
31 1 3 30 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd N ) || K /\ ( K gcd N ) || N ) )
32 31 simpld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) || K )
33 31 simprd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) || N )
34 dvdsmultr2 
 |-  ( ( ( K gcd N ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd N ) || N -> ( K gcd N ) || ( M x. N ) ) )
35 19 2 3 34 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd N ) || N -> ( K gcd N ) || ( M x. N ) ) )
36 33 35 mpd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) || ( M x. N ) )
37 dvdsgcd 
 |-  ( ( ( K gcd N ) e. ZZ /\ K e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( ( K gcd N ) || K /\ ( K gcd N ) || ( M x. N ) ) -> ( K gcd N ) || ( K gcd ( M x. N ) ) ) )
38 19 1 4 37 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K gcd N ) || K /\ ( K gcd N ) || ( M x. N ) ) -> ( K gcd N ) || ( K gcd ( M x. N ) ) ) )
39 32 36 38 mp2and 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) || ( K gcd ( M x. N ) ) )
40 39 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd N ) || ( K gcd ( M x. N ) ) )
41 dvdsval2 
 |-  ( ( ( K gcd N ) e. ZZ /\ ( K gcd N ) =/= 0 /\ ( K gcd ( M x. N ) ) e. ZZ ) -> ( ( K gcd N ) || ( K gcd ( M x. N ) ) <-> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ ) )
42 20 22 16 41 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( K gcd N ) || ( K gcd ( M x. N ) ) <-> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ ) )
43 40 42 mpbid 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ )
44 1 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> K e. ZZ )
45 dvdsmulcr 
 |-  ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ /\ K e. ZZ /\ ( ( K gcd N ) e. ZZ /\ ( K gcd N ) =/= 0 ) ) -> ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( K x. ( K gcd N ) ) <-> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || K ) )
46 43 44 20 22 45 syl112anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( K x. ( K gcd N ) ) <-> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || K ) )
47 29 46 mpbid 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || K )
48 nn0abscl 
 |-  ( M e. ZZ -> ( abs ` M ) e. NN0 )
49 2 48 syl 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( abs ` M ) e. NN0 )
50 49 nn0zd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( abs ` M ) e. ZZ )
51 dvdsmultr2 
 |-  ( ( ( K gcd ( M x. N ) ) e. ZZ /\ ( abs ` M ) e. ZZ /\ K e. ZZ ) -> ( ( K gcd ( M x. N ) ) || K -> ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. K ) ) )
52 6 50 1 51 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd ( M x. N ) ) || K -> ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. K ) ) )
53 26 52 mpd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. K ) )
54 50 3 zmulcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) x. N ) e. ZZ )
55 25 simprd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( M x. N ) )
56 iddvds 
 |-  ( M e. ZZ -> M || M )
57 2 56 syl 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M || M )
58 dvdsabsb 
 |-  ( ( M e. ZZ /\ M e. ZZ ) -> ( M || M <-> M || ( abs ` M ) ) )
59 2 2 58 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M || M <-> M || ( abs ` M ) ) )
60 57 59 mpbid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M || ( abs ` M ) )
61 dvdsmulc 
 |-  ( ( M e. ZZ /\ ( abs ` M ) e. ZZ /\ N e. ZZ ) -> ( M || ( abs ` M ) -> ( M x. N ) || ( ( abs ` M ) x. N ) ) )
62 2 50 3 61 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M || ( abs ` M ) -> ( M x. N ) || ( ( abs ` M ) x. N ) ) )
63 60 62 mpd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M x. N ) || ( ( abs ` M ) x. N ) )
64 6 4 54 55 63 dvdstrd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. N ) )
65 50 1 zmulcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) x. K ) e. ZZ )
66 dvdsgcd 
 |-  ( ( ( K gcd ( M x. N ) ) e. ZZ /\ ( ( abs ` M ) x. K ) e. ZZ /\ ( ( abs ` M ) x. N ) e. ZZ ) -> ( ( ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. K ) /\ ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. N ) ) -> ( K gcd ( M x. N ) ) || ( ( ( abs ` M ) x. K ) gcd ( ( abs ` M ) x. N ) ) ) )
67 6 65 54 66 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. K ) /\ ( K gcd ( M x. N ) ) || ( ( abs ` M ) x. N ) ) -> ( K gcd ( M x. N ) ) || ( ( ( abs ` M ) x. K ) gcd ( ( abs ` M ) x. N ) ) ) )
68 53 64 67 mp2and 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( ( abs ` M ) x. K ) gcd ( ( abs ` M ) x. N ) ) )
69 18 nn0red 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) e. RR )
70 18 nn0ge0d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> 0 <_ ( K gcd N ) )
71 69 70 absidd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( abs ` ( K gcd N ) ) = ( K gcd N ) )
72 71 oveq2d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) x. ( abs ` ( K gcd N ) ) ) = ( ( abs ` M ) x. ( K gcd N ) ) )
73 2 zcnd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. CC )
74 18 nn0cnd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd N ) e. CC )
75 73 74 absmuld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( abs ` ( M x. ( K gcd N ) ) ) = ( ( abs ` M ) x. ( abs ` ( K gcd N ) ) ) )
76 mulgcd 
 |-  ( ( ( abs ` M ) e. NN0 /\ K e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) x. K ) gcd ( ( abs ` M ) x. N ) ) = ( ( abs ` M ) x. ( K gcd N ) ) )
77 49 1 3 76 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) x. K ) gcd ( ( abs ` M ) x. N ) ) = ( ( abs ` M ) x. ( K gcd N ) ) )
78 72 75 77 3eqtr4d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( abs ` ( M x. ( K gcd N ) ) ) = ( ( ( abs ` M ) x. K ) gcd ( ( abs ` M ) x. N ) ) )
79 68 78 breqtrrd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( abs ` ( M x. ( K gcd N ) ) ) )
80 2 19 zmulcld 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M x. ( K gcd N ) ) e. ZZ )
81 dvdsabsb 
 |-  ( ( ( K gcd ( M x. N ) ) e. ZZ /\ ( M x. ( K gcd N ) ) e. ZZ ) -> ( ( K gcd ( M x. N ) ) || ( M x. ( K gcd N ) ) <-> ( K gcd ( M x. N ) ) || ( abs ` ( M x. ( K gcd N ) ) ) ) )
82 6 80 81 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K gcd ( M x. N ) ) || ( M x. ( K gcd N ) ) <-> ( K gcd ( M x. N ) ) || ( abs ` ( M x. ( K gcd N ) ) ) ) )
83 79 82 mpbird 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( M x. ( K gcd N ) ) )
84 83 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd ( M x. N ) ) || ( M x. ( K gcd N ) ) )
85 23 84 eqbrtrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( M x. ( K gcd N ) ) )
86 2 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> M e. ZZ )
87 dvdsmulcr 
 |-  ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ /\ M e. ZZ /\ ( ( K gcd N ) e. ZZ /\ ( K gcd N ) =/= 0 ) ) -> ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( M x. ( K gcd N ) ) <-> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || M ) )
88 43 86 20 22 87 syl112anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( M x. ( K gcd N ) ) <-> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || M ) )
89 85 88 mpbid 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || M )
90 dvdsgcd 
 |-  ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ /\ K e. ZZ /\ M e. ZZ ) -> ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || K /\ ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || M ) -> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || ( K gcd M ) ) )
91 43 44 86 90 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || K /\ ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || M ) -> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || ( K gcd M ) ) )
92 47 89 91 mp2and 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || ( K gcd M ) )
93 11 nn0zd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd M ) e. ZZ )
94 93 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd M ) e. ZZ )
95 dvdsmulc 
 |-  ( ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) e. ZZ /\ ( K gcd M ) e. ZZ /\ ( K gcd N ) e. ZZ ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || ( K gcd M ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) ) )
96 43 94 20 95 syl3anc 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) || ( K gcd M ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) ) )
97 92 96 mpd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( ( ( K gcd ( M x. N ) ) / ( K gcd N ) ) x. ( K gcd N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )
98 23 97 eqbrtrrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K gcd N ) =/= 0 ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )
99 15 98 pm2.61dane 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K gcd ( M x. N ) ) || ( ( K gcd M ) x. ( K gcd N ) ) )