Step | Hyp | Ref
| Expression |
1 | | 2sqmod.6 |
. . . . . 6
โข (๐ โ ๐ด โค ๐ต) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โค ๐ต) |
3 | | 2sqmod.4 |
. . . . . . . 8
โข (๐ โ ๐ถ โ
โ0) |
4 | 3 | nn0red 12481 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
5 | 4 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ถ โ โ) |
6 | | 2sqmod.3 |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ0) |
7 | 6 | nn0red 12481 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
8 | 7 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ต โ โ) |
9 | 3 | nn0ge0d 12483 |
. . . . . . 7
โข (๐ โ 0 โค ๐ถ) |
10 | 9 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ 0 โค ๐ถ) |
11 | 6 | nn0ge0d 12483 |
. . . . . . 7
โข (๐ โ 0 โค ๐ต) |
12 | 11 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ 0 โค ๐ต) |
13 | 3 | nn0cnd 12482 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
14 | 13 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (๐ถโ2) โ โ) |
15 | 14 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ถโ2) โ โ) |
16 | 6 | nn0cnd 12482 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
17 | 16 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (๐ตโ2) โ โ) |
18 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ตโ2) โ โ) |
19 | | 2sqmod.2 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ
โ0) |
20 | 19 | nn0cnd 12482 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
21 | 20 | sqcld 14056 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ2) โ โ) |
22 | | 2sqmod.5 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ท โ
โ0) |
23 | 22 | nn0cnd 12482 |
. . . . . . . . . . . 12
โข (๐ โ ๐ท โ โ) |
24 | 23 | sqcld 14056 |
. . . . . . . . . . 11
โข (๐ โ (๐ทโ2) โ โ) |
25 | | 2sqmod.8 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ดโ2) + (๐ตโ2)) = ๐) |
26 | | 2sqmod.9 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถโ2) + (๐ทโ2)) = ๐) |
27 | 25, 26 | eqtr4d 2780 |
. . . . . . . . . . 11
โข (๐ โ ((๐ดโ2) + (๐ตโ2)) = ((๐ถโ2) + (๐ทโ2))) |
28 | 21, 17, 14, 24, 27 | subaddeqd 11577 |
. . . . . . . . . 10
โข (๐ โ ((๐ดโ2) โ (๐ทโ2)) = ((๐ถโ2) โ (๐ตโ2))) |
29 | 28 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ดโ2) โ (๐ทโ2)) = ((๐ถโ2) โ (๐ตโ2))) |
30 | 19 | nn0zd 12532 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ด โ โค) |
31 | 3 | nn0zd 12532 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ถ โ โค) |
32 | | dvdsmul1 16167 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โค โง ๐ถ โ โค) โ ๐ด โฅ (๐ด ยท ๐ถ)) |
33 | 30, 31, 32 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โฅ (๐ด ยท ๐ถ)) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โฅ (๐ด ยท ๐ถ)) |
35 | 20, 13 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ด ยท ๐ถ) โ โ) |
37 | 16, 23 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ต ยท ๐ท) โ โ) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ต ยท ๐ท) โ โ) |
39 | 19 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ด โ โ) |
40 | 39, 4 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
41 | 22 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ท โ โ) |
42 | 7, 41 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ต ยท ๐ท) โ โ) |
43 | 40, 42 | resubcld 11590 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท)) โ โ) |
44 | 43 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท)) โ โ) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท)) โ โ) |
46 | 43 | sqge0d 14049 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 0 โค (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2)) |
47 | | 2sqmod.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ๐ โ โ) |
48 | 6 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ๐ต โ โค) |
49 | 47, 30, 48, 25 | 2sqn0 26798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ ๐ด โ 0) |
50 | | elnnne0 12434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ด โ โ โ (๐ด โ โ0
โง ๐ด โ
0)) |
51 | 19, 49, 50 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ด โ โ) |
52 | 22 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ๐ท โ โค) |
53 | 24, 14 | addcomd 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ ((๐ทโ2) + (๐ถโ2)) = ((๐ถโ2) + (๐ทโ2))) |
54 | 53, 26 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ((๐ทโ2) + (๐ถโ2)) = ๐) |
55 | 47, 52, 31, 54 | 2sqn0 26798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ ๐ท โ 0) |
56 | | elnnne0 12434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ท โ โ โ (๐ท โ โ0
โง ๐ท โ
0)) |
57 | 22, 55, 56 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ท โ โ) |
58 | 51, 57 | nnmulcld 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐ด ยท ๐ท) โ โ) |
59 | 47, 31, 52, 26 | 2sqn0 26798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ ๐ถ โ 0) |
60 | | elnnne0 12434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ถ โ โ โ (๐ถ โ โ0
โง ๐ถ โ
0)) |
61 | 3, 59, 60 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ถ โ โ) |
62 | 17, 21 | addcomd 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ ((๐ตโ2) + (๐ดโ2)) = ((๐ดโ2) + (๐ตโ2))) |
63 | 62, 25 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ โ ((๐ตโ2) + (๐ดโ2)) = ๐) |
64 | 47, 48, 30, 63 | 2sqn0 26798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ ๐ต โ 0) |
65 | | elnnne0 12434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ต โ โ โ (๐ต โ โ0
โง ๐ต โ
0)) |
66 | 6, 64, 65 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ ๐ต โ โ) |
67 | 61, 66 | nnmulcld 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐ถ ยท ๐ต) โ โ) |
68 | 58, 67 | nnaddcld 12212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โ) |
69 | 68 | nnsqcld 14154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ โ) |
70 | 69 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ โ) |
71 | 43 | resqcld 14037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) โ โ) |
72 | 70, 71 | addge02d 11751 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (0 โค (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โค ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)))) |
73 | 46, 72 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โค ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
74 | 25, 26 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) + (๐ทโ2))) = (๐ ยท ๐)) |
75 | | bhmafibid1 15357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) + (๐ทโ2))) = ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))โ2))) |
76 | 39, 7, 4, 41, 75 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) + (๐ทโ2))) = ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))โ2))) |
77 | 74, 76 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ ยท ๐) = ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))โ2))) |
78 | | prmz 16558 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ ๐ โ
โค) |
79 | 47, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ๐ โ โค) |
80 | 79 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ๐ โ โ) |
81 | 80 | sqvald 14055 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
82 | 13, 16 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐ถ ยท ๐ต) = (๐ต ยท ๐ถ)) |
83 | 82 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))) |
84 | 83 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) = (((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))โ2)) |
85 | 84 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))โ2))) |
86 | 77, 81, 85 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐โ2) = ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
87 | 73, 86 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โค (๐โ2)) |
88 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โค (๐โ2)) |
89 | 30, 52 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ด ยท ๐ท) โ โค) |
90 | 31, 48 | zmulcld 12620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ถ ยท ๐ต) โ โค) |
91 | 89, 90 | zaddcld 12618 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โค) |
92 | | dvdssqim 16442 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โค โง ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โค) โ (๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ (๐โ2) โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
93 | 79, 91, 92 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ (๐โ2) โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
94 | | zsqcl 14041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โค โ (๐โ2) โ
โค) |
95 | 79, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐โ2) โ โค) |
96 | | dvdsle 16199 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐โ2) โ โค โง
(((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ โ) โ ((๐โ2) โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (๐โ2) โค (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
97 | 95, 69, 96 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ((๐โ2) โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (๐โ2) โค (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
98 | 93, 97 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ (๐โ2) โค (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
99 | 98 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐โ2) โค (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) |
100 | 95 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐โ2) โ โ) |
101 | 70, 100 | letri3d 11304 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) = (๐โ2) โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โค (๐โ2) โง (๐โ2) โค (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)))) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) = (๐โ2) โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โค (๐โ2) โง (๐โ2) โค (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)))) |
103 | 88, 99, 102 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) = (๐โ2)) |
104 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐โ2) = ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
105 | 103, 104 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) |
106 | 70 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ โ) |
107 | 71 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) โ โ) |
108 | 106, 106,
107 | subadd2d 11538 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) โ ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) โ ((((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2))) |
110 | 105, 109 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2)) |
111 | 106 | subidd 11507 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = 0) |
112 | 111 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))โ2)) = 0) |
113 | 110, 112 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท))โ2) = 0) |
114 | 45, 113 | sqeq0d 14057 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ด ยท ๐ถ) โ (๐ต ยท ๐ท)) = 0) |
115 | 36, 38, 114 | subeq0d 11527 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ด ยท ๐ถ) = (๐ต ยท ๐ท)) |
116 | 34, 115 | breqtrd 5136 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โฅ (๐ต ยท ๐ท)) |
117 | 47, 30, 48, 25 | 2sqcoprm 26799 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด gcd ๐ต) = 1) |
118 | 117 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ด gcd ๐ต) = 1) |
119 | | coprmdvds 16536 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ท โ โค) โ ((๐ด โฅ (๐ต ยท ๐ท) โง (๐ด gcd ๐ต) = 1) โ ๐ด โฅ ๐ท)) |
120 | 30, 48, 52, 119 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด โฅ (๐ต ยท ๐ท) โง (๐ด gcd ๐ต) = 1) โ ๐ด โฅ ๐ท)) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ด โฅ (๐ต ยท ๐ท) โง (๐ด gcd ๐ต) = 1) โ ๐ด โฅ ๐ท)) |
122 | 116, 118,
121 | mp2and 698 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โฅ ๐ท) |
123 | | dvdsle 16199 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โค โง ๐ท โ โ) โ (๐ด โฅ ๐ท โ ๐ด โค ๐ท)) |
124 | 30, 57, 123 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด โฅ ๐ท โ ๐ด โค ๐ท)) |
125 | 124 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ด โฅ ๐ท โ ๐ด โค ๐ท)) |
126 | 122, 125 | mpd 15 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โค ๐ท) |
127 | 51 | nnrpd 12962 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ
โ+) |
128 | 127 | rprege0d 12971 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด โ โ โง 0 โค ๐ด)) |
129 | 22 | nn0ge0d 12483 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โค ๐ท) |
130 | | le2sq 14046 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ท โ โ โง 0 โค ๐ท)) โ (๐ด โค ๐ท โ (๐ดโ2) โค (๐ทโ2))) |
131 | 128, 41, 129, 130 | syl12anc 836 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด โค ๐ท โ (๐ดโ2) โค (๐ทโ2))) |
132 | 131 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ด โค ๐ท โ (๐ดโ2) โค (๐ทโ2))) |
133 | 126, 132 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ดโ2) โค (๐ทโ2)) |
134 | 51 | nnsqcld 14154 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ดโ2) โ โ) |
135 | 134 | nnred 12175 |
. . . . . . . . . . . 12
โข (๐ โ (๐ดโ2) โ โ) |
136 | | zsqcl 14041 |
. . . . . . . . . . . . . 14
โข (๐ท โ โค โ (๐ทโ2) โ
โค) |
137 | 52, 136 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ทโ2) โ โค) |
138 | 137 | zred 12614 |
. . . . . . . . . . . 12
โข (๐ โ (๐ทโ2) โ โ) |
139 | 135, 138 | suble0d 11753 |
. . . . . . . . . . 11
โข (๐ โ (((๐ดโ2) โ (๐ทโ2)) โค 0 โ (๐ดโ2) โค (๐ทโ2))) |
140 | 139 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((๐ดโ2) โ (๐ทโ2)) โค 0 โ (๐ดโ2) โค (๐ทโ2))) |
141 | 133, 140 | mpbird 257 |
. . . . . . . . 9
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ดโ2) โ (๐ทโ2)) โค 0) |
142 | 29, 141 | eqbrtrrd 5134 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ถโ2) โ (๐ตโ2)) โค 0) |
143 | | dvdsmul1 16167 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ โค โง ๐ท โ โค) โ ๐ต โฅ (๐ต ยท ๐ท)) |
144 | 48, 52, 143 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โฅ (๐ต ยท ๐ท)) |
145 | 144 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ต โฅ (๐ต ยท ๐ท)) |
146 | 145, 115 | breqtrrd 5138 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ต โฅ (๐ด ยท ๐ถ)) |
147 | 30, 48 | gcdcomd 16401 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด gcd ๐ต) = (๐ต gcd ๐ด)) |
148 | 147, 117 | eqtr3d 2779 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ต gcd ๐ด) = 1) |
149 | 148 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ต gcd ๐ด) = 1) |
150 | | coprmdvds 16536 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โค โง ๐ด โ โค โง ๐ถ โ โค) โ ((๐ต โฅ (๐ด ยท ๐ถ) โง (๐ต gcd ๐ด) = 1) โ ๐ต โฅ ๐ถ)) |
151 | 48, 30, 31, 150 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ต โฅ (๐ด ยท ๐ถ) โง (๐ต gcd ๐ด) = 1) โ ๐ต โฅ ๐ถ)) |
152 | 151 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ต โฅ (๐ด ยท ๐ถ) โง (๐ต gcd ๐ด) = 1) โ ๐ต โฅ ๐ถ)) |
153 | 146, 149,
152 | mp2and 698 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ต โฅ ๐ถ) |
154 | | dvdsle 16199 |
. . . . . . . . . . . . 13
โข ((๐ต โ โค โง ๐ถ โ โ) โ (๐ต โฅ ๐ถ โ ๐ต โค ๐ถ)) |
155 | 48, 61, 154 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ (๐ต โฅ ๐ถ โ ๐ต โค ๐ถ)) |
156 | 155 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ต โฅ ๐ถ โ ๐ต โค ๐ถ)) |
157 | 153, 156 | mpd 15 |
. . . . . . . . . 10
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ต โค ๐ถ) |
158 | 7, 4, 11, 9 | le2sqd 14167 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โค ๐ถ โ (๐ตโ2) โค (๐ถโ2))) |
159 | 158 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ต โค ๐ถ โ (๐ตโ2) โค (๐ถโ2))) |
160 | 157, 159 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ตโ2) โค (๐ถโ2)) |
161 | 4 | resqcld 14037 |
. . . . . . . . . . 11
โข (๐ โ (๐ถโ2) โ โ) |
162 | | zsqcl 14041 |
. . . . . . . . . . . . 13
โข (๐ต โ โค โ (๐ตโ2) โ
โค) |
163 | 48, 162 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐ตโ2) โ โค) |
164 | 163 | zred 12614 |
. . . . . . . . . . 11
โข (๐ โ (๐ตโ2) โ โ) |
165 | 161, 164 | subge0d 11752 |
. . . . . . . . . 10
โข (๐ โ (0 โค ((๐ถโ2) โ (๐ตโ2)) โ (๐ตโ2) โค (๐ถโ2))) |
166 | 165 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (0 โค ((๐ถโ2) โ (๐ตโ2)) โ (๐ตโ2) โค (๐ถโ2))) |
167 | 160, 166 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ 0 โค ((๐ถโ2) โ (๐ตโ2))) |
168 | 135, 138 | resubcld 11590 |
. . . . . . . . . . 11
โข (๐ โ ((๐ดโ2) โ (๐ทโ2)) โ โ) |
169 | 28, 168 | eqeltrrd 2839 |
. . . . . . . . . 10
โข (๐ โ ((๐ถโ2) โ (๐ตโ2)) โ โ) |
170 | | 0red 11165 |
. . . . . . . . . 10
โข (๐ โ 0 โ
โ) |
171 | 169, 170 | letri3d 11304 |
. . . . . . . . 9
โข (๐ โ (((๐ถโ2) โ (๐ตโ2)) = 0 โ (((๐ถโ2) โ (๐ตโ2)) โค 0 โง 0 โค ((๐ถโ2) โ (๐ตโ2))))) |
172 | 171 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((๐ถโ2) โ (๐ตโ2)) = 0 โ (((๐ถโ2) โ (๐ตโ2)) โค 0 โง 0 โค ((๐ถโ2) โ (๐ตโ2))))) |
173 | 142, 167,
172 | mpbir2and 712 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ถโ2) โ (๐ตโ2)) = 0) |
174 | 15, 18, 173 | subeq0d 11527 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ถโ2) = (๐ตโ2)) |
175 | 5, 8, 10, 12, 174 | sq11d 14168 |
. . . . 5
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ถ = ๐ต) |
176 | 2, 175 | breqtrrd 5138 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โค ๐ถ) |
177 | | 2sqmod.7 |
. . . . . 6
โข (๐ โ ๐ถ โค ๐ท) |
178 | 177 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ถ โค ๐ท) |
179 | 39 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด โ โ) |
180 | 41 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ท โ โ) |
181 | 19 | nn0ge0d 12483 |
. . . . . . 7
โข (๐ โ 0 โค ๐ด) |
182 | 181 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ 0 โค ๐ด) |
183 | 129 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ 0 โค ๐ท) |
184 | 21 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ดโ2) โ โ) |
185 | 24 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ทโ2) โ โ) |
186 | 167, 29 | breqtrrd 5138 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ 0 โค ((๐ดโ2) โ (๐ทโ2))) |
187 | 168, 170 | letri3d 11304 |
. . . . . . . . 9
โข (๐ โ (((๐ดโ2) โ (๐ทโ2)) = 0 โ (((๐ดโ2) โ (๐ทโ2)) โค 0 โง 0 โค ((๐ดโ2) โ (๐ทโ2))))) |
188 | 187 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (((๐ดโ2) โ (๐ทโ2)) = 0 โ (((๐ดโ2) โ (๐ทโ2)) โค 0 โง 0 โค ((๐ดโ2) โ (๐ทโ2))))) |
189 | 141, 186,
188 | mpbir2and 712 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ((๐ดโ2) โ (๐ทโ2)) = 0) |
190 | 184, 185,
189 | subeq0d 11527 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ดโ2) = (๐ทโ2)) |
191 | 179, 180,
182, 183, 190 | sq11d 14168 |
. . . . 5
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด = ๐ท) |
192 | 178, 191 | breqtrrd 5138 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ถ โค ๐ด) |
193 | 39, 4 | letri3d 11304 |
. . . . 5
โข (๐ โ (๐ด = ๐ถ โ (๐ด โค ๐ถ โง ๐ถ โค ๐ด))) |
194 | 193 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ (๐ด = ๐ถ โ (๐ด โค ๐ถ โง ๐ถ โค ๐ด))) |
195 | 176, 192,
194 | mpbir2and 712 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) โ ๐ด = ๐ถ) |
196 | 20 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ด โ โ) |
197 | 13 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ถ โ โ) |
198 | 16 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ต โ โ) |
199 | 64 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ต โ 0) |
200 | 41 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ท โ โ) |
201 | 7 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ต โ โ) |
202 | 129 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ 0 โค ๐ท) |
203 | 11 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ 0 โค ๐ต) |
204 | 24 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ทโ2) โ โ) |
205 | 17 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ตโ2) โ โ) |
206 | | prmnn 16557 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
207 | 47, 206 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
208 | 207 | nnne0d 12210 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ 0) |
209 | 208 | neneqd 2949 |
. . . . . . . . . 10
โข (๐ โ ยฌ ๐ = 0) |
210 | 209 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ยฌ ๐ = 0) |
211 | 80, 24, 17 | subdid 11618 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ ยท ((๐ทโ2) โ (๐ตโ2))) = ((๐ ยท (๐ทโ2)) โ (๐ ยท (๐ตโ2)))) |
212 | 80, 24 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ ยท (๐ทโ2)) โ โ) |
213 | 21, 24 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ดโ2) ยท (๐ทโ2)) โ โ) |
214 | 80, 17 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ ยท (๐ตโ2)) โ โ) |
215 | 14, 17 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ถโ2) ยท (๐ตโ2)) โ โ) |
216 | 17, 24 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ตโ2) ยท (๐ทโ2)) = ((๐ทโ2) ยท (๐ตโ2))) |
217 | 25 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) โ (๐ดโ2)) = (๐ โ (๐ดโ2))) |
218 | 21, 17 | pncan2d 11521 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) โ (๐ดโ2)) = (๐ตโ2)) |
219 | 217, 218 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ โ (๐ดโ2)) = (๐ตโ2)) |
220 | 219 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ โ (๐ดโ2)) ยท (๐ทโ2)) = ((๐ตโ2) ยท (๐ทโ2))) |
221 | 26 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ถโ2) + (๐ทโ2)) โ (๐ถโ2)) = (๐ โ (๐ถโ2))) |
222 | 14, 24 | pncan2d 11521 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ถโ2) + (๐ทโ2)) โ (๐ถโ2)) = (๐ทโ2)) |
223 | 221, 222 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ โ (๐ถโ2)) = (๐ทโ2)) |
224 | 223 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((๐ โ (๐ถโ2)) ยท (๐ตโ2)) = ((๐ทโ2) ยท (๐ตโ2))) |
225 | 216, 220,
224 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ โ (๐ดโ2)) ยท (๐ทโ2)) = ((๐ โ (๐ถโ2)) ยท (๐ตโ2))) |
226 | 80, 21, 24 | subdird 11619 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ โ (๐ดโ2)) ยท (๐ทโ2)) = ((๐ ยท (๐ทโ2)) โ ((๐ดโ2) ยท (๐ทโ2)))) |
227 | 80, 14, 17 | subdird 11619 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ โ (๐ถโ2)) ยท (๐ตโ2)) = ((๐ ยท (๐ตโ2)) โ ((๐ถโ2) ยท (๐ตโ2)))) |
228 | 225, 226,
227 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ ยท (๐ทโ2)) โ ((๐ดโ2) ยท (๐ทโ2))) = ((๐ ยท (๐ตโ2)) โ ((๐ถโ2) ยท (๐ตโ2)))) |
229 | 212, 213,
214, 215, 228 | subeqxfrd 11571 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ ยท (๐ทโ2)) โ (๐ ยท (๐ตโ2))) = (((๐ดโ2) ยท (๐ทโ2)) โ ((๐ถโ2) ยท (๐ตโ2)))) |
230 | 211, 229 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท ((๐ทโ2) โ (๐ตโ2))) = (((๐ดโ2) ยท (๐ทโ2)) โ ((๐ถโ2) ยท (๐ตโ2)))) |
231 | 20, 23 | sqmuld 14070 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ด ยท ๐ท)โ2) = ((๐ดโ2) ยท (๐ทโ2))) |
232 | 13, 16 | sqmuld 14070 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ถ ยท ๐ต)โ2) = ((๐ถโ2) ยท (๐ตโ2))) |
233 | 231, 232 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ด ยท ๐ท)โ2) โ ((๐ถ ยท ๐ต)โ2)) = (((๐ดโ2) ยท (๐ทโ2)) โ ((๐ถโ2) ยท (๐ตโ2)))) |
234 | 20, 23 | mulcld 11182 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ด ยท ๐ท) โ โ) |
235 | 13, 16 | mulcld 11182 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ถ ยท ๐ต) โ โ) |
236 | | subsq 14121 |
. . . . . . . . . . . . . . 15
โข (((๐ด ยท ๐ท) โ โ โง (๐ถ ยท ๐ต) โ โ) โ (((๐ด ยท ๐ท)โ2) โ ((๐ถ ยท ๐ต)โ2)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)))) |
237 | 234, 235,
236 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ด ยท ๐ท)โ2) โ ((๐ถ ยท ๐ต)โ2)) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)))) |
238 | 230, 233,
237 | 3eqtr2d 2783 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท ((๐ทโ2) โ (๐ตโ2))) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)))) |
239 | 238 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ ยท ((๐ทโ2) โ (๐ตโ2))) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)))) |
240 | 234 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ด ยท ๐ท) โ โ) |
241 | | simpll 766 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ ๐) |
242 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) |
243 | 242 | neqned 2951 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) |
244 | 89, 90 | zsubcld 12619 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ โค) |
245 | | dvdssqim 16442 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ โค) โ (๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
246 | 79, 244, 245 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
247 | 246 | imp 408 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) |
248 | 247 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ (๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) |
249 | 95 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (๐โ2) โ โค) |
250 | 244 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ โค) |
251 | 234 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (๐ด ยท ๐ท) โ โ) |
252 | 235 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (๐ถ ยท ๐ต) โ โ) |
253 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) |
254 | 251, 252,
253 | subne0d 11528 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ 0) |
255 | 250, 254 | znsqcld 14074 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) โ โ) |
256 | | dvdsle 16199 |
. . . . . . . . . . . . . . . . . 18
โข (((๐โ2) โ โค โง
(((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) โ โ) โ ((๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) โ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
257 | 249, 255,
256 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ ((๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) โ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
258 | 257 | imp 408 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โง (๐โ2) โฅ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) โ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) |
259 | 241, 243,
248, 258 | syl21anc 837 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) |
260 | 39, 41 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ด ยท ๐ท) โ โ) |
261 | 4, 7 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ถ ยท ๐ต) โ โ) |
262 | 260, 261 | resubcld 11590 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ โ) |
263 | 262 | resqcld 14037 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) โ โ) |
264 | 61 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ถ โ
โ+) |
265 | 127, 264 | rpmulcld 12980 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ด ยท ๐ถ) โ
โ+) |
266 | 66 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ต โ
โ+) |
267 | 57 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ท โ
โ+) |
268 | 266, 267 | rpmulcld 12980 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ต ยท ๐ท) โ
โ+) |
269 | 265, 268 | rpaddcld 12979 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((๐ด ยท ๐ถ) + (๐ต ยท ๐ท)) โ
โ+) |
270 | | 2z 12542 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 2 โ
โค |
271 | 270 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 2 โ
โค) |
272 | 269, 271 | rpexpcld 14157 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) โ
โ+) |
273 | 263, 272 | ltaddrp2d 12998 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) < ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
274 | | bhmafibid2 15358 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) + (๐ทโ2))) = ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))โ2))) |
275 | 39, 7, 4, 41, 274 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (((๐ดโ2) + (๐ตโ2)) ยท ((๐ถโ2) + (๐ทโ2))) = ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))โ2))) |
276 | 74, 275 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ ยท ๐) = ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))โ2))) |
277 | 82 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) = ((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))) |
278 | 277 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) = (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))โ2)) |
279 | 278 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) = ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))โ2))) |
280 | 276, 279 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ ยท ๐) = ((((๐ด ยท ๐ถ) + (๐ต ยท ๐ท))โ2) + (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
281 | 273, 280 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) < (๐ ยท ๐)) |
282 | 281, 81 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) < (๐โ2)) |
283 | 241, 282 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) < (๐โ2)) |
284 | 263, 100 | ltnled 11309 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) < (๐โ2) โ ยฌ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
285 | 241, 284 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ ((((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2) < (๐โ2) โ ยฌ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2))) |
286 | 283, 285 | mpbid 231 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โง ยฌ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) โ ยฌ (๐โ2) โค (((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))โ2)) |
287 | 259, 286 | condan 817 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ด ยท ๐ท) = (๐ถ ยท ๐ต)) |
288 | 240, 287 | subeq0bd 11588 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) = 0) |
289 | 288 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) = (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท 0)) |
290 | 234, 235 | addcld 11181 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โ) |
291 | 290 | mul01d 11361 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท 0) = 0) |
292 | 291 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท 0) = 0) |
293 | 239, 289,
292 | 3eqtrd 2781 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ ยท ((๐ทโ2) โ (๐ตโ2))) = 0) |
294 | 24, 17 | subcld 11519 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ทโ2) โ (๐ตโ2)) โ โ) |
295 | 80, 294 | mul0ord 11812 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ((๐ทโ2) โ (๐ตโ2))) = 0 โ (๐ = 0 โจ ((๐ทโ2) โ (๐ตโ2)) = 0))) |
296 | 295 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ((๐ ยท ((๐ทโ2) โ (๐ตโ2))) = 0 โ (๐ = 0 โจ ((๐ทโ2) โ (๐ตโ2)) = 0))) |
297 | 293, 296 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ = 0 โจ ((๐ทโ2) โ (๐ตโ2)) = 0)) |
298 | 297 | ord 863 |
. . . . . . . . 9
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (ยฌ ๐ = 0 โ ((๐ทโ2) โ (๐ตโ2)) = 0)) |
299 | 210, 298 | mpd 15 |
. . . . . . . 8
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ((๐ทโ2) โ (๐ตโ2)) = 0) |
300 | 204, 205,
299 | subeq0d 11527 |
. . . . . . 7
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ทโ2) = (๐ตโ2)) |
301 | 200, 201,
202, 203, 300 | sq11d 14168 |
. . . . . 6
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ท = ๐ต) |
302 | 301 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ด ยท ๐ท) = (๐ด ยท ๐ต)) |
303 | 302, 287 | eqtr3d 2779 |
. . . 4
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ด ยท ๐ต) = (๐ถ ยท ๐ต)) |
304 | 196, 197,
198, 199, 303 | mulcan2ad 11798 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ ๐ด = ๐ถ) |
305 | 137, 163 | zsubcld 12619 |
. . . . . 6
โข (๐ โ ((๐ทโ2) โ (๐ตโ2)) โ โค) |
306 | | dvdsmul1 16167 |
. . . . . 6
โข ((๐ โ โค โง ((๐ทโ2) โ (๐ตโ2)) โ โค) โ
๐ โฅ (๐ ยท ((๐ทโ2) โ (๐ตโ2)))) |
307 | 79, 305, 306 | syl2anc 585 |
. . . . 5
โข (๐ โ ๐ โฅ (๐ ยท ((๐ทโ2) โ (๐ตโ2)))) |
308 | 307, 238 | breqtrd 5136 |
. . . 4
โข (๐ โ ๐ โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)))) |
309 | | euclemma 16596 |
. . . . 5
โข ((๐ โ โ โง ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โ โค โง ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)) โ โค) โ (๐ โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โจ ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))))) |
310 | 47, 91, 244, 309 | syl3anc 1372 |
. . . 4
โข (๐ โ (๐ โฅ (((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) ยท ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))) โ (๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โจ ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต))))) |
311 | 308, 310 | mpbid 231 |
. . 3
โข (๐ โ (๐ โฅ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) โจ ๐ โฅ ((๐ด ยท ๐ท) โ (๐ถ ยท ๐ต)))) |
312 | 195, 304,
311 | mpjaodan 958 |
. 2
โข (๐ โ ๐ด = ๐ถ) |
313 | 312 | oveq1d 7377 |
. . . . 5
โข (๐ โ (๐ดโ2) = (๐ถโ2)) |
314 | 313 | oveq2d 7378 |
. . . 4
โข (๐ โ (๐ โ (๐ดโ2)) = (๐ โ (๐ถโ2))) |
315 | 314, 219,
223 | 3eqtr3d 2785 |
. . 3
โข (๐ โ (๐ตโ2) = (๐ทโ2)) |
316 | 7, 41, 11, 129, 315 | sq11d 14168 |
. 2
โข (๐ โ ๐ต = ๐ท) |
317 | 312, 316 | jca 513 |
1
โข (๐ โ (๐ด = ๐ถ โง ๐ต = ๐ท)) |