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 subdir โŠข ( ( 4 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) โˆˆ โ„‚ ) โ†’ ( ( 4 โˆ’ 2 ) ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) = ( ( 4 ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) โˆ’ ( 2 ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) ) )
34 32 7 10 33 mp3an12i โŠข ( ( ๐‘› โˆˆ โ„‚ โˆง ๐‘š โˆˆ โ„‚ ) โ†’ ( ( 4 โˆ’ 2 ) ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) = ( ( 4 ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) โˆ’ ( 2 ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) ) )
35 2p2e4 โŠข ( 2 + 2 ) = 4
36 32 7 7 35 subaddrii โŠข ( 4 โˆ’ 2 ) = 2
37 36 oveq1i โŠข ( ( 4 โˆ’ 2 ) ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) ) = ( 2 ยท ( ( ๐‘š โ†‘ 2 ) ยท ( ๐‘› โ†‘ 2 ) ) )
38 34 37 eqtr3di โŠข ( ( ๐‘› โˆˆ โ„‚ โˆง ๐‘š โˆˆ โ„‚ ) โ†’ ( ( 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 ) )