Step | Hyp | Ref
| Expression |
1 | | zmulcl 9308 |
. . . 4
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
2 | 1 | anim1i 340 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค) โง ๐ โ โค) โ ((๐พ ยท ๐) โ โค โง ๐ โ โค)) |
3 | 2 | 3impa 1194 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โ โค โง ๐ โ โค)) |
4 | | 3simpc 996 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ โ โค โง ๐ โ
โค)) |
5 | | zmulcl 9308 |
. . . 4
โข ((๐ฅ โ โค โง ๐พ โ โค) โ (๐ฅ ยท ๐พ) โ โค) |
6 | 5 | ancoms 268 |
. . 3
โข ((๐พ โ โค โง ๐ฅ โ โค) โ (๐ฅ ยท ๐พ) โ โค) |
7 | 6 | 3ad2antl1 1159 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ (๐ฅ ยท ๐พ) โ โค) |
8 | | zcn 9260 |
. . . . . . . 8
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
9 | | zcn 9260 |
. . . . . . . 8
โข (๐พ โ โค โ ๐พ โ
โ) |
10 | | zcn 9260 |
. . . . . . . 8
โข (๐ โ โค โ ๐ โ
โ) |
11 | | mulass 7944 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐พ โ โ โง ๐ โ โ) โ ((๐ฅ ยท ๐พ) ยท ๐) = (๐ฅ ยท (๐พ ยท ๐))) |
12 | 8, 9, 10, 11 | syl3an 1280 |
. . . . . . 7
โข ((๐ฅ โ โค โง ๐พ โ โค โง ๐ โ โค) โ ((๐ฅ ยท ๐พ) ยท ๐) = (๐ฅ ยท (๐พ ยท ๐))) |
13 | 12 | 3coml 1210 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐พ) ยท ๐) = (๐ฅ ยท (๐พ ยท ๐))) |
14 | 13 | 3expa 1203 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐พ) ยท ๐) = (๐ฅ ยท (๐พ ยท ๐))) |
15 | 14 | 3adantl3 1155 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐พ) ยท ๐) = (๐ฅ ยท (๐พ ยท ๐))) |
16 | 15 | eqeq1d 2186 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ (((๐ฅ ยท ๐พ) ยท ๐) = ๐ โ (๐ฅ ยท (๐พ ยท ๐)) = ๐)) |
17 | 16 | biimprd 158 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐พ ยท ๐)) = ๐ โ ((๐ฅ ยท ๐พ) ยท ๐) = ๐)) |
18 | 3, 4, 7, 17 | dvds1lem 11811 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โฅ ๐ โ ๐ โฅ ๐)) |