Step | Hyp | Ref
| Expression |
1 | | oveq2 5882 |
. . . . 5
โข (๐ฅ = 1 โ (๐ด ยท ๐ฅ) = (๐ด ยท 1)) |
2 | 1 | eleq1d 2246 |
. . . 4
โข (๐ฅ = 1 โ ((๐ด ยท ๐ฅ) โ โ โ (๐ด ยท 1) โ
โ)) |
3 | 2 | imbi2d 230 |
. . 3
โข (๐ฅ = 1 โ ((๐ด โ โ โ (๐ด ยท ๐ฅ) โ โ) โ (๐ด โ โ โ (๐ด ยท 1) โ
โ))) |
4 | | oveq2 5882 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ)) |
5 | 4 | eleq1d 2246 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด ยท ๐ฅ) โ โ โ (๐ด ยท ๐ฆ) โ โ)) |
6 | 5 | imbi2d 230 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ด โ โ โ (๐ด ยท ๐ฅ) โ โ) โ (๐ด โ โ โ (๐ด ยท ๐ฆ) โ โ))) |
7 | | oveq2 5882 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (๐ด ยท ๐ฅ) = (๐ด ยท (๐ฆ + 1))) |
8 | 7 | eleq1d 2246 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ ((๐ด ยท ๐ฅ) โ โ โ (๐ด ยท (๐ฆ + 1)) โ โ)) |
9 | 8 | imbi2d 230 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ ((๐ด โ โ โ (๐ด ยท ๐ฅ) โ โ) โ (๐ด โ โ โ (๐ด ยท (๐ฆ + 1)) โ โ))) |
10 | | oveq2 5882 |
. . . . 5
โข (๐ฅ = ๐ต โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ต)) |
11 | 10 | eleq1d 2246 |
. . . 4
โข (๐ฅ = ๐ต โ ((๐ด ยท ๐ฅ) โ โ โ (๐ด ยท ๐ต) โ โ)) |
12 | 11 | imbi2d 230 |
. . 3
โข (๐ฅ = ๐ต โ ((๐ด โ โ โ (๐ด ยท ๐ฅ) โ โ) โ (๐ด โ โ โ (๐ด ยท ๐ต) โ โ))) |
13 | | nncn 8926 |
. . . 4
โข (๐ด โ โ โ ๐ด โ
โ) |
14 | | mulrid 7953 |
. . . . . 6
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
15 | 14 | eleq1d 2246 |
. . . . 5
โข (๐ด โ โ โ ((๐ด ยท 1) โ โ
โ ๐ด โ
โ)) |
16 | 15 | biimprd 158 |
. . . 4
โข (๐ด โ โ โ (๐ด โ โ โ (๐ด ยท 1) โ
โ)) |
17 | 13, 16 | mpcom 36 |
. . 3
โข (๐ด โ โ โ (๐ด ยท 1) โ
โ) |
18 | | nnaddcl 8938 |
. . . . . . . 8
โข (((๐ด ยท ๐ฆ) โ โ โง ๐ด โ โ) โ ((๐ด ยท ๐ฆ) + ๐ด) โ โ) |
19 | 18 | ancoms 268 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ด ยท ๐ฆ) โ โ) โ ((๐ด ยท ๐ฆ) + ๐ด) โ โ) |
20 | | nncn 8926 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
21 | | ax-1cn 7903 |
. . . . . . . . . . 11
โข 1 โ
โ |
22 | | adddi 7942 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฆ โ โ โง 1 โ
โ) โ (๐ด ยท
(๐ฆ + 1)) = ((๐ด ยท ๐ฆ) + (๐ด ยท 1))) |
23 | 21, 22 | mp3an3 1326 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ฆ โ โ) โ (๐ด ยท (๐ฆ + 1)) = ((๐ด ยท ๐ฆ) + (๐ด ยท 1))) |
24 | 14 | oveq2d 5890 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((๐ด ยท ๐ฆ) + (๐ด ยท 1)) = ((๐ด ยท ๐ฆ) + ๐ด)) |
25 | 24 | adantr 276 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ฆ โ โ) โ ((๐ด ยท ๐ฆ) + (๐ด ยท 1)) = ((๐ด ยท ๐ฆ) + ๐ด)) |
26 | 23, 25 | eqtrd 2210 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ฆ โ โ) โ (๐ด ยท (๐ฆ + 1)) = ((๐ด ยท ๐ฆ) + ๐ด)) |
27 | 13, 20, 26 | syl2an 289 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ฆ โ โ) โ (๐ด ยท (๐ฆ + 1)) = ((๐ด ยท ๐ฆ) + ๐ด)) |
28 | 27 | eleq1d 2246 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ฆ โ โ) โ ((๐ด ยท (๐ฆ + 1)) โ โ โ ((๐ด ยท ๐ฆ) + ๐ด) โ โ)) |
29 | 19, 28 | imbitrrid 156 |
. . . . . 6
โข ((๐ด โ โ โง ๐ฆ โ โ) โ ((๐ด โ โ โง (๐ด ยท ๐ฆ) โ โ) โ (๐ด ยท (๐ฆ + 1)) โ โ)) |
30 | 29 | exp4b 367 |
. . . . 5
โข (๐ด โ โ โ (๐ฆ โ โ โ (๐ด โ โ โ ((๐ด ยท ๐ฆ) โ โ โ (๐ด ยท (๐ฆ + 1)) โ โ)))) |
31 | 30 | pm2.43b 52 |
. . . 4
โข (๐ฆ โ โ โ (๐ด โ โ โ ((๐ด ยท ๐ฆ) โ โ โ (๐ด ยท (๐ฆ + 1)) โ โ))) |
32 | 31 | a2d 26 |
. . 3
โข (๐ฆ โ โ โ ((๐ด โ โ โ (๐ด ยท ๐ฆ) โ โ) โ (๐ด โ โ โ (๐ด ยท (๐ฆ + 1)) โ โ))) |
33 | 3, 6, 9, 12, 17, 32 | nnind 8934 |
. 2
โข (๐ต โ โ โ (๐ด โ โ โ (๐ด ยท ๐ต) โ โ)) |
34 | 33 | impcom 125 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |