Metamath Proof Explorer

Theorem divgcdcoprm0

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

Ref Expression
Assertion divgcdcoprm0 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 )

Proof

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