Step | Hyp | Ref
| Expression |
1 | | ax-1cn 11116 |
. . . 4
โข 1 โ
โ |
2 | | addcl 11140 |
. . . 4
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + ๐ด) โ โ) |
3 | 1, 2 | mpan 689 |
. . 3
โข (๐ด โ โ โ (1 +
๐ด) โ
โ) |
4 | | adddi 11147 |
. . . 4
โข (((1 +
๐ด) โ โ โง 1
โ โ โง ๐ต
โ โ) โ ((1 + ๐ด) ยท (1 + ๐ต)) = (((1 + ๐ด) ยท 1) + ((1 + ๐ด) ยท ๐ต))) |
5 | 1, 4 | mp3an2 1450 |
. . 3
โข (((1 +
๐ด) โ โ โง
๐ต โ โ) โ
((1 + ๐ด) ยท (1 +
๐ต)) = (((1 + ๐ด) ยท 1) + ((1 + ๐ด) ยท ๐ต))) |
6 | 3, 5 | sylan 581 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท (1 + ๐ต)) = (((1 + ๐ด) ยท 1) + ((1 + ๐ด) ยท ๐ต))) |
7 | 3 | mulid1d 11179 |
. . . 4
โข (๐ด โ โ โ ((1 +
๐ด) ยท 1) = (1 + ๐ด)) |
8 | 7 | adantr 482 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท 1) = (1 + ๐ด)) |
9 | | adddir 11153 |
. . . . 5
โข ((1
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((1 + ๐ด) ยท ๐ต) = ((1 ยท ๐ต) + (๐ด ยท ๐ต))) |
10 | 1, 9 | mp3an1 1449 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท ๐ต) = ((1 ยท ๐ต) + (๐ด ยท ๐ต))) |
11 | | mulid2 11161 |
. . . . . 6
โข (๐ต โ โ โ (1
ยท ๐ต) = ๐ต) |
12 | 11 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ๐ต) = ๐ต) |
13 | 12 | oveq1d 7377 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1
ยท ๐ต) + (๐ด ยท ๐ต)) = (๐ต + (๐ด ยท ๐ต))) |
14 | 10, 13 | eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท ๐ต) = (๐ต + (๐ด ยท ๐ต))) |
15 | 8, 14 | oveq12d 7380 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((1 +
๐ด) ยท 1) + ((1 +
๐ด) ยท ๐ต)) = ((1 + ๐ด) + (๐ต + (๐ด ยท ๐ต)))) |
16 | 6, 15 | eqtrd 2777 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท (1 + ๐ต)) = ((1 + ๐ด) + (๐ต + (๐ด ยท ๐ต)))) |