This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pythagtriplem8

Description: Lemma for pythagtrip . Show that ( sqrt( C - B ) ) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem8 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B ∈ ℕ

Proof

Step Hyp Ref Expression
1 pythagtriplem6 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B = C − B gcd A
2 nnz ⊢ C ∈ ℕ → C ∈ ℤ
3 nnz ⊢ B ∈ ℕ → B ∈ ℤ
4 zsubcl ⊢ C ∈ ℤ ∧ B ∈ ℤ → C − B ∈ ℤ
5 2 3 4 syl2anr ⊢ B ∈ ℕ ∧ C ∈ ℕ → C − B ∈ ℤ
6 5 3adant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C − B ∈ ℤ
7 nnz ⊢ A ∈ ℕ → A ∈ ℤ
8 7 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → A ∈ ℤ
9 nnne0 ⊢ A ∈ ℕ → A ≠ 0
10 9 neneqd ⊢ A ∈ ℕ → ¬ A = 0
11 10 intnand ⊢ A ∈ ℕ → ¬ C − B = 0 ∧ A = 0
12 11 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → ¬ C − B = 0 ∧ A = 0
13 gcdn0cl ⊢ C − B ∈ ℤ ∧ A ∈ ℤ ∧ ¬ C − B = 0 ∧ A = 0 → C − B gcd A ∈ ℕ
14 6 8 12 13 syl21anc ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ → C − B gcd A ∈ ℕ
15 14 3ad2ant1 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B gcd A ∈ ℕ
16 1 15 eqeltrd ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ C ∈ ℕ ∧ A 2 + B 2 = C 2 ∧ A gcd B = 1 ∧ ¬ 2 ∥ A → C − B ∈ ℕ