Step | Hyp | Ref
| Expression |
1 | | 2sqlem4.3 |
. . . . . . . 8
โข (๐ โ ๐ด โ โค) |
2 | | 2sqlem4.4 |
. . . . . . . 8
โข (๐ โ ๐ต โ โค) |
3 | | gzreim 12376 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด + (i ยท ๐ต)) โ โค[i]) |
4 | 1, 2, 3 | syl2anc 411 |
. . . . . . 7
โข (๐ โ (๐ด + (i ยท ๐ต)) โ โค[i]) |
5 | | 2sqlem4.5 |
. . . . . . . 8
โข (๐ โ ๐ถ โ โค) |
6 | | 2sqlem4.6 |
. . . . . . . 8
โข (๐ โ ๐ท โ โค) |
7 | | gzreim 12376 |
. . . . . . . 8
โข ((๐ถ โ โค โง ๐ท โ โค) โ (๐ถ + (i ยท ๐ท)) โ โค[i]) |
8 | 5, 6, 7 | syl2anc 411 |
. . . . . . 7
โข (๐ โ (๐ถ + (i ยท ๐ท)) โ โค[i]) |
9 | | gzmulcl 12375 |
. . . . . . 7
โข (((๐ด + (i ยท ๐ต)) โ โค[i] โง (๐ถ + (i ยท ๐ท)) โ โค[i]) โ ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โค[i]) |
10 | 4, 8, 9 | syl2anc 411 |
. . . . . 6
โข (๐ โ ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โค[i]) |
11 | | gzcn 12369 |
. . . . . 6
โข (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โค[i] โ ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โ) |
12 | 10, 11 | syl 14 |
. . . . 5
โข (๐ โ ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โ) |
13 | | 2sqlem5.2 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
14 | | prmnn 12109 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
15 | 13, 14 | syl 14 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
16 | 15 | nncnd 8932 |
. . . . 5
โข (๐ โ ๐ โ โ) |
17 | 15 | nnap0d 8964 |
. . . . 5
โข (๐ โ ๐ # 0) |
18 | 12, 16, 17 | divclapd 8746 |
. . . 4
โข (๐ โ (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ โ) |
19 | 15 | nnred 8931 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
20 | 19, 12, 17 | redivapd 10982 |
. . . . 5
โข (๐ โ (โโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐)) = ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐)) |
21 | | prmz 12110 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
22 | 13, 21 | syl 14 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
23 | | zsqcl 10590 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐โ2) โ
โค) |
24 | 22, 23 | syl 14 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) โ โค) |
25 | | 2sqlem5.1 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
26 | 25 | nnzd 9373 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
27 | 26, 24 | zmulcld 9380 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท (๐โ2)) โ โค) |
28 | | dvdsmul2 11820 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) |
29 | 22, 22, 28 | syl2anc 411 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โฅ (๐ ยท ๐)) |
30 | 16 | sqvald 10650 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ2) = (๐ ยท ๐)) |
31 | 29, 30 | breqtrrd 4031 |
. . . . . . . . . . 11
โข (๐ โ ๐ โฅ (๐โ2)) |
32 | | dvdsmul2 11820 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐โ2) โ โค) โ
(๐โ2) โฅ (๐ ยท (๐โ2))) |
33 | 26, 24, 32 | syl2anc 411 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) โฅ (๐ ยท (๐โ2))) |
34 | 22, 24, 27, 31, 33 | dvdstrd 11836 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ (๐ ยท (๐โ2))) |
35 | | gzcn 12369 |
. . . . . . . . . . . . . . . 16
โข ((๐ด + (i ยท ๐ต)) โ โค[i] โ (๐ด + (i ยท ๐ต)) โ โ) |
36 | 4, 35 | syl 14 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ด + (i ยท ๐ต)) โ โ) |
37 | 36 | abscld 11189 |
. . . . . . . . . . . . . 14
โข (๐ โ (absโ(๐ด + (i ยท ๐ต))) โ โ) |
38 | 37 | recnd 7985 |
. . . . . . . . . . . . 13
โข (๐ โ (absโ(๐ด + (i ยท ๐ต))) โ โ) |
39 | | gzcn 12369 |
. . . . . . . . . . . . . . . 16
โข ((๐ถ + (i ยท ๐ท)) โ โค[i] โ (๐ถ + (i ยท ๐ท)) โ โ) |
40 | 8, 39 | syl 14 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ถ + (i ยท ๐ท)) โ โ) |
41 | 40 | abscld 11189 |
. . . . . . . . . . . . . 14
โข (๐ โ (absโ(๐ถ + (i ยท ๐ท))) โ โ) |
42 | 41 | recnd 7985 |
. . . . . . . . . . . . 13
โข (๐ โ (absโ(๐ถ + (i ยท ๐ท))) โ โ) |
43 | 38, 42 | sqmuld 10665 |
. . . . . . . . . . . 12
โข (๐ โ (((absโ(๐ด + (i ยท ๐ต))) ยท (absโ(๐ถ + (i ยท ๐ท))))โ2) = (((absโ(๐ด + (i ยท ๐ต)))โ2) ยท ((absโ(๐ถ + (i ยท ๐ท)))โ2))) |
44 | 1 | zred 9374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ด โ โ) |
45 | 2 | zred 9374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ โ) |
46 | 44, 45 | crred 10984 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ด) |
47 | 46 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ(๐ด + (i ยท ๐ต)))โ2) = (๐ดโ2)) |
48 | 44, 45 | crimd 10985 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ต) |
49 | 48 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ(๐ด + (i ยท ๐ต)))โ2) = (๐ตโ2)) |
50 | 47, 49 | oveq12d 5892 |
. . . . . . . . . . . . . 14
โข (๐ โ (((โโ(๐ด + (i ยท ๐ต)))โ2) + ((โโ(๐ด + (i ยท ๐ต)))โ2)) = ((๐ดโ2) + (๐ตโ2))) |
51 | 36 | absvalsq2d 11191 |
. . . . . . . . . . . . . 14
โข (๐ โ ((absโ(๐ด + (i ยท ๐ต)))โ2) = (((โโ(๐ด + (i ยท ๐ต)))โ2) + ((โโ(๐ด + (i ยท ๐ต)))โ2))) |
52 | | 2sqlem4.7 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท ๐) = ((๐ดโ2) + (๐ตโ2))) |
53 | 50, 51, 52 | 3eqtr4d 2220 |
. . . . . . . . . . . . 13
โข (๐ โ ((absโ(๐ด + (i ยท ๐ต)))โ2) = (๐ ยท ๐)) |
54 | 5 | zred 9374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ถ โ โ) |
55 | 6 | zred 9374 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ท โ โ) |
56 | 54, 55 | crred 10984 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โโ(๐ถ + (i ยท ๐ท))) = ๐ถ) |
57 | 56 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ(๐ถ + (i ยท ๐ท)))โ2) = (๐ถโ2)) |
58 | 54, 55 | crimd 10985 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (โโ(๐ถ + (i ยท ๐ท))) = ๐ท) |
59 | 58 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((โโ(๐ถ + (i ยท ๐ท)))โ2) = (๐ทโ2)) |
60 | 57, 59 | oveq12d 5892 |
. . . . . . . . . . . . . 14
โข (๐ โ (((โโ(๐ถ + (i ยท ๐ท)))โ2) + ((โโ(๐ถ + (i ยท ๐ท)))โ2)) = ((๐ถโ2) + (๐ทโ2))) |
61 | 40 | absvalsq2d 11191 |
. . . . . . . . . . . . . 14
โข (๐ โ ((absโ(๐ถ + (i ยท ๐ท)))โ2) = (((โโ(๐ถ + (i ยท ๐ท)))โ2) + ((โโ(๐ถ + (i ยท ๐ท)))โ2))) |
62 | | 2sqlem4.8 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ = ((๐ถโ2) + (๐ทโ2))) |
63 | 60, 61, 62 | 3eqtr4d 2220 |
. . . . . . . . . . . . 13
โข (๐ โ ((absโ(๐ถ + (i ยท ๐ท)))โ2) = ๐) |
64 | 53, 63 | oveq12d 5892 |
. . . . . . . . . . . 12
โข (๐ โ (((absโ(๐ด + (i ยท ๐ต)))โ2) ยท ((absโ(๐ถ + (i ยท ๐ท)))โ2)) = ((๐ ยท ๐) ยท ๐)) |
65 | 25 | nncnd 8932 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
66 | 65, 16, 16 | mulassd 7980 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |
67 | 43, 64, 66 | 3eqtrd 2214 |
. . . . . . . . . . 11
โข (๐ โ (((absโ(๐ด + (i ยท ๐ต))) ยท (absโ(๐ถ + (i ยท ๐ท))))โ2) = (๐ ยท (๐ ยท ๐))) |
68 | 36, 40 | absmuld 11202 |
. . . . . . . . . . . 12
โข (๐ โ (absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) = ((absโ(๐ด + (i ยท ๐ต))) ยท (absโ(๐ถ + (i ยท ๐ท))))) |
69 | 68 | oveq1d 5889 |
. . . . . . . . . . 11
โข (๐ โ ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) = (((absโ(๐ด + (i ยท ๐ต))) ยท (absโ(๐ถ + (i ยท ๐ท))))โ2)) |
70 | 30 | oveq2d 5890 |
. . . . . . . . . . 11
โข (๐ โ (๐ ยท (๐โ2)) = (๐ ยท (๐ ยท ๐))) |
71 | 67, 69, 70 | 3eqtr4d 2220 |
. . . . . . . . . 10
โข (๐ โ ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) = (๐ ยท (๐โ2))) |
72 | 34, 71 | breqtrrd 4031 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2)) |
73 | 12 | absvalsq2d 11191 |
. . . . . . . . . 10
โข (๐ โ ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) = (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2))) |
74 | | elgz 12368 |
. . . . . . . . . . . . . . 15
โข (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โค[i] โ (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โ โง
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค โง
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ
โค)) |
75 | 74 | simp2bi 1013 |
. . . . . . . . . . . . . 14
โข (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โค[i] โ
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ
โค) |
76 | 10, 75 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) โ โค) |
77 | | zsqcl 10590 |
. . . . . . . . . . . . 13
โข
((โโ((๐ด +
(i ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค โ
((โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2) โ
โค) |
78 | 76, 77 | syl 14 |
. . . . . . . . . . . 12
โข (๐ โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ
โค) |
79 | 78 | zcnd 9375 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ
โ) |
80 | 74 | simp3bi 1014 |
. . . . . . . . . . . . . 14
โข (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) โ โค[i] โ
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ
โค) |
81 | 10, 80 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) โ โค) |
82 | | zsqcl 10590 |
. . . . . . . . . . . . 13
โข
((โโ((๐ด
+ (i ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค โ
((โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2) โ
โค) |
83 | 81, 82 | syl 14 |
. . . . . . . . . . . 12
โข (๐ โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ
โค) |
84 | 83 | zcnd 9375 |
. . . . . . . . . . 11
โข (๐ โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ
โ) |
85 | 79, 84 | addcomd 8107 |
. . . . . . . . . 10
โข (๐ โ (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2)) = (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2))) |
86 | 73, 85 | eqtrd 2210 |
. . . . . . . . 9
โข (๐ โ ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) = (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2))) |
87 | 72, 86 | breqtrd 4029 |
. . . . . . . 8
โข (๐ โ ๐ โฅ (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2))) |
88 | | 2sqlem4.9 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โฅ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท))) |
89 | 5 | zcnd 9375 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ถ โ โ) |
90 | 2 | zcnd 9375 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ โ) |
91 | 89, 90 | mulcld 7977 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ถ ยท ๐ต) โ โ) |
92 | 1 | zcnd 9375 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ โ) |
93 | 6 | zcnd 9375 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ท โ โ) |
94 | 92, 93 | mulcld 7977 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด ยท ๐ท) โ โ) |
95 | 91, 94 | addcomd 8107 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) = ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต))) |
96 | 89, 90 | mulcomd 7978 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ถ ยท ๐ต) = (๐ต ยท ๐ถ)) |
97 | 96 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))) |
98 | 95, 97 | eqtrd 2210 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ถ ยท ๐ต) + (๐ด ยท ๐ท)) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))) |
99 | 88, 98 | breqtrd 4029 |
. . . . . . . . . . 11
โข (๐ โ ๐ โฅ ((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))) |
100 | 36, 40 | immuld 10972 |
. . . . . . . . . . . 12
โข (๐ โ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) = (((โโ(๐ด + (i ยท ๐ต))) ยท (โโ(๐ถ + (i ยท ๐ท)))) + ((โโ(๐ด + (i ยท ๐ต))) ยท (โโ(๐ถ + (i ยท ๐ท)))))) |
101 | 46, 58 | oveq12d 5892 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(๐ด + (i ยท ๐ต))) ยท (โโ(๐ถ + (i ยท ๐ท)))) = (๐ด ยท ๐ท)) |
102 | 48, 56 | oveq12d 5892 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(๐ด + (i ยท ๐ต))) ยท (โโ(๐ถ + (i ยท ๐ท)))) = (๐ต ยท ๐ถ)) |
103 | 101, 102 | oveq12d 5892 |
. . . . . . . . . . . 12
โข (๐ โ (((โโ(๐ด + (i ยท ๐ต))) ยท (โโ(๐ถ + (i ยท ๐ท)))) + ((โโ(๐ด + (i ยท ๐ต))) ยท (โโ(๐ถ + (i ยท ๐ท))))) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))) |
104 | 100, 103 | eqtrd 2210 |
. . . . . . . . . . 11
โข (๐ โ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ถ))) |
105 | 99, 104 | breqtrrd 4031 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))) |
106 | | 2nn 9079 |
. . . . . . . . . . . 12
โข 2 โ
โ |
107 | 106 | a1i 9 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
108 | | prmdvdsexp 12147 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค โง 2
โ โ) โ (๐
โฅ ((โโ((๐ด
+ (i ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2) โ ๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))))) |
109 | 13, 81, 107, 108 | syl3anc 1238 |
. . . . . . . . . 10
โข (๐ โ (๐ โฅ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ ๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))))) |
110 | 105, 109 | mpbird 167 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2)) |
111 | | dvdsadd2b 11846 |
. . . . . . . . 9
โข ((๐ โ โค โง
((โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2) โ โค
โง (((โโ((๐ด
+ (i ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2) โ โค
โง ๐ โฅ
((โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2))) โ (๐ โฅ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ ๐ โฅ (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2)))) |
112 | 22, 78, 83, 110, 111 | syl112anc 1242 |
. . . . . . . 8
โข (๐ โ (๐ โฅ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ ๐ โฅ (((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) + ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2)))) |
113 | 87, 112 | mpbird 167 |
. . . . . . 7
โข (๐ โ ๐ โฅ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2)) |
114 | | prmdvdsexp 12147 |
. . . . . . . 8
โข ((๐ โ โ โง
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค โง 2
โ โ) โ (๐
โฅ ((โโ((๐ด
+ (i ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))))โ2) โ ๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))))) |
115 | 13, 76, 107, 114 | syl3anc 1238 |
. . . . . . 7
โข (๐ โ (๐ โฅ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) โ ๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))))) |
116 | 113, 115 | mpbid 147 |
. . . . . 6
โข (๐ โ ๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))) |
117 | 15 | nnne0d 8963 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
118 | | dvdsval2 11796 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0 โง
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค) โ
(๐ โฅ
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ
((โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) / ๐) โ โค)) |
119 | 22, 117, 76, 118 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐) โ โค)) |
120 | 116, 119 | mpbid 147 |
. . . . 5
โข (๐ โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐) โ โค) |
121 | 20, 120 | eqeltrd 2254 |
. . . 4
โข (๐ โ (โโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐)) โ โค) |
122 | 19, 12, 17 | imdivapd 10983 |
. . . . 5
โข (๐ โ (โโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐)) = ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐)) |
123 | | dvdsval2 11796 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ 0 โง
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ โค) โ
(๐ โฅ
(โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) โ
((โโ((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท)))) / ๐) โ โค)) |
124 | 22, 117, 81, 123 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐ โฅ (โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐) โ โค)) |
125 | 105, 124 | mpbid 147 |
. . . . 5
โข (๐ โ ((โโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐) โ โค) |
126 | 122, 125 | eqeltrd 2254 |
. . . 4
โข (๐ โ (โโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐)) โ โค) |
127 | | elgz 12368 |
. . . 4
โข ((((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ โค[i] โ ((((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ โ โง
(โโ(((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))) / ๐)) โ โค โง
(โโ(((๐ด + (i
ยท ๐ต)) ยท
(๐ถ + (i ยท ๐ท))) / ๐)) โ โค)) |
128 | 18, 121, 126, 127 | syl3anbrc 1181 |
. . 3
โข (๐ โ (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ โค[i]) |
129 | 12, 16, 17 | absdivapd 11203 |
. . . . . 6
โข (๐ โ (absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐)) = ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / (absโ๐))) |
130 | 15 | nnnn0d 9228 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
131 | 130 | nn0ge0d 9231 |
. . . . . . . 8
โข (๐ โ 0 โค ๐) |
132 | 19, 131 | absidd 11175 |
. . . . . . 7
โข (๐ โ (absโ๐) = ๐) |
133 | 132 | oveq2d 5890 |
. . . . . 6
โข (๐ โ ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / (absโ๐)) = ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐)) |
134 | 129, 133 | eqtrd 2210 |
. . . . 5
โข (๐ โ (absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐)) = ((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐)) |
135 | 134 | oveq1d 5889 |
. . . 4
โข (๐ โ ((absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐))โ2) = (((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐)โ2)) |
136 | 12 | abscld 11189 |
. . . . . 6
โข (๐ โ (absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) โ โ) |
137 | 136 | recnd 7985 |
. . . . 5
โข (๐ โ (absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) โ โ) |
138 | 137, 16, 17 | sqdivapd 10666 |
. . . 4
โข (๐ โ (((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท)))) / ๐)โ2) = (((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) / (๐โ2))) |
139 | 71 | oveq1d 5889 |
. . . . 5
โข (๐ โ (((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) / (๐โ2)) = ((๐ ยท (๐โ2)) / (๐โ2))) |
140 | 15 | nnsqcld 10674 |
. . . . . . 7
โข (๐ โ (๐โ2) โ โ) |
141 | 140 | nncnd 8932 |
. . . . . 6
โข (๐ โ (๐โ2) โ โ) |
142 | 140 | nnap0d 8964 |
. . . . . 6
โข (๐ โ (๐โ2) # 0) |
143 | 65, 141, 142 | divcanap4d 8752 |
. . . . 5
โข (๐ โ ((๐ ยท (๐โ2)) / (๐โ2)) = ๐) |
144 | 139, 143 | eqtrd 2210 |
. . . 4
โข (๐ โ (((absโ((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))))โ2) / (๐โ2)) = ๐) |
145 | 135, 138,
144 | 3eqtrrd 2215 |
. . 3
โข (๐ โ ๐ = ((absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐))โ2)) |
146 | | fveq2 5515 |
. . . . 5
โข (๐ฅ = (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ (absโ๐ฅ) = (absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐))) |
147 | 146 | oveq1d 5889 |
. . . 4
โข (๐ฅ = (((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ ((absโ๐ฅ)โ2) = ((absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐))โ2)) |
148 | 147 | rspceeqv 2859 |
. . 3
โข
(((((๐ด + (i ยท
๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐) โ โค[i] โง ๐ = ((absโ(((๐ด + (i ยท ๐ต)) ยท (๐ถ + (i ยท ๐ท))) / ๐))โ2)) โ โ๐ฅ โ โค[i] ๐ = ((absโ๐ฅ)โ2)) |
149 | 128, 145,
148 | syl2anc 411 |
. 2
โข (๐ โ โ๐ฅ โ โค[i] ๐ = ((absโ๐ฅ)โ2)) |
150 | | 2sq.1 |
. . 3
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) |
151 | 150 | 2sqlem1 14431 |
. 2
โข (๐ โ ๐ โ โ๐ฅ โ โค[i] ๐ = ((absโ๐ฅ)โ2)) |
152 | 149, 151 | sylibr 134 |
1
โข (๐ โ ๐ โ ๐) |