Step | Hyp | Ref
| Expression |
1 | | oveq1 7412 |
. . . . 5
โข (๐ฅ = 1 โ (๐ฅ ยท ๐ต) = (1 ยท ๐ต)) |
2 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = 1 โ (๐ต ยท ๐ฅ) = (๐ต ยท 1)) |
3 | 1, 2 | eqeq12d 2742 |
. . . 4
โข (๐ฅ = 1 โ ((๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ) โ (1 ยท ๐ต) = (๐ต ยท 1))) |
4 | 3 | imbi2d 340 |
. . 3
โข (๐ฅ = 1 โ ((๐ต โ โ โ (๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ)) โ (๐ต โ โ โ (1 ยท ๐ต) = (๐ต ยท 1)))) |
5 | | oveq1 7412 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ฅ ยท ๐ต) = (๐ฆ ยท ๐ต)) |
6 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
7 | 5, 6 | eqeq12d 2742 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ) โ (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ))) |
8 | 7 | imbi2d 340 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ต โ โ โ (๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ)) โ (๐ต โ โ โ (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)))) |
9 | | oveq1 7412 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (๐ฅ ยท ๐ต) = ((๐ฆ + 1) ยท ๐ต)) |
10 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (๐ต ยท ๐ฅ) = (๐ต ยท (๐ฆ + 1))) |
11 | 9, 10 | eqeq12d 2742 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ ((๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ) โ ((๐ฆ + 1) ยท ๐ต) = (๐ต ยท (๐ฆ + 1)))) |
12 | 11 | imbi2d 340 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ ((๐ต โ โ โ (๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ)) โ (๐ต โ โ โ ((๐ฆ + 1) ยท ๐ต) = (๐ต ยท (๐ฆ + 1))))) |
13 | | oveq1 7412 |
. . . . 5
โข (๐ฅ = ๐ด โ (๐ฅ ยท ๐ต) = (๐ด ยท ๐ต)) |
14 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = ๐ด โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ด)) |
15 | 13, 14 | eqeq12d 2742 |
. . . 4
โข (๐ฅ = ๐ด โ ((๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด))) |
16 | 15 | imbi2d 340 |
. . 3
โข (๐ฅ = ๐ด โ ((๐ต โ โ โ (๐ฅ ยท ๐ต) = (๐ต ยท ๐ฅ)) โ (๐ต โ โ โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)))) |
17 | | nnmul1com 41739 |
. . 3
โข (๐ต โ โ โ (1
ยท ๐ต) = (๐ต ยท 1)) |
18 | | simp3 1135 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) |
19 | 17 | 3ad2ant2 1131 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ (1 ยท ๐ต) = (๐ต ยท 1)) |
20 | 18, 19 | oveq12d 7423 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ((๐ฆ ยท ๐ต) + (1 ยท ๐ต)) = ((๐ต ยท ๐ฆ) + (๐ต ยท 1))) |
21 | | simp1 1133 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ๐ฆ โ โ) |
22 | | 1nn 12227 |
. . . . . . . 8
โข 1 โ
โ |
23 | 22 | a1i 11 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ 1 โ โ) |
24 | | simp2 1134 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ๐ต โ โ) |
25 | | nnadddir 41738 |
. . . . . . 7
โข ((๐ฆ โ โ โง 1 โ
โ โง ๐ต โ
โ) โ ((๐ฆ + 1)
ยท ๐ต) = ((๐ฆ ยท ๐ต) + (1 ยท ๐ต))) |
26 | 21, 23, 24, 25 | syl3anc 1368 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ((๐ฆ + 1) ยท ๐ต) = ((๐ฆ ยท ๐ต) + (1 ยท ๐ต))) |
27 | 24 | nncnd 12232 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ๐ต โ โ) |
28 | 21 | nncnd 12232 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ๐ฆ โ โ) |
29 | | 1cnd 11213 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ 1 โ โ) |
30 | 27, 28, 29 | adddid 11242 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ (๐ต ยท (๐ฆ + 1)) = ((๐ต ยท ๐ฆ) + (๐ต ยท 1))) |
31 | 20, 26, 30 | 3eqtr4d 2776 |
. . . . 5
โข ((๐ฆ โ โ โง ๐ต โ โ โง (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ ((๐ฆ + 1) ยท ๐ต) = (๐ต ยท (๐ฆ + 1))) |
32 | 31 | 3exp 1116 |
. . . 4
โข (๐ฆ โ โ โ (๐ต โ โ โ ((๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ) โ ((๐ฆ + 1) ยท ๐ต) = (๐ต ยท (๐ฆ + 1))))) |
33 | 32 | a2d 29 |
. . 3
โข (๐ฆ โ โ โ ((๐ต โ โ โ (๐ฆ ยท ๐ต) = (๐ต ยท ๐ฆ)) โ (๐ต โ โ โ ((๐ฆ + 1) ยท ๐ต) = (๐ต ยท (๐ฆ + 1))))) |
34 | 4, 8, 12, 16, 17, 33 | nnind 12234 |
. 2
โข (๐ด โ โ โ (๐ต โ โ โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด))) |
35 | 34 | imp 406 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |