Metamath Proof Explorer

Theorem coprimeprodsq

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, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion coprimeprodsq 
|- ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) -> A = ( ( A gcd C ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
2 nn0z 
 |-  ( C e. NN0 -> C e. ZZ )
3 gcdcl 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> ( A gcd C ) e. NN0 )
4 1 2 3 syl2an 
 |-  ( ( A e. NN0 /\ C e. NN0 ) -> ( A gcd C ) e. NN0 )
5 4 3adant2 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( A gcd C ) e. NN0 )
6 5 3ad2ant1 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( A gcd C ) e. NN0 )
7 6 nn0cnd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( A gcd C ) e. CC )
8 7 sqvald 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( A gcd C ) ^ 2 ) = ( ( A gcd C ) x. ( A gcd C ) ) )
9 simp13 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> C e. NN0 )
10 9 nn0cnd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> C e. CC )
11 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
12 11 3ad2ant1 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> A e. CC )
13 12 3ad2ant1 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> A e. CC )
14 10 13 mulcomd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( C x. A ) = ( A x. C ) )
15 simpl3 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> C e. NN0 )
16 15 nn0cnd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> C e. CC )
17 16 sqvald 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( C ^ 2 ) = ( C x. C ) )
18 17 eqeq1d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) <-> ( C x. C ) = ( A x. B ) ) )
19 18 biimp3a 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( C x. C ) = ( A x. B ) )
20 14 19 oveq12d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( C x. A ) gcd ( C x. C ) ) = ( ( A x. C ) gcd ( A x. B ) ) )
21 simp11 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> A e. NN0 )
22 21 nn0zd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> A e. ZZ )
23 9 nn0zd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> C e. ZZ )
24 mulgcd 
 |-  ( ( C e. NN0 /\ A e. ZZ /\ C e. ZZ ) -> ( ( C x. A ) gcd ( C x. C ) ) = ( C x. ( A gcd C ) ) )
25 9 22 23 24 syl3anc 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( C x. A ) gcd ( C x. C ) ) = ( C x. ( A gcd C ) ) )
26 simp12 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> B e. ZZ )
27 mulgcd 
 |-  ( ( A e. NN0 /\ C e. ZZ /\ B e. ZZ ) -> ( ( A x. C ) gcd ( A x. B ) ) = ( A x. ( C gcd B ) ) )
28 21 23 26 27 syl3anc 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( A x. C ) gcd ( A x. B ) ) = ( A x. ( C gcd B ) ) )
29 20 25 28 3eqtr3d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( C x. ( A gcd C ) ) = ( A x. ( C gcd B ) ) )
30 29 oveq2d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( A x. ( A gcd C ) ) gcd ( C x. ( A gcd C ) ) ) = ( ( A x. ( A gcd C ) ) gcd ( A x. ( C gcd B ) ) ) )
31 mulgcdr 
 |-  ( ( A e. ZZ /\ C e. ZZ /\ ( A gcd C ) e. NN0 ) -> ( ( A x. ( A gcd C ) ) gcd ( C x. ( A gcd C ) ) ) = ( ( A gcd C ) x. ( A gcd C ) ) )
32 22 23 6 31 syl3anc 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( A x. ( A gcd C ) ) gcd ( C x. ( A gcd C ) ) ) = ( ( A gcd C ) x. ( A gcd C ) ) )
33 6 nn0zd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( A gcd C ) e. ZZ )
34 gcdcl 
 |-  ( ( C e. ZZ /\ B e. ZZ ) -> ( C gcd B ) e. NN0 )
35 2 34 sylan 
 |-  ( ( C e. NN0 /\ B e. ZZ ) -> ( C gcd B ) e. NN0 )
36 35 ancoms 
 |-  ( ( B e. ZZ /\ C e. NN0 ) -> ( C gcd B ) e. NN0 )
37 36 3adant1 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( C gcd B ) e. NN0 )
38 37 3ad2ant1 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( C gcd B ) e. NN0 )
39 38 nn0zd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( C gcd B ) e. ZZ )
40 mulgcd 
 |-  ( ( A e. NN0 /\ ( A gcd C ) e. ZZ /\ ( C gcd B ) e. ZZ ) -> ( ( A x. ( A gcd C ) ) gcd ( A x. ( C gcd B ) ) ) = ( A x. ( ( A gcd C ) gcd ( C gcd B ) ) ) )
