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	$⊢ ((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		pythagtriplem7	$⊢ ((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		zaddcl	$⊢ (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	6	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 \in ℤ$
8		nnz	$⊢ A \in ℕ \to A \in ℤ$
9	8	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
10	9	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 A \in ℤ$
11		nnne0	$⊢ A \in ℕ \to A \neq 0$
12	11	neneqd	$⊢ A \in ℕ \to \neg A = 0$
13	12	intnand	$⊢ A \in ℕ \to \neg (C + B = 0 \land A = 0)$
14	13	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to \neg (C + B = 0 \land A = 0)$
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 \neg (C + B = 0 \land A = 0)$
16		gcdn0cl	$⊢ ((C + B \in ℤ \land A \in ℤ) \land \neg (C + B = 0 \land A = 0)) \to (C + B) \gcd A \in ℕ$
17	7 10 15 16	syl21anc	$⊢ ((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 ℕ$
18	1 17	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 ℕ$