Step | Hyp | Ref
| Expression |
1 | | 3simpc 997 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ โ โค โง ๐ โ
โค)) |
2 | | zmulcl 9319 |
. . . . . 6
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
3 | 2 | 3adant2 1017 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
4 | | zmulcl 9319 |
. . . . . 6
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
5 | 4 | 3adant1 1016 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
6 | 3, 5 | jca 306 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ ((๐ ยท ๐พ) โ โค โง (๐ ยท ๐พ) โ โค)) |
7 | 6 | 3comr 1212 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ ยท ๐พ) โ โค โง (๐ ยท ๐พ) โ โค)) |
8 | | simpr 110 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ๐ฅ โ
โค) |
9 | | zcn 9271 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
10 | | zcn 9271 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
11 | | zcn 9271 |
. . . . . . . . 9
โข (๐พ โ โค โ ๐พ โ
โ) |
12 | | mulass 7955 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ โ โ โง ๐พ โ โ) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
13 | 9, 10, 11, 12 | syl3an 1290 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โค โง ๐พ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
14 | 13 | 3com13 1209 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
15 | 14 | 3expa 1204 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
16 | 15 | 3adantl3 1156 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
17 | | oveq1 5895 |
. . . . 5
โข ((๐ฅ ยท ๐) = ๐ โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ ยท ๐พ)) |
18 | 16, 17 | sylan9req 2241 |
. . . 4
โข ((((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โง (๐ฅ ยท ๐) = ๐) โ (๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ)) |
19 | 18 | ex 115 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = ๐ โ (๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ))) |
20 | 1, 7, 8, 19 | dvds1lem 11822 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) |
21 | 20 | 3coml 1211 |
1
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) |