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 ) ) )