divnumden

Description: Calculate the reduced form of a quotient using gcd . (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	divnumden	$⊢ (A \in ℤ \land B \in ℕ) \to (numer (\frac{A}{B}) = \frac{A}{A \gcd B} \land denom (\frac{A}{B}) = \frac{B}{A \gcd B})$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℤ \land B \in ℕ) \to A \in ℤ$
2		nnz	$⊢ B \in ℕ \to B \in ℤ$
3	2	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℤ$
4		nnne0	$⊢ B \in ℕ \to B \neq 0$
5	4	neneqd	$⊢ B \in ℕ \to \neg B = 0$
6	5	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to \neg B = 0$
7	6	intnand	$⊢ (A \in ℤ \land B \in ℕ) \to \neg (A = 0 \land B = 0)$
8		gcdn0cl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
9	1 3 7 8	syl21anc	$⊢ (A \in ℤ \land B \in ℕ) \to A \gcd B \in ℕ$
10		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
11	2 10	sylan2	$⊢ (A \in ℤ \land B \in ℕ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
12		gcddiv	$⊢ ((A \in ℤ \land B \in ℤ \land A \gcd B \in ℕ) \land ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
13	1 3 9 11 12	syl31anc	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A \gcd B}{A \gcd B} = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
14	9	nncnd	$⊢ (A \in ℤ \land B \in ℕ) \to A \gcd B \in ℂ$
15	9	nnne0d	$⊢ (A \in ℤ \land B \in ℕ) \to A \gcd B \neq 0$
16	14 15	dividd	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A \gcd B}{A \gcd B} = 1$
17	13 16	eqtr3d	$⊢ (A \in ℤ \land B \in ℕ) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
18		zcn	$⊢ A \in ℤ \to A \in ℂ$
19	18	adantr	$⊢ (A \in ℤ \land B \in ℕ) \to A \in ℂ$
20		nncn	$⊢ B \in ℕ \to B \in ℂ$
21	20	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℂ$
22	4	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \neq 0$
23		divcan7	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (A \gcd B \in ℂ \land A \gcd B \neq 0)) \to \frac{\frac{A}{A \gcd B}}{\frac{B}{A \gcd B}} = \frac{A}{B}$
24	23	eqcomd	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (A \gcd B \in ℂ \land A \gcd B \neq 0)) \to \frac{A}{B} = \frac{\frac{A}{A \gcd B}}{\frac{B}{A \gcd B}}$
25	19 21 22 14 15 24	syl122anc	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A}{B} = \frac{\frac{A}{A \gcd B}}{\frac{B}{A \gcd B}}$
26		znq	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A}{B} \in ℚ$
27	11	simpld	$⊢ (A \in ℤ \land B \in ℕ) \to (A \gcd B) ∥ A$
28		gcdcl	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℕ_{0}$
29	28	nn0zd	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℤ$
30	2 29	sylan2	$⊢ (A \in ℤ \land B \in ℕ) \to A \gcd B \in ℤ$
31		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land A \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
32	30 15 1 31	syl3anc	$⊢ (A \in ℤ \land B \in ℕ) \to ((A \gcd B) ∥ A \leftrightarrow \frac{A}{A \gcd B} \in ℤ)$
33	27 32	mpbid	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A}{A \gcd B} \in ℤ$
34	11	simprd	$⊢ (A \in ℤ \land B \in ℕ) \to (A \gcd B) ∥ B$
35		simpr	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℕ$
36		nndivdvds	$⊢ (B \in ℕ \land A \gcd B \in ℕ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℕ)$
37	35 9 36	syl2anc	$⊢ (A \in ℤ \land B \in ℕ) \to ((A \gcd B) ∥ B \leftrightarrow \frac{B}{A \gcd B} \in ℕ)$
38	34 37	mpbid	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{B}{A \gcd B} \in ℕ$
39		qnumdenbi	$⊢ (\frac{A}{B} \in ℚ \land \frac{A}{A \gcd B} \in ℤ \land \frac{B}{A \gcd B} \in ℕ) \to (((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1 \land \frac{A}{B} = \frac{\frac{A}{A \gcd B}}{\frac{B}{A \gcd B}}) \leftrightarrow (numer (\frac{A}{B}) = \frac{A}{A \gcd B} \land denom (\frac{A}{B}) = \frac{B}{A \gcd B}))$
40	26 33 38 39	syl3anc	$⊢ (A \in ℤ \land B \in ℕ) \to (((\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1 \land \frac{A}{B} = \frac{\frac{A}{A \gcd B}}{\frac{B}{A \gcd B}}) \leftrightarrow (numer (\frac{A}{B}) = \frac{A}{A \gcd B} \land denom (\frac{A}{B}) = \frac{B}{A \gcd B}))$
41	17 25 40	mpbi2and	$⊢ (A \in ℤ \land B \in ℕ) \to (numer (\frac{A}{B}) = \frac{A}{A \gcd B} \land denom (\frac{A}{B}) = \frac{B}{A \gcd B})$

Metamath Proof Explorer

Theorem divnumden

Proof