Step | Hyp | Ref
| Expression |
1 | | zmulcl 12483 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
2 | 1 | 3adant3 1133 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
3 | | zmulcl 12483 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
4 | 3 | 3adant2 1132 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
5 | 2, 4 | jca 513 |
. . . . 5
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค)) |
6 | 5 | 3coml 1128 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ ((๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค)) |
7 | 6 | 3adant3r 1182 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค)) |
8 | | 3simpa 1149 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ (๐ โ โค โง ๐ โ
โค)) |
9 | | simpr 486 |
. . 3
โข (((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ๐ฅ โ
โค) |
10 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
11 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
12 | 10, 11 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ โ โ โง ๐ โ
โ)) |
13 | | zcn 12438 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
14 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐พ โ โค โ ๐พ โ
โ) |
15 | 14 | anim1i 616 |
. . . . . . . . . . 11
โข ((๐พ โ โค โง ๐พ โ 0) โ (๐พ โ โ โง ๐พ โ 0)) |
16 | | mul12 11254 |
. . . . . . . . . . . . . . . . 17
โข ((๐พ โ โ โง ๐ฅ โ โ โง ๐ โ โ) โ (๐พ ยท (๐ฅ ยท ๐)) = (๐ฅ ยท (๐พ ยท ๐))) |
17 | 16 | 3adant1r 1178 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ โง ๐พ โ 0) โง ๐ฅ โ โ โง ๐ โ โ) โ (๐พ ยท (๐ฅ ยท ๐)) = (๐ฅ ยท (๐พ ยท ๐))) |
18 | 17 | 3expb 1121 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง ๐พ โ 0) โง (๐ฅ โ โ โง ๐ โ โ)) โ (๐พ ยท (๐ฅ ยท ๐)) = (๐ฅ ยท (๐พ ยท ๐))) |
19 | 18 | ancoms 460 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง ๐ โ โ) โง (๐พ โ โ โง ๐พ โ 0)) โ (๐พ ยท (๐ฅ ยท ๐)) = (๐ฅ ยท (๐พ ยท ๐))) |
20 | 19 | 3adant2 1132 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ (๐พ ยท (๐ฅ ยท ๐)) = (๐ฅ ยท (๐พ ยท ๐))) |
21 | 20 | eqeq1d 2740 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐พ ยท (๐ฅ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐))) |
22 | | mulcl 11069 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ ยท ๐) โ โ) |
23 | | mulcan 11726 |
. . . . . . . . . . . . 13
โข (((๐ฅ ยท ๐) โ โ โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐พ ยท (๐ฅ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
24 | 22, 23 | syl3an1 1164 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐พ ยท (๐ฅ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
25 | 21, 24 | bitr3d 281 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
26 | 12, 13, 15, 25 | syl3an 1161 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ โ โค) โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
27 | 26 | 3expb 1121 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ โ โค) โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0))) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
28 | 27 | 3impa 1111 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โค โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0))) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
29 | 28 | 3coml 1128 |
. . . . . . 7
โข ((๐ โ โค โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
30 | 29 | 3expia 1122 |
. . . . . 6
โข ((๐ โ โค โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0))) โ (๐ฅ โ โค โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐))) |
31 | 30 | 3impb 1116 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ (๐ฅ โ โค โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐))) |
32 | 31 | imp 408 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
33 | 32 | biimpd 228 |
. . 3
โข (((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐พ ยท ๐)) = (๐พ ยท ๐) โ (๐ฅ ยท ๐) = ๐)) |
34 | 7, 8, 9, 33 | dvds1lem 16085 |
. 2
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐พ ยท ๐) โฅ (๐พ ยท ๐) โ ๐ โฅ ๐)) |
35 | | dvdscmul 16100 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐พ ยท ๐) โฅ (๐พ ยท ๐))) |
36 | 35 | 3adant3r 1182 |
. 2
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ (๐ โฅ ๐ โ (๐พ ยท ๐) โฅ (๐พ ยท ๐))) |
37 | 34, 36 | impbid 211 |
1
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐พ ยท ๐) โฅ (๐พ ยท ๐) โ ๐ โฅ ๐)) |