Step | Hyp | Ref
| Expression |
1 | | 2cn 8990 |
. . . . . . . 8
โข 2 โ
โ |
2 | | mulcl 7938 |
. . . . . . . 8
โข ((2
โ โ โง ๐ต
โ โ) โ (2 ยท ๐ต) โ โ) |
3 | 1, 2 | mpan 424 |
. . . . . . 7
โข (๐ต โ โ โ (2
ยท ๐ต) โ
โ) |
4 | 3 | adantl 277 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ต) โ
โ) |
5 | | subadd23 8169 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง (2
ยท ๐ต) โ โ)
โ ((๐ด โ ๐ต) + (2 ยท ๐ต)) = (๐ด + ((2 ยท ๐ต) โ ๐ต))) |
6 | 4, 5 | mpd3an3 1338 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) + (2 ยท ๐ต)) = (๐ด + ((2 ยท ๐ต) โ ๐ต))) |
7 | | 2times 9047 |
. . . . . . . . 9
โข (๐ต โ โ โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
8 | 7 | oveq1d 5890 |
. . . . . . . 8
โข (๐ต โ โ โ ((2
ยท ๐ต) โ ๐ต) = ((๐ต + ๐ต) โ ๐ต)) |
9 | | pncan 8163 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ต โ โ) โ ((๐ต + ๐ต) โ ๐ต) = ๐ต) |
10 | 9 | anidms 397 |
. . . . . . . 8
โข (๐ต โ โ โ ((๐ต + ๐ต) โ ๐ต) = ๐ต) |
11 | 8, 10 | eqtrd 2210 |
. . . . . . 7
โข (๐ต โ โ โ ((2
ยท ๐ต) โ ๐ต) = ๐ต) |
12 | 11 | adantl 277 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท ๐ต) โ ๐ต) = ๐ต) |
13 | 12 | oveq2d 5891 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ((2 ยท ๐ต) โ ๐ต)) = (๐ด + ๐ต)) |
14 | 6, 13 | eqtrd 2210 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) + (2 ยท ๐ต)) = (๐ด + ๐ต)) |
15 | 14 | oveq1d 5890 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด โ ๐ต) + (2 ยท ๐ต)) ยท (๐ด โ ๐ต)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
16 | | subcl 8156 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) |
17 | 16, 4, 16 | adddird 7983 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด โ ๐ต) + (2 ยท ๐ต)) ยท (๐ด โ ๐ต)) = (((๐ด โ ๐ต) ยท (๐ด โ ๐ต)) + ((2 ยท ๐ต) ยท (๐ด โ ๐ต)))) |
18 | 15, 17 | eqtr3d 2212 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) ยท (๐ด โ ๐ต)) = (((๐ด โ ๐ต) ยท (๐ด โ ๐ต)) + ((2 ยท ๐ต) ยท (๐ด โ ๐ต)))) |
19 | | subsq 10627 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) โ (๐ตโ2)) = ((๐ด + ๐ต) ยท (๐ด โ ๐ต))) |
20 | | sqval 10578 |
. . . 4
โข ((๐ด โ ๐ต) โ โ โ ((๐ด โ ๐ต)โ2) = ((๐ด โ ๐ต) ยท (๐ด โ ๐ต))) |
21 | 16, 20 | syl 14 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต)โ2) = ((๐ด โ ๐ต) ยท (๐ด โ ๐ต))) |
22 | 21 | oveq1d 5890 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด โ ๐ต)โ2) + ((2 ยท ๐ต) ยท (๐ด โ ๐ต))) = (((๐ด โ ๐ต) ยท (๐ด โ ๐ต)) + ((2 ยท ๐ต) ยท (๐ด โ ๐ต)))) |
23 | 18, 19, 22 | 3eqtr4d 2220 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) โ (๐ตโ2)) = (((๐ด โ ๐ต)โ2) + ((2 ยท ๐ต) ยท (๐ด โ ๐ต)))) |