Metamath Proof Explorer

Theorem pythagtriplem2

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

Ref Expression
Assertion pythagtriplem2 ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 ovex โŠข ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆˆ V
2 ovex โŠข ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆˆ V
3 preq12bg โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โˆง ( ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆˆ V โˆง ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆˆ V ) ) โ†’ ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
4 1 2 3 mpanr12 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
5 4 anbi1d โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
6 andir โŠข ( ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
7 df-3an โŠข ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
8 df-3an โŠข ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
9 7 8 orbi12i โŠข ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
10 6 9 bitr4i โŠข ( ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
11 5 10 bitrdi โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
12 11 rexbidv โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
13 12 2rexbidv โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
14 r19.43 โŠข ( โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
15 14 2rexbii โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
16 r19.43 โŠข ( โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
17 16 rexbii โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• ( โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
18 r19.43 โŠข ( โˆƒ ๐‘› โˆˆ โ„• ( โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
19 15 17 18 3bitri โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
20 13 19 bitrdi โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
21 pythagtriplem1 โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) )
22 21 a1i โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
23 3ancoma โŠข ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
24 23 rexbii โŠข ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
25 24 2rexbii โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
26 pythagtriplem1 โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) )
27 25 26 sylbi โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) )
28 nncn โŠข ( ๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„‚ )
29 28 sqcld โŠข ( ๐ด โˆˆ โ„• โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„‚ )
30 nncn โŠข ( ๐ต โˆˆ โ„• โ†’ ๐ต โˆˆ โ„‚ )
31 30 sqcld โŠข ( ๐ต โˆˆ โ„• โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„‚ )
32 addcom โŠข ( ( ( ๐ด โ†‘ 2 ) โˆˆ โ„‚ โˆง ( ๐ต โ†‘ 2 ) โˆˆ โ„‚ ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) )
33 29 31 32 syl2an โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) )
34 33 eqeq1d โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โ†” ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
35 27 34 imbitrrid โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
36 22 35 jaod โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
37 20 36 sylbid โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )