Step | Hyp | Ref
| Expression |
1 | | 3simpc 998 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ โ โค โง ๐ โ
โค)) |
2 | | zmulcl 9324 |
. . . . . 6
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
3 | 2 | 3adant2 1018 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
4 | | zmulcl 9324 |
. . . . . 6
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
5 | 4 | 3adant1 1017 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
6 | 3, 5 | jca 306 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ ((๐ ยท ๐พ) โ โค โง (๐ ยท ๐พ) โ โค)) |
7 | 6 | 3comr 1213 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ ยท ๐พ) โ โค โง (๐ ยท ๐พ) โ โค)) |
8 | | simpr 110 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ๐ฅ โ
โค) |
9 | | zcn 9276 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
10 | | zcn 9276 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
11 | | zcn 9276 |
. . . . . . . . 9
โข (๐พ โ โค โ ๐พ โ
โ) |
12 | | mulass 7960 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ โ โ โง ๐พ โ โ) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
13 | 9, 10, 11, 12 | syl3an 1291 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โค โง ๐พ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
14 | 13 | 3com13 1210 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
15 | 14 | 3expa 1205 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
16 | 15 | 3adantl3 1157 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
17 | | oveq1 5898 |
. . . . 5
โข ((๐ฅ ยท ๐) = ๐ โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ ยท ๐พ)) |
18 | 16, 17 | sylan9req 2243 |
. . . 4
โข ((((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โง (๐ฅ ยท ๐) = ๐) โ (๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ)) |
19 | 18 | ex 115 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = ๐ โ (๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ))) |
20 | 1, 7, 8, 19 | dvds1lem 11827 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) |
21 | 20 | 3coml 1212 |
1
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) |