This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐵 = ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) ) )

Proof

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