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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
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 ) ) )