Step | Hyp | Ref
| Expression |
1 | | ax-1cn 7906 |
. . . 4
โข 1 โ
โ |
2 | | addcl 7938 |
. . . 4
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + ๐ด) โ โ) |
3 | 1, 2 | mpan 424 |
. . 3
โข (๐ด โ โ โ (1 +
๐ด) โ
โ) |
4 | | adddi 7945 |
. . . 4
โข (((1 +
๐ด) โ โ โง 1
โ โ โง ๐ต
โ โ) โ ((1 + ๐ด) ยท (1 + ๐ต)) = (((1 + ๐ด) ยท 1) + ((1 + ๐ด) ยท ๐ต))) |
5 | 1, 4 | mp3an2 1325 |
. . 3
โข (((1 +
๐ด) โ โ โง
๐ต โ โ) โ
((1 + ๐ด) ยท (1 +
๐ต)) = (((1 + ๐ด) ยท 1) + ((1 + ๐ด) ยท ๐ต))) |
6 | 3, 5 | sylan 283 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท (1 + ๐ต)) = (((1 + ๐ด) ยท 1) + ((1 + ๐ด) ยท ๐ต))) |
7 | 3 | mulridd 7976 |
. . . 4
โข (๐ด โ โ โ ((1 +
๐ด) ยท 1) = (1 + ๐ด)) |
8 | 7 | adantr 276 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท 1) = (1 + ๐ด)) |
9 | | adddir 7950 |
. . . . 5
โข ((1
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((1 + ๐ด) ยท ๐ต) = ((1 ยท ๐ต) + (๐ด ยท ๐ต))) |
10 | 1, 9 | mp3an1 1324 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท ๐ต) = ((1 ยท ๐ต) + (๐ด ยท ๐ต))) |
11 | | mullid 7957 |
. . . . . 6
โข (๐ต โ โ โ (1
ยท ๐ต) = ๐ต) |
12 | 11 | adantl 277 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (1
ยท ๐ต) = ๐ต) |
13 | 12 | oveq1d 5892 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1
ยท ๐ต) + (๐ด ยท ๐ต)) = (๐ต + (๐ด ยท ๐ต))) |
14 | 10, 13 | eqtrd 2210 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท ๐ต) = (๐ต + (๐ด ยท ๐ต))) |
15 | 8, 14 | oveq12d 5895 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((1 +
๐ด) ยท 1) + ((1 +
๐ด) ยท ๐ต)) = ((1 + ๐ด) + (๐ต + (๐ด ยท ๐ต)))) |
16 | 6, 15 | eqtrd 2210 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((1 +
๐ด) ยท (1 + ๐ต)) = ((1 + ๐ด) + (๐ต + (๐ด ยท ๐ต)))) |