Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . . . . . 7
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
2 | | 4sq.2 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
3 | | 4sq.3 |
. . . . . . 7
โข (๐ โ ๐ = ((2 ยท ๐) + 1)) |
4 | | 4sq.4 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
5 | | 4sq.5 |
. . . . . . 7
โข (๐ โ (0...(2 ยท ๐)) โ ๐) |
6 | | 4sq.6 |
. . . . . . 7
โข ๐ = {๐ โ โ โฃ (๐ ยท ๐) โ ๐} |
7 | | 4sq.7 |
. . . . . . 7
โข ๐ = inf(๐, โ, < ) |
8 | | 4sq.m |
. . . . . . 7
โข (๐ โ ๐ โ
(โคโฅโ2)) |
9 | | 4sq.a |
. . . . . . 7
โข (๐ โ ๐ด โ โค) |
10 | | 4sq.b |
. . . . . . 7
โข (๐ โ ๐ต โ โค) |
11 | | 4sq.c |
. . . . . . 7
โข (๐ โ ๐ถ โ โค) |
12 | | 4sq.d |
. . . . . . 7
โข (๐ โ ๐ท โ โค) |
13 | | 4sq.e |
. . . . . . 7
โข ๐ธ = (((๐ด + (๐ / 2)) mod ๐) โ (๐ / 2)) |
14 | | 4sq.f |
. . . . . . 7
โข ๐น = (((๐ต + (๐ / 2)) mod ๐) โ (๐ / 2)) |
15 | | 4sq.g |
. . . . . . 7
โข ๐บ = (((๐ถ + (๐ / 2)) mod ๐) โ (๐ / 2)) |
16 | | 4sq.h |
. . . . . . 7
โข ๐ป = (((๐ท + (๐ / 2)) mod ๐) โ (๐ / 2)) |
17 | | 4sq.r |
. . . . . . 7
โข ๐
= ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐) |
18 | | 4sq.p |
. . . . . . 7
โข (๐ โ (๐ ยท ๐) = (((๐ดโ2) + (๐ตโ2)) + ((๐ถโ2) + (๐ทโ2)))) |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem16 16839 |
. . . . . 6
โข (๐ โ (๐
โค ๐ โง ((๐
= 0 โจ ๐
= ๐) โ (๐โ2) โฅ (๐ ยท ๐)))) |
20 | 19 | simpld 496 |
. . . . 5
โข (๐ โ ๐
โค ๐) |
21 | 6 | ssrab3 4045 |
. . . . . . . 8
โข ๐ โ
โ |
22 | | nnuz 12813 |
. . . . . . . 8
โข โ =
(โคโฅโ1) |
23 | 21, 22 | sseqtri 3985 |
. . . . . . 7
โข ๐ โ
(โคโฅโ1) |
24 | 1, 2, 3, 4, 5, 6, 7 | 4sqlem13 16836 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โ โ
โง ๐ < ๐)) |
25 | 24 | simpld 496 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ
) |
26 | | infssuzcl 12864 |
. . . . . . . . . . . . . . 15
โข ((๐ โ
(โคโฅโ1) โง ๐ โ โ
) โ inf(๐, โ, < ) โ ๐) |
27 | 23, 25, 26 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (๐ โ inf(๐, โ, < ) โ ๐) |
28 | 7, 27 | eqeltrid 2842 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ ๐) |
29 | 21, 28 | sselid 3947 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
30 | 29 | nnred 12175 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
31 | 24 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ ๐ < ๐) |
32 | 30, 31 | ltned 11298 |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐) |
33 | 29 | nncnd 12176 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
34 | 33 | sqvald 14055 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
35 | 34 | breq1d 5120 |
. . . . . . . . . . . 12
โข (๐ โ ((๐โ2) โฅ (๐ ยท ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
36 | 29 | nnzd 12533 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โค) |
37 | | prmz 16558 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โค) |
38 | 4, 37 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โค) |
39 | 29 | nnne0d 12210 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ 0) |
40 | | dvdscmulr 16174 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค โง (๐ โ โค โง ๐ โ 0)) โ ((๐ ยท ๐) โฅ (๐ ยท ๐) โ ๐ โฅ ๐)) |
41 | 36, 38, 36, 39, 40 | syl112anc 1375 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ๐) โฅ (๐ ยท ๐) โ ๐ โฅ ๐)) |
42 | | dvdsprm 16586 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ = ๐)) |
43 | 8, 4, 42 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โฅ ๐ โ ๐ = ๐)) |
44 | 35, 41, 43 | 3bitrd 305 |
. . . . . . . . . . 11
โข (๐ โ ((๐โ2) โฅ (๐ ยท ๐) โ ๐ = ๐)) |
45 | 44 | necon3bbid 2982 |
. . . . . . . . . 10
โข (๐ โ (ยฌ (๐โ2) โฅ (๐ ยท ๐) โ ๐ โ ๐)) |
46 | 32, 45 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ ยฌ (๐โ2) โฅ (๐ ยท ๐)) |
47 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem14 16837 |
. . . . . . . . . . . 12
โข (๐ โ ๐
โ
โ0) |
48 | | elnn0 12422 |
. . . . . . . . . . . 12
โข (๐
โ โ0
โ (๐
โ โ
โจ ๐
=
0)) |
49 | 47, 48 | sylib 217 |
. . . . . . . . . . 11
โข (๐ โ (๐
โ โ โจ ๐
= 0)) |
50 | 49 | ord 863 |
. . . . . . . . . 10
โข (๐ โ (ยฌ ๐
โ โ โ ๐
= 0)) |
51 | | orc 866 |
. . . . . . . . . . 11
โข (๐
= 0 โ (๐
= 0 โจ ๐
= ๐)) |
52 | 19 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ ((๐
= 0 โจ ๐
= ๐) โ (๐โ2) โฅ (๐ ยท ๐))) |
53 | 51, 52 | syl5 34 |
. . . . . . . . . 10
โข (๐ โ (๐
= 0 โ (๐โ2) โฅ (๐ ยท ๐))) |
54 | 50, 53 | syld 47 |
. . . . . . . . 9
โข (๐ โ (ยฌ ๐
โ โ โ (๐โ2) โฅ (๐ ยท ๐))) |
55 | 46, 54 | mt3d 148 |
. . . . . . . 8
โข (๐ โ ๐
โ โ) |
56 | | gzreim 16818 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด + (i ยท ๐ต)) โ โค[i]) |
57 | 9, 10, 56 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ด + (i ยท ๐ต)) โ โค[i]) |
58 | | gzcn 16811 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด + (i ยท ๐ต)) โ โค[i] โ (๐ด + (i ยท ๐ต)) โ โ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ด + (i ยท ๐ต)) โ โ) |
60 | 59 | absvalsq2d 15335 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((absโ(๐ด + (i ยท ๐ต)))โ2) = (((โโ(๐ด + (i ยท ๐ต)))โ2) + ((โโ(๐ด + (i ยท ๐ต)))โ2))) |
61 | 9 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ด โ โ) |
62 | 10 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ต โ โ) |
63 | 61, 62 | crred 15123 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ด) |
64 | 63 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ(๐ด + (i ยท ๐ต)))โ2) = (๐ดโ2)) |
65 | 61, 62 | crimd 15124 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ต) |
66 | 65 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ(๐ด + (i ยท ๐ต)))โ2) = (๐ตโ2)) |
67 | 64, 66 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((โโ(๐ด + (i ยท ๐ต)))โ2) + ((โโ(๐ด + (i ยท ๐ต)))โ2)) = ((๐ดโ2) + (๐ตโ2))) |
68 | 60, 67 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((absโ(๐ด + (i ยท ๐ต)))โ2) = ((๐ดโ2) + (๐ตโ2))) |
69 | | gzreim 16818 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ถ โ โค โง ๐ท โ โค) โ (๐ถ + (i ยท ๐ท)) โ โค[i]) |
70 | 11, 12, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ถ + (i ยท ๐ท)) โ โค[i]) |
71 | | gzcn 16811 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ถ + (i ยท ๐ท)) โ โค[i] โ (๐ถ + (i ยท ๐ท)) โ โ) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ถ + (i ยท ๐ท)) โ โ) |
73 | 72 | absvalsq2d 15335 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((absโ(๐ถ + (i ยท ๐ท)))โ2) = (((โโ(๐ถ + (i ยท ๐ท)))โ2) + ((โโ(๐ถ + (i ยท ๐ท)))โ2))) |
74 | 11 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ถ โ โ) |
75 | 12 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ท โ โ) |
76 | 74, 75 | crred 15123 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ(๐ถ + (i ยท ๐ท))) = ๐ถ) |
77 | 76 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ(๐ถ + (i ยท ๐ท)))โ2) = (๐ถโ2)) |
78 | 74, 75 | crimd 15124 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ(๐ถ + (i ยท ๐ท))) = ๐ท) |
79 | 78 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((โโ(๐ถ + (i ยท ๐ท)))โ2) = (๐ทโ2)) |
80 | 77, 79 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((โโ(๐ถ + (i ยท ๐ท)))โ2) + ((โโ(๐ถ + (i ยท ๐ท)))โ2)) = ((๐ถโ2) + (๐ทโ2))) |
81 | 73, 80 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((absโ(๐ถ + (i ยท ๐ท)))โ2) = ((๐ถโ2) + (๐ทโ2))) |
82 | 68, 81 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข (๐ โ (((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) = (((๐ดโ2) + (๐ตโ2)) + ((๐ถโ2) + (๐ทโ2)))) |
83 | 18, 82 | eqtr4d 2780 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท ๐) = (((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2))) |
84 | 83 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ๐) / ๐) = ((((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) / ๐)) |
85 | | prmnn 16557 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
86 | 4, 85 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
87 | 86 | nncnd 12176 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
88 | 87, 33, 39 | divcan3d 11943 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ๐) / ๐) = ๐) |
89 | 84, 88 | eqtr3d 2779 |
. . . . . . . . . . 11
โข (๐ โ ((((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) / ๐) = ๐) |
90 | 9, 29, 13 | 4sqlem5 16821 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ธ โ โค โง ((๐ด โ ๐ธ) / ๐) โ โค)) |
91 | 90 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ธ โ โค) |
92 | 10, 29, 14 | 4sqlem5 16821 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐น โ โค โง ((๐ต โ ๐น) / ๐) โ โค)) |
93 | 92 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐น โ โค) |
94 | | gzreim 16818 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ธ โ โค โง ๐น โ โค) โ (๐ธ + (i ยท ๐น)) โ โค[i]) |
95 | 91, 93, 94 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ธ + (i ยท ๐น)) โ โค[i]) |
96 | | gzcn 16811 |
. . . . . . . . . . . . . . . . 17
โข ((๐ธ + (i ยท ๐น)) โ โค[i] โ (๐ธ + (i ยท ๐น)) โ โ) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ธ + (i ยท ๐น)) โ โ) |
98 | 97 | absvalsq2d 15335 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((absโ(๐ธ + (i ยท ๐น)))โ2) = (((โโ(๐ธ + (i ยท ๐น)))โ2) + ((โโ(๐ธ + (i ยท ๐น)))โ2))) |
99 | 91 | zred 12614 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ธ โ โ) |
100 | 93 | zred 12614 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐น โ โ) |
101 | 99, 100 | crred 15123 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(๐ธ + (i ยท ๐น))) = ๐ธ) |
102 | 101 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ(๐ธ + (i ยท ๐น)))โ2) = (๐ธโ2)) |
103 | 99, 100 | crimd 15124 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(๐ธ + (i ยท ๐น))) = ๐น) |
104 | 103 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ(๐ธ + (i ยท ๐น)))โ2) = (๐นโ2)) |
105 | 102, 104 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((โโ(๐ธ + (i ยท ๐น)))โ2) + ((โโ(๐ธ + (i ยท ๐น)))โ2)) = ((๐ธโ2) + (๐นโ2))) |
106 | 98, 105 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((absโ(๐ธ + (i ยท ๐น)))โ2) = ((๐ธโ2) + (๐นโ2))) |
107 | 11, 29, 15 | 4sqlem5 16821 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐บ โ โค โง ((๐ถ โ ๐บ) / ๐) โ โค)) |
108 | 107 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐บ โ โค) |
109 | 12, 29, 16 | 4sqlem5 16821 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ป โ โค โง ((๐ท โ ๐ป) / ๐) โ โค)) |
110 | 109 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ป โ โค) |
111 | | gzreim 16818 |
. . . . . . . . . . . . . . . . . 18
โข ((๐บ โ โค โง ๐ป โ โค) โ (๐บ + (i ยท ๐ป)) โ โค[i]) |
112 | 108, 110,
111 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐บ + (i ยท ๐ป)) โ โค[i]) |
113 | | gzcn 16811 |
. . . . . . . . . . . . . . . . 17
โข ((๐บ + (i ยท ๐ป)) โ โค[i] โ (๐บ + (i ยท ๐ป)) โ โ) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐บ + (i ยท ๐ป)) โ โ) |
115 | 114 | absvalsq2d 15335 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((absโ(๐บ + (i ยท ๐ป)))โ2) = (((โโ(๐บ + (i ยท ๐ป)))โ2) + ((โโ(๐บ + (i ยท ๐ป)))โ2))) |
116 | 108 | zred 12614 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐บ โ โ) |
117 | 110 | zred 12614 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ป โ โ) |
118 | 116, 117 | crred 15123 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(๐บ + (i ยท ๐ป))) = ๐บ) |
119 | 118 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ(๐บ + (i ยท ๐ป)))โ2) = (๐บโ2)) |
120 | 116, 117 | crimd 15124 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ(๐บ + (i ยท ๐ป))) = ๐ป) |
121 | 120 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((โโ(๐บ + (i ยท ๐ป)))โ2) = (๐ปโ2)) |
122 | 119, 121 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((โโ(๐บ + (i ยท ๐ป)))โ2) + ((โโ(๐บ + (i ยท ๐ป)))โ2)) = ((๐บโ2) + (๐ปโ2))) |
123 | 115, 122 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ ((absโ(๐บ + (i ยท ๐ป)))โ2) = ((๐บโ2) + (๐ปโ2))) |
124 | 106, 123 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ โ (((absโ(๐ธ + (i ยท ๐น)))โ2) + ((absโ(๐บ + (i ยท ๐ป)))โ2)) = (((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2)))) |
125 | 124 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ ((((absโ(๐ธ + (i ยท ๐น)))โ2) + ((absโ(๐บ + (i ยท ๐ป)))โ2)) / ๐) = ((((๐ธโ2) + (๐นโ2)) + ((๐บโ2) + (๐ปโ2))) / ๐)) |
126 | 125, 17 | eqtr4di 2795 |
. . . . . . . . . . 11
โข (๐ โ ((((absโ(๐ธ + (i ยท ๐น)))โ2) + ((absโ(๐บ + (i ยท ๐ป)))โ2)) / ๐) = ๐
) |
127 | 89, 126 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ โ (((((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) / ๐) ยท ((((absโ(๐ธ + (i ยท ๐น)))โ2) + ((absโ(๐บ + (i ยท ๐ป)))โ2)) / ๐)) = (๐ ยท ๐
)) |
128 | 55 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ โ) |
129 | 87, 128 | mulcomd 11183 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท ๐
) = (๐
ยท ๐)) |
130 | 127, 129 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ (((((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) / ๐) ยท ((((absโ(๐ธ + (i ยท ๐น)))โ2) + ((absโ(๐บ + (i ยท ๐ป)))โ2)) / ๐)) = (๐
ยท ๐)) |
131 | | eqid 2737 |
. . . . . . . . . 10
โข
(((absโ(๐ด + (i
ยท ๐ต)))โ2) +
((absโ(๐ถ + (i
ยท ๐ท)))โ2)) =
(((absโ(๐ด + (i
ยท ๐ต)))โ2) +
((absโ(๐ถ + (i
ยท ๐ท)))โ2)) |
132 | | eqid 2737 |
. . . . . . . . . 10
โข
(((absโ(๐ธ + (i
ยท ๐น)))โ2) +
((absโ(๐บ + (i
ยท ๐ป)))โ2)) =
(((absโ(๐ธ + (i
ยท ๐น)))โ2) +
((absโ(๐บ + (i
ยท ๐ป)))โ2)) |
133 | 9 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ โ) |
134 | | ax-icn 11117 |
. . . . . . . . . . . . . . . 16
โข i โ
โ |
135 | 10 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ โ) |
136 | | mulcl 11142 |
. . . . . . . . . . . . . . . 16
โข ((i
โ โ โง ๐ต
โ โ) โ (i ยท ๐ต) โ โ) |
137 | 134, 135,
136 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (๐ โ (i ยท ๐ต) โ
โ) |
138 | 91 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ธ โ โ) |
139 | 93 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐น โ โ) |
140 | | mulcl 11142 |
. . . . . . . . . . . . . . . 16
โข ((i
โ โ โง ๐น
โ โ) โ (i ยท ๐น) โ โ) |
141 | 134, 139,
140 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (๐ โ (i ยท ๐น) โ
โ) |
142 | 133, 137,
138, 141 | addsub4d 11566 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด + (i ยท ๐ต)) โ (๐ธ + (i ยท ๐น))) = ((๐ด โ ๐ธ) + ((i ยท ๐ต) โ (i ยท ๐น)))) |
143 | 134 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ i โ
โ) |
144 | 143, 135,
139 | subdid 11618 |
. . . . . . . . . . . . . . 15
โข (๐ โ (i ยท (๐ต โ ๐น)) = ((i ยท ๐ต) โ (i ยท ๐น))) |
145 | 144 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด โ ๐ธ) + (i ยท (๐ต โ ๐น))) = ((๐ด โ ๐ธ) + ((i ยท ๐ต) โ (i ยท ๐น)))) |
146 | 142, 145 | eqtr4d 2780 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด + (i ยท ๐ต)) โ (๐ธ + (i ยท ๐น))) = ((๐ด โ ๐ธ) + (i ยท (๐ต โ ๐น)))) |
147 | 146 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด + (i ยท ๐ต)) โ (๐ธ + (i ยท ๐น))) / ๐) = (((๐ด โ ๐ธ) + (i ยท (๐ต โ ๐น))) / ๐)) |
148 | 133, 138 | subcld 11519 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด โ ๐ธ) โ โ) |
149 | 135, 139 | subcld 11519 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ต โ ๐น) โ โ) |
150 | | mulcl 11142 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง (๐ต
โ ๐น) โ โ)
โ (i ยท (๐ต
โ ๐น)) โ
โ) |
151 | 134, 149,
150 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ โ (i ยท (๐ต โ ๐น)) โ โ) |
152 | 148, 151,
33, 39 | divdird 11976 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด โ ๐ธ) + (i ยท (๐ต โ ๐น))) / ๐) = (((๐ด โ ๐ธ) / ๐) + ((i ยท (๐ต โ ๐น)) / ๐))) |
153 | 143, 149,
33, 39 | divassd 11973 |
. . . . . . . . . . . . 13
โข (๐ โ ((i ยท (๐ต โ ๐น)) / ๐) = (i ยท ((๐ต โ ๐น) / ๐))) |
154 | 153 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด โ ๐ธ) / ๐) + ((i ยท (๐ต โ ๐น)) / ๐)) = (((๐ด โ ๐ธ) / ๐) + (i ยท ((๐ต โ ๐น) / ๐)))) |
155 | 147, 152,
154 | 3eqtrd 2781 |
. . . . . . . . . . 11
โข (๐ โ (((๐ด + (i ยท ๐ต)) โ (๐ธ + (i ยท ๐น))) / ๐) = (((๐ด โ ๐ธ) / ๐) + (i ยท ((๐ต โ ๐น) / ๐)))) |
156 | 90 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ด โ ๐ธ) / ๐) โ โค) |
157 | 92 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ต โ ๐น) / ๐) โ โค) |
158 | | gzreim 16818 |
. . . . . . . . . . . 12
โข ((((๐ด โ ๐ธ) / ๐) โ โค โง ((๐ต โ ๐น) / ๐) โ โค) โ (((๐ด โ ๐ธ) / ๐) + (i ยท ((๐ต โ ๐น) / ๐))) โ โค[i]) |
159 | 156, 157,
158 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (((๐ด โ ๐ธ) / ๐) + (i ยท ((๐ต โ ๐น) / ๐))) โ โค[i]) |
160 | 155, 159 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ (((๐ด + (i ยท ๐ต)) โ (๐ธ + (i ยท ๐น))) / ๐) โ โค[i]) |
161 | 11 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ถ โ โ) |
162 | 12 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ท โ โ) |
163 | | mulcl 11142 |
. . . . . . . . . . . . . . . 16
โข ((i
โ โ โง ๐ท
โ โ) โ (i ยท ๐ท) โ โ) |
164 | 134, 162,
163 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (๐ โ (i ยท ๐ท) โ
โ) |
165 | 108 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐บ โ โ) |
166 | 110 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ป โ โ) |
167 | | mulcl 11142 |
. . . . . . . . . . . . . . . 16
โข ((i
โ โ โง ๐ป
โ โ) โ (i ยท ๐ป) โ โ) |
168 | 134, 166,
167 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (๐ โ (i ยท ๐ป) โ
โ) |
169 | 161, 164,
165, 168 | addsub4d 11566 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ถ + (i ยท ๐ท)) โ (๐บ + (i ยท ๐ป))) = ((๐ถ โ ๐บ) + ((i ยท ๐ท) โ (i ยท ๐ป)))) |
170 | 143, 162,
166 | subdid 11618 |
. . . . . . . . . . . . . . 15
โข (๐ โ (i ยท (๐ท โ ๐ป)) = ((i ยท ๐ท) โ (i ยท ๐ป))) |
171 | 170 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ถ โ ๐บ) + (i ยท (๐ท โ ๐ป))) = ((๐ถ โ ๐บ) + ((i ยท ๐ท) โ (i ยท ๐ป)))) |
172 | 169, 171 | eqtr4d 2780 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ + (i ยท ๐ท)) โ (๐บ + (i ยท ๐ป))) = ((๐ถ โ ๐บ) + (i ยท (๐ท โ ๐ป)))) |
173 | 172 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ถ + (i ยท ๐ท)) โ (๐บ + (i ยท ๐ป))) / ๐) = (((๐ถ โ ๐บ) + (i ยท (๐ท โ ๐ป))) / ๐)) |
174 | 161, 165 | subcld 11519 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ถ โ ๐บ) โ โ) |
175 | 162, 166 | subcld 11519 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ท โ ๐ป) โ โ) |
176 | | mulcl 11142 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง (๐ท
โ ๐ป) โ โ)
โ (i ยท (๐ท
โ ๐ป)) โ
โ) |
177 | 134, 175,
176 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ โ (i ยท (๐ท โ ๐ป)) โ โ) |
178 | 174, 177,
33, 39 | divdird 11976 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ถ โ ๐บ) + (i ยท (๐ท โ ๐ป))) / ๐) = (((๐ถ โ ๐บ) / ๐) + ((i ยท (๐ท โ ๐ป)) / ๐))) |
179 | 143, 175,
33, 39 | divassd 11973 |
. . . . . . . . . . . . 13
โข (๐ โ ((i ยท (๐ท โ ๐ป)) / ๐) = (i ยท ((๐ท โ ๐ป) / ๐))) |
180 | 179 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ถ โ ๐บ) / ๐) + ((i ยท (๐ท โ ๐ป)) / ๐)) = (((๐ถ โ ๐บ) / ๐) + (i ยท ((๐ท โ ๐ป) / ๐)))) |
181 | 173, 178,
180 | 3eqtrd 2781 |
. . . . . . . . . . 11
โข (๐ โ (((๐ถ + (i ยท ๐ท)) โ (๐บ + (i ยท ๐ป))) / ๐) = (((๐ถ โ ๐บ) / ๐) + (i ยท ((๐ท โ ๐ป) / ๐)))) |
182 | 107 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ โ ๐บ) / ๐) โ โค) |
183 | 109 | simprd 497 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ท โ ๐ป) / ๐) โ โค) |
184 | | gzreim 16818 |
. . . . . . . . . . . 12
โข ((((๐ถ โ ๐บ) / ๐) โ โค โง ((๐ท โ ๐ป) / ๐) โ โค) โ (((๐ถ โ ๐บ) / ๐) + (i ยท ((๐ท โ ๐ป) / ๐))) โ โค[i]) |
185 | 182, 183,
184 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (((๐ถ โ ๐บ) / ๐) + (i ยท ((๐ท โ ๐ป) / ๐))) โ โค[i]) |
186 | 181, 185 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ (((๐ถ + (i ยท ๐ท)) โ (๐บ + (i ยท ๐ป))) / ๐) โ โค[i]) |
187 | 86 | nnnn0d 12480 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ
โ0) |
188 | 89, 187 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ ((((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) / ๐) โ
โ0) |
189 | 1, 57, 70, 95, 112, 131, 132, 29, 160, 186, 188 | mul4sqlem 16832 |
. . . . . . . . 9
โข (๐ โ (((((absโ(๐ด + (i ยท ๐ต)))โ2) + ((absโ(๐ถ + (i ยท ๐ท)))โ2)) / ๐) ยท ((((absโ(๐ธ + (i ยท ๐น)))โ2) + ((absโ(๐บ + (i ยท ๐ป)))โ2)) / ๐)) โ ๐) |
190 | 130, 189 | eqeltrrd 2839 |
. . . . . . . 8
โข (๐ โ (๐
ยท ๐) โ ๐) |
191 | | oveq1 7369 |
. . . . . . . . . 10
โข (๐ = ๐
โ (๐ ยท ๐) = (๐
ยท ๐)) |
192 | 191 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ = ๐
โ ((๐ ยท ๐) โ ๐ โ (๐
ยท ๐) โ ๐)) |
193 | 192, 6 | elrab2 3653 |
. . . . . . . 8
โข (๐
โ ๐ โ (๐
โ โ โง (๐
ยท ๐) โ ๐)) |
194 | 55, 190, 193 | sylanbrc 584 |
. . . . . . 7
โข (๐ โ ๐
โ ๐) |
195 | | infssuzle 12863 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ1) โง ๐
โ ๐) โ inf(๐, โ, < ) โค ๐
) |
196 | 23, 194, 195 | sylancr 588 |
. . . . . 6
โข (๐ โ inf(๐, โ, < ) โค ๐
) |
197 | 7, 196 | eqbrtrid 5145 |
. . . . 5
โข (๐ โ ๐ โค ๐
) |
198 | 55 | nnred 12175 |
. . . . . 6
โข (๐ โ ๐
โ โ) |
199 | 198, 30 | letri3d 11304 |
. . . . 5
โข (๐ โ (๐
= ๐ โ (๐
โค ๐ โง ๐ โค ๐
))) |
200 | 20, 197, 199 | mpbir2and 712 |
. . . 4
โข (๐ โ ๐
= ๐) |
201 | 200 | olcd 873 |
. . 3
โข (๐ โ (๐
= 0 โจ ๐
= ๐)) |
202 | 201, 52 | mpd 15 |
. 2
โข (๐ โ (๐โ2) โฅ (๐ ยท ๐)) |
203 | 202, 46 | pm2.65i 193 |
1
โข ยฌ
๐ |