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	$⊢ (A \in ℤ \land (B \in ℤ \land B \neq 0) \land M = A \gcd B) \to \exists a \in ℤ \exists b \in ℤ (A = M a \land B = M b \land a \gcd b = 1)$

Proof

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

Metamath Proof Explorer

Theorem divgcdcoprmex

Proof