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

Proof

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