pythagtrip

Description: Parameterize the Pythagorean triples. If A , B , and C are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml . This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		divgcdodd	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$
2	1	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$
3	2	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B}))$
4		pythagtriplem19	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{A}{A \gcd B})) \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}))$
5	4	3expia	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (\neg 2 ∥ (\frac{A}{A \gcd B}) \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})))$
6		simp12	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{A \gcd B})) \to B \in ℕ$
7		simp11	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{A \gcd B})) \to A \in ℕ$
8		simp13	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{A \gcd B})) \to C \in ℕ$
9		nnsqcl	$⊢ A \in ℕ \to A^{2} \in ℕ$
10	9	nncnd	$⊢ A \in ℕ \to A^{2} \in ℂ$
11	10	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} \in ℂ$
12		nnsqcl	$⊢ B \in ℕ \to B^{2} \in ℕ$
13	12	nncnd	$⊢ B \in ℕ \to B^{2} \in ℂ$
14	13	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B^{2} \in ℂ$
15	11 14	addcomd	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A^{2} + B^{2} = B^{2} + A^{2}$
16	15	eqeq1d	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A^{2} + B^{2} = C^{2} \leftrightarrow B^{2} + A^{2} = C^{2})$
17	16	biimpa	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B^{2} + A^{2} = C^{2}$
18	17	3adant3	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{A \gcd B})) \to B^{2} + A^{2} = C^{2}$
19		nnz	$⊢ A \in ℕ \to A \in ℤ$
20	19	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to A \in ℤ$
21		nnz	$⊢ B \in ℕ \to B \in ℤ$
22	21	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to B \in ℤ$
23	22	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to B \in ℤ$
24		gcdcom	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B = B \gcd A$
25	20 23 24	syl2an2r	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to A \gcd B = B \gcd A$
26	25	oveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to \frac{B}{A \gcd B} = \frac{B}{B \gcd A}$
27	26	breq2d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (2 ∥ (\frac{B}{A \gcd B}) \leftrightarrow 2 ∥ (\frac{B}{B \gcd A}))$
28	27	notbid	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (\neg 2 ∥ (\frac{B}{A \gcd B}) \leftrightarrow \neg 2 ∥ (\frac{B}{B \gcd A}))$
29	28	biimp3a	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{A \gcd B})) \to \neg 2 ∥ (\frac{B}{B \gcd A})$
30		pythagtriplem19	$⊢ ((B \in ℕ \land A \in ℕ \land C \in ℕ) \land B^{2} + A^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{B \gcd A})) \to \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}))$
31	6 7 8 18 29 30	syl311anc	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2} \land \neg 2 ∥ (\frac{B}{A \gcd B})) \to \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}))$
32	31	3expia	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to (\neg 2 ∥ (\frac{B}{A \gcd B}) \to \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})))$
33	5 32	orim12d	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \to ((\neg 2 ∥ (\frac{A}{A \gcd B}) \lor \neg 2 ∥ (\frac{B}{A \gcd B})) \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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))))$
34	3 33	mpd	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
35		ovex	$⊢ k (m^{2} - n^{2}) \in V$
36		ovex	$⊢ k 2 m n \in V$
37		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}))))$
38	35 36 37	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}))))$
39	38	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})))$
40	39	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) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))) \land C = k (m^{2} + n^{2})))$
41	40	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) \lor (A = k 2 m n \land B = k (m^{2} - n^{2}))) \land C = k (m^{2} + n^{2})))$
42		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})))$
43		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}))$
44		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}))$
45	43 44	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})))$
46		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}))$
47	46	orbi2i	$⊢ ((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 (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
48	42 45 47	3bitr2i	$⊢ (((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 (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
49	48	rexbii	$⊢ \exists k \in ℕ (((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 \exists k \in ℕ ((A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \lor (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
50	49	2rexbii	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (((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 \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 (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
51		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 (B = k (m^{2} - n^{2}) \land A = 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 \exists k \in ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
52	51	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 (B = k (m^{2} - n^{2}) \land A = 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 k \in ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
53		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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
54	53	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 ℕ (B = k (m^{2} - n^{2}) \land A = 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 m \in ℕ \exists k \in ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
55		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 ℕ (B = k (m^{2} - n^{2}) \land A = 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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
56	54 55	bitri	$⊢ \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 ℕ (B = k (m^{2} - n^{2}) \land A = 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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
57	52 56	bitri	$⊢ \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 (B = k (m^{2} - n^{2}) \land A = 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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
58	50 57	bitri	$⊢ \exists n \in ℕ \exists m \in ℕ \exists k \in ℕ (((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 (\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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2})))$
59	41 58	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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))))$
60	59	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land C \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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))))$
61	60	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \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 ℕ (B = k (m^{2} - n^{2}) \land A = k 2 m n \land C = k (m^{2} + n^{2}))))$
62	34 61	mpbird	$⊢ ((A \in ℕ \land B \in ℕ \land C \in ℕ) \land A^{2} + B^{2} = C^{2}) \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}))$
63	62	ex	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A^{2} + B^{2} = C^{2} \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})))$
64		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})$
65	64	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land C \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})$
66	63 65	impbid	$⊢ (A \in ℕ \land B \in ℕ \land C \in ℕ) \to (A^{2} + B^{2} = C^{2} \leftrightarrow \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})))$

Metamath Proof Explorer

Theorem pythagtrip

Proof