pythagtriplem2

Description: Lemma for pythagtrip . Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	pythagtriplem2	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \to A^{2} + B^{2} = C^{2})$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ k (m^{2} - n^{2}) \in V$
2		ovex	$⊢ k 2 m n \in V$
3		preq12bg	$⊢ ((A \in ℕ \land B \in ℕ) \land (k (m^{2} - n^{2}) \in V \land k 2 m n \in V)) \to (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \leftrightarrow ((A = k (m^{2} - n^{2}) \land B = k 2 m n) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))))$
4	1 2 3	mpanr12	$⊢ (A \in ℕ \land B \in ℕ) \to (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \leftrightarrow ((A = k (m^{2} - n^{2}) \land B = k 2 m n) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))))$
5	4	anbi1d	$⊢ (A \in ℕ \land B \in ℕ) \to ((\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \leftrightarrow (((A = k (m^{2} - n^{2}) \land B = k 2 m n) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))) \land C = k (m^{2} + n^{2})))$
6		andir	$⊢ (((A = k (m^{2} - n^{2}) \land B = k 2 m n) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))) \land C = k (m^{2} + n^{2})) \leftrightarrow (((A = k (m^{2} - n^{2}) \land B = k 2 m n) \land C = k (m^{2} + n^{2})) \lor ((A = k 2 m n \land B = k (m^{2} - n^{2})) \land C = k (m^{2} + n^{2})))$
7		df-3an	$⊢ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \leftrightarrow ((A = k (m^{2} - n^{2}) \land B = k 2 m n) \land C = k (m^{2} + n^{2}))$
8		df-3an	$⊢ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})) \leftrightarrow ((A = k 2 m n \land B = k (m^{2} - n^{2})) \land C = k (m^{2} + n^{2}))$
9	7 8	orbi12i	$⊢ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow (((A = k (m^{2} - n^{2}) \land B = k 2 m n) \land C = k (m^{2} + n^{2})) \lor ((A = k 2 m n \land B = k (m^{2} - n^{2})) \land C = k (m^{2} + n^{2})))$
10	6 9	bitr4i	$⊢ (((A = k (m^{2} - n^{2}) \land B = k 2 m n) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))) \land C = k (m^{2} + n^{2})) \leftrightarrow ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
11	5 10	bitrdi	$⊢ (A \in ℕ \land B \in ℕ) \to ((\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \leftrightarrow ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))))$
12	11	rexbidv	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists k \in ℕ (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \leftrightarrow \exists k \in ℕ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))))$
13	12	2rexbidv	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \leftrightarrow \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))))$
14		r19.43	$⊢ \exists k \in ℕ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow (\exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
15	14	2rexbii	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow \exists n \in ℕ \exists m \in ℕ (\exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
16		r19.43	$⊢ \exists m \in ℕ (\exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow (\exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
17	16	rexbii	$⊢ \exists n \in ℕ \exists m \in ℕ (\exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow \exists n \in ℕ (\exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
18		r19.43	$⊢ \exists n \in ℕ (\exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
19	15 17 18	3bitri	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \leftrightarrow (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})))$
20	13 19	bitrdi	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \leftrightarrow (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))))$
21		pythagtriplem1	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \to A^{2} + B^{2} = C^{2}$
22	21	a1i	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \to A^{2} + B^{2} = C^{2})$
23		3ancoma	$⊢ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})) \leftrightarrow (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))$
24	23	rexbii	$⊢ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})) \leftrightarrow \exists k \in ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))$
25	24	2rexbii	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})) \leftrightarrow \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))$
26		pythagtriplem1	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})) \to B^{2} + A^{2} = C^{2}$
27	25 26	sylbi	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})) \to B^{2} + A^{2} = C^{2}$
28		nncn	$⊢ A \in ℕ \to A \in ℂ$
29	28	sqcld	$⊢ A \in ℕ \to A^{2} \in ℂ$
30		nncn	$⊢ B \in ℕ \to B \in ℂ$
31	30	sqcld	$⊢ B \in ℕ \to B^{2} \in ℂ$
32		addcom	$⊢ (A^{2} \in ℂ \land B^{2} \in ℂ) \to A^{2} + B^{2} = B^{2} + A^{2}$
33	29 31 32	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to A^{2} + B^{2} = B^{2} + A^{2}$
34	33	eqeq1d	$⊢ (A \in ℕ \land B \in ℕ) \to (A^{2} + B^{2} = C^{2} \leftrightarrow B^{2} + A^{2} = C^{2})$
35	27 34	syl5ibr	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2})) \to A^{2} + B^{2} = C^{2})$
36	22 35	jaod	$⊢ (A \in ℕ \land B \in ℕ) \to ((\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (A = k 2 m n \land B = k (m^{2} - n^{2}) \land C = k (m^{2} + n^{2}))) \to A^{2} + B^{2} = C^{2})$
37	20 36	sylbid	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (\{A, B\} = \{k (m^{2} - n^{2}), k 2 m n\} \land C = k (m^{2} + n^{2})) \to A^{2} + B^{2} = C^{2})$

Metamath Proof Explorer

Theorem pythagtriplem2

Proof