Step | Hyp | Ref
| Expression |
1 | | pythagtriplem13.1 |
. . 3
โข ๐ = (((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต))) / 2) |
2 | 1 | oveq1i 7313 |
. 2
โข (๐โ2) =
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต))) /
2)โ2) |
3 | | nncn 12023 |
. . . . . . . . 9
โข (๐ถ โ โ โ ๐ถ โ
โ) |
4 | | nncn 12023 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต โ
โ) |
5 | | addcl 10995 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ + ๐ต) โ โ) |
6 | 3, 4, 5 | syl2anr 598 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ต) โ โ) |
7 | 6 | sqrtcld 15190 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ
(โโ(๐ถ + ๐ต)) โ
โ) |
8 | | subcl 11262 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ โ ๐ต) โ โ) |
9 | 3, 4, 8 | syl2anr 598 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โ) |
10 | 9 | sqrtcld 15190 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ
(โโ(๐ถ โ
๐ต)) โ
โ) |
11 | 7, 10 | subcld 11374 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ
((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต))) โ โ) |
12 | 11 | 3adant1 1130 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต))) โ โ) |
13 | 12 | 3ad2ant1 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))) |
17 | 14, 15, 16 | mp3an23 1453 |
. . . 4
โข
(((โโ(๐ถ
+ ๐ต)) โ
(โโ(๐ถ โ
๐ต))) โ โ โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต))) / 2)โ2) =
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) /
(2โ2))) |
18 | 13, 17 | syl 17 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต))) / 2)โ2) =
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) /
(2โ2))) |
19 | 14 | sqvali 13939 |
. . . . 5
โข
(2โ2) = (2 ยท 2) |
20 | 19 | oveq2i 7314 |
. . . 4
โข
((((โโ(๐ถ
+ ๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / (2โ2))
= ((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / (2 ยท
2)) |
21 | 13 | sqcld 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))) |
24 | 22, 22, 23 | mp3an23 1453 |
. . . . . 6
โข
((((โโ(๐ถ
+ ๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) โ โ
โ (((((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต)))โ2) / 2) / 2) =
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / (2 ยท
2))) |
25 | 21, 24 | syl 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 โฅ ๐ด)) โ ๐ถ โ โ) |
28 | 26, 27, 7 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โโ(๐ถ + ๐ต)) โ โ) |
29 | 26, 27, 10 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โโ(๐ถ โ ๐ต)) โ โ) |
30 | | binom2sub 13977 |
. . . . . . . . . 10
โข
(((โโ(๐ถ
+ ๐ต)) โ โ โง
(โโ(๐ถ โ
๐ต)) โ โ) โ
(((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต)))โ2) = ((((โโ(๐ถ + ๐ต))โ2) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) +
((โโ(๐ถ โ
๐ต))โ2))) |
31 | 28, 29, 30 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
(((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต)))โ2) = ((((โโ(๐ถ + ๐ต))โ2) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) +
((โโ(๐ถ โ
๐ต))โ2))) |
32 | | nnre 12022 |
. . . . . . . . . . . . . . 15
โข (๐ถ โ โ โ ๐ถ โ
โ) |
33 | | nnre 12022 |
. . . . . . . . . . . . . . 15
โข (๐ต โ โ โ ๐ต โ
โ) |
34 | | readdcl 10996 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ + ๐ต) โ โ) |
35 | 32, 33, 34 | syl2anr 598 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ต) โ โ) |
36 | 35 | 3adant1 1130 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ต) โ โ) |
37 | 36 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ + ๐ต) โ โ) |
38 | 37 | recnd 11045 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ + ๐ต) โ โ) |
39 | | resubcl 11327 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ โ ๐ต) โ โ) |
40 | 32, 33, 39 | syl2anr 598 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โ) |
41 | 40 | 3adant1 1130 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โ) |
42 | 41 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ โ ๐ต) โ โ) |
43 | 42 | recnd 11045 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ โ ๐ต) โ โ) |
44 | 7 | 3adant1 1130 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(โโ(๐ถ + ๐ต)) โ
โ) |
45 | 10 | 3adant1 1130 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(โโ(๐ถ โ
๐ต)) โ
โ) |
46 | 44, 45 | mulcld 11037 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต))) โ
โ) |
47 | | mulcl 10997 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง ((โโ(๐ถ + ๐ต)) ยท (โโ(๐ถ โ ๐ต))) โ โ) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต)))) โ
โ) |
48 | 14, 46, 47 | sylancr 588 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (2
ยท ((โโ(๐ถ
+ ๐ต)) ยท
(โโ(๐ถ โ
๐ต)))) โ
โ) |
49 | 48 | 3ad2ant1 1133 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต)))) โ
โ) |
50 | 38, 43, 49 | addsubd 11395 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ + ๐ต) + (๐ถ โ ๐ต)) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) = (((๐ถ + ๐ต) โ (2 ยท ((โโ(๐ถ + ๐ต)) ยท (โโ(๐ถ โ ๐ต))))) + (๐ถ โ ๐ต))) |
51 | 27 | nncnd 12031 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ถ โ โ) |
52 | | simp11 1203 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ด โ โ) |
53 | 52 | nncnd 12031 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ด โ โ) |
54 | | subdi 11450 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐ถ
โ โ โง ๐ด
โ โ) โ (2 ยท (๐ถ โ ๐ด)) = ((2 ยท ๐ถ) โ (2 ยท ๐ด))) |
55 | 14, 51, 53, 54 | mp3an2i 1466 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท (๐ถ โ ๐ด)) = ((2 ยท ๐ถ) โ (2 ยท ๐ด))) |
56 | | ppncan 11305 |
. . . . . . . . . . . . . . . . 17
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (๐ถ + ๐ถ)) |
57 | 56 | 3anidm13 1420 |
. . . . . . . . . . . . . . . 16
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (๐ถ + ๐ถ)) |
58 | | 2times 12151 |
. . . . . . . . . . . . . . . . 17
โข (๐ถ โ โ โ (2
ยท ๐ถ) = (๐ถ + ๐ถ)) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ถ โ โ โง ๐ต โ โ) โ (2
ยท ๐ถ) = (๐ถ + ๐ถ)) |
60 | 57, 59 | eqtr4d 2779 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (2 ยท ๐ถ)) |
61 | 3, 4, 60 | syl2anr 598 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (2 ยท ๐ถ)) |
62 | 61 | 3adant1 1130 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (2 ยท ๐ถ)) |
63 | 62 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (2 ยท ๐ถ)) |
64 | 26 | nncnd 12031 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ต โ โ) |
65 | | subsq 13968 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถโ2) โ (๐ตโ2)) = ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) |
66 | 51, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถโ2) โ (๐ตโ2)) = ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) |
67 | | oveq1 7310 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โ (((๐ดโ2) + (๐ตโ2)) โ (๐ตโ2)) = ((๐ถโ2) โ (๐ตโ2))) |
68 | 67 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ดโ2) + (๐ตโ2)) โ (๐ตโ2)) = ((๐ถโ2) โ (๐ตโ2))) |
69 | | nncn 12023 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ด โ โ โ ๐ด โ
โ) |
70 | 69 | sqcld 13904 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
71 | 70 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ดโ2) โ
โ) |
72 | 4 | sqcld 13904 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ต โ โ โ (๐ตโ2) โ
โ) |
73 | 72 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ตโ2) โ
โ) |
74 | 71, 73 | pncand 11375 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ดโ2) + (๐ตโ2)) โ (๐ตโ2)) = (๐ดโ2)) |
75 | 74 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ดโ2) + (๐ตโ2)) โ (๐ตโ2)) = (๐ดโ2)) |
76 | 68, 75 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถโ2) โ (๐ตโ2)) = (๐ดโ2)) |
77 | 66, 76 | eqtr3d 2778 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต)) = (๐ดโ2)) |
78 | 77 | fveq2d 6804 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โโ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) = (โโ(๐ดโ2))) |
79 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
80 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
81 | | nngt0 12046 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ถ โ โ โ 0 <
๐ถ) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ โ โง ๐ถ โ โ) โ 0 <
๐ถ) |
83 | | nngt0 12046 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ต โ โ โ 0 <
๐ต) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ต โ โ โง ๐ถ โ โ) โ 0 <
๐ต) |
85 | 79, 80, 82, 84 | addgt0d 11592 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ โ โง ๐ถ โ โ) โ 0 <
(๐ถ + ๐ต)) |
86 | | 0re 11019 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 โ
โ |
87 | | ltle 11105 |
. . . . . . . . . . . . . . . . . . . 20
โข ((0
โ โ โง (๐ถ +
๐ต) โ โ) โ
(0 < (๐ถ + ๐ต) โ 0 โค (๐ถ + ๐ต))) |
88 | 86, 87 | mpan 688 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ถ + ๐ต) โ โ โ (0 < (๐ถ + ๐ต) โ 0 โค (๐ถ + ๐ต))) |
89 | 35, 85, 88 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต โ โ โง ๐ถ โ โ) โ 0 โค
(๐ถ + ๐ต)) |
90 | 89 | 3adant1 1130 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ 0 โค
(๐ถ + ๐ต)) |
91 | 90 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ 0 โค (๐ถ + ๐ต)) |
92 | | pythagtriplem10 16562 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2)) โ 0 < (๐ถ โ ๐ต)) |
93 | 92 | 3adant3 1132 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ 0 < (๐ถ โ ๐ต)) |
94 | | ltle 11105 |
. . . . . . . . . . . . . . . . . 18
โข ((0
โ โ โง (๐ถ
โ ๐ต) โ โ)
โ (0 < (๐ถ โ
๐ต) โ 0 โค (๐ถ โ ๐ต))) |
95 | 86, 94 | mpan 688 |
. . . . . . . . . . . . . . . . 17
โข ((๐ถ โ ๐ต) โ โ โ (0 < (๐ถ โ ๐ต) โ 0 โค (๐ถ โ ๐ต))) |
96 | 42, 93, 95 | sylc 65 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ 0 โค (๐ถ โ ๐ต)) |
97 | 37, 91, 42, 96 | sqrtmuld 15177 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โโ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) = ((โโ(๐ถ + ๐ต)) ยท (โโ(๐ถ โ ๐ต)))) |
98 | 78, 97 | eqtr3d 2778 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โโ(๐ดโ2)) =
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต)))) |
99 | | nnre 12022 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ โ ๐ด โ
โ) |
100 | 99 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
101 | 100 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ด โ โ) |
102 | | nnnn0 12282 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ โ โ ๐ด โ
โ0) |
103 | 102 | nn0ge0d 12338 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ โ 0 โค
๐ด) |
104 | 103 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ 0 โค
๐ด) |
105 | 104 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ 0 โค ๐ด) |
106 | 101, 105 | sqrtsqd 15172 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โโ(๐ดโ2)) = ๐ด) |
107 | 98, 106 | eqtr3d 2778 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((โโ(๐ถ + ๐ต)) ยท (โโ(๐ถ โ ๐ต))) = ๐ด) |
108 | 107 | oveq2d 7319 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต)))) = (2 ยท ๐ด)) |
109 | 63, 108 | oveq12d 7321 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ + ๐ต) + (๐ถ โ ๐ต)) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) = ((2 ยท ๐ถ) โ (2 ยท ๐ด))) |
110 | 55, 109 | eqtr4d 2779 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท (๐ถ โ ๐ด)) = (((๐ถ + ๐ต) + (๐ถ โ ๐ต)) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต)))))) |
111 | | resqrtth 15008 |
. . . . . . . . . . . . 13
โข (((๐ถ + ๐ต) โ โ โง 0 โค (๐ถ + ๐ต)) โ ((โโ(๐ถ + ๐ต))โ2) = (๐ถ + ๐ต)) |
112 | 37, 91, 111 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((โโ(๐ถ + ๐ต))โ2) = (๐ถ + ๐ต)) |
113 | 112 | oveq1d 7318 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
(((โโ(๐ถ + ๐ต))โ2) โ (2 ยท
((โโ(๐ถ + ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) = ((๐ถ + ๐ต) โ (2 ยท ((โโ(๐ถ + ๐ต)) ยท (โโ(๐ถ โ ๐ต)))))) |
114 | | resqrtth 15008 |
. . . . . . . . . . . 12
โข (((๐ถ โ ๐ต) โ โ โง 0 โค (๐ถ โ ๐ต)) โ ((โโ(๐ถ โ ๐ต))โ2) = (๐ถ โ ๐ต)) |
115 | 42, 96, 114 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((โโ(๐ถ โ ๐ต))โ2) = (๐ถ โ ๐ต)) |
116 | 113, 115 | oveq12d 7321 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต))โ2) โ (2
ยท ((โโ(๐ถ
+ ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) +
((โโ(๐ถ โ
๐ต))โ2)) = (((๐ถ + ๐ต) โ (2 ยท ((โโ(๐ถ + ๐ต)) ยท (โโ(๐ถ โ ๐ต))))) + (๐ถ โ ๐ต))) |
117 | 50, 110, 116 | 3eqtr4rd 2787 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต))โ2) โ (2
ยท ((โโ(๐ถ
+ ๐ต)) ยท
(โโ(๐ถ โ
๐ต))))) +
((โโ(๐ถ โ
๐ต))โ2)) = (2 ยท
(๐ถ โ ๐ด))) |
118 | 31, 117 | eqtrd 2776 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
(((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต)))โ2) = (2 ยท (๐ถ โ ๐ด))) |
119 | 118 | oveq1d 7318 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / 2) = ((2
ยท (๐ถ โ ๐ด)) / 2)) |
120 | | subcl 11262 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ด โ โ) โ (๐ถ โ ๐ด) โ โ) |
121 | 3, 69, 120 | syl2anr 598 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ด) โ โ) |
122 | 121 | 3adant2 1131 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ด) โ โ) |
123 | 122 | 3ad2ant1 1133 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ โ ๐ด) โ โ) |
124 | | divcan3 11701 |
. . . . . . . . 9
โข (((๐ถ โ ๐ด) โ โ โง 2 โ โ
โง 2 โ 0) โ ((2 ยท (๐ถ โ ๐ด)) / 2) = (๐ถ โ ๐ด)) |
125 | 14, 15, 124 | mp3an23 1453 |
. . . . . . . 8
โข ((๐ถ โ ๐ด) โ โ โ ((2 ยท (๐ถ โ ๐ด)) / 2) = (๐ถ โ ๐ด)) |
126 | 123, 125 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((2 ยท (๐ถ โ ๐ด)) / 2) = (๐ถ โ ๐ด)) |
127 | 119, 126 | eqtrd 2776 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / 2) = (๐ถ โ ๐ด)) |
128 | 127 | oveq1d 7318 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
(((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / 2) / 2) =
((๐ถ โ ๐ด) / 2)) |
129 | 25, 128 | eqtr3d 2778 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / (2 ยท
2)) = ((๐ถ โ ๐ด) / 2)) |
130 | 20, 129 | eqtrid 2788 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต)))โ2) / (2โ2))
= ((๐ถ โ ๐ด) / 2)) |
131 | 18, 130 | eqtrd 2776 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ
((((โโ(๐ถ +
๐ต)) โ
(โโ(๐ถ โ
๐ต))) / 2)โ2) = ((๐ถ โ ๐ด) / 2)) |
132 | 2, 131 | eqtrid 2788 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐โ2) = ((๐ถ โ ๐ด) / 2)) |