Step | Hyp | Ref
| Expression |
1 | | 3simpa 994 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โ โค โง ๐ โ
โค)) |
2 | | 3simpb 995 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โ โค โง ๐ โ
โค)) |
3 | | zsubcl 9296 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ ๐) โ โค) |
4 | 3 | anim2i 342 |
. . 3
โข ((๐พ โ โค โง (๐ โ โค โง ๐ โ โค)) โ (๐พ โ โค โง (๐ โ ๐) โ โค)) |
5 | 4 | 3impb 1199 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โ โค โง (๐ โ ๐) โ โค)) |
6 | | zsubcl 9296 |
. . 3
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ โ ๐ฆ) โ โค) |
7 | 6 | adantl 277 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ โ ๐ฆ) โ โค) |
8 | | zcn 9260 |
. . . . . . . 8
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
9 | | zcn 9260 |
. . . . . . . 8
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
10 | | zcn 9260 |
. . . . . . . 8
โข (๐พ โ โค โ ๐พ โ
โ) |
11 | | subdir 8345 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐พ โ โ) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) โ (๐ฆ ยท ๐พ))) |
12 | 8, 9, 10, 11 | syl3an 1280 |
. . . . . . 7
โข ((๐ฅ โ โค โง ๐ฆ โ โค โง ๐พ โ โค) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) โ (๐ฆ ยท ๐พ))) |
13 | 12 | 3comr 1211 |
. . . . . 6
โข ((๐พ โ โค โง ๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) โ (๐ฆ ยท ๐พ))) |
14 | 13 | 3expb 1204 |
. . . . 5
โข ((๐พ โ โค โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = ((๐ฅ ยท ๐พ) โ (๐ฆ ยท ๐พ))) |
15 | | oveq12 5886 |
. . . . 5
โข (((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ฅ ยท ๐พ) โ (๐ฆ ยท ๐พ)) = (๐ โ ๐)) |
16 | 14, 15 | sylan9eq 2230 |
. . . 4
โข (((๐พ โ โค โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐)) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = (๐ โ ๐)) |
17 | 16 | ex 115 |
. . 3
โข ((๐พ โ โค โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = (๐ โ ๐))) |
18 | 17 | 3ad2antl1 1159 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ
(((๐ฅ ยท ๐พ) = ๐ โง (๐ฆ ยท ๐พ) = ๐) โ ((๐ฅ โ ๐ฆ) ยท ๐พ) = (๐ โ ๐))) |
19 | 1, 2, 5, 7, 18 | dvds2lem 11812 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ โ ๐))) |