Step | Hyp | Ref
| Expression |
1 | | 2sq.1 |
. . 3
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) |
2 | | 2sqlem5.1 |
. . . 4
โข (๐ โ ๐ โ โ) |
3 | 2 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ โ โ) |
4 | | 2sqlem5.2 |
. . . 4
โข (๐ โ ๐ โ โ) |
5 | 4 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ โ โ) |
6 | | 2sqlem4.3 |
. . . 4
โข (๐ โ ๐ด โ โค) |
7 | 6 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ด โ โค) |
8 | | 2sqlem4.4 |
. . . 4
โข (๐ โ ๐ต โ โค) |
9 | 8 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ต โ โค) |
10 | | 2sqlem4.5 |
. . . 4
โข (๐ โ ๐ถ โ โค) |
11 | 10 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ถ โ โค) |
12 | | 2sqlem4.6 |
. . . 4
โข (๐ โ ๐ท โ โค) |
13 | 12 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ท โ โค) |
14 | | 2sqlem4.7 |
. . . 4
โข (๐ โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) |
15 | 14 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) |
16 | | 2sqlem4.8 |
. . . 4
โข (๐ โ ๐ = ((๐ถโ2) + (๐ทโ2))) |
17 | 16 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ = ((๐ถโ2) + (๐ทโ2))) |
18 | | simpr 486 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) |
19 | 1, 3, 5, 7, 9, 11,
13, 15, 17, 18 | 2sqlem3 26771 |
. 2
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) โ ๐ โ ๐) |
20 | 2 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ โ โ) |
21 | 4 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ โ โ) |
22 | 6 | znegcld 12610 |
. . . 4
โข (๐ โ -๐ด โ โค) |
23 | 22 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ -๐ด โ โค) |
24 | 8 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ต โ โค) |
25 | 10 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ถ โ โค) |
26 | 12 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ท โ โค) |
27 | 6 | zcnd 12609 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
28 | | sqneg 14022 |
. . . . . . 7
โข (๐ด โ โ โ (-๐ดโ2) = (๐ดโ2)) |
29 | 27, 28 | syl 17 |
. . . . . 6
โข (๐ โ (-๐ดโ2) = (๐ดโ2)) |
30 | 29 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((-๐ดโ2) + (๐ตโ2)) = ((๐ดโ2) + (๐ตโ2))) |
31 | 14, 30 | eqtr4d 2780 |
. . . 4
โข (๐ โ (๐ ยท ๐) = ((-๐ดโ2) + (๐ตโ2))) |
32 | 31 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ (๐ ยท ๐) = ((-๐ดโ2) + (๐ตโ2))) |
33 | 16 | adantr 482 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ = ((๐ถโ2) + (๐ทโ2))) |
34 | 12 | zcnd 12609 |
. . . . . . . 8
โข (๐ โ ๐ท โ โ) |
35 | 27, 34 | mulneg1d 11609 |
. . . . . . 7
โข (๐ โ (-๐ด ยท ๐ท) = -(๐ด ยท ๐ท)) |
36 | 35 | oveq2d 7374 |
. . . . . 6
โข (๐ โ ((๐ถ ยท ๐ต) + (-๐ด ยท ๐ท)) = ((๐ถ ยท ๐ต) + -(๐ด ยท ๐ท))) |
37 | 10, 8 | zmulcld 12614 |
. . . . . . . 8
โข (๐ โ (๐ถ ยท ๐ต) โ โค) |
38 | 37 | zcnd 12609 |
. . . . . . 7
โข (๐ โ (๐ถ ยท ๐ต) โ โ) |
39 | 6, 12 | zmulcld 12614 |
. . . . . . . 8
โข (๐ โ (๐ด ยท ๐ท) โ โค) |
40 | 39 | zcnd 12609 |
. . . . . . 7
โข (๐ โ (๐ด ยท ๐ท) โ โ) |
41 | 38, 40 | negsubd 11519 |
. . . . . 6
โข (๐ โ ((๐ถ ยท ๐ต) + -(๐ด ยท ๐ท)) = ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) |
42 | 36, 41 | eqtrd 2777 |
. . . . 5
โข (๐ โ ((๐ถ ยท ๐ต) + (-๐ด ยท ๐ท)) = ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) |
43 | 42 | breq2d 5118 |
. . . 4
โข (๐ โ (๐ โฅ ((๐ถ ยท ๐ต) + (-๐ด ยท ๐ท)) โ ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)))) |
44 | 43 | biimpar 479 |
. . 3
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ โฅ ((๐ถ ยท ๐ต) + (-๐ด ยท ๐ท))) |
45 | 1, 20, 21, 23, 24, 25, 26, 32, 33, 44 | 2sqlem3 26771 |
. 2
โข ((๐ โง ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ ๐ โ ๐) |
46 | | prmz 16552 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
47 | 4, 46 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โค) |
48 | | zsqcl 14035 |
. . . . . . . 8
โข (๐ถ โ โค โ (๐ถโ2) โ
โค) |
49 | 10, 48 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ถโ2) โ โค) |
50 | 2 | nnzd 12527 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
51 | 49, 50 | zmulcld 12614 |
. . . . . 6
โข (๐ โ ((๐ถโ2) ยท ๐) โ โค) |
52 | | zsqcl 14035 |
. . . . . . 7
โข (๐ด โ โค โ (๐ดโ2) โ
โค) |
53 | 6, 52 | syl 17 |
. . . . . 6
โข (๐ โ (๐ดโ2) โ โค) |
54 | 51, 53 | zsubcld 12613 |
. . . . 5
โข (๐ โ (((๐ถโ2) ยท ๐) โ (๐ดโ2)) โ โค) |
55 | | dvdsmul1 16161 |
. . . . 5
โข ((๐ โ โค โง (((๐ถโ2) ยท ๐) โ (๐ดโ2)) โ โค) โ ๐ โฅ (๐ ยท (((๐ถโ2) ยท ๐) โ (๐ดโ2)))) |
56 | 47, 54, 55 | syl2anc 585 |
. . . 4
โข (๐ โ ๐ โฅ (๐ ยท (((๐ถโ2) ยท ๐) โ (๐ดโ2)))) |
57 | 10, 6 | zmulcld 12614 |
. . . . . . . . 9
โข (๐ โ (๐ถ ยท ๐ด) โ โค) |
58 | 57 | zcnd 12609 |
. . . . . . . 8
โข (๐ โ (๐ถ ยท ๐ด) โ โ) |
59 | 58 | sqcld 14050 |
. . . . . . 7
โข (๐ โ ((๐ถ ยท ๐ด)โ2) โ โ) |
60 | 38 | sqcld 14050 |
. . . . . . 7
โข (๐ โ ((๐ถ ยท ๐ต)โ2) โ โ) |
61 | 40 | sqcld 14050 |
. . . . . . 7
โข (๐ โ ((๐ด ยท ๐ท)โ2) โ โ) |
62 | 59, 60, 61 | pnpcand 11550 |
. . . . . 6
โข (๐ โ ((((๐ถ ยท ๐ด)โ2) + ((๐ถ ยท ๐ต)โ2)) โ (((๐ถ ยท ๐ด)โ2) + ((๐ด ยท ๐ท)โ2))) = (((๐ถ ยท ๐ต)โ2) โ ((๐ด ยท ๐ท)โ2))) |
63 | 10 | zcnd 12609 |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
64 | 63, 27 | sqmuld 14064 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ ยท ๐ด)โ2) = ((๐ถโ2) ยท (๐ดโ2))) |
65 | 8 | zcnd 12609 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โ) |
66 | 63, 65 | sqmuld 14064 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ ยท ๐ต)โ2) = ((๐ถโ2) ยท (๐ตโ2))) |
67 | 64, 66 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ (((๐ถ ยท ๐ด)โ2) + ((๐ถ ยท ๐ต)โ2)) = (((๐ถโ2) ยท (๐ดโ2)) + ((๐ถโ2) ยท (๐ตโ2)))) |
68 | 63 | sqcld 14050 |
. . . . . . . . . . 11
โข (๐ โ (๐ถโ2) โ โ) |
69 | 53 | zcnd 12609 |
. . . . . . . . . . 11
โข (๐ โ (๐ดโ2) โ โ) |
70 | 65 | sqcld 14050 |
. . . . . . . . . . 11
โข (๐ โ (๐ตโ2) โ โ) |
71 | 68, 69, 70 | adddid 11180 |
. . . . . . . . . 10
โข (๐ โ ((๐ถโ2) ยท ((๐ดโ2) + (๐ตโ2))) = (((๐ถโ2) ยท (๐ดโ2)) + ((๐ถโ2) ยท (๐ตโ2)))) |
72 | 67, 71 | eqtr4d 2780 |
. . . . . . . . 9
โข (๐ โ (((๐ถ ยท ๐ด)โ2) + ((๐ถ ยท ๐ต)โ2)) = ((๐ถโ2) ยท ((๐ดโ2) + (๐ตโ2)))) |
73 | 2 | nncnd 12170 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
74 | 47 | zcnd 12609 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
75 | 73, 74 | mulcomd 11177 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
76 | 14, 75 | eqtr3d 2779 |
. . . . . . . . . . 11
โข (๐ โ ((๐ดโ2) + (๐ตโ2)) = (๐ ยท ๐)) |
77 | 76 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ โ ((๐ถโ2) ยท ((๐ดโ2) + (๐ตโ2))) = ((๐ถโ2) ยท (๐ ยท ๐))) |
78 | 68, 74, 73 | mul12d 11365 |
. . . . . . . . . 10
โข (๐ โ ((๐ถโ2) ยท (๐ ยท ๐)) = (๐ ยท ((๐ถโ2) ยท ๐))) |
79 | 77, 78 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ ((๐ถโ2) ยท ((๐ดโ2) + (๐ตโ2))) = (๐ ยท ((๐ถโ2) ยท ๐))) |
80 | 72, 79 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((๐ถ ยท ๐ด)โ2) + ((๐ถ ยท ๐ต)โ2)) = (๐ ยท ((๐ถโ2) ยท ๐))) |
81 | 27, 34 | sqmuld 14064 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ด ยท ๐ท)โ2) = ((๐ดโ2) ยท (๐ทโ2))) |
82 | 34 | sqcld 14050 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ทโ2) โ โ) |
83 | 69, 82 | mulcomd 11177 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ดโ2) ยท (๐ทโ2)) = ((๐ทโ2) ยท (๐ดโ2))) |
84 | 81, 83 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด ยท ๐ท)โ2) = ((๐ทโ2) ยท (๐ดโ2))) |
85 | 64, 84 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ (((๐ถ ยท ๐ด)โ2) + ((๐ด ยท ๐ท)โ2)) = (((๐ถโ2) ยท (๐ดโ2)) + ((๐ทโ2) ยท (๐ดโ2)))) |
86 | 49 | zcnd 12609 |
. . . . . . . . . . 11
โข (๐ โ (๐ถโ2) โ โ) |
87 | 86, 82, 69 | adddird 11181 |
. . . . . . . . . 10
โข (๐ โ (((๐ถโ2) + (๐ทโ2)) ยท (๐ดโ2)) = (((๐ถโ2) ยท (๐ดโ2)) + ((๐ทโ2) ยท (๐ดโ2)))) |
88 | 85, 87 | eqtr4d 2780 |
. . . . . . . . 9
โข (๐ โ (((๐ถ ยท ๐ด)โ2) + ((๐ด ยท ๐ท)โ2)) = (((๐ถโ2) + (๐ทโ2)) ยท (๐ดโ2))) |
89 | 16 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ (๐ ยท (๐ดโ2)) = (((๐ถโ2) + (๐ทโ2)) ยท (๐ดโ2))) |
90 | 88, 89 | eqtr4d 2780 |
. . . . . . . 8
โข (๐ โ (((๐ถ ยท ๐ด)โ2) + ((๐ด ยท ๐ท)โ2)) = (๐ ยท (๐ดโ2))) |
91 | 80, 90 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ ((((๐ถ ยท ๐ด)โ2) + ((๐ถ ยท ๐ต)โ2)) โ (((๐ถ ยท ๐ด)โ2) + ((๐ด ยท ๐ท)โ2))) = ((๐ ยท ((๐ถโ2) ยท ๐)) โ (๐ ยท (๐ดโ2)))) |
92 | 51 | zcnd 12609 |
. . . . . . . 8
โข (๐ โ ((๐ถโ2) ยท ๐) โ โ) |
93 | 74, 92, 69 | subdid 11612 |
. . . . . . 7
โข (๐ โ (๐ ยท (((๐ถโ2) ยท ๐) โ (๐ดโ2))) = ((๐ ยท ((๐ถโ2) ยท ๐)) โ (๐ ยท (๐ดโ2)))) |
94 | 91, 93 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ ((((๐ถ ยท ๐ด)โ2) + ((๐ถ ยท ๐ต)โ2)) โ (((๐ถ ยท ๐ด)โ2) + ((๐ด ยท ๐ท)โ2))) = (๐ ยท (((๐ถโ2) ยท ๐) โ (๐ดโ2)))) |
95 | 62, 94 | eqtr3d 2779 |
. . . . 5
โข (๐ โ (((๐ถ ยท ๐ต)โ2) โ ((๐ด ยท ๐ท)โ2)) = (๐ ยท (((๐ถโ2) ยท ๐) โ (๐ดโ2)))) |
96 | | subsq 14115 |
. . . . . 6
โข (((๐ถ ยท ๐ต) โ โ โง (๐ด ยท ๐ท) โ โ) โ (((๐ถ ยท ๐ต)โ2) โ ((๐ด ยท ๐ท)โ2)) = (((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) ยท ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)))) |
97 | 38, 40, 96 | syl2anc 585 |
. . . . 5
โข (๐ โ (((๐ถ ยท ๐ต)โ2) โ ((๐ด ยท ๐ท)โ2)) = (((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) ยท ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)))) |
98 | 95, 97 | eqtr3d 2779 |
. . . 4
โข (๐ โ (๐ ยท (((๐ถโ2) ยท ๐) โ (๐ดโ2))) = (((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) ยท ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)))) |
99 | 56, 98 | breqtrd 5132 |
. . 3
โข (๐ โ ๐ โฅ (((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) ยท ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)))) |
100 | 37, 39 | zaddcld 12612 |
. . . 4
โข (๐ โ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) โ โค) |
101 | 37, 39 | zsubcld 12613 |
. . . 4
โข (๐ โ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)) โ โค) |
102 | | euclemma 16590 |
. . . 4
โข ((๐ โ โ โง ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) โ โค โง ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)) โ โค) โ (๐ โฅ (((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) ยท ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ (๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) โจ ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))))) |
103 | 4, 100, 101, 102 | syl3anc 1372 |
. . 3
โข (๐ โ (๐ โฅ (((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) ยท ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))) โ (๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) โจ ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท))))) |
104 | 99, 103 | mpbid 231 |
. 2
โข (๐ โ (๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) โจ ๐ โฅ ((๐ถ ยท ๐ต) โ (๐ด ยท ๐ท)))) |
105 | 19, 45, 104 | mpjaodan 958 |
1
โข (๐ โ ๐ โ ๐) |