divgcdcoprm0

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

		Ref	Expression
	Assertion	divgcdcoprm0	$⊢ (A \in ℤ \land B \in ℤ \land B \neq 0) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$

Proof

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

Metamath Proof Explorer

Theorem divgcdcoprm0

Proof