coprimeprodsq2

Description: If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	coprimeprodsq2	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to (C^{2} = A B \to B = {(B \gcd C)}^{2})$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2		nn0cn	$⊢ B \in ℕ_{0} \to B \in ℂ$
3		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
4	1 2 3	syl2an	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to A B = B A$
5	4	3adant3	$⊢ (A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \to A B = B A$
6	5	adantr	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to A B = B A$
7	6	eqeq2d	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to (C^{2} = A B \leftrightarrow C^{2} = B A)$
8		simpl2	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to B \in ℕ_{0}$
9		simpl1	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to A \in ℤ$
10		simpl3	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to C \in ℕ_{0}$
11		nn0z	$⊢ B \in ℕ_{0} \to B \in ℤ$
12		gcdcom	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B = B \gcd A$
13	12	oveq1d	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B) \gcd C = (B \gcd A) \gcd C$
14	13	eqeq1d	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) \gcd C = 1 \leftrightarrow (B \gcd A) \gcd C = 1)$
15	11 14	sylan2	$⊢ (A \in ℤ \land B \in ℕ_{0}) \to ((A \gcd B) \gcd C = 1 \leftrightarrow (B \gcd A) \gcd C = 1)$
16	15	3adant3	$⊢ (A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \to ((A \gcd B) \gcd C = 1 \leftrightarrow (B \gcd A) \gcd C = 1)$
17	16	biimpa	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to (B \gcd A) \gcd C = 1$
18		coprimeprodsq	$⊢ ((B \in ℕ_{0} \land A \in ℤ \land C \in ℕ_{0}) \land (B \gcd A) \gcd C = 1) \to (C^{2} = B A \to B = {(B \gcd C)}^{2})$
19	8 9 10 17 18	syl31anc	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to (C^{2} = B A \to B = {(B \gcd C)}^{2})$
20	7 19	sylbid	$⊢ ((A \in ℤ \land B \in ℕ_{0} \land C \in ℕ_{0}) \land (A \gcd B) \gcd C = 1) \to (C^{2} = A B \to B = {(B \gcd C)}^{2})$

Metamath Proof Explorer

Theorem coprimeprodsq2

Proof