Step | Hyp | Ref
| Expression |
1 | | simp3l 1202 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ด gcd ๐ต) = 1) |
2 | | simp11 1204 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ด โ โ) |
3 | | simp12 1205 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ต โ โ) |
4 | | coprmgcdb 16530 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ โ โ
((๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ ๐ = 1) โ (๐ด gcd ๐ต) = 1)) |
5 | 2, 3, 4 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โ๐ โ โ ((๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ ๐ = 1) โ (๐ด gcd ๐ต) = 1)) |
6 | 1, 5 | mpbird 257 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ โ๐ โ โ ((๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ ๐ = 1)) |
7 | | simplr 768 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โ โ) |
8 | 7 | nnzd 12531 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โ โค) |
9 | | flt4lem5.1 |
. . . . . . . . . . . . 13
โข ๐ = (((โโ(๐ถ + ๐ต)) + (โโ(๐ถ โ ๐ต))) / 2) |
10 | 9 | pythagtriplem11 16702 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ โ โ) |
11 | 10 | ad2antrr 725 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โ โ) |
12 | 11 | nnsqcld 14153 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐โ2) โ โ) |
13 | 12 | nnzd 12531 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐โ2) โ โค) |
14 | | flt4lem5.2 |
. . . . . . . . . . . . 13
โข ๐ = (((โโ(๐ถ + ๐ต)) โ (โโ(๐ถ โ ๐ต))) / 2) |
15 | 14 | pythagtriplem13 16704 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ โ โ) |
16 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โ โ) |
17 | 16 | nnsqcld 14153 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐โ2) โ โ) |
18 | 17 | nnzd 12531 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐โ2) โ โค) |
19 | | simprl 770 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ ๐) |
20 | 11 | nnzd 12531 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โ โค) |
21 | | 2nn 12231 |
. . . . . . . . . . . 12
โข 2 โ
โ |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ 2 โ โ) |
23 | | dvdsexp2im 16214 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง 2 โ
โ) โ (๐ โฅ
๐ โ ๐ โฅ (๐โ2))) |
24 | 8, 20, 22, 23 | syl3anc 1372 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐ โฅ ๐ โ ๐ โฅ (๐โ2))) |
25 | 19, 24 | mpd 15 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ (๐โ2)) |
26 | | simprr 772 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ ๐) |
27 | 16 | nnzd 12531 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โ โค) |
28 | | dvdsexp2im 16214 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง 2 โ
โ) โ (๐ โฅ
๐ โ ๐ โฅ (๐โ2))) |
29 | 8, 27, 22, 28 | syl3anc 1372 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐ โฅ ๐ โ ๐ โฅ (๐โ2))) |
30 | 26, 29 | mpd 15 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ (๐โ2)) |
31 | 8, 13, 18, 25, 30 | dvds2subd 16180 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ ((๐โ2) โ (๐โ2))) |
32 | 9, 14 | pythagtriplem15 16706 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ด = ((๐โ2) โ (๐โ2))) |
33 | 32 | ad2antrr 725 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ด = ((๐โ2) โ (๐โ2))) |
34 | 31, 33 | breqtrrd 5134 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ ๐ด) |
35 | | 2z 12540 |
. . . . . . . . . 10
โข 2 โ
โค |
36 | 35 | a1i 11 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ 2 โ โค) |
37 | 11, 16 | nnmulcld 12211 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐ ยท ๐) โ โ) |
38 | 37 | nnzd 12531 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐ ยท ๐) โ โค) |
39 | 8, 20, 27, 26 | dvdsmultr2d 16186 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ (๐ ยท ๐)) |
40 | 8, 36, 38, 39 | dvdsmultr2d 16186 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ (2 ยท (๐ ยท ๐))) |
41 | 9, 14 | pythagtriplem16 16707 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ต = (2 ยท (๐ ยท ๐))) |
42 | 41 | ad2antrr 725 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ต = (2 ยท (๐ ยท ๐))) |
43 | 40, 42 | breqtrrd 5134 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ โฅ ๐ต) |
44 | 34, 43 | jca 513 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง ((๐ดโ2)
+ (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ (๐ โฅ ๐ด โง ๐ โฅ ๐ต)) |
45 | 44 | ex 414 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (๐ โฅ ๐ด โง ๐ โฅ ๐ต))) |
46 | 45 | imim1d 82 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ๐ โ โ) โ (((๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ ๐ = 1) โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ = 1))) |
47 | 46 | ralimdva 3161 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โ๐ โ โ ((๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ ๐ = 1) โ โ๐ โ โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ = 1))) |
48 | 6, 47 | mpd 15 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ โ๐ โ โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ = 1)) |
49 | | coprmgcdb 16530 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
(โ๐ โ โ
((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ = 1) โ (๐ gcd ๐) = 1)) |
50 | 10, 15, 49 | syl2anc 585 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (โ๐ โ โ ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ = 1) โ (๐ gcd ๐) = 1)) |
51 | 48, 50 | mpbid 231 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ gcd ๐) = 1) |