pythagtriplem1

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

		Ref	Expression
	Assertion	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}$

Proof

Step	Hyp	Ref	Expression
1		nncn	$⊢ n \in ℕ \to n \in ℂ$
2		nncn	$⊢ m \in ℕ \to m \in ℂ$
3		nncn	$⊢ k \in ℕ \to k \in ℂ$
4		sqcl	$⊢ m \in ℂ \to m^{2} \in ℂ$
5	4	adantl	$⊢ (n \in ℂ \land m \in ℂ) \to m^{2} \in ℂ$
6	5	sqcld	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2})}^{2} \in ℂ$
7		2cn	$⊢ 2 \in ℂ$
8		sqcl	$⊢ n \in ℂ \to n^{2} \in ℂ$
9		mulcl	$⊢ (m^{2} \in ℂ \land n^{2} \in ℂ) \to m^{2} n^{2} \in ℂ$
10	4 8 9	syl2anr	$⊢ (n \in ℂ \land m \in ℂ) \to m^{2} n^{2} \in ℂ$
11		mulcl	$⊢ (2 \in ℂ \land m^{2} n^{2} \in ℂ) \to 2 m^{2} n^{2} \in ℂ$
12	7 10 11	sylancr	$⊢ (n \in ℂ \land m \in ℂ) \to 2 m^{2} n^{2} \in ℂ$
13	6 12	subcld	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2})}^{2} - 2 m^{2} n^{2} \in ℂ$
14	8	adantr	$⊢ (n \in ℂ \land m \in ℂ) \to n^{2} \in ℂ$
15	14	sqcld	$⊢ (n \in ℂ \land m \in ℂ) \to {(n^{2})}^{2} \in ℂ$
16		mulcl	$⊢ (m \in ℂ \land n \in ℂ) \to m n \in ℂ$
17	16	ancoms	$⊢ (n \in ℂ \land m \in ℂ) \to m n \in ℂ$
18		mulcl	$⊢ (2 \in ℂ \land m n \in ℂ) \to 2 m n \in ℂ$
19	7 17 18	sylancr	$⊢ (n \in ℂ \land m \in ℂ) \to 2 m n \in ℂ$
20	19	sqcld	$⊢ (n \in ℂ \land m \in ℂ) \to {2 m n}^{2} \in ℂ$
21	13 15 20	add32d	$⊢ (n \in ℂ \land m \in ℂ) \to ({(m^{2})}^{2} - 2 m^{2} n^{2}) + {(n^{2})}^{2} + {2 m n}^{2} = ({(m^{2})}^{2} - 2 m^{2} n^{2}) + {2 m n}^{2} + {(n^{2})}^{2}$
22	6 12 20	subadd23d	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2})}^{2} - 2 m^{2} n^{2} + {2 m n}^{2} = {(m^{2})}^{2} + {2 m n}^{2} - 2 m^{2} n^{2}$
23		sqmul	$⊢ (2 \in ℂ \land m n \in ℂ) \to {2 m n}^{2} = 2^{2} {m n}^{2}$
24	7 17 23	sylancr	$⊢ (n \in ℂ \land m \in ℂ) \to {2 m n}^{2} = 2^{2} {m n}^{2}$
25		sq2	$⊢ 2^{2} = 4$
26	25	a1i	$⊢ (n \in ℂ \land m \in ℂ) \to 2^{2} = 4$
27		sqmul	$⊢ (m \in ℂ \land n \in ℂ) \to {m n}^{2} = m^{2} n^{2}$
28	27	ancoms	$⊢ (n \in ℂ \land m \in ℂ) \to {m n}^{2} = m^{2} n^{2}$
29	26 28	oveq12d	$⊢ (n \in ℂ \land m \in ℂ) \to 2^{2} {m n}^{2} = 4 m^{2} n^{2}$
30	24 29	eqtrd	$⊢ (n \in ℂ \land m \in ℂ) \to {2 m n}^{2} = 4 m^{2} n^{2}$
31	30	oveq1d	$⊢ (n \in ℂ \land m \in ℂ) \to {2 m n}^{2} - 2 m^{2} n^{2} = 4 m^{2} n^{2} - 2 m^{2} n^{2}$
32		4cn	$⊢ 4 \in ℂ$
33		subdir	$⊢ (4 \in ℂ \land 2 \in ℂ \land m^{2} n^{2} \in ℂ) \to (4 - 2) m^{2} n^{2} = 4 m^{2} n^{2} - 2 m^{2} n^{2}$
34	32 7 10 33	mp3an12i	$⊢ (n \in ℂ \land m \in ℂ) \to (4 - 2) m^{2} n^{2} = 4 m^{2} n^{2} - 2 m^{2} n^{2}$
35		2p2e4	$⊢ 2 + 2 = 4$
36	32 7 7 35	subaddrii	$⊢ 4 - 2 = 2$
37	36	oveq1i	$⊢ (4 - 2) m^{2} n^{2} = 2 m^{2} n^{2}$
38	34 37	eqtr3di	$⊢ (n \in ℂ \land m \in ℂ) \to 4 m^{2} n^{2} - 2 m^{2} n^{2} = 2 m^{2} n^{2}$
39	31 38	eqtrd	$⊢ (n \in ℂ \land m \in ℂ) \to {2 m n}^{2} - 2 m^{2} n^{2} = 2 m^{2} n^{2}$
40	39	oveq2d	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2})}^{2} + {2 m n}^{2} - 2 m^{2} n^{2} = {(m^{2})}^{2} + 2 m^{2} n^{2}$
41	22 40	eqtrd	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2})}^{2} - 2 m^{2} n^{2} + {2 m n}^{2} = {(m^{2})}^{2} + 2 m^{2} n^{2}$
42	41	oveq1d	$⊢ (n \in ℂ \land m \in ℂ) \to ({(m^{2})}^{2} - 2 m^{2} n^{2}) + {2 m n}^{2} + {(n^{2})}^{2} = {(m^{2})}^{2} + 2 m^{2} n^{2} + {(n^{2})}^{2}$
43	21 42	eqtrd	$⊢ (n \in ℂ \land m \in ℂ) \to ({(m^{2})}^{2} - 2 m^{2} n^{2}) + {(n^{2})}^{2} + {2 m n}^{2} = {(m^{2})}^{2} + 2 m^{2} n^{2} + {(n^{2})}^{2}$
44		binom2sub	$⊢ (m^{2} \in ℂ \land n^{2} \in ℂ) \to {(m^{2} - n^{2})}^{2} = {(m^{2})}^{2} - 2 m^{2} n^{2} + {(n^{2})}^{2}$
45	4 8 44	syl2anr	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2} - n^{2})}^{2} = {(m^{2})}^{2} - 2 m^{2} n^{2} + {(n^{2})}^{2}$
46	45	oveq1d	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2} - n^{2})}^{2} + {2 m n}^{2} = ({(m^{2})}^{2} - 2 m^{2} n^{2}) + {(n^{2})}^{2} + {2 m n}^{2}$
47		binom2	$⊢ (m^{2} \in ℂ \land n^{2} \in ℂ) \to {(m^{2} + n^{2})}^{2} = {(m^{2})}^{2} + 2 m^{2} n^{2} + {(n^{2})}^{2}$
48	4 8 47	syl2anr	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2} + n^{2})}^{2} = {(m^{2})}^{2} + 2 m^{2} n^{2} + {(n^{2})}^{2}$
49	43 46 48	3eqtr4d	$⊢ (n \in ℂ \land m \in ℂ) \to {(m^{2} - n^{2})}^{2} + {2 m n}^{2} = {(m^{2} + n^{2})}^{2}$
50	49	3adant3	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {(m^{2} - n^{2})}^{2} + {2 m n}^{2} = {(m^{2} + n^{2})}^{2}$
51	50	oveq2d	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to k^{2} ({(m^{2} - n^{2})}^{2} + {2 m n}^{2}) = k^{2} {(m^{2} + n^{2})}^{2}$
52		simp3	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to k \in ℂ$
53	4	3ad2ant2	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to m^{2} \in ℂ$
54	8	3ad2ant1	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to n^{2} \in ℂ$
55	53 54	subcld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to m^{2} - n^{2} \in ℂ$
56	52 55	sqmuld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {k (m^{2} - n^{2})}^{2} = k^{2} {(m^{2} - n^{2})}^{2}$
57	17	3adant3	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to m n \in ℂ$
58	7 57 18	sylancr	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to 2 m n \in ℂ$
59	52 58	sqmuld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {k 2 m n}^{2} = k^{2} {2 m n}^{2}$
60	56 59	oveq12d	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2} = k^{2} {(m^{2} - n^{2})}^{2} + k^{2} {2 m n}^{2}$
61		sqcl	$⊢ k \in ℂ \to k^{2} \in ℂ$
62	61	3ad2ant3	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to k^{2} \in ℂ$
63	55	sqcld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {(m^{2} - n^{2})}^{2} \in ℂ$
64	58	sqcld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {2 m n}^{2} \in ℂ$
65	62 63 64	adddid	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to k^{2} ({(m^{2} - n^{2})}^{2} + {2 m n}^{2}) = k^{2} {(m^{2} - n^{2})}^{2} + k^{2} {2 m n}^{2}$
66	60 65	eqtr4d	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2} = k^{2} ({(m^{2} - n^{2})}^{2} + {2 m n}^{2})$
67	53 54	addcld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to m^{2} + n^{2} \in ℂ$
68	52 67	sqmuld	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {k (m^{2} + n^{2})}^{2} = k^{2} {(m^{2} + n^{2})}^{2}$
69	51 66 68	3eqtr4d	$⊢ (n \in ℂ \land m \in ℂ \land k \in ℂ) \to {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2} = {k (m^{2} + n^{2})}^{2}$
70	1 2 3 69	syl3an	$⊢ (n \in ℕ \land m \in ℕ \land k \in ℕ) \to {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2} = {k (m^{2} + n^{2})}^{2}$
71		oveq1	$⊢ A = k (m^{2} - n^{2}) \to A^{2} = {k (m^{2} - n^{2})}^{2}$
72		oveq1	$⊢ B = k 2 m n \to B^{2} = {k 2 m n}^{2}$
73	71 72	oveqan12d	$⊢ (A = k (m^{2} - n^{2}) \land B = k 2 m n) \to A^{2} + B^{2} = {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2}$
74	73	3adant3	$⊢ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \to A^{2} + B^{2} = {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2}$
75		oveq1	$⊢ C = k (m^{2} + n^{2}) \to C^{2} = {k (m^{2} + n^{2})}^{2}$
76	75	3ad2ant3	$⊢ (A = k (m^{2} - n^{2}) \land B = k 2 m n \land C = k (m^{2} + n^{2})) \to C^{2} = {k (m^{2} + n^{2})}^{2}$
77	74 76	eqeq12d	$⊢ (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} \leftrightarrow {k (m^{2} - n^{2})}^{2} + {k 2 m n}^{2} = {k (m^{2} + n^{2})}^{2})$
78	70 77	syl5ibrcom	$⊢ (n \in ℕ \land m \in ℕ \land k \in ℕ) \to ((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})$
79	78	3expa	$⊢ ((n \in ℕ \land m \in ℕ) \land k \in ℕ) \to ((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})$
80	79	rexlimdva	$⊢ (n \in ℕ \land m \in ℕ) \to (\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})$
81	80	rexlimivv	$⊢ \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}$

Metamath Proof Explorer

Theorem pythagtriplem1

Proof