Metamath Proof Explorer

Theorem 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 ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → C 2 = A ⁢ B → B = B gcd C 2

Proof

Step Hyp Ref Expression
1 zcn ⊢ A ∈ ℤ → A ∈ ℂ
2 nn0cn ⊢ B ∈ ℕ 0 → B ∈ ℂ
3 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
4 1 2 3 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 → A ⁢ B = B ⁢ A
5 4 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → A ⁢ B = B ⁢ A
6 5 adantr ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → A ⁢ B = B ⁢ A
7 6 eqeq2d ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → C 2 = A ⁢ B ↔ C 2 = B ⁢ A
8 simpl2 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → B ∈ ℕ 0
9 simpl1 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → A ∈ ℤ
10 simpl3 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → C ∈ ℕ 0
11 nn0z ⊢ B ∈ ℕ 0 → B ∈ ℤ
12 gcdcom ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = B gcd A
13 12 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B gcd C = B gcd A gcd C
14 13 eqeq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B gcd C = 1 ↔ B gcd A gcd C = 1
15 11 14 sylan2 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 → A gcd B gcd C = 1 ↔ B gcd A gcd C = 1
16 15 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 → A gcd B gcd C = 1 ↔ B gcd A gcd C = 1
17 16 biimpa ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → B gcd A gcd C = 1
18 coprimeprodsq ⊢ B ∈ ℕ 0 ∧ A ∈ ℤ ∧ C ∈ ℕ 0 ∧ B gcd A gcd C = 1 → C 2 = B ⁢ A → B = B gcd C 2
19 8 9 10 17 18 syl31anc ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → C 2 = B ⁢ A → B = B gcd C 2
20 7 19 sylbid ⊢ A ∈ ℤ ∧ B ∈ ℕ 0 ∧ C ∈ ℕ 0 ∧ A gcd B gcd C = 1 → C 2 = A ⁢ B → B = B gcd C 2