Theorem pythagtriplem1 16350

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

Assertion

Ref	Expression
pythagtriplem1	⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))

Distinct variable groups:   𝐴,𝑛,𝑚,𝑘   𝐵,𝑛,𝑚,𝑘   𝐶,𝑛,𝑚,𝑘

Proof of Theorem pythagtriplem1

Step	Hyp	Ref	Expression
1		nncn 11821	. . . . . 6 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
2		nncn 11821	. . . . . 6 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
3		nncn 11821	. . . . . 6 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
4		sqcl 13673	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℂ → (𝑚↑2) ∈ ℂ)
5	4	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑚↑2) ∈ ℂ)
6	5	sqcld 13697	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚↑2)↑2) ∈ ℂ)
7		2cn 11888	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
8		sqcl 13673	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℂ → (𝑛↑2) ∈ ℂ)
9		mulcl 10796	. . . . . . . . . . . . . . 15 ⊢ (((𝑚↑2) ∈ ℂ ∧ (𝑛↑2) ∈ ℂ) → ((𝑚↑2) · (𝑛↑2)) ∈ ℂ)
10	4, 8, 9	syl2anr 600	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚↑2) · (𝑛↑2)) ∈ ℂ)
11		mulcl 10796	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ ((𝑚↑2) · (𝑛↑2)) ∈ ℂ) → (2 · ((𝑚↑2) · (𝑛↑2))) ∈ ℂ)
12	7, 10, 11	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · ((𝑚↑2) · (𝑛↑2))) ∈ ℂ)
13	6, 12	subcld 11172	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) ∈ ℂ)
14	8	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑛↑2) ∈ ℂ)
15	14	sqcld 13697	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑛↑2)↑2) ∈ ℂ)
16		mulcl 10796	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ)
17	16	ancoms 462	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ)
18		mulcl 10796	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ (𝑚 · 𝑛) ∈ ℂ) → (2 · (𝑚 · 𝑛)) ∈ ℂ)
19	7, 17, 18	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · (𝑚 · 𝑛)) ∈ ℂ)
20	19	sqcld 13697	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2 · (𝑚 · 𝑛))↑2) ∈ ℂ)
21	13, 15, 20	add32d 11042	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)) = (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) + ((𝑛↑2)↑2)))
22	6, 12, 20	subadd23d 11194	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2)↑2) + (((2 · (𝑚 · 𝑛))↑2) − (2 · ((𝑚↑2) · (𝑛↑2))))))
23		sqmul 13674	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ (𝑚 · 𝑛) ∈ ℂ) → ((2 · (𝑚 · 𝑛))↑2) = ((2↑2) · ((𝑚 · 𝑛)↑2)))
24	7, 17, 23	sylancr 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2 · (𝑚 · 𝑛))↑2) = ((2↑2) · ((𝑚 · 𝑛)↑2)))
25		sq2 13749	. . . . . . . . . . . . . . . . . . 19 ⊢ (2↑2) = 4
26	25	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2↑2) = 4)
27		sqmul 13674	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑚 · 𝑛)↑2) = ((𝑚↑2) · (𝑛↑2)))
28	27	ancoms 462	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((𝑚 · 𝑛)↑2) = ((𝑚↑2) · (𝑛↑2)))
29	26, 28	oveq12d 7220	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2↑2) · ((𝑚 · 𝑛)↑2)) = (4 · ((𝑚↑2) · (𝑛↑2))))
30	24, 29	eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((2 · (𝑚 · 𝑛))↑2) = (4 · ((𝑚↑2) · (𝑛↑2))))
31	30	oveq1d 7217	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((2 · (𝑚 · 𝑛))↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) = ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 · ((𝑚↑2) · (𝑛↑2)))))
32		4cn 11898	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℂ
33		subdir 11249	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 2 ∈ ℂ ∧ ((𝑚↑2) · (𝑛↑2)) ∈ ℂ) → ((4 − 2) · ((𝑚↑2) · (𝑛↑2))) = ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 · ((𝑚↑2) · (𝑛↑2)))))
34	32, 7, 10, 33	mp3an12i 1467	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((4 − 2) · ((𝑚↑2) · (𝑛↑2))) = ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 · ((𝑚↑2) · (𝑛↑2)))))
35		2p2e4 11948	. . . . . . . . . . . . . . . . . 18 ⊢ (2 + 2) = 4
36	32, 7, 7, 35	subaddrii 11150	. . . . . . . . . . . . . . . . 17 ⊢ (4 − 2) = 2
37	36	oveq1i 7212	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 2) · ((𝑚↑2) · (𝑛↑2))) = (2 · ((𝑚↑2) · (𝑛↑2)))
38	34, 37	eqtr3di 2789	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((4 · ((𝑚↑2) · (𝑛↑2))) − (2 · ((𝑚↑2) · (𝑛↑2)))) = (2 · ((𝑚↑2) · (𝑛↑2))))
39	31, 38	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((2 · (𝑚 · 𝑛))↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) = (2 · ((𝑚↑2) · (𝑛↑2))))
40	39	oveq2d 7218	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2)↑2) + (((2 · (𝑚 · 𝑛))↑2) − (2 · ((𝑚↑2) · (𝑛↑2))))) = (((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))))
41	22, 40	eqtrd 2774	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))))
42	41	oveq1d 7217	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((2 · (𝑚 · 𝑛))↑2)) + ((𝑛↑2)↑2)) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)))
43	21, 42	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)))
44		binom2sub 13770	. . . . . . . . . . . 12 ⊢ (((𝑚↑2) ∈ ℂ ∧ (𝑛↑2) ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) = ((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)))
45	4, 8, 44	syl2anr 600	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) = ((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)))
46	45	oveq1d 7217	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2)) = (((((𝑚↑2)↑2) − (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)) + ((2 · (𝑚 · 𝑛))↑2)))
47		binom2 13768	. . . . . . . . . . 11 ⊢ (((𝑚↑2) ∈ ℂ ∧ (𝑛↑2) ∈ ℂ) → (((𝑚↑2) + (𝑛↑2))↑2) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)))
48	4, 8, 47	syl2anr 600	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (((𝑚↑2) + (𝑛↑2))↑2) = ((((𝑚↑2)↑2) + (2 · ((𝑚↑2) · (𝑛↑2)))) + ((𝑛↑2)↑2)))
49	43, 46, 48	3eqtr4d 2784	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ) → ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2) + (𝑛↑2))↑2))
50	49	3adant3 1134	. . . . . . . 8 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2)) = (((𝑚↑2) + (𝑛↑2))↑2))
51	50	oveq2d 7218	. . . . . . 7 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2))) = ((𝑘↑2) · (((𝑚↑2) + (𝑛↑2))↑2)))
52		simp3 1140	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → 𝑘 ∈ ℂ)
53	4	3ad2ant2 1136	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚↑2) ∈ ℂ)
54	8	3ad2ant1 1135	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑛↑2) ∈ ℂ)
55	53, 54	subcld 11172	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚↑2) − (𝑛↑2)) ∈ ℂ)
56	52, 55	sqmuld 13711	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) = ((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)))
57	17	3adant3 1134	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 · 𝑛) ∈ ℂ)
58	7, 57, 18	sylancr 590	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · (𝑚 · 𝑛)) ∈ ℂ)
59	52, 58	sqmuld 13711	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · (2 · (𝑚 · 𝑛)))↑2) = ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2)))
60	56, 59	oveq12d 7220	. . . . . . . 8 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = (((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)) + ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2))))
61		sqcl 13673	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℂ → (𝑘↑2) ∈ ℂ)
62	61	3ad2ant3 1137	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘↑2) ∈ ℂ)
63	55	sqcld 13697	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑚↑2) − (𝑛↑2))↑2) ∈ ℂ)
64	58	sqcld 13697	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2 · (𝑚 · 𝑛))↑2) ∈ ℂ)
65	62, 63, 64	adddid 10840	. . . . . . . 8 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2))) = (((𝑘↑2) · (((𝑚↑2) − (𝑛↑2))↑2)) + ((𝑘↑2) · ((2 · (𝑚 · 𝑛))↑2))))
66	60, 65	eqtr4d 2777	. . . . . . 7 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘↑2) · ((((𝑚↑2) − (𝑛↑2))↑2) + ((2 · (𝑚 · 𝑛))↑2))))
67	53, 54	addcld 10835	. . . . . . . 8 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚↑2) + (𝑛↑2)) ∈ ℂ)
68	52, 67	sqmuld 13711	. . . . . . 7 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2) = ((𝑘↑2) · (((𝑚↑2) + (𝑛↑2))↑2)))
69	51, 66, 68	3eqtr4d 2784	. . . . . 6 ⊢ ((𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2))
70	1, 2, 3, 69	syl3an 1162	. . . . 5 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2))
71		oveq1 7209	. . . . . . . 8 ⊢ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) → (𝐴↑2) = ((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2))
72		oveq1 7209	. . . . . . . 8 ⊢ (𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) → (𝐵↑2) = ((𝑘 · (2 · (𝑚 · 𝑛)))↑2))
73	71, 72	oveqan12d 7221	. . . . . . 7 ⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛)))) → ((𝐴↑2) + (𝐵↑2)) = (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)))
74	73	3adant3 1134	. . . . . 6 ⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)))
75		oveq1 7209	. . . . . . 7 ⊢ (𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))) → (𝐶↑2) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2))
76	75	3ad2ant3 1137	. . . . . 6 ⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → (𝐶↑2) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2))
77	74, 76	eqeq12d 2750	. . . . 5 ⊢ ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ (((𝑘 · ((𝑚↑2) − (𝑛↑2)))↑2) + ((𝑘 · (2 · (𝑚 · 𝑛)))↑2)) = ((𝑘 · ((𝑚↑2) + (𝑛↑2)))↑2)))
78	70, 77	syl5ibrcom 250	. . . 4 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
79	78	3expa 1120	. . 3 ⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
80	79	rexlimdva 3196	. 2 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
81	80	rexlimivv 3204	1 ⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  ∃wrex 3055  (class class class)co 7202  ℂcc 10710   + caddc 10715   · cmul 10717   − cmin 11045  ℕcn 11813  2c2 11868  4c4 11870  ↑cexp 13618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-iun 4896  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-om 7634  df-2nd 7751  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-er 8380  df-en 8616  df-dom 8617  df-sdom 8618  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-nn 11814  df-2 11876  df-3 11877  df-4 11878  df-n0 12074  df-z 12160  df-uz 12422  df-seq 13558  df-exp 13619

This theorem is referenced by:  pythagtriplem2  16351