Metamath Proof Explorer

Theorem 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 ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
2 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
3 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
4 sqcl ⊢ ( 𝑚 ∈ ℂ → ( 𝑚 ↑ 2 ) ∈ ℂ )
5 4 adantl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑚 ↑ 2 ) ∈ ℂ )
6 5 sqcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 𝑚 ↑ 2 ) ↑ 2 ) ∈ ℂ )
7 2cn ⊢ 2 ∈ ℂ
8 sqcl ⊢ ( 𝑛 ∈ ℂ → ( 𝑛 ↑ 2 ) ∈ ℂ )
9 mulcl ⊢ ( ( ( 𝑚 ↑ 2 ) ∈ ℂ ∧ ( 𝑛 ↑ 2 ) ∈ ℂ ) → ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ∈ ℂ )
10 4 8 9 syl2anr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ∈ ℂ )
11 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ∈ ℂ ) → ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ∈ ℂ )
12 7 10 11 sylancr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ∈ ℂ )
13 6 12 subcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) ∈ ℂ )
14 8 adantr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
15 14 sqcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 𝑛 ↑ 2 ) ↑ 2 ) ∈ ℂ )
16 mulcl ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑚 · 𝑛 ) ∈ ℂ )
17 16 ancoms ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑚 · 𝑛 ) ∈ ℂ )
18 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑚 · 𝑛 ) ∈ ℂ ) → ( 2 · ( 𝑚 · 𝑛 ) ) ∈ ℂ )
19 7 17 18 sylancr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 2 · ( 𝑚 · 𝑛 ) ) ∈ ℂ )
20 19 sqcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ∈ ℂ )
21 13 15 20 add32d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
22 6 12 20 subadd23d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) ) )
23 sqmul ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑚 · 𝑛 ) ∈ ℂ ) → ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑚 · 𝑛 ) ↑ 2 ) ) )
24 7 17 23 sylancr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑚 · 𝑛 ) ↑ 2 ) ) )
25 sq2 ⊢ ( 2 ↑ 2 ) = 4
26 25 a1i ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 2 ↑ 2 ) = 4 )
27 sqmul ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑚 · 𝑛 ) ↑ 2 ) = ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) )
28 27 ancoms ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 𝑚 · 𝑛 ) ↑ 2 ) = ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) )
29 26 28 oveq12d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 2 ↑ 2 ) · ( ( 𝑚 · 𝑛 ) ↑ 2 ) ) = ( 4 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) )
30 24 29 eqtrd ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) = ( 4 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) )
31 30 oveq1d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) = ( ( 4 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) )
32 4cn ⊢ 4 ∈ ℂ
33 2p2e4 ⊢ ( 2 + 2 ) = 4
34 32 7 7 33 subaddrii ⊢ ( 4 − 2 ) = 2
35 34 oveq1i ⊢ ( ( 4 − 2 ) · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) = ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) )
36 subdir ⊢ ( ( 4 ∈ ℂ ∧ 2 ∈ ℂ ∧ ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ∈ ℂ ) → ( ( 4 − 2 ) · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) = ( ( 4 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) )
37 32 7 10 36 mp3an12i ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 4 − 2 ) · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) = ( ( 4 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) )
38 35 37 syl5reqr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( 4 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) = ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) )
39 31 38 eqtrd ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) = ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) )
40 39 oveq2d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) ) = ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) )
41 22 40 eqtrd ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) )
42 41 oveq1d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) = ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
43 21 42 eqtrd ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
44 binom2sub ⊢ ( ( ( 𝑚 ↑ 2 ) ∈ ℂ ∧ ( 𝑛 ↑ 2 ) ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) = ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
45 4 8 44 syl2anr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) = ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
46 45 oveq1d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) − ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) )
47 binom2 ⊢ ( ( ( 𝑚 ↑ 2 ) ∈ ℂ ∧ ( 𝑛 ↑ 2 ) ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↑ 2 ) = ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
48 4 8 47 syl2anr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↑ 2 ) = ( ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( 2 · ( ( 𝑚 ↑ 2 ) · ( 𝑛 ↑ 2 ) ) ) ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
49 43 46 48 3eqtr4d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↑ 2 ) )
50 49 3adant3 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) = ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↑ 2 ) )
51 50 oveq2d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 ↑ 2 ) · ( ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) ) = ( ( 𝑘 ↑ 2 ) · ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↑ 2 ) ) )
52 simp3 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → 𝑘 ∈ ℂ )
53 4 3ad2ant2 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑚 ↑ 2 ) ∈ ℂ )
54 8 3ad2ant1 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
55 53 54 subcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ∈ ℂ )
56 52 55 sqmuld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) ) )
57 17 3adant3 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑚 · 𝑛 ) ∈ ℂ )
58 7 57 18 sylancr ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 2 · ( 𝑚 · 𝑛 ) ) ∈ ℂ )
59 52 58 sqmuld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) )
60 56 59 oveq12d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) = ( ( ( 𝑘 ↑ 2 ) · ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) ) + ( ( 𝑘 ↑ 2 ) · ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) ) )
61 sqcl ⊢ ( 𝑘 ∈ ℂ → ( 𝑘 ↑ 2 ) ∈ ℂ )
62 61 3ad2ant3 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑘 ↑ 2 ) ∈ ℂ )
63 55 sqcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) ∈ ℂ )
64 58 sqcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ∈ ℂ )
65 62 63 64 adddid ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 ↑ 2 ) · ( ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) ) = ( ( ( 𝑘 ↑ 2 ) · ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) ) + ( ( 𝑘 ↑ 2 ) · ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) ) )
66 60 65 eqtr4d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) = ( ( 𝑘 ↑ 2 ) · ( ( ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ↑ 2 ) + ( ( 2 · ( 𝑚 · 𝑛 ) ) ↑ 2 ) ) ) )
67 53 54 addcld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ∈ ℂ )
68 52 67 sqmuld ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ↑ 2 ) ) )
69 51 66 68 3eqtr4d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) = ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) )
70 1 2 3 69 syl3an ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) = ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) )
71 oveq1 ⊢ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) → ( 𝐴 ↑ 2 ) = ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) )
72 oveq1 ⊢ ( 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) → ( 𝐵 ↑ 2 ) = ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) )
73 71 72 oveqan12d ⊢ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) )
74 73 3adant3 ⊢ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) )
75 oveq1 ⊢ ( 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) → ( 𝐶 ↑ 2 ) = ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) )
76 75 3ad2ant3 ⊢ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( 𝐶 ↑ 2 ) = ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) )
77 74 76 eqeq12d ⊢ ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ↔ ( ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) + ( ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ↑ 2 ) ) = ( ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ↑ 2 ) ) )
78 70 77 syl5ibrcom ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
79 78 3expa ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
80 79 rexlimdva ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ) )
81 80 rexlimivv ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ∃ 𝑘 ∈ ℕ ( 𝐴 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) − ( 𝑛 ↑ 2 ) ) ) ∧ 𝐵 = ( 𝑘 · ( 2 · ( 𝑚 · 𝑛 ) ) ) ∧ 𝐶 = ( 𝑘 · ( ( 𝑚 ↑ 2 ) + ( 𝑛 ↑ 2 ) ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )