Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . 3
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
2 | 1 | 4sqlem4 16832 |
. 2
โข (๐ด โ ๐ โ โ๐ โ โค[i] โ๐ โ โค[i] ๐ด = (((absโ๐)โ2) + ((absโ๐)โ2))) |
3 | 1 | 4sqlem4 16832 |
. 2
โข (๐ต โ ๐ โ โ๐ โ โค[i] โ๐ โ โค[i] ๐ต = (((absโ๐)โ2) + ((absโ๐)โ2))) |
4 | | reeanv 3216 |
. . 3
โข
(โ๐ โ
โค[i] โ๐ โ
โค[i] (โ๐ โ
โค[i] ๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง โ๐ โ
โค[i] ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))
โ (โ๐ โ
โค[i] โ๐ โ
โค[i] ๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง โ๐ โ
โค[i] โ๐ โ
โค[i] ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))) |
5 | | reeanv 3216 |
. . . . 5
โข
(โ๐ โ
โค[i] โ๐ โ
โค[i] (๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))
โ (โ๐ โ
โค[i] ๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง โ๐ โ
โค[i] ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))) |
6 | | simpll 766 |
. . . . . . . . . . . . 13
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
๐ โ
โค[i]) |
7 | | gzabssqcl 16821 |
. . . . . . . . . . . . 13
โข (๐ โ โค[i] โ
((absโ๐)โ2)
โ โ0) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((absโ๐)โ2)
โ โ0) |
9 | | simprl 770 |
. . . . . . . . . . . . 13
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
๐ โ
โค[i]) |
10 | | gzabssqcl 16821 |
. . . . . . . . . . . . 13
โข (๐ โ โค[i] โ
((absโ๐)โ2)
โ โ0) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((absโ๐)โ2)
โ โ0) |
12 | 8, 11 | nn0addcld 12485 |
. . . . . . . . . . 11
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(((absโ๐)โ2) +
((absโ๐)โ2))
โ โ0) |
13 | 12 | nn0cnd 12483 |
. . . . . . . . . 10
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(((absโ๐)โ2) +
((absโ๐)โ2))
โ โ) |
14 | 13 | div1d 11931 |
. . . . . . . . 9
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((((absโ๐)โ2) +
((absโ๐)โ2)) /
1) = (((absโ๐)โ2) + ((absโ๐)โ2))) |
15 | | simplr 768 |
. . . . . . . . . . . . 13
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
๐ โ
โค[i]) |
16 | | gzabssqcl 16821 |
. . . . . . . . . . . . 13
โข (๐ โ โค[i] โ
((absโ๐)โ2)
โ โ0) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((absโ๐)โ2)
โ โ0) |
18 | | simprr 772 |
. . . . . . . . . . . . 13
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
๐ โ
โค[i]) |
19 | | gzabssqcl 16821 |
. . . . . . . . . . . . 13
โข (๐ โ โค[i] โ
((absโ๐)โ2)
โ โ0) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((absโ๐)โ2)
โ โ0) |
21 | 17, 20 | nn0addcld 12485 |
. . . . . . . . . . 11
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(((absโ๐)โ2) +
((absโ๐)โ2))
โ โ0) |
22 | 21 | nn0cnd 12483 |
. . . . . . . . . 10
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(((absโ๐)โ2) +
((absโ๐)โ2))
โ โ) |
23 | 22 | div1d 11931 |
. . . . . . . . 9
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((((absโ๐)โ2) +
((absโ๐)โ2)) /
1) = (((absโ๐)โ2) + ((absโ๐)โ2))) |
24 | 14, 23 | oveq12d 7379 |
. . . . . . . 8
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(((((absโ๐)โ2) +
((absโ๐)โ2)) /
1) ยท ((((absโ๐)โ2) + ((absโ๐)โ2)) / 1)) = ((((absโ๐)โ2) + ((absโ๐)โ2)) ยท
(((absโ๐)โ2) +
((absโ๐)โ2)))) |
25 | | eqid 2733 |
. . . . . . . . 9
โข
(((absโ๐)โ2) + ((absโ๐)โ2)) = (((absโ๐)โ2) + ((absโ๐)โ2)) |
26 | | eqid 2733 |
. . . . . . . . 9
โข
(((absโ๐)โ2) + ((absโ๐)โ2)) = (((absโ๐)โ2) + ((absโ๐)โ2)) |
27 | | 1nn 12172 |
. . . . . . . . . 10
โข 1 โ
โ |
28 | 27 | a1i 11 |
. . . . . . . . 9
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ 1
โ โ) |
29 | | gzsubcl 16820 |
. . . . . . . . . . . . 13
โข ((๐ โ โค[i] โง ๐ โ โค[i]) โ
(๐ โ ๐) โ
โค[i]) |
30 | 29 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(๐ โ ๐) โ
โค[i]) |
31 | | gzcn 16812 |
. . . . . . . . . . . 12
โข ((๐ โ ๐) โ โค[i] โ (๐ โ ๐) โ โ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(๐ โ ๐) โ
โ) |
33 | 32 | div1d 11931 |
. . . . . . . . . 10
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((๐ โ ๐) / 1) = (๐ โ ๐)) |
34 | 33, 30 | eqeltrd 2834 |
. . . . . . . . 9
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((๐ โ ๐) / 1) โ
โค[i]) |
35 | | gzsubcl 16820 |
. . . . . . . . . . . . 13
โข ((๐ โ โค[i] โง ๐ โ โค[i]) โ
(๐ โ ๐) โ
โค[i]) |
36 | 35 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(๐ โ ๐) โ
โค[i]) |
37 | | gzcn 16812 |
. . . . . . . . . . . 12
โข ((๐ โ ๐) โ โค[i] โ (๐ โ ๐) โ โ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(๐ โ ๐) โ
โ) |
39 | 38 | div1d 11931 |
. . . . . . . . . 10
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((๐ โ ๐) / 1) = (๐ โ ๐)) |
40 | 39, 36 | eqeltrd 2834 |
. . . . . . . . 9
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((๐ โ ๐) / 1) โ
โค[i]) |
41 | 14, 12 | eqeltrd 2834 |
. . . . . . . . 9
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((((absโ๐)โ2) +
((absโ๐)โ2)) /
1) โ โ0) |
42 | 1, 6, 9, 15, 18, 25, 26, 28, 34, 40, 41 | mul4sqlem 16833 |
. . . . . . . 8
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
(((((absโ๐)โ2) +
((absโ๐)โ2)) /
1) ยท ((((absโ๐)โ2) + ((absโ๐)โ2)) / 1)) โ ๐) |
43 | 24, 42 | eqeltrrd 2835 |
. . . . . . 7
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((((absโ๐)โ2) +
((absโ๐)โ2))
ยท (((absโ๐)โ2) + ((absโ๐)โ2))) โ ๐) |
44 | | oveq12 7370 |
. . . . . . . 8
โข ((๐ด = (((absโ๐)โ2) + ((absโ๐)โ2)) โง ๐ต = (((absโ๐)โ2) + ((absโ๐)โ2))) โ (๐ด ยท ๐ต) = ((((absโ๐)โ2) + ((absโ๐)โ2)) ยท (((absโ๐)โ2) + ((absโ๐)โ2)))) |
45 | 44 | eleq1d 2819 |
. . . . . . 7
โข ((๐ด = (((absโ๐)โ2) + ((absโ๐)โ2)) โง ๐ต = (((absโ๐)โ2) + ((absโ๐)โ2))) โ ((๐ด ยท ๐ต) โ ๐ โ ((((absโ๐)โ2) + ((absโ๐)โ2)) ยท (((absโ๐)โ2) + ((absโ๐)โ2))) โ ๐)) |
46 | 43, 45 | syl5ibrcom 247 |
. . . . . 6
โข (((๐ โ โค[i] โง ๐ โ โค[i]) โง (๐ โ โค[i] โง ๐ โ โค[i])) โ
((๐ด = (((absโ๐)โ2) + ((absโ๐)โ2)) โง ๐ต = (((absโ๐)โ2) + ((absโ๐)โ2))) โ (๐ด ยท ๐ต) โ ๐)) |
47 | 46 | rexlimdvva 3202 |
. . . . 5
โข ((๐ โ โค[i] โง ๐ โ โค[i]) โ
(โ๐ โ โค[i]
โ๐ โ โค[i]
(๐ด = (((absโ๐)โ2) + ((absโ๐)โ2)) โง ๐ต = (((absโ๐)โ2) + ((absโ๐)โ2))) โ (๐ด ยท ๐ต) โ ๐)) |
48 | 5, 47 | biimtrrid 242 |
. . . 4
โข ((๐ โ โค[i] โง ๐ โ โค[i]) โ
((โ๐ โ
โค[i] ๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง โ๐ โ
โค[i] ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))
โ (๐ด ยท ๐ต) โ ๐)) |
49 | 48 | rexlimivv 3193 |
. . 3
โข
(โ๐ โ
โค[i] โ๐ โ
โค[i] (โ๐ โ
โค[i] ๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง โ๐ โ
โค[i] ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))
โ (๐ด ยท ๐ต) โ ๐) |
50 | 4, 49 | sylbir 234 |
. 2
โข
((โ๐ โ
โค[i] โ๐ โ
โค[i] ๐ด =
(((absโ๐)โ2) +
((absโ๐)โ2))
โง โ๐ โ
โค[i] โ๐ โ
โค[i] ๐ต =
(((absโ๐)โ2) +
((absโ๐)โ2)))
โ (๐ด ยท ๐ต) โ ๐) |
51 | 2, 3, 50 | syl2anb 599 |
1
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด ยท ๐ต) โ ๐) |