Step | Hyp | Ref
| Expression |
1 | | 2itscplem3.s |
. . 3
โข ๐ = (((๐
โ2) ยท ๐) โ (๐ถโ2)) |
2 | 1 | a1i 11 |
. 2
โข (๐ โ ๐ = (((๐
โ2) ยท ๐) โ (๐ถโ2))) |
3 | | 2itscplem3.q |
. . . . . 6
โข ๐ = ((๐ธโ2) + (๐ทโ2)) |
4 | 3 | a1i 11 |
. . . . 5
โข (๐ โ ๐ = ((๐ธโ2) + (๐ทโ2))) |
5 | 4 | oveq2d 7377 |
. . . 4
โข (๐ โ ((๐
โ2) ยท ๐) = ((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2)))) |
6 | | 2itscp.r |
. . . . . . 7
โข (๐ โ ๐
โ โ) |
7 | 6 | recnd 11191 |
. . . . . 6
โข (๐ โ ๐
โ โ) |
8 | 7 | sqcld 14058 |
. . . . 5
โข (๐ โ (๐
โ2) โ โ) |
9 | | 2itscp.e |
. . . . . . . 8
โข ๐ธ = (๐ต โ ๐) |
10 | | 2itscp.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
11 | 10 | recnd 11191 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
12 | | 2itscp.y |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
13 | 12 | recnd 11191 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
14 | 11, 13 | subcld 11520 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐) โ โ) |
15 | 9, 14 | eqeltrid 2838 |
. . . . . . 7
โข (๐ โ ๐ธ โ โ) |
16 | 15 | sqcld 14058 |
. . . . . 6
โข (๐ โ (๐ธโ2) โ โ) |
17 | | 2itscp.d |
. . . . . . . 8
โข ๐ท = (๐ โ ๐ด) |
18 | | 2itscp.x |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
19 | 18 | recnd 11191 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
20 | | 2itscp.a |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
21 | 20 | recnd 11191 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
22 | 19, 21 | subcld 11520 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ด) โ โ) |
23 | 17, 22 | eqeltrid 2838 |
. . . . . . 7
โข (๐ โ ๐ท โ โ) |
24 | 23 | sqcld 14058 |
. . . . . 6
โข (๐ โ (๐ทโ2) โ โ) |
25 | 16, 24 | addcld 11182 |
. . . . 5
โข (๐ โ ((๐ธโ2) + (๐ทโ2)) โ โ) |
26 | 8, 25 | mulcomd 11184 |
. . . 4
โข (๐ โ ((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2))) = (((๐ธโ2) + (๐ทโ2)) ยท (๐
โ2))) |
27 | 16, 24, 8 | adddird 11188 |
. . . 4
โข (๐ โ (((๐ธโ2) + (๐ทโ2)) ยท (๐
โ2)) = (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2)))) |
28 | 5, 26, 27 | 3eqtrd 2777 |
. . 3
โข (๐ โ ((๐
โ2) ยท ๐) = (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2)))) |
29 | | 2itscp.c |
. . . 4
โข ๐ถ = ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)) |
30 | 20, 10, 18, 12, 17, 9, 29 | 2itscplem2 46955 |
. . 3
โข (๐ โ (๐ถโ2) = ((((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธโ2) ยท (๐ดโ2)))) |
31 | 28, 30 | oveq12d 7379 |
. 2
โข (๐ โ (((๐
โ2) ยท ๐) โ (๐ถโ2)) = ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธโ2) ยท (๐ดโ2))))) |
32 | 16, 8 | mulcld 11183 |
. . . . . . . 8
โข (๐ โ ((๐ธโ2) ยท (๐
โ2)) โ โ) |
33 | 24, 8 | mulcld 11183 |
. . . . . . . 8
โข (๐ โ ((๐ทโ2) ยท (๐
โ2)) โ โ) |
34 | 32, 33 | addcld 11182 |
. . . . . . 7
โข (๐ โ (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ โ) |
35 | 11 | sqcld 14058 |
. . . . . . . 8
โข (๐ โ (๐ตโ2) โ โ) |
36 | 24, 35 | mulcld 11183 |
. . . . . . 7
โข (๐ โ ((๐ทโ2) ยท (๐ตโ2)) โ โ) |
37 | | 2cnd 12239 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
38 | 23, 21 | mulcld 11183 |
. . . . . . . . 9
โข (๐ โ (๐ท ยท ๐ด) โ โ) |
39 | 15, 11 | mulcld 11183 |
. . . . . . . . 9
โข (๐ โ (๐ธ ยท ๐ต) โ โ) |
40 | 38, 39 | mulcld 11183 |
. . . . . . . 8
โข (๐ โ ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)) โ โ) |
41 | 37, 40 | mulcld 11183 |
. . . . . . 7
โข (๐ โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))) โ โ) |
42 | 34, 36, 41 | subsub4d 11551 |
. . . . . 6
โข (๐ โ (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) = ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))))) |
43 | 42 | eqcomd 2739 |
. . . . 5
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) = (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |
44 | 43 | oveq1d 7376 |
. . . 4
โข (๐ โ (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) โ ((๐ธโ2) ยท (๐ดโ2))) = ((((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) โ ((๐ธโ2) ยท (๐ดโ2)))) |
45 | 34, 36 | subcld 11520 |
. . . . 5
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ โ) |
46 | 21 | sqcld 14058 |
. . . . . 6
โข (๐ โ (๐ดโ2) โ โ) |
47 | 16, 46 | mulcld 11183 |
. . . . 5
โข (๐ โ ((๐ธโ2) ยท (๐ดโ2)) โ โ) |
48 | 45, 41, 47 | sub32d 11552 |
. . . 4
โข (๐ โ ((((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) โ ((๐ธโ2) ยท (๐ดโ2))) = ((((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ ((๐ธโ2) ยท (๐ดโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |
49 | 44, 48 | eqtrd 2773 |
. . 3
โข (๐ โ (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) โ ((๐ธโ2) ยท (๐ดโ2))) = ((((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ ((๐ธโ2) ยท (๐ดโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |
50 | 36, 41 | addcld 11182 |
. . . 4
โข (๐ โ (((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) โ โ) |
51 | 34, 50, 47 | subsub4d 11551 |
. . 3
โข (๐ โ (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) โ ((๐ธโ2) ยท (๐ดโ2))) = ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธโ2) ยท (๐ดโ2))))) |
52 | 32, 33, 36 | addsubassd 11540 |
. . . . . . 7
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) = (((๐ธโ2) ยท (๐
โ2)) + (((๐ทโ2) ยท (๐
โ2)) โ ((๐ทโ2) ยท (๐ตโ2))))) |
53 | 24, 8, 35 | subdid 11619 |
. . . . . . . . 9
โข (๐ โ ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))) = (((๐ทโ2) ยท (๐
โ2)) โ ((๐ทโ2) ยท (๐ตโ2)))) |
54 | 53 | eqcomd 2739 |
. . . . . . . 8
โข (๐ โ (((๐ทโ2) ยท (๐
โ2)) โ ((๐ทโ2) ยท (๐ตโ2))) = ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) |
55 | 54 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ (((๐ธโ2) ยท (๐
โ2)) + (((๐ทโ2) ยท (๐
โ2)) โ ((๐ทโ2) ยท (๐ตโ2)))) = (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))))) |
56 | 52, 55 | eqtrd 2773 |
. . . . . 6
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) = (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))))) |
57 | 56 | oveq1d 7376 |
. . . . 5
โข (๐ โ (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ ((๐ธโ2) ยท (๐ดโ2))) = ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) โ ((๐ธโ2) ยท (๐ดโ2)))) |
58 | 8, 35 | subcld 11520 |
. . . . . . 7
โข (๐ โ ((๐
โ2) โ (๐ตโ2)) โ โ) |
59 | 24, 58 | mulcld 11183 |
. . . . . 6
โข (๐ โ ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))) โ โ) |
60 | 32, 59, 47 | addsubd 11541 |
. . . . 5
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) โ ((๐ธโ2) ยท (๐ดโ2))) = ((((๐ธโ2) ยท (๐
โ2)) โ ((๐ธโ2) ยท (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))))) |
61 | 16, 8, 46 | subdid 11619 |
. . . . . . 7
โข (๐ โ ((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2))) = (((๐ธโ2) ยท (๐
โ2)) โ ((๐ธโ2) ยท (๐ดโ2)))) |
62 | 61 | eqcomd 2739 |
. . . . . 6
โข (๐ โ (((๐ธโ2) ยท (๐
โ2)) โ ((๐ธโ2) ยท (๐ดโ2))) = ((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2)))) |
63 | 62 | oveq1d 7376 |
. . . . 5
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) โ ((๐ธโ2) ยท (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) = (((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))))) |
64 | 57, 60, 63 | 3eqtrd 2777 |
. . . 4
โข (๐ โ (((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ ((๐ธโ2) ยท (๐ดโ2))) = (((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2))))) |
65 | 64 | oveq1d 7376 |
. . 3
โข (๐ โ ((((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((๐ทโ2) ยท (๐ตโ2))) โ ((๐ธโ2) ยท (๐ดโ2))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) = ((((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |
66 | 49, 51, 65 | 3eqtr3d 2781 |
. 2
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ ((((๐ทโ2) ยท (๐ตโ2)) + (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต)))) + ((๐ธโ2) ยท (๐ดโ2)))) = ((((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |
67 | 2, 31, 66 | 3eqtrd 2777 |
1
โข (๐ โ ๐ = ((((๐ธโ2) ยท ((๐
โ2) โ (๐ดโ2))) + ((๐ทโ2) ยท ((๐
โ2) โ (๐ตโ2)))) โ (2 ยท ((๐ท ยท ๐ด) ยท (๐ธ ยท ๐ต))))) |