Metamath Proof Explorer

Theorem pythagtrip

Description: Parameterize the Pythagorean triples. If A , B , and C are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml . This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 divgcdodd โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ยฌ 2 โˆฅ ( ๐ด / ( ๐ด gcd ๐ต ) ) โˆจ ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) )
2 1 3adant3 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ยฌ 2 โˆฅ ( ๐ด / ( ๐ด gcd ๐ต ) ) โˆจ ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) )
3 2 adantr โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ยฌ 2 โˆฅ ( ๐ด / ( ๐ด gcd ๐ต ) ) โˆจ ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) )
4 pythagtriplem19 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ด / ( ๐ด gcd ๐ต ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
5 4 3expia โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ยฌ 2 โˆฅ ( ๐ด / ( ๐ด gcd ๐ต ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
6 simp12 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ ๐ต โˆˆ โ„• )
7 simp11 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ ๐ด โˆˆ โ„• )
8 simp13 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ ๐ถ โˆˆ โ„• )
9 nnsqcl โŠข ( ๐ด โˆˆ โ„• โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„• )
10 9 nncnd โŠข ( ๐ด โˆˆ โ„• โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„‚ )
11 10 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ๐ด โ†‘ 2 ) โˆˆ โ„‚ )
12 nnsqcl โŠข ( ๐ต โˆˆ โ„• โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„• )
13 12 nncnd โŠข ( ๐ต โˆˆ โ„• โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„‚ )
14 13 3ad2ant2 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ๐ต โ†‘ 2 ) โˆˆ โ„‚ )
15 11 14 addcomd โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) )
16 15 eqeq1d โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โ†” ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
17 16 biimpa โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) )
18 17 3adant3 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) )
19 nnz โŠข ( ๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„ค )
20 19 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ๐ด โˆˆ โ„ค )
21 nnz โŠข ( ๐ต โˆˆ โ„• โ†’ ๐ต โˆˆ โ„ค )
22 21 3ad2ant2 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ๐ต โˆˆ โ„ค )
23 22 adantr โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ๐ต โˆˆ โ„ค )
24 gcdcom โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค ) โ†’ ( ๐ด gcd ๐ต ) = ( ๐ต gcd ๐ด ) )
25 20 23 24 syl2an2r โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ๐ด gcd ๐ต ) = ( ๐ต gcd ๐ด ) )
26 25 oveq2d โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ๐ต / ( ๐ด gcd ๐ต ) ) = ( ๐ต / ( ๐ต gcd ๐ด ) ) )
27 26 breq2d โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) โ†” 2 โˆฅ ( ๐ต / ( ๐ต gcd ๐ด ) ) ) )
28 27 notbid โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) โ†” ยฌ 2 โˆฅ ( ๐ต / ( ๐ต gcd ๐ด ) ) ) )
29 28 biimp3a โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ ยฌ 2 โˆฅ ( ๐ต / ( ๐ต gcd ๐ด ) ) )
30 pythagtriplem19 โŠข ( ( ( ๐ต โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ต โ†‘ 2 ) + ( ๐ด โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ต gcd ๐ด ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
31 6 7 8 18 29 30 syl311anc โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
32 31 3expia โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
33 5 32 orim12d โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( ( ยฌ 2 โˆฅ ( ๐ด / ( ๐ด gcd ๐ต ) ) โˆจ ยฌ 2 โˆฅ ( ๐ต / ( ๐ด gcd ๐ต ) ) ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
34 3 33 mpd โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
35 ovex โŠข ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆˆ V
36 ovex โŠข ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆˆ V
37 preq12bg โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โˆง ( ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆˆ V โˆง ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆˆ V ) ) โ†’ ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
38 35 36 37 mpanr12 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
39 38 anbi1d โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
40 39 rexbidv โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
41 40 2rexbidv โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
42 andir โŠข ( ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
43 df-3an โŠข ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
44 df-3an โŠข ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
45 43 44 orbi12i โŠข ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
46 3ancoma โŠข ( ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
47 46 orbi2i โŠข ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
48 42 45 47 3bitr2i โŠข ( ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
49 48 rexbii โŠข ( โˆƒ ๐‘˜ โˆˆ โ„• ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
50 49 2rexbii โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
51 r19.43 โŠข ( โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
52 51 2rexbii โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
53 r19.43 โŠข ( โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
54 53 rexbii โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„• ( โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
55 r19.43 โŠข ( โˆƒ ๐‘› โˆˆ โ„• ( โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
56 54 55 bitri โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
57 52 56 bitri โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
58 50 57 bitri โŠข ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ( ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) ) โˆจ ( ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
59 41 58 bitrdi โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
60 59 3adant3 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
61 60 adantr โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ด = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ต = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โˆจ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( ๐ต = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) โˆง ๐ด = ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) ) )
62 34 61 mpbird โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) )
63 62 ex โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )
64 pythagtriplem2 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
65 64 3adant3 โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) โ†’ ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) ) )
66 63 65 impbid โŠข ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โ†’ ( ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โ†” โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘˜ โˆˆ โ„• ( { ๐ด , ๐ต } = { ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) ) , ( ๐‘˜ ยท ( 2 ยท ( ๐‘š ยท ๐‘› ) ) ) } โˆง ๐ถ = ( ๐‘˜ ยท ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) ) ) )