Metamath Proof Explorer

Theorem divgcdcoprmex

Description: Integers divided by gcd are coprime (see ProofWiki "Integers Divided by GCD are Coprime", 11-Jul-2021, https://proofwiki.org/wiki/Integers_Divided_by_GCD_are_Coprime ): Any pair of integers, not both zero, can be reduced to a pair of coprime ones by dividing them by their gcd. (Contributed by AV, 12-Jul-2021)

Ref Expression
Assertion divgcdcoprmex 
|- ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> E. a e. ZZ E. b e. ZZ ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( B e. ZZ /\ B =/= 0 ) -> B e. ZZ )
2 1 anim2i 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( A e. ZZ /\ B e. ZZ ) )
3 zeqzmulgcd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> E. a e. ZZ A = ( a x. ( A gcd B ) ) )
4 2 3 syl 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> E. a e. ZZ A = ( a x. ( A gcd B ) ) )
5 4 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> E. a e. ZZ A = ( a x. ( A gcd B ) ) )
6 zeqzmulgcd 
 |-  ( ( B e. ZZ /\ A e. ZZ ) -> E. b e. ZZ B = ( b x. ( B gcd A ) ) )
7 6 adantlr 
 |-  ( ( ( B e. ZZ /\ B =/= 0 ) /\ A e. ZZ ) -> E. b e. ZZ B = ( b x. ( B gcd A ) ) )
8 7 ancoms 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> E. b e. ZZ B = ( b x. ( B gcd A ) ) )
9 8 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> E. b e. ZZ B = ( b x. ( B gcd A ) ) )
10 reeanv 
 |-  ( E. a e. ZZ E. b e. ZZ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) <-> ( E. a e. ZZ A = ( a x. ( A gcd B ) ) /\ E. b e. ZZ B = ( b x. ( B gcd A ) ) ) )
11 zcn 
 |-  ( a e. ZZ -> a e. CC )
12 11 adantl 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) -> a e. CC )
13 gcdcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
14 2 13 syl 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( A gcd B ) e. NN0 )
15 14 nn0cnd 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( A gcd B ) e. CC )
16 15 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) e. CC )
17 16 adantr 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) -> ( A gcd B ) e. CC )
18 12 17 mulcomd 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) -> ( a x. ( A gcd B ) ) = ( ( A gcd B ) x. a ) )
19 simp3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> M = ( A gcd B ) )
20 19 eqcomd 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) = M )
21 20 oveq1d 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( ( A gcd B ) x. a ) = ( M x. a ) )
22 21 adantr 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) -> ( ( A gcd B ) x. a ) = ( M x. a ) )
23 18 22 eqtrd 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) -> ( a x. ( A gcd B ) ) = ( M x. a ) )
24 23 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) /\ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) ) -> ( a x. ( A gcd B ) ) = ( M x. a ) )
25 eqeq1 
 |-  ( A = ( a x. ( A gcd B ) ) -> ( A = ( M x. a ) <-> ( a x. ( A gcd B ) ) = ( M x. a ) ) )
26 25 adantr 
 |-  ( ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) -> ( A = ( M x. a ) <-> ( a x. ( A gcd B ) ) = ( M x. a ) ) )
27 26 adantl 
 |-  ( ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) /\ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) ) -> ( A = ( M x. a ) <-> ( a x. ( A gcd B ) ) = ( M x. a ) ) )
28 24 27 mpbird 
 |-  ( ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) /\ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) ) -> A = ( M x. a ) )
29 simpr 
 |-  ( ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) -> B = ( b x. ( B gcd A ) ) )
30 2 ancomd 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( B e. ZZ /\ A e. ZZ ) )
31 gcdcom 
 |-  ( ( B e. ZZ /\ A e. ZZ ) -> ( B gcd A ) = ( A gcd B ) )
32 30 31 syl 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( B gcd A ) = ( A gcd B ) )
33 32 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( B gcd A ) = ( A gcd B ) )
34 33 oveq2d 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( b x. ( B gcd A ) ) = ( b x. ( A gcd B ) ) )
35 34 adantr 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( b x. ( B gcd A ) ) = ( b x. ( A gcd B ) ) )
36 zcn 
 |-  ( b e. ZZ -> b e. CC )
37 36 adantl 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> b e. CC )
38 14 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) e. NN0 )
39 38 adantr 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( A gcd B ) e. NN0 )
40 39 nn0cnd 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( A gcd B ) e. CC )
41 37 40 mulcomd 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( b x. ( A gcd B ) ) = ( ( A gcd B ) x. b ) )
42 20 adantr 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( A gcd B ) = M )
43 42 oveq1d 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( ( A gcd B ) x. b ) = ( M x. b ) )
44 35 41 43 3eqtrd 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ b e. ZZ ) -> ( b x. ( B gcd A ) ) = ( M x. b ) )
45 44 adantlr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( b x. ( B gcd A ) ) = ( M x. b ) )
46 29 45 sylan9eqr 
 |-  ( ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) /\ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) ) -> B = ( M x. b ) )
