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

Metamath Proof Explorer

Theorem pythagtriplem9

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 pythagtriplem9 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 pythagtriplem7 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) = ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) )
2 nnz ⊢ ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
3 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
4 zaddcl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐶 + 𝐵 ) ∈ ℤ )
5 2 3 4 syl2anr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℤ )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ( 𝐶 + 𝐵 ) ∈ ℤ )
7 6 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝐶 + 𝐵 ) ∈ ℤ )
8 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
10 9 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝐴 ∈ ℤ )
11 nnne0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
12 11 neneqd ⊢ ( 𝐴 ∈ ℕ → ¬ 𝐴 = 0 )
13 12 intnand ⊢ ( 𝐴 ∈ ℕ → ¬ ( ( 𝐶 + 𝐵 ) = 0 ∧ 𝐴 = 0 ) )
14 13 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) → ¬ ( ( 𝐶 + 𝐵 ) = 0 ∧ 𝐴 = 0 ) )
15 14 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ¬ ( ( 𝐶 + 𝐵 ) = 0 ∧ 𝐴 = 0 ) )
16 gcdn0cl ⊢ ( ( ( ( 𝐶 + 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ¬ ( ( 𝐶 + 𝐵 ) = 0 ∧ 𝐴 = 0 ) ) → ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ∈ ℕ )
17 7 10 15 16 syl21anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( ( 𝐶 + 𝐵 ) gcd 𝐴 ) ∈ ℕ )
18 1 17 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝐵 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( √ ‘ ( 𝐶 + 𝐵 ) ) ∈ ℕ )