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 ${⊢}\left({A}\in ℤ\wedge \left({B}\in ℤ\wedge {B}\ne 0\right)\wedge {M}={A}\mathrm{gcd}{B}\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}={M}{a}\wedge {B}={M}{b}\wedge {a}\mathrm{gcd}{b}=1\right)$

Proof

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