Step | Hyp | Ref
| Expression |
1 | | simp3r 1203 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ยฌ 2 โฅ ๐ด) |
2 | | nnz 12528 |
. . . . . . . . . . . . 13
โข (๐ถ โ โ โ ๐ถ โ
โค) |
3 | | nnz 12528 |
. . . . . . . . . . . . 13
โข (๐ต โ โ โ ๐ต โ
โค) |
4 | | zsubcl 12553 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โค โง ๐ต โ โค) โ (๐ถ โ ๐ต) โ โค) |
5 | 2, 3, 4 | syl2anr 598 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โค) |
6 | 5 | 3adant1 1131 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โค) |
7 | 6 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ โ ๐ต) โ โค) |
8 | | simp13 1206 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ถ โ โ) |
9 | | simp12 1205 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ต โ โ) |
10 | 8, 9 | nnaddcld 12213 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ + ๐ต) โ โ) |
11 | 10 | nnzd 12534 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ + ๐ต) โ โค) |
12 | | gcddvds 16391 |
. . . . . . . . . 10
โข (((๐ถ โ ๐ต) โ โค โง (๐ถ + ๐ต) โ โค) โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ โ ๐ต) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ + ๐ต))) |
13 | 7, 11, 12 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ โ ๐ต) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ + ๐ต))) |
14 | 13 | simprd 497 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ + ๐ต)) |
15 | | breq1 5112 |
. . . . . . . . 9
โข (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ + ๐ต) โ 2 โฅ (๐ถ + ๐ต))) |
16 | 15 | biimpd 228 |
. . . . . . . 8
โข (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (๐ถ + ๐ต) โ 2 โฅ (๐ถ + ๐ต))) |
17 | 14, 16 | mpan9 508 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ 2 โฅ (๐ถ + ๐ต)) |
18 | | 2z 12543 |
. . . . . . . 8
โข 2 โ
โค |
19 | | simpl13 1251 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ถ โ โ) |
20 | 19 | nnzd 12534 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ถ โ โค) |
21 | | simpl12 1250 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ต โ โ) |
22 | 21 | nnzd 12534 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ต โ โค) |
23 | 20, 22 | zaddcld 12619 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (๐ถ + ๐ต) โ โค) |
24 | 20, 22 | zsubcld 12620 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (๐ถ โ ๐ต) โ โค) |
25 | | dvdsmultr1 16186 |
. . . . . . . 8
โข ((2
โ โค โง (๐ถ +
๐ต) โ โค โง
(๐ถ โ ๐ต) โ โค) โ (2
โฅ (๐ถ + ๐ต) โ 2 โฅ ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต)))) |
26 | 18, 23, 24, 25 | mp3an2i 1467 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (2 โฅ (๐ถ + ๐ต) โ 2 โฅ ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต)))) |
27 | 17, 26 | mpd 15 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ 2 โฅ ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) |
28 | 19 | nncnd 12177 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ถ โ โ) |
29 | 21 | nncnd 12177 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ต โ โ) |
30 | | subsq 14123 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถโ2) โ (๐ตโ2)) = ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) |
31 | 28, 29, 30 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ((๐ถโ2) โ (๐ตโ2)) = ((๐ถ + ๐ต) ยท (๐ถ โ ๐ต))) |
32 | 27, 31 | breqtrrd 5137 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ 2 โฅ ((๐ถโ2) โ (๐ตโ2))) |
33 | | simpl2 1193 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2)) |
34 | 33 | oveq1d 7376 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (((๐ดโ2) + (๐ตโ2)) โ (๐ตโ2)) = ((๐ถโ2) โ (๐ตโ2))) |
35 | | simpl11 1249 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ด โ โ) |
36 | 35 | nnsqcld 14156 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (๐ดโ2) โ โ) |
37 | 36 | nncnd 12177 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (๐ดโ2) โ โ) |
38 | 21 | nnsqcld 14156 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (๐ตโ2) โ โ) |
39 | 38 | nncnd 12177 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (๐ตโ2) โ โ) |
40 | 37, 39 | pncand 11521 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (((๐ดโ2) + (๐ตโ2)) โ (๐ตโ2)) = (๐ดโ2)) |
41 | 34, 40 | eqtr3d 2775 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ((๐ถโ2) โ (๐ตโ2)) = (๐ดโ2)) |
42 | 32, 41 | breqtrd 5135 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ 2 โฅ (๐ดโ2)) |
43 | | nnz 12528 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โค) |
44 | 43 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โค) |
45 | 44 | 3ad2ant1 1134 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ด โ โค) |
46 | 45 | adantr 482 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ ๐ด โ โค) |
47 | | 2prm 16576 |
. . . . . 6
โข 2 โ
โ |
48 | | 2nn 12234 |
. . . . . 6
โข 2 โ
โ |
49 | | prmdvdsexp 16599 |
. . . . . 6
โข ((2
โ โ โง ๐ด
โ โค โง 2 โ โ) โ (2 โฅ (๐ดโ2) โ 2 โฅ ๐ด)) |
50 | 47, 48, 49 | mp3an13 1453 |
. . . . 5
โข (๐ด โ โค โ (2
โฅ (๐ดโ2) โ 2
โฅ ๐ด)) |
51 | 46, 50 | syl 17 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ (2 โฅ (๐ดโ2) โ 2 โฅ ๐ด)) |
52 | 42, 51 | mpbid 231 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) โ 2 โฅ ๐ด) |
53 | 1, 52 | mtand 815 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ยฌ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2) |
54 | | neg1z 12547 |
. . . . . . . 8
โข -1 โ
โค |
55 | | gcdaddm 16413 |
. . . . . . . 8
โข ((-1
โ โค โง (๐ถ
โ ๐ต) โ โค
โง (๐ถ + ๐ต) โ โค) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต))))) |
56 | 54, 7, 11, 55 | mp3an2i 1467 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต))))) |
57 | 8 | nncnd 12177 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ถ โ โ) |
58 | 9 | nncnd 12177 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ต โ โ) |
59 | | pnncan 11450 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) โ (๐ถ โ ๐ต)) = (๐ต + ๐ต)) |
60 | 59 | 3anidm23 1422 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) โ (๐ถ โ ๐ต)) = (๐ต + ๐ต)) |
61 | | subcl 11408 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ โ ๐ต) โ โ) |
62 | 61 | mulm1d 11615 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ต โ โ) โ (-1
ยท (๐ถ โ ๐ต)) = -(๐ถ โ ๐ต)) |
63 | 62 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต))) = ((๐ถ + ๐ต) + -(๐ถ โ ๐ต))) |
64 | | addcl 11141 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ + ๐ต) โ โ) |
65 | 64, 61 | negsubd 11526 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + -(๐ถ โ ๐ต)) = ((๐ถ + ๐ต) โ (๐ถ โ ๐ต))) |
66 | 63, 65 | eqtrd 2773 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต))) = ((๐ถ + ๐ต) โ (๐ถ โ ๐ต))) |
67 | | 2times 12297 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
68 | 67 | adantl 483 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ต โ โ) โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
69 | 60, 66, 68 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต))) = (2 ยท ๐ต)) |
70 | 69 | oveq2d 7377 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต)))) = ((๐ถ โ ๐ต) gcd (2 ยท ๐ต))) |
71 | 57, 58, 70 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (-1 ยท (๐ถ โ ๐ต)))) = ((๐ถ โ ๐ต) gcd (2 ยท ๐ต))) |
72 | 56, 71 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = ((๐ถ โ ๐ต) gcd (2 ยท ๐ต))) |
73 | 9 | nnzd 12534 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ต โ โค) |
74 | | zmulcl 12560 |
. . . . . . . . 9
โข ((2
โ โค โง ๐ต
โ โค) โ (2 ยท ๐ต) โ โค) |
75 | 18, 73, 74 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท ๐ต) โ
โค) |
76 | | gcddvds 16391 |
. . . . . . . 8
โข (((๐ถ โ ๐ต) โ โค โง (2 ยท ๐ต) โ โค) โ
(((๐ถ โ ๐ต) gcd (2 ยท ๐ต)) โฅ (๐ถ โ ๐ต) โง ((๐ถ โ ๐ต) gcd (2 ยท ๐ต)) โฅ (2 ยท ๐ต))) |
77 | 7, 75, 76 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ โ ๐ต) gcd (2 ยท ๐ต)) โฅ (๐ถ โ ๐ต) โง ((๐ถ โ ๐ต) gcd (2 ยท ๐ต)) โฅ (2 ยท ๐ต))) |
78 | 77 | simprd 497 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (2 ยท ๐ต)) โฅ (2 ยท ๐ต)) |
79 | 72, 78 | eqbrtrd 5131 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (2 ยท ๐ต)) |
80 | | 1z 12541 |
. . . . . . . 8
โข 1 โ
โค |
81 | | gcdaddm 16413 |
. . . . . . . 8
โข ((1
โ โค โง (๐ถ
โ ๐ต) โ โค
โง (๐ถ + ๐ต) โ โค) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (1 ยท (๐ถ โ ๐ต))))) |
82 | 80, 7, 11, 81 | mp3an2i 1467 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (1 ยท (๐ถ โ ๐ต))))) |
83 | | ppncan 11451 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (๐ถ + ๐ถ)) |
84 | 83 | 3anidm13 1421 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (๐ถ โ ๐ต)) = (๐ถ + ๐ถ)) |
85 | 61 | mulid2d 11181 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ต โ โ) โ (1
ยท (๐ถ โ ๐ต)) = (๐ถ โ ๐ต)) |
86 | 85 | oveq2d 7377 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (1 ยท (๐ถ โ ๐ต))) = ((๐ถ + ๐ต) + (๐ถ โ ๐ต))) |
87 | | 2times 12297 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ (2
ยท ๐ถ) = (๐ถ + ๐ถ)) |
88 | 87 | adantr 482 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ต โ โ) โ (2
ยท ๐ถ) = (๐ถ + ๐ถ)) |
89 | 84, 86, 88 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ + ๐ต) + (1 ยท (๐ถ โ ๐ต))) = (2 ยท ๐ถ)) |
90 | 57, 58, 89 | syl2anc 585 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ + ๐ต) + (1 ยท (๐ถ โ ๐ต))) = (2 ยท ๐ถ)) |
91 | 90 | oveq2d 7377 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd ((๐ถ + ๐ต) + (1 ยท (๐ถ โ ๐ต)))) = ((๐ถ โ ๐ต) gcd (2 ยท ๐ถ))) |
92 | 82, 91 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = ((๐ถ โ ๐ต) gcd (2 ยท ๐ถ))) |
93 | 8 | nnzd 12534 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ๐ถ โ โค) |
94 | | zmulcl 12560 |
. . . . . . . . 9
โข ((2
โ โค โง ๐ถ
โ โค) โ (2 ยท ๐ถ) โ โค) |
95 | 18, 93, 94 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท ๐ถ) โ
โค) |
96 | | gcddvds 16391 |
. . . . . . . 8
โข (((๐ถ โ ๐ต) โ โค โง (2 ยท ๐ถ) โ โค) โ
(((๐ถ โ ๐ต) gcd (2 ยท ๐ถ)) โฅ (๐ถ โ ๐ต) โง ((๐ถ โ ๐ต) gcd (2 ยท ๐ถ)) โฅ (2 ยท ๐ถ))) |
97 | 7, 95, 96 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ โ ๐ต) gcd (2 ยท ๐ถ)) โฅ (๐ถ โ ๐ต) โง ((๐ถ โ ๐ต) gcd (2 ยท ๐ถ)) โฅ (2 ยท ๐ถ))) |
98 | 97 | simprd 497 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (2 ยท ๐ถ)) โฅ (2 ยท ๐ถ)) |
99 | 92, 98 | eqbrtrd 5131 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (2 ยท ๐ถ)) |
100 | | nnaddcl 12184 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ + ๐ต) โ โ) |
101 | 100 | nnne0d 12211 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ + ๐ต) โ 0) |
102 | 101 | ancoms 460 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ต) โ 0) |
103 | 102 | 3adant1 1131 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ต) โ 0) |
104 | 103 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ถ + ๐ต) โ 0) |
105 | 104 | neneqd 2945 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ยฌ (๐ถ + ๐ต) = 0) |
106 | 105 | intnand 490 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ยฌ ((๐ถ โ ๐ต) = 0 โง (๐ถ + ๐ต) = 0)) |
107 | | gcdn0cl 16390 |
. . . . . . . 8
โข ((((๐ถ โ ๐ต) โ โค โง (๐ถ + ๐ต) โ โค) โง ยฌ ((๐ถ โ ๐ต) = 0 โง (๐ถ + ๐ต) = 0)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โ โ) |
108 | 7, 11, 106, 107 | syl21anc 837 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โ โ) |
109 | 108 | nnzd 12534 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โ โค) |
110 | | dvdsgcd 16433 |
. . . . . 6
โข ((((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โ โค โง (2 ยท ๐ต) โ โค โง (2
ยท ๐ถ) โ โค)
โ ((((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (2 ยท ๐ต) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (2 ยท ๐ถ)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ ((2 ยท ๐ต) gcd (2 ยท ๐ถ)))) |
111 | 109, 75, 95, 110 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (2 ยท ๐ต) โง ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ (2 ยท ๐ถ)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ ((2 ยท ๐ต) gcd (2 ยท ๐ถ)))) |
112 | 79, 99, 111 | mp2and 698 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ ((2 ยท ๐ต) gcd (2 ยท ๐ถ))) |
113 | | 2nn0 12438 |
. . . . . 6
โข 2 โ
โ0 |
114 | | mulgcd 16437 |
. . . . . 6
โข ((2
โ โ0 โง ๐ต โ โค โง ๐ถ โ โค) โ ((2 ยท ๐ต) gcd (2 ยท ๐ถ)) = (2 ยท (๐ต gcd ๐ถ))) |
115 | 113, 73, 93, 114 | mp3an2i 1467 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((2 ยท ๐ต) gcd (2 ยท ๐ถ)) = (2 ยท (๐ต gcd ๐ถ))) |
116 | | pythagtriplem3 16698 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (๐ต gcd ๐ถ) = 1) |
117 | 116 | oveq2d 7377 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท (๐ต gcd ๐ถ)) = (2 ยท 1)) |
118 | | 2t1e2 12324 |
. . . . . 6
โข (2
ยท 1) = 2 |
119 | 117, 118 | eqtrdi 2789 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (2 ยท (๐ต gcd ๐ถ)) = 2) |
120 | 115, 119 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((2 ยท ๐ต) gcd (2 ยท ๐ถ)) = 2) |
121 | 112, 120 | breqtrd 5135 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ 2) |
122 | | dvdsprime 16571 |
. . . 4
โข ((2
โ โ โง ((๐ถ
โ ๐ต) gcd (๐ถ + ๐ต)) โ โ) โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ 2 โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โจ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 1))) |
123 | 47, 108, 122 | sylancr 588 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) โฅ 2 โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โจ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 1))) |
124 | 121, 123 | mpbid 231 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ (((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โจ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 1)) |
125 | | orel1 888 |
. 2
โข (ยฌ
((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โ ((((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 2 โจ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 1) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 1)) |
126 | 53, 124, 125 | sylc 65 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ดโ2) + (๐ตโ2)) = (๐ถโ2) โง ((๐ด gcd ๐ต) = 1 โง ยฌ 2 โฅ ๐ด)) โ ((๐ถ โ ๐ต) gcd (๐ถ + ๐ต)) = 1) |