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 
|- ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) -> B = ( ( B gcd C ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 nn0cn 
 |-  ( B e. NN0 -> B e. CC )
3 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
4 1 2 3 syl2an 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A x. B ) = ( B x. A ) )
5 4 3adant3 
 |-  ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) -> ( A x. B ) = ( B x. A ) )
6 5 adantr 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( A x. B ) = ( B x. A ) )
7 6 eqeq2d 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) <-> ( C ^ 2 ) = ( B x. A ) ) )
8 simpl2 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> B e. NN0 )
9 simpl1 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> A e. ZZ )
10 simpl3 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> C e. NN0 )
11 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
12 gcdcom 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
13 12 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) gcd C ) = ( ( B gcd A ) gcd C ) )
14 13 eqeq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( A gcd B ) gcd C ) = 1 <-> ( ( B gcd A ) gcd C ) = 1 ) )
15 11 14 sylan2 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( ( ( A gcd B ) gcd C ) = 1 <-> ( ( B gcd A ) gcd C ) = 1 ) )
16 15 3adant3 
 |-  ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) -> ( ( ( A gcd B ) gcd C ) = 1 <-> ( ( B gcd A ) gcd C ) = 1 ) )
17 16 biimpa 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( B gcd A ) gcd C ) = 1 )
18 coprimeprodsq 
 |-  ( ( ( B e. NN0 /\ A e. ZZ /\ C e. NN0 ) /\ ( ( B gcd A ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( B x. A ) -> B = ( ( B gcd C ) ^ 2 ) ) )
19 8 9 10 17 18 syl31anc 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( B x. A ) -> B = ( ( B gcd C ) ^ 2 ) ) )
20 7 19 sylbid 
 |-  ( ( ( A e. ZZ /\ B e. NN0 /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) -> B = ( ( B gcd C ) ^ 2 ) ) )