Step | Hyp | Ref
| Expression |
1 | | divides 16143 |
. . . . 5
โข ((๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ โ๐ฅ โ โค (๐ฅ ยท ๐) = ๐พ)) |
2 | 1 | 3adant1 1131 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐พ โ โ๐ฅ โ โค (๐ฅ ยท ๐) = ๐พ)) |
3 | 2 | adantr 482 |
. . 3
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง (๐ gcd ๐) = 1) โ (๐ โฅ ๐พ โ โ๐ฅ โ โค (๐ฅ ยท ๐) = ๐พ)) |
4 | | simprr 772 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ ๐ฅ โ โค) |
5 | | simpl2 1193 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ ๐ โ โค) |
6 | | zcn 12509 |
. . . . . . . . . . 11
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
7 | | zcn 12509 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
8 | | mulcom 11142 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
9 | 6, 7, 8 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
10 | 4, 5, 9 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
11 | 10 | breq2d 5118 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐) โ ๐ โฅ (๐ ยท ๐ฅ))) |
12 | | simprl 770 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ gcd ๐) = 1) |
13 | | simpl1 1192 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ ๐ โ โค) |
14 | | coprmdvds 16534 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ ((๐ โฅ (๐ ยท ๐ฅ) โง (๐ gcd ๐) = 1) โ ๐ โฅ ๐ฅ)) |
15 | 13, 5, 4, 14 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ ((๐ โฅ (๐ ยท ๐ฅ) โง (๐ gcd ๐) = 1) โ ๐ โฅ ๐ฅ)) |
16 | 12, 15 | mpan2d 693 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ โฅ (๐ ยท ๐ฅ) โ ๐ โฅ ๐ฅ)) |
17 | 11, 16 | sylbid 239 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐) โ ๐ โฅ ๐ฅ)) |
18 | | dvdsmulc 16171 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ฅ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ฅ โ (๐ ยท ๐) โฅ (๐ฅ ยท ๐))) |
19 | 13, 4, 5, 18 | syl3anc 1372 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ โฅ ๐ฅ โ (๐ ยท ๐) โฅ (๐ฅ ยท ๐))) |
20 | 17, 19 | syld 47 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐) โ (๐ ยท ๐) โฅ (๐ฅ ยท ๐))) |
21 | | breq2 5110 |
. . . . . . 7
โข ((๐ฅ ยท ๐) = ๐พ โ (๐ โฅ (๐ฅ ยท ๐) โ ๐ โฅ ๐พ)) |
22 | | breq2 5110 |
. . . . . . 7
โข ((๐ฅ ยท ๐) = ๐พ โ ((๐ ยท ๐) โฅ (๐ฅ ยท ๐) โ (๐ ยท ๐) โฅ ๐พ)) |
23 | 21, 22 | imbi12d 345 |
. . . . . 6
โข ((๐ฅ ยท ๐) = ๐พ โ ((๐ โฅ (๐ฅ ยท ๐) โ (๐ ยท ๐) โฅ (๐ฅ ยท ๐)) โ (๐ โฅ ๐พ โ (๐ ยท ๐) โฅ ๐พ))) |
24 | 20, 23 | syl5ibcom 244 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง ((๐ gcd ๐) = 1 โง ๐ฅ โ โค)) โ ((๐ฅ ยท ๐) = ๐พ โ (๐ โฅ ๐พ โ (๐ ยท ๐) โฅ ๐พ))) |
25 | 24 | anassrs 469 |
. . . 4
โข ((((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง (๐ gcd ๐) = 1) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = ๐พ โ (๐ โฅ ๐พ โ (๐ ยท ๐) โฅ ๐พ))) |
26 | 25 | rexlimdva 3149 |
. . 3
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง (๐ gcd ๐) = 1) โ (โ๐ฅ โ โค (๐ฅ ยท ๐) = ๐พ โ (๐ โฅ ๐พ โ (๐ ยท ๐) โฅ ๐พ))) |
27 | 3, 26 | sylbid 239 |
. 2
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง (๐ gcd ๐) = 1) โ (๐ โฅ ๐พ โ (๐ โฅ ๐พ โ (๐ ยท ๐) โฅ ๐พ))) |
28 | 27 | impcomd 413 |
1
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง (๐ gcd ๐) = 1) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ ยท ๐) โฅ ๐พ)) |