Metamath Proof Explorer

Theorem pythagtriplem18

Description: Lemma for pythagtrip . Wrap the previous M and N up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion pythagtriplem18 ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ๐‘š ยท ๐‘› ) ) โˆง ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid โŠข ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 )
2 1 pythagtriplem13 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โˆˆ โ„• )
3 eqid โŠข ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 )
4 3 pythagtriplem11 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โˆˆ โ„• )
5 3 1 pythagtriplem15 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ ๐ด = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) )
6 3 1 pythagtriplem16 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ ๐ต = ( 2 ยท ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) )
7 3 1 pythagtriplem17 โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ ๐ถ = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) )
8 oveq1 โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐‘› โ†‘ 2 ) = ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) )
9 8 oveq2d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) )
10 9 eqeq2d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) โ†” ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) )
11 oveq2 โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐‘š ยท ๐‘› ) = ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) )
12 11 oveq2d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( 2 ยท ( ๐‘š ยท ๐‘› ) ) = ( 2 ยท ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) )
13 12 eqeq2d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐ต = ( 2 ยท ( ๐‘š ยท ๐‘› ) ) โ†” ๐ต = ( 2 ยท ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) ) )
14 8 oveq2d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) = ( ( ๐‘š โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) )
15 14 eqeq2d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) โ†” ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) )
16 10 13 15 3anbi123d โŠข ( ๐‘› = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ๐‘š ยท ๐‘› ) ) โˆง ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) โ†” ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) โˆง ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) ) )
17 oveq1 โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐‘š โ†‘ 2 ) = ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) )
18 17 oveq1d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) )
19 18 eqeq2d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) โ†” ๐ด = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) )
20 oveq1 โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) = ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) )
21 20 oveq2d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( 2 ยท ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) = ( 2 ยท ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) )
22 21 eqeq2d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐ต = ( 2 ยท ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) โ†” ๐ต = ( 2 ยท ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) ) )
23 17 oveq1d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ( ๐‘š โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) )
24 23 eqeq2d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) โ†” ๐ถ = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) )
25 19 22 24 3anbi123d โŠข ( ๐‘š = ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†’ ( ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ๐‘š ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) โˆง ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) โ†” ( ๐ด = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) โˆง ๐ถ = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) ) )
26 16 25 rspc2ev โŠข ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โˆˆ โ„• โˆง ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โˆˆ โ„• โˆง ( ๐ด = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) โˆ’ ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ยท ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) ) ) โˆง ๐ถ = ( ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) + ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) + ( ( ( ( โˆš โ€˜ ( ๐ถ + ๐ต ) ) โˆ’ ( โˆš โ€˜ ( ๐ถ โˆ’ ๐ต ) ) ) / 2 ) โ†‘ 2 ) ) ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ๐‘š ยท ๐‘› ) ) โˆง ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) )
27 2 4 5 6 7 26 syl113anc โŠข ( ( ( ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„• ) โˆง ( ( ๐ด โ†‘ 2 ) + ( ๐ต โ†‘ 2 ) ) = ( ๐ถ โ†‘ 2 ) โˆง ( ( ๐ด gcd ๐ต ) = 1 โˆง ยฌ 2 โˆฅ ๐ด ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„• โˆƒ ๐‘š โˆˆ โ„• ( ๐ด = ( ( ๐‘š โ†‘ 2 ) โˆ’ ( ๐‘› โ†‘ 2 ) ) โˆง ๐ต = ( 2 ยท ( ๐‘š ยท ๐‘› ) ) โˆง ๐ถ = ( ( ๐‘š โ†‘ 2 ) + ( ๐‘› โ†‘ 2 ) ) ) )