pythagtriplem6

Description: Lemma for pythagtrip . Calculate ( sqrt( C - B ) ) . (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ C \in ℕ \to C \in ℤ$
2	1	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℤ$
3		nnz	$⊢ B \in ℕ \to B \in ℤ$
4	3	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℤ$
5	2 4	zsubcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℤ$
6	5	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 ℤ$
7		pythagtriplem10	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to 0 < C - B$
8	7	3adant3	$⊢ ((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 0 < C - B$
9		elnnz	$⊢ C - B \in ℕ \leftrightarrow (C - B \in ℤ \land 0 < C - B)$
10	6 8 9	sylanbrc	$⊢ ((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 ℕ$
11	10	nnnn0d	$⊢ ((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 ℕ_{0}$
12		simp3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℕ$
13		simp2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℕ$
14	12 13	nnaddcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℕ$
15	14	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℤ$
16	15	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 ℤ$
17		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
18	17	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℕ_{0}$
19	18	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 ℕ_{0}$
20	11 16 19	3jca	$⊢ ((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 ℕ_{0} \land C + B \in ℤ \land A \in ℕ_{0})$
21		pythagtriplem4	$⊢ ((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 (C + B) = 1$
22	21	oveq1d	$⊢ ((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 (C + B)) \gcd A = 1 \gcd A$
23		nnz	$⊢ A \in ℕ \to A \in ℤ$
24	23	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
25	24	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 ℤ$
26		1gcd	$⊢ A \in ℤ \to 1 \gcd A = 1$
27	25 26	syl	$⊢ ((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 1 \gcd A = 1$
28	22 27	eqtrd	$⊢ ((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 (C + B)) \gcd A = 1$
29	20 28	jca	$⊢ ((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 ℕ_{0} \land C + B \in ℤ \land A \in ℕ_{0}) \land ((C - B) \gcd (C + B)) \gcd A = 1)$
30		oveq1	$⊢ A^{2} + B^{2} = C^{2} \to A^{2} + B^{2} - B^{2} = C^{2} - B^{2}$
31	30	3ad2ant2	$⊢ ((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^{2} + B^{2} - B^{2} = C^{2} - B^{2}$
32	24	zcnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℂ$
33	32	sqcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℂ$
34		nncn	$⊢ B \in ℕ \to B \in ℂ$
35	34	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℂ$
36	35	sqcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℂ$
37	33 36	pncand	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} + B^{2} - B^{2} = A^{2}$
38	37	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^{2} + B^{2} - B^{2} = A^{2}$
39		nncn	$⊢ C \in ℕ \to C \in ℂ$
40	39	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℂ$
41		subsq	$⊢ (C \in ℂ \land B \in ℂ) \to C^{2} - B^{2} = (C + B) (C - B)$
42	40 35 41	syl2anc	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C^{2} - B^{2} = (C + B) (C - B)$
43	14	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + B \in ℂ$
44	5	zcnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - B \in ℂ$
45	43 44	mulcomd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (C + B) (C - B) = (C - B) (C + B)$
46	42 45	eqtrd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C^{2} - B^{2} = (C - B) (C + B)$
47	46	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^{2} - B^{2} = (C - B) (C + B)$
48	31 38 47	3eqtr3d	$⊢ ((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^{2} = (C - B) (C + B)$
49		coprimeprodsq	$⊢ ((C - B \in ℕ_{0} \land C + B \in ℤ \land A \in ℕ_{0}) \land ((C - B) \gcd (C + B)) \gcd A = 1) \to (A^{2} = (C - B) (C + B) \to C - B = {((C - B) \gcd A)}^{2})$
50	29 48 49	sylc	$⊢ ((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 = {((C - B) \gcd A)}^{2}$
51	50	fveq2d	$⊢ ((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} = \sqrt{{((C - B) \gcd A)}^{2}}$
52	6 25	gcdcld	$⊢ ((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 ℕ_{0}$
53	52	nn0red	$⊢ ((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 ℝ$
54	52	nn0ge0d	$⊢ ((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 0 \leq (C - B) \gcd A$
55	53 54	sqrtsqd	$⊢ ((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) \gcd A)}^{2}} = (C - B) \gcd A$
56	51 55	eqtrd	$⊢ ((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$

Metamath Proof Explorer

Theorem pythagtriplem6

Proof