# Metamath Proof Explorer

## Theorem divgcdcoprm0

Description: Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021)

Ref Expression
Assertion 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$

### Proof

Step Hyp Ref Expression
1 gcddvds ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)$
2 1 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)$
3 gcdcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\mathrm{gcd}{B}\in {ℕ}_{0}$
4 3 nn0zd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\mathrm{gcd}{B}\in ℤ$
5 simpl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\in ℤ$
6 4 5 jca ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({A}\mathrm{gcd}{B}\in ℤ\wedge {A}\in ℤ\right)$
7 6 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left({A}\mathrm{gcd}{B}\in ℤ\wedge {A}\in ℤ\right)$
8 divides ${⊢}\left({A}\mathrm{gcd}{B}\in ℤ\wedge {A}\in ℤ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}\left({A}\mathrm{gcd}{B}\right)={A}\right)$
9 7 8 syl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}\left({A}\mathrm{gcd}{B}\right)={A}\right)$
10 simpr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {B}\in ℤ$
11 4 10 jca ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left({A}\mathrm{gcd}{B}\in ℤ\wedge {B}\in ℤ\right)$
12 11 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left({A}\mathrm{gcd}{B}\in ℤ\wedge {B}\in ℤ\right)$
13 divides ${⊢}\left({A}\mathrm{gcd}{B}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\right)$
14 12 13 syl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\right)$
15 9 14 anbi12d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}\left({A}\mathrm{gcd}{B}\right)={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\right)\right)$
16 bezout ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{m}+{B}{n}$
17 16 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{m}+{B}{n}$
18 oveq1 ${⊢}{a}\left({A}\mathrm{gcd}{B}\right)={A}\to {a}\left({A}\mathrm{gcd}{B}\right){m}={A}{m}$
19 oveq1 ${⊢}{b}\left({A}\mathrm{gcd}{B}\right)={B}\to {b}\left({A}\mathrm{gcd}{B}\right){n}={B}{n}$
20 18 19 oveqan12rd ${⊢}\left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\to {a}\left({A}\mathrm{gcd}{B}\right){m}+{b}\left({A}\mathrm{gcd}{B}\right){n}={A}{m}+{B}{n}$
21 20 eqeq2d ${⊢}\left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\to \left({A}\mathrm{gcd}{B}={a}\left({A}\mathrm{gcd}{B}\right){m}+{b}\left({A}\mathrm{gcd}{B}\right){n}↔{A}\mathrm{gcd}{B}={A}{m}+{B}{n}\right)$
22 21 bicomd ${⊢}\left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}↔{A}\mathrm{gcd}{B}={a}\left({A}\mathrm{gcd}{B}\right){m}+{b}\left({A}\mathrm{gcd}{B}\right){n}\right)$
23 simpl ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {a}\in ℤ$
24 23 zcnd ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {a}\in ℂ$
25 24 adantl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}\in ℂ$
26 3 nn0cnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\mathrm{gcd}{B}\in ℂ$
27 26 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {A}\mathrm{gcd}{B}\in ℂ$
28 27 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\mathrm{gcd}{B}\in ℂ$
29 simpl ${⊢}\left({m}\in ℤ\wedge {n}\in ℤ\right)\to {m}\in ℤ$
30 29 zcnd ${⊢}\left({m}\in ℤ\wedge {n}\in ℤ\right)\to {m}\in ℂ$
31 30 ad2antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {m}\in ℂ$
32 25 28 31 mul32d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}\left({A}\mathrm{gcd}{B}\right){m}={a}{m}\left({A}\mathrm{gcd}{B}\right)$
33 simpr ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {b}\in ℤ$
34 33 zcnd ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {b}\in ℂ$
35 34 adantl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}\in ℂ$
36 simpr ${⊢}\left({m}\in ℤ\wedge {n}\in ℤ\right)\to {n}\in ℤ$
37 36 zcnd ${⊢}\left({m}\in ℤ\wedge {n}\in ℤ\right)\to {n}\in ℂ$
38 37 ad2antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {n}\in ℂ$
39 35 28 38 mul32d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}\left({A}\mathrm{gcd}{B}\right){n}={b}{n}\left({A}\mathrm{gcd}{B}\right)$
40 32 39 oveq12d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}\left({A}\mathrm{gcd}{B}\right){m}+{b}\left({A}\mathrm{gcd}{B}\right){n}={a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)$
41 40 eqeq2d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({A}\mathrm{gcd}{B}={a}\left({A}\mathrm{gcd}{B}\right){m}+{b}\left({A}\mathrm{gcd}{B}\right){n}↔{A}\mathrm{gcd}{B}={a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)\right)$
42 23 adantl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}\in ℤ$
43 29 ad2antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {m}\in ℤ$
44 42 43 zmulcld ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}{m}\in ℤ$
45 4 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {A}\mathrm{gcd}{B}\in ℤ$
46 45 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\mathrm{gcd}{B}\in ℤ$
47 44 46 zmulcld ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}{m}\left({A}\mathrm{gcd}{B}\right)\in ℤ$
48 33 adantl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}\in ℤ$
49 36 ad2antlr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {n}\in ℤ$
50 48 49 zmulcld ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}{n}\in ℤ$
51 3 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {A}\mathrm{gcd}{B}\in {ℕ}_{0}$
52 51 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\mathrm{gcd}{B}\in {ℕ}_{0}$
53 52 nn0zd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\mathrm{gcd}{B}\in ℤ$
54 50 53 zmulcld ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}{n}\left({A}\mathrm{gcd}{B}\right)\in ℤ$
55 47 54 zaddcld ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)\in ℤ$
56 55 zcnd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)\in ℂ$
57 gcd2n0cl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {A}\mathrm{gcd}{B}\in ℕ$
58 nnrp ${⊢}{A}\mathrm{gcd}{B}\in ℕ\to {A}\mathrm{gcd}{B}\in {ℝ}^{+}$
59 58 rpcnne0d ${⊢}{A}\mathrm{gcd}{B}\in ℕ\to \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)$
60 57 59 syl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)$
61 60 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)$
62 div11 ${⊢}\left({A}\mathrm{gcd}{B}\in ℂ\wedge {a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)\in ℂ\wedge \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)\right)\to \left(\frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=\frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}↔{A}\mathrm{gcd}{B}={a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)\right)$
63 28 56 61 62 syl3anc ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=\frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}↔{A}\mathrm{gcd}{B}={a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)\right)$
64 divid ${⊢}\left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)\to \frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=1$
65 61 64 syl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=1$
66 47 zcnd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}{m}\left({A}\mathrm{gcd}{B}\right)\in ℂ$
67 54 zcnd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}{n}\left({A}\mathrm{gcd}{B}\right)\in ℂ$
68 divdir ${⊢}\left({a}{m}\left({A}\mathrm{gcd}{B}\right)\in ℂ\wedge {b}{n}\left({A}\mathrm{gcd}{B}\right)\in ℂ\wedge \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)\right)\to \frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}=\left(\frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}\right)+\left(\frac{{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}\right)$
69 66 67 61 68 syl3anc ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}=\left(\frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}\right)+\left(\frac{{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}\right)$
70 44 zcnd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {a}{m}\in ℂ$
71 51 nn0cnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {A}\mathrm{gcd}{B}\in ℂ$
72 71 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\mathrm{gcd}{B}\in ℂ$
73 57 nnne0d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {A}\mathrm{gcd}{B}\ne 0$
74 73 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\mathrm{gcd}{B}\ne 0$
75 70 72 74 divcan4d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}={a}{m}$
76 50 zcnd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {b}{n}\in ℂ$
77 76 28 74 divcan4d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \frac{{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}={b}{n}$
78 75 77 oveq12d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}\right)+\left(\frac{{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}\right)={a}{m}+{b}{n}$
79 69 78 eqtrd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}={a}{m}+{b}{n}$
80 65 79 eqeq12d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=\frac{{a}{m}\left({A}\mathrm{gcd}{B}\right)+{b}{n}\left({A}\mathrm{gcd}{B}\right)}{{A}\mathrm{gcd}{B}}↔1={a}{m}+{b}{n}\right)$
81 41 63 80 3bitr2d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({A}\mathrm{gcd}{B}={a}\left({A}\mathrm{gcd}{B}\right){m}+{b}\left({A}\mathrm{gcd}{B}\right){n}↔1={a}{m}+{b}{n}\right)$
82 22 81 sylan9bbr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}↔1={a}{m}+{b}{n}\right)$
83 eqcom ${⊢}1={a}{m}+{b}{n}↔{a}{m}+{b}{n}=1$
84 simpr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\to \left({m}\in ℤ\wedge {n}\in ℤ\right)$
85 84 anim1ci ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)$
86 bezoutr1 ${⊢}\left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\to \left({a}{m}+{b}{n}=1\to {a}\mathrm{gcd}{b}=1\right)$
87 85 86 syl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({a}{m}+{b}{n}=1\to {a}\mathrm{gcd}{b}=1\right)$
88 87 adantr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to \left({a}{m}+{b}{n}=1\to {a}\mathrm{gcd}{b}=1\right)$
89 83 88 syl5bi ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to \left(1={a}{m}+{b}{n}\to {a}\mathrm{gcd}{b}=1\right)$
90 simpll1 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\in ℤ$
91 90 zcnd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {A}\in ℂ$
92 divmul3 ${⊢}\left({A}\in ℂ\wedge {a}\in ℂ\wedge \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)\right)\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}={a}↔{A}={a}\left({A}\mathrm{gcd}{B}\right)\right)$
93 91 25 61 92 syl3anc ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}={a}↔{A}={a}\left({A}\mathrm{gcd}{B}\right)\right)$
94 eqcom ${⊢}{a}=\frac{{A}}{{A}\mathrm{gcd}{B}}↔\frac{{A}}{{A}\mathrm{gcd}{B}}={a}$
95 eqcom ${⊢}{a}\left({A}\mathrm{gcd}{B}\right)={A}↔{A}={a}\left({A}\mathrm{gcd}{B}\right)$
96 93 94 95 3bitr4g ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({a}=\frac{{A}}{{A}\mathrm{gcd}{B}}↔{a}\left({A}\mathrm{gcd}{B}\right)={A}\right)$
97 96 biimprd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to {a}=\frac{{A}}{{A}\mathrm{gcd}{B}}\right)$
98 97 a1d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to {a}=\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\right)$
99 98 imp32 ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to {a}=\frac{{A}}{{A}\mathrm{gcd}{B}}$
100 simp2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {B}\in ℤ$
101 100 zcnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to {B}\in ℂ$
102 101 ad2antrr ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to {B}\in ℂ$
103 divmul3 ${⊢}\left({B}\in ℂ\wedge {b}\in ℂ\wedge \left({A}\mathrm{gcd}{B}\in ℂ\wedge {A}\mathrm{gcd}{B}\ne 0\right)\right)\to \left(\frac{{B}}{{A}\mathrm{gcd}{B}}={b}↔{B}={b}\left({A}\mathrm{gcd}{B}\right)\right)$
104 102 35 61 103 syl3anc ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left(\frac{{B}}{{A}\mathrm{gcd}{B}}={b}↔{B}={b}\left({A}\mathrm{gcd}{B}\right)\right)$
105 eqcom ${⊢}{b}=\frac{{B}}{{A}\mathrm{gcd}{B}}↔\frac{{B}}{{A}\mathrm{gcd}{B}}={b}$
106 eqcom ${⊢}{b}\left({A}\mathrm{gcd}{B}\right)={B}↔{B}={b}\left({A}\mathrm{gcd}{B}\right)$
107 104 105 106 3bitr4g ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({b}=\frac{{B}}{{A}\mathrm{gcd}{B}}↔{b}\left({A}\mathrm{gcd}{B}\right)={B}\right)$
108 107 biimprd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to {b}=\frac{{B}}{{A}\mathrm{gcd}{B}}\right)$
109 108 a1dd ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to {b}=\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)$
110 109 imp32 ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to {b}=\frac{{B}}{{A}\mathrm{gcd}{B}}$
111 99 110 oveq12d ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to {a}\mathrm{gcd}{b}=\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)$
112 111 eqeq1d ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to \left({a}\mathrm{gcd}{b}=1↔\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)$
113 89 112 sylibd ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to \left(1={a}{m}+{b}{n}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)$
114 82 113 sylbid ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\wedge \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\wedge {a}\left({A}\mathrm{gcd}{B}\right)={A}\right)\right)\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)$
115 114 exp32 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)$
116 115 com34 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)$
117 116 com23 ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)$
118 117 ex ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\to \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)\right)$
119 118 com23 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge \left({m}\in ℤ\wedge {n}\in ℤ\right)\right)\to \left({A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)\right)$
120 119 rexlimdvva ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{m}+{B}{n}\to \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)\right)$
121 17 120 mpd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)\right)$
122 121 impl ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge {a}\in ℤ\right)\wedge {b}\in ℤ\right)\to \left({b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)$
123 122 rexlimdva ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge {a}\in ℤ\right)\to \left(\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)$
124 123 com23 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\wedge {a}\in ℤ\right)\to \left({a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)$
125 124 rexlimdva ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}\left({A}\mathrm{gcd}{B}\right)={A}\to \left(\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)\right)$
126 125 impd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}\left({A}\mathrm{gcd}{B}\right)={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}\left({A}\mathrm{gcd}{B}\right)={B}\right)\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)$
127 15 126 sylbid ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {B}\ne 0\right)\to \left(\left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1\right)$
128 2 127 mpd ${⊢}\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$