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 )