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

Metamath Proof Explorer

Theorem flt4lem4

Description: If the product of two coprime factors is a perfect square, the factors are perfect squares. (Contributed by SN, 22-Aug-2024)

Ref Expression
Hypotheses flt4lem4.a 
|- ( ph -> A e. NN )
flt4lem4.b 
|- ( ph -> B e. NN )
flt4lem4.c 
|- ( ph -> C e. NN )
flt4lem4.1 
|- ( ph -> ( A gcd B ) = 1 )
flt4lem4.2 
|- ( ph -> ( A x. B ) = ( C ^ 2 ) )
Assertion flt4lem4 
|- ( ph -> ( A = ( ( A gcd C ) ^ 2 ) /\ B = ( ( B gcd C ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 flt4lem4.a 
 |-  ( ph -> A e. NN )
2 flt4lem4.b 
 |-  ( ph -> B e. NN )
3 flt4lem4.c 
 |-  ( ph -> C e. NN )
4 flt4lem4.1 
 |-  ( ph -> ( A gcd B ) = 1 )
5 flt4lem4.2 
 |-  ( ph -> ( A x. B ) = ( C ^ 2 ) )
6 5 eqcomd 
 |-  ( ph -> ( C ^ 2 ) = ( A x. B ) )
7 1 nnnn0d 
 |-  ( ph -> A e. NN0 )
8 2 nnnn0d 
 |-  ( ph -> B e. NN0 )
9 8 nn0zd 
 |-  ( ph -> B e. ZZ )
10 3 nnnn0d 
 |-  ( ph -> C e. NN0 )
11 4 oveq1d 
 |-  ( ph -> ( ( A gcd B ) gcd C ) = ( 1 gcd C ) )
12 10 nn0zd 
 |-  ( ph -> C e. ZZ )
13 1gcd 
 |-  ( C e. ZZ -> ( 1 gcd C ) = 1 )
14 12 13 syl 
 |-  ( ph -> ( 1 gcd C ) = 1 )
15 11 14 eqtrd 
 |-  ( ph -> ( ( A gcd B ) gcd C ) = 1 )
16 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 ) ) )
17 7 9 10 15 16 syl31anc 
 |-  ( ph -> ( ( C ^ 2 ) = ( A x. B ) -> A = ( ( A gcd C ) ^ 2 ) ) )
18 6 17 mpd 
 |-  ( ph -> A = ( ( A gcd C ) ^ 2 ) )
19 1 nnzd 
 |-  ( ph -> A e. ZZ )
20 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 ) ) )
21 19 8 10 15 20 syl31anc 
 |-  ( ph -> ( ( C ^ 2 ) = ( A x. B ) -> B = ( ( B gcd C ) ^ 2 ) ) )
22 6 21 mpd 
 |-  ( ph -> B = ( ( B gcd C ) ^ 2 ) )
23 18 22 jca 
 |-  ( ph -> ( A = ( ( A gcd C ) ^ 2 ) /\ B = ( ( B gcd C ) ^ 2 ) ) )