Metamath Proof Explorer

Theorem flt4lem3

Description: Equivalent to pythagtriplem4 . Show that C + A and C - A are coprime. (Contributed by SN, 22-Aug-2024)

Ref Expression
Hypotheses flt4lem3.a ⊢ φ → A ∈ ℕ
flt4lem3.b ⊢ φ → B ∈ ℕ
flt4lem3.c ⊢ φ → C ∈ ℕ
flt4lem3.1 ⊢ φ → 2 ∥ A
flt4lem3.2 ⊢ φ → A gcd C = 1
flt4lem3.3 ⊢ φ → A 2 + B 2 = C 2
Assertion flt4lem3 ⊢ φ → C + A gcd C − A = 1

Proof

Step Hyp Ref Expression
1 flt4lem3.a ⊢ φ → A ∈ ℕ
2 flt4lem3.b ⊢ φ → B ∈ ℕ
3 flt4lem3.c ⊢ φ → C ∈ ℕ
4 flt4lem3.1 ⊢ φ → 2 ∥ A
5 flt4lem3.2 ⊢ φ → A gcd C = 1
6 flt4lem3.3 ⊢ φ → A 2 + B 2 = C 2
7 3 nnzd ⊢ φ → C ∈ ℤ
8 1 nnzd ⊢ φ → A ∈ ℤ
9 7 8 zaddcld ⊢ φ → C + A ∈ ℤ
10 7 8 zsubcld ⊢ φ → C − A ∈ ℤ
11 9 10 gcdcomd ⊢ φ → C + A gcd C − A = C − A gcd C + A
12 1 2 3 4 5 6 flt4lem2 ⊢ φ → ¬ 2 ∥ B
13 2nn0 ⊢ 2 ∈ ℕ 0
14 13 a1i ⊢ φ → 2 ∈ ℕ 0
15 1 2 3 5 6 fltabcoprm ⊢ φ → A gcd B = 1
16 1 2 3 14 6 15 fltbccoprm ⊢ φ → B gcd C = 1
17 2 nnsqcld ⊢ φ → B 2 ∈ ℕ
18 17 nncnd ⊢ φ → B 2 ∈ ℂ
19 1 nnsqcld ⊢ φ → A 2 ∈ ℕ
20 19 nncnd ⊢ φ → A 2 ∈ ℂ
21 18 20 addcomd ⊢ φ → B 2 + A 2 = A 2 + B 2
22 21 6 eqtrd ⊢ φ → B 2 + A 2 = C 2
23 2 1 3 12 16 22 flt4lem1 ⊢ φ → B ∈ ℕ ∧ A ∈ ℕ ∧ C ∈ ℕ ∧ B 2 + A 2 = C 2 ∧ B gcd A = 1 ∧ ¬ 2 ∥ B
24 pythagtriplem4 ⊢ B ∈ ℕ ∧ A ∈ ℕ ∧ C ∈ ℕ ∧ B 2 + A 2 = C 2 ∧ B gcd A = 1 ∧ ¬ 2 ∥ B → C − A gcd C + A = 1
25 23 24 syl ⊢ φ → C − A gcd C + A = 1
26 11 25 eqtrd ⊢ φ → C + A gcd C − A = 1