47 zcn 
 |-  ( A e. ZZ -> A e. CC )
48 47 3ad2ant1 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> A e. CC )
49 48 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> A e. CC )
50 12 adantr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> a e. CC )
51 simp1 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> A e. ZZ )
52 1 3ad2ant2 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> B e. ZZ )
53 51 52 gcdcld 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) e. NN0 )
54 53 nn0cnd 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) e. CC )
55 54 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( A gcd B ) e. CC )
56 gcdeq0 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
57 simpr 
 |-  ( ( A = 0 /\ B = 0 ) -> B = 0 )
58 56 57 biimtrdi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) = 0 -> B = 0 ) )
59 58 necon3d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( B =/= 0 -> ( A gcd B ) =/= 0 ) )
60 59 impr 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( A gcd B ) =/= 0 )
61 60 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) =/= 0 )
62 61 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( A gcd B ) =/= 0 )
63 49 50 55 62 divmul3d 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( A / ( A gcd B ) ) = a <-> A = ( a x. ( A gcd B ) ) ) )
64 63 bicomd 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( A = ( a x. ( A gcd B ) ) <-> ( A / ( A gcd B ) ) = a ) )
65 zcn 
 |-  ( B e. ZZ -> B e. CC )
66 65 adantr 
 |-  ( ( B e. ZZ /\ B =/= 0 ) -> B e. CC )
67 66 3ad2ant2 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> B e. CC )
68 67 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> B e. CC )
69 36 adantl 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> b e. CC )
70 68 69 55 62 divmul3d 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( B / ( A gcd B ) ) = b <-> B = ( b x. ( A gcd B ) ) ) )
71 2 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A e. ZZ /\ B e. ZZ ) )
72 gcdcom 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
73 71 72 syl 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A gcd B ) = ( B gcd A ) )
74 73 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
75 74 oveq2d 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( b x. ( A gcd B ) ) = ( b x. ( B gcd A ) ) )
76 75 eqeq2d 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( B = ( b x. ( A gcd B ) ) <-> B = ( b x. ( B gcd A ) ) ) )
77 70 76 bitr2d 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( B = ( b x. ( B gcd A ) ) <-> ( B / ( A gcd B ) ) = b ) )
78 64 77 anbi12d 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) <-> ( ( A / ( A gcd B ) ) = a /\ ( B / ( A gcd B ) ) = b ) ) )
79 3anass 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) <-> ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) )
80 79 biimpri 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) )
81 80 3adant3 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) )
82 divgcdcoprm0 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
83 81 82 syl 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
84 oveq12 
 |-  ( ( ( A / ( A gcd B ) ) = a /\ ( B / ( A gcd B ) ) = b ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = ( a gcd b ) )
85 84 eqeq1d 
 |-  ( ( ( A / ( A gcd B ) ) = a /\ ( B / ( A gcd B ) ) = b ) -> ( ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 <-> ( a gcd b ) = 1 ) )
86 83 85 syl5ibcom 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( ( ( A / ( A gcd B ) ) = a /\ ( B / ( A gcd B ) ) = b ) -> ( a gcd b ) = 1 ) )
87 86 ad2antrr 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( ( A / ( A gcd B ) ) = a /\ ( B / ( A gcd B ) ) = b ) -> ( a gcd b ) = 1 ) )
88 78 87 sylbid 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) -> ( a gcd b ) = 1 ) )
89 88 imp 
 |-  ( ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) /\ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) ) -> ( a gcd b ) = 1 )
90 28 46 89 3jca 
 |-  ( ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) /\ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) ) -> ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) )
91 90 ex 
 |-  ( ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) /\ b e. ZZ ) -> ( ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) -> ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) ) )
92 91 reximdva 
 |-  ( ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) /\ a e. ZZ ) -> ( E. b e. ZZ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) -> E. b e. ZZ ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) ) )
93 92 reximdva 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( E. a e. ZZ E. b e. ZZ ( A = ( a x. ( A gcd B ) ) /\ B = ( b x. ( B gcd A ) ) ) -> E. a e. ZZ E. b e. ZZ ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) ) )
94 10 93 biimtrrid 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> ( ( E. a e. ZZ A = ( a x. ( A gcd B ) ) /\ E. b e. ZZ B = ( b x. ( B gcd A ) ) ) -> E. a e. ZZ E. b e. ZZ ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) ) )
95 5 9 94 mp2and 
 |-  ( ( A e. ZZ /\ ( B e. ZZ /\ B =/= 0 ) /\ M = ( A gcd B ) ) -> E. a e. ZZ E. b e. ZZ ( A = ( M x. a ) /\ B = ( M x. b ) /\ ( a gcd b ) = 1 ) )