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 ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ 𝑀 = ( 𝐴 gcd 𝐵 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑀 · 𝑎 ) ∧ 𝐵 = ( 𝑀 · 𝑏 ) ∧ ( 𝑎 gcd 𝑏 ) = 1 ) )

Proof

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