Step | Hyp | Ref
| Expression |
1 | | 1cnd 11157 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
2 | 1, 1 | addcld 11181 |
. . . . . . 7
โข (๐ โ (1 + 1) โ
โ) |
3 | | muld.1 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
4 | | addcomd.2 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
5 | 2, 3, 4 | adddid 11186 |
. . . . . 6
โข (๐ โ ((1 + 1) ยท (๐ด + ๐ต)) = (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต))) |
6 | 3, 4 | addcld 11181 |
. . . . . . 7
โข (๐ โ (๐ด + ๐ต) โ โ) |
7 | | 1p1times 11333 |
. . . . . . 7
โข ((๐ด + ๐ต) โ โ โ ((1 + 1) ยท
(๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
8 | 6, 7 | syl 17 |
. . . . . 6
โข (๐ โ ((1 + 1) ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
9 | | 1p1times 11333 |
. . . . . . . 8
โข (๐ด โ โ โ ((1 + 1)
ยท ๐ด) = (๐ด + ๐ด)) |
10 | 3, 9 | syl 17 |
. . . . . . 7
โข (๐ โ ((1 + 1) ยท ๐ด) = (๐ด + ๐ด)) |
11 | | 1p1times 11333 |
. . . . . . . 8
โข (๐ต โ โ โ ((1 + 1)
ยท ๐ต) = (๐ต + ๐ต)) |
12 | 4, 11 | syl 17 |
. . . . . . 7
โข (๐ โ ((1 + 1) ยท ๐ต) = (๐ต + ๐ต)) |
13 | 10, 12 | oveq12d 7380 |
. . . . . 6
โข (๐ โ (((1 + 1) ยท ๐ด) + ((1 + 1) ยท ๐ต)) = ((๐ด + ๐ด) + (๐ต + ๐ต))) |
14 | 5, 8, 13 | 3eqtr3rd 2786 |
. . . . 5
โข (๐ โ ((๐ด + ๐ด) + (๐ต + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
15 | 3, 3 | addcld 11181 |
. . . . . 6
โข (๐ โ (๐ด + ๐ด) โ โ) |
16 | 15, 4, 4 | addassd 11184 |
. . . . 5
โข (๐ โ (((๐ด + ๐ด) + ๐ต) + ๐ต) = ((๐ด + ๐ด) + (๐ต + ๐ต))) |
17 | 6, 3, 4 | addassd 11184 |
. . . . 5
โข (๐ โ (((๐ด + ๐ต) + ๐ด) + ๐ต) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
18 | 14, 16, 17 | 3eqtr4d 2787 |
. . . 4
โข (๐ โ (((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต)) |
19 | 15, 4 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐ด + ๐ด) + ๐ต) โ โ) |
20 | 6, 3 | addcld 11181 |
. . . . 5
โข (๐ โ ((๐ด + ๐ต) + ๐ด) โ โ) |
21 | | addcan2 11347 |
. . . . 5
โข ((((๐ด + ๐ด) + ๐ต) โ โ โง ((๐ด + ๐ต) + ๐ด) โ โ โง ๐ต โ โ) โ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))) |
22 | 19, 20, 4, 21 | syl3anc 1372 |
. . . 4
โข (๐ โ ((((๐ด + ๐ด) + ๐ต) + ๐ต) = (((๐ด + ๐ต) + ๐ด) + ๐ต) โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด))) |
23 | 18, 22 | mpbid 231 |
. . 3
โข (๐ โ ((๐ด + ๐ด) + ๐ต) = ((๐ด + ๐ต) + ๐ด)) |
24 | 3, 3, 4 | addassd 11184 |
. . 3
โข (๐ โ ((๐ด + ๐ด) + ๐ต) = (๐ด + (๐ด + ๐ต))) |
25 | 3, 4, 3 | addassd 11184 |
. . 3
โข (๐ โ ((๐ด + ๐ต) + ๐ด) = (๐ด + (๐ต + ๐ด))) |
26 | 23, 24, 25 | 3eqtr3d 2785 |
. 2
โข (๐ โ (๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด))) |
27 | 4, 3 | addcld 11181 |
. . 3
โข (๐ โ (๐ต + ๐ด) โ โ) |
28 | | addcan 11346 |
. . 3
โข ((๐ด โ โ โง (๐ด + ๐ต) โ โ โง (๐ต + ๐ด) โ โ) โ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ (๐ด + ๐ต) = (๐ต + ๐ด))) |
29 | 3, 6, 27, 28 | syl3anc 1372 |
. 2
โข (๐ โ ((๐ด + (๐ด + ๐ต)) = (๐ด + (๐ต + ๐ด)) โ (๐ด + ๐ต) = (๐ต + ๐ด))) |
30 | 26, 29 | mpbid 231 |
1
โข (๐ โ (๐ด + ๐ต) = (๐ต + ๐ด)) |