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 ⊢ φ → A ∈ ℕ
flt4lem4.b ⊢ φ → B ∈ ℕ
flt4lem4.c ⊢ φ → C ∈ ℕ
flt4lem4.1 ⊢ φ → A gcd B = 1
flt4lem4.2 ⊢ φ → A ⁢ B = C 2
Assertion flt4lem4 ⊢ φ → A = A gcd C 2 ∧ B = B gcd C 2

Proof

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