Step | Hyp | Ref
| Expression |
1 | | zmulcl 12483 |
. . . . . 6
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
2 | 1 | 3adant2 1132 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
3 | | zmulcl 12483 |
. . . . . 6
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
4 | 3 | 3adant1 1131 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ ยท ๐พ) โ โค) |
5 | 2, 4 | jca 513 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ ((๐ ยท ๐พ) โ โค โง (๐ ยท ๐พ) โ โค)) |
6 | 5 | 3adant3r 1182 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ ยท ๐พ) โ โค โง (๐ ยท ๐พ) โ โค)) |
7 | | 3simpa 1149 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ (๐ โ โค โง ๐ โ
โค)) |
8 | | simpr 486 |
. . 3
โข (((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ๐ฅ โ
โค) |
9 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
10 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
11 | 9, 10 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ โ โ โง ๐ โ
โ)) |
12 | | zcn 12438 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
13 | | zcn 12438 |
. . . . . . . . . . . 12
โข (๐พ โ โค โ ๐พ โ
โ) |
14 | 13 | anim1i 616 |
. . . . . . . . . . 11
โข ((๐พ โ โค โง ๐พ โ 0) โ (๐พ โ โ โง ๐พ โ 0)) |
15 | | mulass 11073 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โ โง ๐ โ โ โง ๐พ โ โ) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
16 | 15 | 3expa 1119 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐พ โ โ) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
17 | 16 | adantrr 716 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง ๐ โ โ) โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
18 | 17 | 3adant2 1132 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐ฅ ยท ๐) ยท ๐พ) = (๐ฅ ยท (๐ ยท ๐พ))) |
19 | 18 | eqeq1d 2740 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ (((๐ฅ ยท ๐) ยท ๐พ) = (๐ ยท ๐พ) โ (๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ))) |
20 | | mulcl 11069 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ ยท ๐) โ โ) |
21 | | mulcan2 11727 |
. . . . . . . . . . . . 13
โข (((๐ฅ ยท ๐) โ โ โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ (((๐ฅ ยท ๐) ยท ๐พ) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
22 | 20, 21 | syl3an1 1164 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ (((๐ฅ ยท ๐) ยท ๐พ) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
23 | 19, 22 | bitr3d 281 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ โง (๐พ โ โ โง ๐พ โ 0)) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
24 | 11, 12, 14, 23 | syl3an 1161 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ โ โค) โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
25 | 24 | 3expb 1121 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ โ โค) โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0))) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
26 | 25 | 3impa 1111 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ โ โค โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0))) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
27 | 26 | 3coml 1128 |
. . . . . . 7
โข ((๐ โ โค โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
28 | 27 | 3expia 1122 |
. . . . . 6
โข ((๐ โ โค โง (๐ โ โค โง (๐พ โ โค โง ๐พ โ 0))) โ (๐ฅ โ โค โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐))) |
29 | 28 | 3impb 1116 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ (๐ฅ โ โค โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐))) |
30 | 29 | imp 408 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
31 | 30 | biimpd 228 |
. . 3
โข (((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โง ๐ฅ โ โค) โ ((๐ฅ ยท (๐ ยท ๐พ)) = (๐ ยท ๐พ) โ (๐ฅ ยท ๐) = ๐)) |
32 | 6, 7, 8, 31 | dvds1lem 16085 |
. 2
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ ยท ๐พ) โฅ (๐ ยท ๐พ) โ ๐ โฅ ๐)) |
33 | | dvdsmulc 16101 |
. . 3
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) |
34 | 33 | 3adant3r 1182 |
. 2
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) |
35 | 32, 34 | impbid 211 |
1
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ ยท ๐พ) โฅ (๐ ยท ๐พ) โ ๐ โฅ ๐)) |