pythagtriplem17

Description: Lemma for pythagtrip . Show the relationship between M , N , and C . (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	pythagtriplem17	$⊢ ((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 = 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		nncn	$⊢ C \in ℕ \to C \in ℂ$
7	6	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to C \in ℂ$
8	7	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 ℂ$
9		nncn	$⊢ A \in ℕ \to A \in ℂ$
10	9	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℂ$
11	10	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 ℂ$
12	8 11	addcld	$⊢ ((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 ℂ$
13	8 11	subcld	$⊢ ((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 ℂ$
14		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
15		divdir	$⊢ (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})$
16	14 15	mp3an3	$⊢ (C + A \in ℂ \land C - A \in ℂ) \to \frac{C + A + (C - A)}{2} = (\frac{C + A}{2}) + (\frac{C - A}{2})$
17	12 13 16	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})$
18	5 17	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}$
19	8 11 8	ppncand	$⊢ ((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) = C + C$
20	8	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 C = C + C$
21	19 20	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 C$
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 \frac{C + A + (C - A)}{2} = \frac{2 C}{2}$
23		2cn	$⊢ 2 \in ℂ$
24		2ne0	$⊢ 2 \neq 0$
25		divcan3	$⊢ (C \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 C}{2} = C$
26	23 24 25	mp3an23	$⊢ C \in ℂ \to \frac{2 C}{2} = C$
27	8 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 \frac{2 C}{2} = C$
28	18 22 27	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 C = M^{2} + N^{2}$

Metamath Proof Explorer

Theorem pythagtriplem17

Proof