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	$$⊢\phi \to A\in \mathbb{N}$$
	flt4lem4.b	$$⊢\phi \to B\in \mathbb{N}$$
	flt4lem4.c	$$⊢\phi \to C\in \mathbb{N}$$
	flt4lem4.1	$$⊢\phi \to A\gcd B=1$$
	flt4lem4.2	$$⊢\phi \to AB=C^2$$
Assertion	flt4lem4	$$⊢\phi \to \left(A={\left(A\gcd C\right)}^2\wedge B={\left(B\gcd C\right)}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		flt4lem4.a	$$⊢\phi \to A\in \mathbb{N}$$
2		flt4lem4.b	$$⊢\phi \to B\in \mathbb{N}$$
3		flt4lem4.c	$$⊢\phi \to C\in \mathbb{N}$$
4		flt4lem4.1	$$⊢\phi \to A\gcd B=1$$
5		flt4lem4.2	$$⊢\phi \to AB=C^2$$
6	5	eqcomd	$$⊢\phi \to C^2=AB$$
7	1	nnnn0d	$$⊢\phi \to A\in {\mathbb{N}}_0$$
8	2	nnnn0d	$$⊢\phi \to B\in {\mathbb{N}}_0$$
9	8	nn0zd	$$⊢\phi \to B\in \mathbb{Z}$$
10	3	nnnn0d	$$⊢\phi \to C\in {\mathbb{N}}_0$$
11	4	oveq1d	$$⊢\phi \to \left(A\gcd B\right)\gcd C=1\gcd C$$
12	10	nn0zd	$$⊢\phi \to C\in \mathbb{Z}$$
13		1gcd	$$⊢C\in \mathbb{Z}\to 1\gcd C=1$$
14	12 13	syl	$$⊢\phi \to 1\gcd C=1$$
15	11 14	eqtrd	$$⊢\phi \to \left(A\gcd B\right)\gcd C=1$$
16		coprimeprodsq	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{Z}\wedge C\in {\mathbb{N}}_0\right)\wedge \left(A\gcd B\right)\gcd C=1\right)\to \left(C^2=AB\to A={\left(A\gcd C\right)}^2\right)$$
17	7 9 10 15 16	syl31anc	$$⊢\phi \to \left(C^2=AB\to A={\left(A\gcd C\right)}^2\right)$$
18	6 17	mpd	$$⊢\phi \to A={\left(A\gcd C\right)}^2$$
19	1	nnzd	$$⊢\phi \to A\in \mathbb{Z}$$
20		coprimeprodsq2	$$⊢\left(\left(A\in \mathbb{Z}\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\wedge \left(A\gcd B\right)\gcd C=1\right)\to \left(C^2=AB\to B={\left(B\gcd C\right)}^2\right)$$
21	19 8 10 15 20	syl31anc	$$⊢\phi \to \left(C^2=AB\to B={\left(B\gcd C\right)}^2\right)$$
22	6 21	mpd	$$⊢\phi \to B={\left(B\gcd C\right)}^2$$
23	18 22	jca	$$⊢\phi \to \left(A={\left(A\gcd C\right)}^2\wedge B={\left(B\gcd C\right)}^2\right)$$