Step | Hyp | Ref
| Expression |
1 | | 2itscp.e |
. . . . . . 7
โข ๐ธ = (๐ต โ ๐) |
2 | | 2itscp.b |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
3 | 2 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
4 | | 2itscp.y |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
5 | 4 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
6 | 3, 5 | subcld 11520 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐) โ โ) |
7 | 1, 6 | eqeltrid 2838 |
. . . . . 6
โข (๐ โ ๐ธ โ โ) |
8 | 7 | sqcld 14058 |
. . . . 5
โข (๐ โ (๐ธโ2) โ โ) |
9 | 3 | sqcld 14058 |
. . . . 5
โข (๐ โ (๐ตโ2) โ โ) |
10 | 8, 9 | mulcld 11183 |
. . . 4
โข (๐ โ ((๐ธโ2) ยท (๐ตโ2)) โ โ) |
11 | | 2itscp.d |
. . . . . . 7
โข ๐ท = (๐ โ ๐ด) |
12 | | 2itscp.x |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
13 | 12 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
14 | | 2itscp.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
15 | 14 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
16 | 13, 15 | subcld 11520 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ด) โ โ) |
17 | 11, 16 | eqeltrid 2838 |
. . . . . 6
โข (๐ โ ๐ท โ โ) |
18 | 17 | sqcld 14058 |
. . . . 5
โข (๐ โ (๐ทโ2) โ โ) |
19 | 15 | sqcld 14058 |
. . . . 5
โข (๐ โ (๐ดโ2) โ โ) |
20 | 18, 19 | mulcld 11183 |
. . . 4
โข (๐ โ ((๐ทโ2) ยท (๐ดโ2)) โ โ) |
21 | | 2cnd 12239 |
. . . . 5
โข (๐ โ 2 โ
โ) |
22 | 17, 15 | mulcld 11183 |
. . . . . 6
โข (๐ โ (๐ท ยท ๐ด) โ โ) |
23 | 7, 3 | mulcld 11183 |
. . . . . 6
โข (๐ โ (๐ธ ยท ๐ต) โ โ) |
24 | 22, 23 | mulcld 11183 |
. . . . 5
โข (๐ โ ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)) โ โ) |
25 | 21, 24 | mulcld 11183 |
. . . 4
โข (๐ โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))) โ โ) |
26 | 10, 20, 25 | addsubassd 11540 |
. . 3
โข (๐ โ ((((๐ธโ2) ยท (๐ตโ2)) + ((๐ทโ2) ยท (๐ดโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) = (((๐ธโ2) ยท (๐ตโ2)) + (((๐ทโ2) ยท (๐ดโ2)) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))))) |
27 | 20, 25 | subcld 11520 |
. . . 4
โข (๐ โ (((๐ทโ2) ยท (๐ดโ2)) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) โ โ) |
28 | 10, 27 | addcomd 11365 |
. . 3
โข (๐ โ (((๐ธโ2) ยท (๐ตโ2)) + (((๐ทโ2) ยท (๐ดโ2)) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) = ((((๐ทโ2) ยท (๐ดโ2)) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธโ2) ยท (๐ตโ2)))) |
29 | 17, 15 | sqmuld 14072 |
. . . . . 6
โข (๐ โ ((๐ท ยท ๐ด)โ2) = ((๐ทโ2) ยท (๐ดโ2))) |
30 | 29 | eqcomd 2739 |
. . . . 5
โข (๐ โ ((๐ทโ2) ยท (๐ดโ2)) = ((๐ท ยท ๐ด)โ2)) |
31 | 30 | oveq1d 7376 |
. . . 4
โข (๐ โ (((๐ทโ2) ยท (๐ดโ2)) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) = (((๐ท ยท ๐ด)โ2) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |
32 | 7, 3 | sqmuld 14072 |
. . . . 5
โข (๐ โ ((๐ธ ยท ๐ต)โ2) = ((๐ธโ2) ยท (๐ตโ2))) |
33 | 32 | eqcomd 2739 |
. . . 4
โข (๐ โ ((๐ธโ2) ยท (๐ตโ2)) = ((๐ธ ยท ๐ต)โ2)) |
34 | 31, 33 | oveq12d 7379 |
. . 3
โข (๐ โ ((((๐ทโ2) ยท (๐ดโ2)) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธโ2) ยท (๐ตโ2))) = ((((๐ท ยท ๐ด)โ2) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธ ยท ๐ต)โ2))) |
35 | 26, 28, 34 | 3eqtrd 2777 |
. 2
โข (๐ โ ((((๐ธโ2) ยท (๐ตโ2)) + ((๐ทโ2) ยท (๐ดโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) = ((((๐ท ยท ๐ด)โ2) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธ ยท ๐ต)โ2))) |
36 | | binom2sub 14132 |
. . 3
โข (((๐ท ยท ๐ด) โ โ โง (๐ธ ยท ๐ต) โ โ) โ (((๐ท ยท ๐ด) โ (๐ธ ยท ๐ต))โ2) = ((((๐ท ยท ๐ด)โ2) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธ ยท ๐ต)โ2))) |
37 | 22, 23, 36 | syl2anc 585 |
. 2
โข (๐ โ (((๐ท ยท ๐ด) โ (๐ธ ยท ๐ต))โ2) = ((((๐ท ยท ๐ด)โ2) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธ ยท ๐ต)โ2))) |
38 | 35, 37 | eqtr4d 2776 |
1
โข (๐ โ ((((๐ธโ2) ยท (๐ตโ2)) + ((๐ทโ2) ยท (๐ดโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) = (((๐ท ยท ๐ด) โ (๐ธ ยท ๐ต))โ2)) |