pythagtriplem18

Description: Lemma for pythagtrip . Wrap the previous M and N up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	pythagtriplem18	$⊢ ((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 \exists n \in ℕ \exists m \in ℕ (A = m^{2} - n^{2} \land B = 2 m n \land C = m^{2} + n^{2})$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ \frac{\sqrt{C + B} - \sqrt{C - B}}{2} = \frac{\sqrt{C + B} - \sqrt{C - B}}{2}$
2	1	pythagtriplem13	$⊢ ((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{\sqrt{C + B} - \sqrt{C - B}}{2} \in ℕ$
3		eqid	$⊢ \frac{\sqrt{C + B} + \sqrt{C - B}}{2} = \frac{\sqrt{C + B} + \sqrt{C - B}}{2}$
4	3	pythagtriplem11	$⊢ ((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{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℕ$
5	3 1	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 = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
6	3 1	pythagtriplem16	$⊢ ((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 B = 2 (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2})$
7	3 1	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 = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
8		oveq1	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to n^{2} = {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
9	8	oveq2d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to m^{2} - n^{2} = m^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
10	9	eqeq2d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to (A = m^{2} - n^{2} \leftrightarrow A = m^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2})$
11		oveq2	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to m n = m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2})$
12	11	oveq2d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to 2 m n = 2 m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2})$
13	12	eqeq2d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to (B = 2 m n \leftrightarrow B = 2 m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}))$
14	8	oveq2d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to m^{2} + n^{2} = m^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
15	14	eqeq2d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to (C = m^{2} + n^{2} \leftrightarrow C = m^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2})$
16	10 13 15	3anbi123d	$⊢ n = \frac{\sqrt{C + B} - \sqrt{C - B}}{2} \to ((A = m^{2} - n^{2} \land B = 2 m n \land C = m^{2} + n^{2}) \leftrightarrow (A = m^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} \land B = 2 m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) \land C = m^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}))$
17		oveq1	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to m^{2} = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2}$
18	17	oveq1d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to m^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
19	18	eqeq2d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to (A = m^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} \leftrightarrow A = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2})$
20		oveq1	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2})$
21	20	oveq2d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to 2 m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) = 2 (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2})$
22	21	eqeq2d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to (B = 2 m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) \leftrightarrow B = 2 (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}))$
23	17	oveq1d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to m^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}$
24	23	eqeq2d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to (C = m^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} \leftrightarrow C = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2})$
25	19 22 24	3anbi123d	$⊢ m = \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \to ((A = m^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} \land B = 2 m (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) \land C = m^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}) \leftrightarrow (A = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} \land B = 2 (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) \land C = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2}))$
26	16 25	rspc2ev	$⊢ (\frac{\sqrt{C + B} - \sqrt{C - B}}{2} \in ℕ \land \frac{\sqrt{C + B} + \sqrt{C - B}}{2} \in ℕ \land (A = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} - {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2} \land B = 2 (\frac{\sqrt{C + B} + \sqrt{C - B}}{2}) (\frac{\sqrt{C + B} - \sqrt{C - B}}{2}) \land C = {(\frac{\sqrt{C + B} + \sqrt{C - B}}{2})}^{2} + {(\frac{\sqrt{C + B} - \sqrt{C - B}}{2})}^{2})) \to \exists n \in ℕ \exists m \in ℕ (A = m^{2} - n^{2} \land B = 2 m n \land C = m^{2} + n^{2})$
27	2 4 5 6 7 26	syl113anc	$⊢ ((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 \exists n \in ℕ \exists m \in ℕ (A = m^{2} - n^{2} \land B = 2 m n \land C = m^{2} + n^{2})$

Metamath Proof Explorer

Theorem pythagtriplem18

Proof