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	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem4.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem4.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	flt4lem4.1	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
	flt4lem4.2	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐶 ↑ 2 ) )
Assertion	flt4lem4	⊢ ( 𝜑 → ( 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) ∧ 𝐵 = ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem4.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		flt4lem4.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		flt4lem4.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		flt4lem4.1	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
5		flt4lem4.2	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐶 ↑ 2 ) )
6	5	eqcomd	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) )
7	1	nnnn0d	⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
8	2	nnnn0d	⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
9	8	nn0zd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
10	3	nnnn0d	⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
11	4	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = ( 1 gcd 𝐶 ) )
12	10	nn0zd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
13		1gcd	⊢ ( 𝐶 ∈ ℤ → ( 1 gcd 𝐶 ) = 1 )
14	12 13	syl	⊢ ( 𝜑 → ( 1 gcd 𝐶 ) = 1 )
15	11 14	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 )
16		coprimeprodsq	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) ) )
17	7 9 10 15 16	syl31anc	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) ) )
18	6 17	mpd	⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) )
19	1	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
20		coprimeprodsq2	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ ( ( 𝐴 gcd 𝐵 ) gcd 𝐶 ) = 1 ) → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐵 = ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) ) )
21	19 8 10 15 20	syl31anc	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) = ( 𝐴 · 𝐵 ) → 𝐵 = ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) ) )
22	6 21	mpd	⊢ ( 𝜑 → 𝐵 = ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) )
23	18 22	jca	⊢ ( 𝜑 → ( 𝐴 = ( ( 𝐴 gcd 𝐶 ) ↑ 2 ) ∧ 𝐵 = ( ( 𝐵 gcd 𝐶 ) ↑ 2 ) ) )