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	biimtrrid	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ 𝑀 = ( 𝐴 gcd 𝐵 ) ) → ( ( ∃ 𝑎 ∈ ℤ 𝐴 = ( 𝑎 · ( 𝐴 gcd 𝐵 ) ) ∧ ∃ 𝑏 ∈ ℤ 𝐵 = ( 𝑏 · ( 𝐵 gcd 𝐴 ) ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑀 · 𝑎 ) ∧ 𝐵 = ( 𝑀 · 𝑏 ) ∧ ( 𝑎 gcd 𝑏 ) = 1 ) ) )
95	5 9 94	mp2and	⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ∧ 𝑀 = ( 𝐴 gcd 𝐵 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑀 · 𝑎 ) ∧ 𝐵 = ( 𝑀 · 𝑏 ) ∧ ( 𝑎 gcd 𝑏 ) = 1 ) )