MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pythagtriplem14 Structured version   Visualization version   GIF version

Theorem pythagtriplem14 16570
Description: Lemma for pythagtrip 16576. Calculate the square of ๐‘. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Hypothesis
Ref Expression
pythagtriplem13.1 ๐‘ = (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)
Assertion
Ref Expression
pythagtriplem14 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐‘โ†‘2) = ((๐ถ โˆ’ ๐ด) / 2))

Proof of Theorem pythagtriplem14
StepHypRef Expression
1 pythagtriplem13.1 . . 3 ๐‘ = (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)
21oveq1i 7313 . 2 (๐‘โ†‘2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)โ†‘2)
3 nncn 12023 . . . . . . . . 9 (๐ถ โˆˆ โ„• โ†’ ๐ถ โˆˆ โ„‚)
4 nncn 12023 . . . . . . . . 9 (๐ต โˆˆ โ„• โ†’ ๐ต โˆˆ โ„‚)
5 addcl 10995 . . . . . . . . 9 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ถ + ๐ต) โˆˆ โ„‚)
63, 4, 5syl2anr 598 . . . . . . . 8 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ + ๐ต) โˆˆ โ„‚)
76sqrtcld 15190 . . . . . . 7 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (โˆšโ€˜(๐ถ + ๐ต)) โˆˆ โ„‚)
8 subcl 11262 . . . . . . . . 9 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„‚)
93, 4, 8syl2anr 598 . . . . . . . 8 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„‚)
109sqrtcld 15190 . . . . . . 7 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)) โˆˆ โ„‚)
117, 10subcld 11374 . . . . . 6 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚)
12113adant1 1130 . . . . 5 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚)
13123ad2ant1 1133 . . . 4 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚)
14 2cn 12090 . . . . 5 2 โˆˆ โ„‚
15 2ne0 12119 . . . . 5 2 โ‰  0
16 sqdiv 13883 . . . . 5 ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 โ‰  0) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)โ†‘2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2โ†‘2)))
1714, 15, 16mp3an23 1453 . . . 4 (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)โ†‘2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2โ†‘2)))
1813, 17syl 17 . . 3 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)โ†‘2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2โ†‘2)))
1914sqvali 13939 . . . . 5 (2โ†‘2) = (2 ยท 2)
2019oveq2i 7314 . . . 4 ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2โ†‘2)) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2 ยท 2))
2113sqcld 13904 . . . . . 6 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) โˆˆ โ„‚)
22 2cnne0 12225 . . . . . . 7 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
23 divdiv1 11728 . . . . . . 7 (((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / 2) / 2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2 ยท 2)))
2422, 22, 23mp3an23 1453 . . . . . 6 ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) โˆˆ โ„‚ โ†’ (((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / 2) / 2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2 ยท 2)))
2521, 24syl 17 . . . . 5 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / 2) / 2) = ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2 ยท 2)))
26 simp12 1204 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ต โˆˆ โ„•)
27 simp13 1205 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ถ โˆˆ โ„•)
2826, 27, 7syl2anc 585 . . . . . . . . . 10 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (โˆšโ€˜(๐ถ + ๐ต)) โˆˆ โ„‚)
2926, 27, 10syl2anc 585 . . . . . . . . . 10 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)) โˆˆ โ„‚)
30 binom2sub 13977 . . . . . . . . . 10 (((โˆšโ€˜(๐ถ + ๐ต)) โˆˆ โ„‚ โˆง (โˆšโ€˜(๐ถ โˆ’ ๐ต)) โˆˆ โ„‚) โ†’ (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) = ((((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) + ((โˆšโ€˜(๐ถ โˆ’ ๐ต))โ†‘2)))
3128, 29, 30syl2anc 585 . . . . . . . . 9 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) = ((((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) + ((โˆšโ€˜(๐ถ โˆ’ ๐ต))โ†‘2)))
32 nnre 12022 . . . . . . . . . . . . . . 15 (๐ถ โˆˆ โ„• โ†’ ๐ถ โˆˆ โ„)
33 nnre 12022 . . . . . . . . . . . . . . 15 (๐ต โˆˆ โ„• โ†’ ๐ต โˆˆ โ„)
34 readdcl 10996 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ถ + ๐ต) โˆˆ โ„)
3532, 33, 34syl2anr 598 . . . . . . . . . . . . . 14 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ + ๐ต) โˆˆ โ„)
36353adant1 1130 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ + ๐ต) โˆˆ โ„)
37363ad2ant1 1133 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐ถ + ๐ต) โˆˆ โ„)
3837recnd 11045 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐ถ + ๐ต) โˆˆ โ„‚)
39 resubcl 11327 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„)
4032, 33, 39syl2anr 598 . . . . . . . . . . . . . 14 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„)
41403adant1 1130 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„)
42413ad2ant1 1133 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„)
4342recnd 11045 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐ถ โˆ’ ๐ต) โˆˆ โ„‚)
4473adant1 1130 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (โˆšโ€˜(๐ถ + ๐ต)) โˆˆ โ„‚)
45103adant1 1130 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)) โˆˆ โ„‚)
4644, 45mulcld 11037 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚)
47 mulcl 10997 . . . . . . . . . . . . 13 ((2 โˆˆ โ„‚ โˆง ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))) โˆˆ โ„‚) โ†’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต)))) โˆˆ โ„‚)
4814, 46, 47sylancr 588 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต)))) โˆˆ โ„‚)
49483ad2ant1 1133 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต)))) โˆˆ โ„‚)
5038, 43, 49addsubd 11395 . . . . . . . . . 10 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) = (((๐ถ + ๐ต) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) + (๐ถ โˆ’ ๐ต)))
5127nncnd 12031 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ถ โˆˆ โ„‚)
52 simp11 1203 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ด โˆˆ โ„•)
5352nncnd 12031 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ด โˆˆ โ„‚)
54 subdi 11450 . . . . . . . . . . . 12 ((2 โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (2 ยท (๐ถ โˆ’ ๐ด)) = ((2 ยท ๐ถ) โˆ’ (2 ยท ๐ด)))
5514, 51, 53, 54mp3an2i 1466 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (2 ยท (๐ถ โˆ’ ๐ด)) = ((2 ยท ๐ถ) โˆ’ (2 ยท ๐ด)))
56 ppncan 11305 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) = (๐ถ + ๐ถ))
57563anidm13 1420 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) = (๐ถ + ๐ถ))
58 2times 12151 . . . . . . . . . . . . . . . . 17 (๐ถ โˆˆ โ„‚ โ†’ (2 ยท ๐ถ) = (๐ถ + ๐ถ))
5958adantr 482 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (2 ยท ๐ถ) = (๐ถ + ๐ถ))
6057, 59eqtr4d 2779 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) = (2 ยท ๐ถ))
613, 4, 60syl2anr 598 . . . . . . . . . . . . . 14 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) = (2 ยท ๐ถ))
62613adant1 1130 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) = (2 ยท ๐ถ))
63623ad2ant1 1133 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) = (2 ยท ๐ถ))
6426nncnd 12031 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ต โˆˆ โ„‚)
65 subsq 13968 . . . . . . . . . . . . . . . . . 18 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ ((๐ถโ†‘2) โˆ’ (๐ตโ†‘2)) = ((๐ถ + ๐ต) ยท (๐ถ โˆ’ ๐ต)))
6651, 64, 65syl2anc 585 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((๐ถโ†‘2) โˆ’ (๐ตโ†‘2)) = ((๐ถ + ๐ต) ยท (๐ถ โˆ’ ๐ต)))
67 oveq1 7310 . . . . . . . . . . . . . . . . . . 19 (((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โ†’ (((๐ดโ†‘2) + (๐ตโ†‘2)) โˆ’ (๐ตโ†‘2)) = ((๐ถโ†‘2) โˆ’ (๐ตโ†‘2)))
68673ad2ant2 1134 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((๐ดโ†‘2) + (๐ตโ†‘2)) โˆ’ (๐ตโ†‘2)) = ((๐ถโ†‘2) โˆ’ (๐ตโ†‘2)))
69 nncn 12023 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„‚)
7069sqcld 13904 . . . . . . . . . . . . . . . . . . . . 21 (๐ด โˆˆ โ„• โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
71703ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
724sqcld 13904 . . . . . . . . . . . . . . . . . . . . 21 (๐ต โˆˆ โ„• โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
73723ad2ant2 1134 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
7471, 73pncand 11375 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (((๐ดโ†‘2) + (๐ตโ†‘2)) โˆ’ (๐ตโ†‘2)) = (๐ดโ†‘2))
75743ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((๐ดโ†‘2) + (๐ตโ†‘2)) โˆ’ (๐ตโ†‘2)) = (๐ดโ†‘2))
7668, 75eqtr3d 2778 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((๐ถโ†‘2) โˆ’ (๐ตโ†‘2)) = (๐ดโ†‘2))
7766, 76eqtr3d 2778 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((๐ถ + ๐ต) ยท (๐ถ โˆ’ ๐ต)) = (๐ดโ†‘2))
7877fveq2d 6804 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (โˆšโ€˜((๐ถ + ๐ต) ยท (๐ถ โˆ’ ๐ต))) = (โˆšโ€˜(๐ดโ†‘2)))
7932adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ๐ถ โˆˆ โ„)
8033adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ๐ต โˆˆ โ„)
81 nngt0 12046 . . . . . . . . . . . . . . . . . . . . 21 (๐ถ โˆˆ โ„• โ†’ 0 < ๐ถ)
8281adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ 0 < ๐ถ)
83 nngt0 12046 . . . . . . . . . . . . . . . . . . . . 21 (๐ต โˆˆ โ„• โ†’ 0 < ๐ต)
8483adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ 0 < ๐ต)
8579, 80, 82, 84addgt0d 11592 . . . . . . . . . . . . . . . . . . 19 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ 0 < (๐ถ + ๐ต))
86 0re 11019 . . . . . . . . . . . . . . . . . . . 20 0 โˆˆ โ„
87 ltle 11105 . . . . . . . . . . . . . . . . . . . 20 ((0 โˆˆ โ„ โˆง (๐ถ + ๐ต) โˆˆ โ„) โ†’ (0 < (๐ถ + ๐ต) โ†’ 0 โ‰ค (๐ถ + ๐ต)))
8886, 87mpan 688 . . . . . . . . . . . . . . . . . . 19 ((๐ถ + ๐ต) โˆˆ โ„ โ†’ (0 < (๐ถ + ๐ต) โ†’ 0 โ‰ค (๐ถ + ๐ต)))
8935, 85, 88sylc 65 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ 0 โ‰ค (๐ถ + ๐ต))
90893adant1 1130 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ 0 โ‰ค (๐ถ + ๐ต))
91903ad2ant1 1133 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ 0 โ‰ค (๐ถ + ๐ต))
92 pythagtriplem10 16562 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2)) โ†’ 0 < (๐ถ โˆ’ ๐ต))
93923adant3 1132 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ 0 < (๐ถ โˆ’ ๐ต))
94 ltle 11105 . . . . . . . . . . . . . . . . . 18 ((0 โˆˆ โ„ โˆง (๐ถ โˆ’ ๐ต) โˆˆ โ„) โ†’ (0 < (๐ถ โˆ’ ๐ต) โ†’ 0 โ‰ค (๐ถ โˆ’ ๐ต)))
9586, 94mpan 688 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆ’ ๐ต) โˆˆ โ„ โ†’ (0 < (๐ถ โˆ’ ๐ต) โ†’ 0 โ‰ค (๐ถ โˆ’ ๐ต)))
9642, 93, 95sylc 65 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ 0 โ‰ค (๐ถ โˆ’ ๐ต))
9737, 91, 42, 96sqrtmuld 15177 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (โˆšโ€˜((๐ถ + ๐ต) ยท (๐ถ โˆ’ ๐ต))) = ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))
9878, 97eqtr3d 2778 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (โˆšโ€˜(๐ดโ†‘2)) = ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))
99 nnre 12022 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„)
100993ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ ๐ด โˆˆ โ„)
1011003ad2ant1 1133 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ๐ด โˆˆ โ„)
102 nnnn0 12282 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„• โ†’ ๐ด โˆˆ โ„•0)
103102nn0ge0d 12338 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„• โ†’ 0 โ‰ค ๐ด)
1041033ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ 0 โ‰ค ๐ด)
1051043ad2ant1 1133 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ 0 โ‰ค ๐ด)
106101, 105sqrtsqd 15172 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (โˆšโ€˜(๐ดโ†‘2)) = ๐ด)
10798, 106eqtr3d 2778 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))) = ๐ด)
108107oveq2d 7319 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต)))) = (2 ยท ๐ด))
10963, 108oveq12d 7321 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) = ((2 ยท ๐ถ) โˆ’ (2 ยท ๐ด)))
11055, 109eqtr4d 2779 . . . . . . . . . 10 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (2 ยท (๐ถ โˆ’ ๐ด)) = (((๐ถ + ๐ต) + (๐ถ โˆ’ ๐ต)) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))))
111 resqrtth 15008 . . . . . . . . . . . . 13 (((๐ถ + ๐ต) โˆˆ โ„ โˆง 0 โ‰ค (๐ถ + ๐ต)) โ†’ ((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) = (๐ถ + ๐ต))
11237, 91, 111syl2anc 585 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) = (๐ถ + ๐ต))
113112oveq1d 7318 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) = ((๐ถ + ๐ต) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))))
114 resqrtth 15008 . . . . . . . . . . . 12 (((๐ถ โˆ’ ๐ต) โˆˆ โ„ โˆง 0 โ‰ค (๐ถ โˆ’ ๐ต)) โ†’ ((โˆšโ€˜(๐ถ โˆ’ ๐ต))โ†‘2) = (๐ถ โˆ’ ๐ต))
11542, 96, 114syl2anc 585 . . . . . . . . . . 11 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((โˆšโ€˜(๐ถ โˆ’ ๐ต))โ†‘2) = (๐ถ โˆ’ ๐ต))
116113, 115oveq12d 7321 . . . . . . . . . 10 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) + ((โˆšโ€˜(๐ถ โˆ’ ๐ต))โ†‘2)) = (((๐ถ + ๐ต) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) + (๐ถ โˆ’ ๐ต)))
11750, 110, 1163eqtr4rd 2787 . . . . . . . . 9 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต))โ†‘2) โˆ’ (2 ยท ((โˆšโ€˜(๐ถ + ๐ต)) ยท (โˆšโ€˜(๐ถ โˆ’ ๐ต))))) + ((โˆšโ€˜(๐ถ โˆ’ ๐ต))โ†‘2)) = (2 ยท (๐ถ โˆ’ ๐ด)))
11831, 117eqtrd 2776 . . . . . . . 8 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) = (2 ยท (๐ถ โˆ’ ๐ด)))
119118oveq1d 7318 . . . . . . 7 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / 2) = ((2 ยท (๐ถ โˆ’ ๐ด)) / 2))
120 subcl 11262 . . . . . . . . . . 11 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (๐ถ โˆ’ ๐ด) โˆˆ โ„‚)
1213, 69, 120syl2anr 598 . . . . . . . . . 10 ((๐ด โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ โˆ’ ๐ด) โˆˆ โ„‚)
1221213adant2 1131 . . . . . . . . 9 ((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โ†’ (๐ถ โˆ’ ๐ด) โˆˆ โ„‚)
1231223ad2ant1 1133 . . . . . . . 8 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐ถ โˆ’ ๐ด) โˆˆ โ„‚)
124 divcan3 11701 . . . . . . . . 9 (((๐ถ โˆ’ ๐ด) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 โ‰  0) โ†’ ((2 ยท (๐ถ โˆ’ ๐ด)) / 2) = (๐ถ โˆ’ ๐ด))
12514, 15, 124mp3an23 1453 . . . . . . . 8 ((๐ถ โˆ’ ๐ด) โˆˆ โ„‚ โ†’ ((2 ยท (๐ถ โˆ’ ๐ด)) / 2) = (๐ถ โˆ’ ๐ด))
126123, 125syl 17 . . . . . . 7 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((2 ยท (๐ถ โˆ’ ๐ด)) / 2) = (๐ถ โˆ’ ๐ด))
127119, 126eqtrd 2776 . . . . . 6 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / 2) = (๐ถ โˆ’ ๐ด))
128127oveq1d 7318 . . . . 5 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / 2) / 2) = ((๐ถ โˆ’ ๐ด) / 2))
12925, 128eqtr3d 2778 . . . 4 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2 ยท 2)) = ((๐ถ โˆ’ ๐ด) / 2))
13020, 129eqtrid 2788 . . 3 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต)))โ†‘2) / (2โ†‘2)) = ((๐ถ โˆ’ ๐ด) / 2))
13118, 130eqtrd 2776 . 2 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ ((((โˆšโ€˜(๐ถ + ๐ต)) โˆ’ (โˆšโ€˜(๐ถ โˆ’ ๐ต))) / 2)โ†‘2) = ((๐ถ โˆ’ ๐ด) / 2))
1322, 131eqtrid 2788 1 (((๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„• โˆง ๐ถ โˆˆ โ„•) โˆง ((๐ดโ†‘2) + (๐ตโ†‘2)) = (๐ถโ†‘2) โˆง ((๐ด gcd ๐ต) = 1 โˆง ยฌ 2 โˆฅ ๐ด)) โ†’ (๐‘โ†‘2) = ((๐ถ โˆ’ ๐ด) / 2))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 397   โˆง w3a 1087   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2941   class class class wbr 5081  โ€˜cfv 6454  (class class class)co 7303  โ„‚cc 10911  โ„cr 10912  0cc0 10913  1c1 10914   + caddc 10916   ยท cmul 10918   < clt 11051   โ‰ค cle 11052   โˆ’ cmin 11247   / cdiv 11674  โ„•cn 12015  2c2 12070  โ†‘cexp 13824  โˆšcsqrt 14985   โˆฅ cdvds 16004   gcd cgcd 16242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-cnex 10969  ax-resscn 10970  ax-1cn 10971  ax-icn 10972  ax-addcl 10973  ax-addrcl 10974  ax-mulcl 10975  ax-mulrcl 10976  ax-mulcom 10977  ax-addass 10978  ax-mulass 10979  ax-distr 10980  ax-i2m1 10981  ax-1ne0 10982  ax-1rid 10983  ax-rnegex 10984  ax-rrecex 10985  ax-cnre 10986  ax-pre-lttri 10987  ax-pre-lttrn 10988  ax-pre-ltadd 10989  ax-pre-mulgt0 10990  ax-pre-sup 10991
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-riota 7260  df-ov 7306  df-oprab 7307  df-mpo 7308  df-om 7741  df-2nd 7860  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-er 8525  df-en 8761  df-dom 8762  df-sdom 8763  df-sup 9241  df-pnf 11053  df-mnf 11054  df-xr 11055  df-ltxr 11056  df-le 11057  df-sub 11249  df-neg 11250  df-div 11675  df-nn 12016  df-2 12078  df-3 12079  df-n0 12276  df-z 12362  df-uz 12625  df-rp 12773  df-seq 13764  df-exp 13825  df-cj 14851  df-re 14852  df-im 14853  df-sqrt 14987  df-abs 14988
This theorem is referenced by:  pythagtriplem15  16571  pythagtriplem17  16573
  Copyright terms: Public domain W3C validator