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 \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem6	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} = (C - B) \gcd A$
2		nnz	$⊢ C \in ℕ \to C \in ℤ$
3		nnz	$⊢ B \in ℕ \to B \in ℤ$
4		zsubcl	$⊢ (C \in ℤ \land B \in ℤ) \to C - B \in ℤ$
5	2 3 4	syl2anr	$⊢ (B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
6	5	3adant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
7		nnz	$⊢ A \in ℕ \to A \in ℤ$
8	7	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
9		nnne0	$⊢ A \in ℕ \to A \neq 0$
10	9	neneqd	$⊢ A \in ℕ \to \neg A = 0$
11	10	intnand	$⊢ A \in ℕ \to \neg (C - B = 0 \land A = 0)$
12	11	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \neg (C - B = 0 \land A = 0)$
13		gcdn0cl	$⊢ ((C - B \in ℤ \land A \in ℤ) \land \neg (C - B = 0 \land A = 0)) \to (C - B) \gcd A \in ℕ$
14	6 8 12 13	syl21anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (C - B) \gcd A \in ℕ$
15	14	3ad2ant1	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to (C - B) \gcd A \in ℕ$
16	1 15	eqeltrd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land (A \gcd B = 1 \land \neg 2 ∥ A)) \to \sqrt{C - B} \in ℕ$