pythagtriplem15

Description: Lemma for pythagtrip . Show the relationship between M , N , and A . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	pythagtriplem15.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
	pythagtriplem15.2	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
Assertion	pythagtriplem15	$⊢ ((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 = M^{2} - N^{2}$

Proof

Step	Hyp	Ref	Expression
1		pythagtriplem15.1	$⊢ M = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
2		pythagtriplem15.2	$⊢ N = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
3	1	pythagtriplem12	$⊢ ((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 M^{2} = \frac{C + A}{2}$
4	2	pythagtriplem14	$⊢ ((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 N^{2} = \frac{C - A}{2}$
5	3 4	oveq12d	$⊢ ((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 M^{2} - N^{2} = (\frac{C + A}{2}) - (\frac{C - A}{2})$
6		simp3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℕ$
7		simp1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℕ$
8	6 7	nnaddcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + A \in ℕ$
9	8	nncnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C + 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 C + A \in ℂ$
11		nnz	$⊢ C \in ℕ \to C \in ℤ$
12	11	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℤ$
13		nnz	$⊢ A \in ℕ \to A \in ℤ$
14	13	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
15	12 14	zsubcld	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - A \in ℤ$
16	15	zcnd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C - A \in ℂ$
17	16	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 - A \in ℂ$
18		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
19		divsubdir	$⊢ (C + A \in ℂ \land C - A \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{C + A - (C - A)}{2} = (\frac{C + A}{2}) - (\frac{C - A}{2})$
20	18 19	mp3an3	$⊢ (C + A \in ℂ \land C - A \in ℂ) \to \frac{C + A - (C - A)}{2} = (\frac{C + A}{2}) - (\frac{C - A}{2})$
21	10 17 20	syl2anc	$⊢ ((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 \frac{C + A - (C - A)}{2} = (\frac{C + A}{2}) - (\frac{C - A}{2})$
22	5 21	eqtr4d	$⊢ ((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 M^{2} - N^{2} = \frac{C + A - (C - A)}{2}$
23		nncn	$⊢ C \in ℕ \to C \in ℂ$
24	23	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \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 C \in ℂ$
26		nncn	$⊢ A \in ℕ \to A \in ℂ$
27	26	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℂ$
28	27	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 ℂ$
29	25 28 28	pnncand	$⊢ ((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 + A - (C - A) = A + A$
30	28	2timesd	$⊢ ((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 2 A = A + A$
31	29 30	eqtr4d	$⊢ ((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 + A - (C - A) = 2 A$
32	31	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 \frac{C + A - (C - A)}{2} = \frac{2 A}{2}$
33		2cn	$⊢ 2 \in ℂ$
34		2ne0	$⊢ 2 \neq 0$
35		divcan3	$⊢ (A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 A}{2} = A$
36	33 34 35	mp3an23	$⊢ A \in ℂ \to \frac{2 A}{2} = A$
37	28 36	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 \frac{2 A}{2} = A$
38	22 32 37	3eqtrrd	$⊢ ((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 = M^{2} - N^{2}$

Metamath Proof Explorer

Theorem pythagtriplem15

Proof