41 21 33 39 40 syl3anc 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( A x. ( A gcd C ) ) gcd ( A x. ( C gcd B ) ) ) = ( A x. ( ( A gcd C ) gcd ( C gcd B ) ) ) )
42 30 32 41 3eqtr3d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( ( A gcd C ) x. ( A gcd C ) ) = ( A x. ( ( A gcd C ) gcd ( C gcd B ) ) ) )
43 2 3ad2ant3 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> C e. ZZ )
44 gcdid 
 |-  ( C e. ZZ -> ( C gcd C ) = ( abs ` C ) )
45 43 44 syl 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( C gcd C ) = ( abs ` C ) )
46 45 oveq1d 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( C gcd C ) gcd B ) = ( ( abs ` C ) gcd B ) )
47 simp2 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> B e. ZZ )
48 gcdabs1 
 |-  ( ( C e. ZZ /\ B e. ZZ ) -> ( ( abs ` C ) gcd B ) = ( C gcd B ) )
49 43 47 48 syl2anc 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( abs ` C ) gcd B ) = ( C gcd B ) )
50 46 49 eqtrd 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( C gcd C ) gcd B ) = ( C gcd B ) )
51 gcdass 
 |-  ( ( C e. ZZ /\ C e. ZZ /\ B e. ZZ ) -> ( ( C gcd C ) gcd B ) = ( C gcd ( C gcd B ) ) )
52 43 43 47 51 syl3anc 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( C gcd C ) gcd B ) = ( C gcd ( C gcd B ) ) )
53 43 47 gcdcomd 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( C gcd B ) = ( B gcd C ) )
54 50 52 53 3eqtr3d 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( C gcd ( C gcd B ) ) = ( B gcd C ) )
55 54 oveq2d 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( A gcd ( C gcd ( C gcd B ) ) ) = ( A gcd ( B gcd C ) ) )
56 1 3ad2ant1 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> A e. ZZ )
57 37 nn0zd 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( C gcd B ) e. ZZ )
58 gcdass 
 |-  ( ( A e. ZZ /\ C e. ZZ /\ ( C gcd B ) e. ZZ ) -> ( ( A gcd C ) gcd ( C gcd B ) ) = ( A gcd ( C gcd ( C gcd B ) ) ) )
59 56 43 57 58 syl3anc 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( A gcd C ) gcd ( C gcd B ) ) = ( A gcd ( C gcd ( C gcd B ) ) ) )
60 gcdass 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A gcd B ) gcd C ) = ( A gcd ( B gcd C ) ) )
61 56 47 43 60 syl3anc 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( A gcd B ) gcd C ) = ( A gcd ( B gcd C ) ) )
62 55 59 61 3eqtr4d 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( A gcd C ) gcd ( C gcd B ) ) = ( ( A gcd B ) gcd C ) )
63 62 eqeq1d 
 |-  ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) -> ( ( ( A gcd C ) gcd ( C gcd B ) ) = 1 <-> ( ( A gcd B ) gcd C ) = 1 ) )
64 63 biimpar 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( A gcd C ) gcd ( C gcd B ) ) = 1 )
65 64 oveq2d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( A x. ( ( A gcd C ) gcd ( C gcd B ) ) ) = ( A x. 1 ) )
66 65 3adant3 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( A x. ( ( A gcd C ) gcd ( C gcd B ) ) ) = ( A x. 1 ) )
67 13 mulid1d 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( A x. 1 ) = A )
68 66 67 eqtrd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> ( A x. ( ( A gcd C ) gcd ( C gcd B ) ) ) = A )
69 8 42 68 3eqtrrd 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 /\ ( C ^ 2 ) = ( A x. B ) ) -> A = ( ( A gcd C ) ^ 2 ) )
70 69 3expia 
 |-  ( ( ( A e. NN0 /\ B e. ZZ /\ C e. NN0 ) /\ ( ( A gcd B ) gcd C ) = 1 ) -> ( ( C ^ 2 ) = ( A x. B ) -> A = ( ( A gcd C ) ^ 2 ) ) )