Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ๐พ โ โค) |
2 | | simpl2 1193 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ๐ โ โค) |
3 | | simpl3 1194 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ๐ โ โค) |
4 | 2, 3 | zmulcld 12618 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐ ยท ๐) โ โค) |
5 | 1, 4 | gcdcld 16393 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) โ
โ0) |
6 | 1, 2 | gcdcld 16393 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โ
โ0) |
7 | 1, 3 | gcdcld 16393 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โ
โ0) |
8 | 6, 7 | nn0mulcld 12483 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โ
โ0) |
9 | | mulgcddvds 16536 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ gcd (๐ ยท ๐)) โฅ ((๐พ gcd ๐) ยท (๐พ gcd ๐))) |
10 | 9 | adantr 482 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) โฅ ((๐พ gcd ๐) ยท (๐พ gcd ๐))) |
11 | | gcddvds 16388 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค) โ ((๐พ gcd ๐) โฅ ๐พ โง (๐พ gcd ๐) โฅ ๐)) |
12 | 1, 2, 11 | syl2anc 585 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) โฅ ๐พ โง (๐พ gcd ๐) โฅ ๐)) |
13 | 12 | simpld 496 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โฅ ๐พ) |
14 | | gcddvds 16388 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค) โ ((๐พ gcd ๐) โฅ ๐พ โง (๐พ gcd ๐) โฅ ๐)) |
15 | 1, 3, 14 | syl2anc 585 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) โฅ ๐พ โง (๐พ gcd ๐) โฅ ๐)) |
16 | 15 | simpld 496 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โฅ ๐พ) |
17 | 6 | nn0zd 12530 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โ โค) |
18 | 7 | nn0zd 12530 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โ โค) |
19 | 17, 18 | gcdcld 16393 |
. . . . . . . . . 10
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โ
โ0) |
20 | 19 | nn0zd 12530 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โ โค) |
21 | | gcddvds 16388 |
. . . . . . . . . . 11
โข (((๐พ gcd ๐) โ โค โง (๐พ gcd ๐) โ โค) โ (((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐พ gcd ๐) โง ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐พ gcd ๐))) |
22 | 17, 18, 21 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐พ gcd ๐) โง ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐พ gcd ๐))) |
23 | 22 | simpld 496 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐พ gcd ๐)) |
24 | 12 | simprd 497 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โฅ ๐) |
25 | 20, 17, 2, 23, 24 | dvdstrd 16182 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ ๐) |
26 | 22 | simprd 497 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐พ gcd ๐)) |
27 | 15 | simprd 497 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd ๐) โฅ ๐) |
28 | 20, 18, 3, 26, 27 | dvdstrd 16182 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ ๐) |
29 | | dvdsgcd 16430 |
. . . . . . . . 9
โข ((((๐พ gcd ๐) gcd (๐พ gcd ๐)) โ โค โง ๐ โ โค โง ๐ โ โค) โ ((((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ ๐ โง ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ ๐) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐ gcd ๐))) |
30 | 20, 2, 3, 29 | syl3anc 1372 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ ๐ โง ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ ๐) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐ gcd ๐))) |
31 | 25, 28, 30 | mp2and 698 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ (๐ gcd ๐)) |
32 | | simpr 486 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = 1) |
33 | 31, 32 | breqtrd 5132 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ 1) |
34 | | dvds1 16206 |
. . . . . . 7
โข (((๐พ gcd ๐) gcd (๐พ gcd ๐)) โ โ0 โ
(((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ 1 โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) = 1)) |
35 | 19, 34 | syl 17 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (((๐พ gcd ๐) gcd (๐พ gcd ๐)) โฅ 1 โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) = 1)) |
36 | 33, 35 | mpbid 231 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) gcd (๐พ gcd ๐)) = 1) |
37 | | coprmdvds2 16535 |
. . . . 5
โข ((((๐พ gcd ๐) โ โค โง (๐พ gcd ๐) โ โค โง ๐พ โ โค) โง ((๐พ gcd ๐) gcd (๐พ gcd ๐)) = 1) โ (((๐พ gcd ๐) โฅ ๐พ โง (๐พ gcd ๐) โฅ ๐พ) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ๐พ)) |
38 | 17, 18, 1, 36, 37 | syl31anc 1374 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (((๐พ gcd ๐) โฅ ๐พ โง (๐พ gcd ๐) โฅ ๐พ) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ๐พ)) |
39 | 13, 16, 38 | mp2and 698 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ๐พ) |
40 | | dvdscmul 16170 |
. . . . . 6
โข (((๐พ gcd ๐) โ โค โง ๐ โ โค โง (๐พ gcd ๐) โ โค) โ ((๐พ gcd ๐) โฅ ๐ โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ((๐พ gcd ๐) ยท ๐))) |
41 | 18, 3, 17, 40 | syl3anc 1372 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) โฅ ๐ โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ((๐พ gcd ๐) ยท ๐))) |
42 | | dvdsmulc 16171 |
. . . . . 6
โข (((๐พ gcd ๐) โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ gcd ๐) โฅ ๐ โ ((๐พ gcd ๐) ยท ๐) โฅ (๐ ยท ๐))) |
43 | 17, 2, 3, 42 | syl3anc 1372 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) โฅ ๐ โ ((๐พ gcd ๐) ยท ๐) โฅ (๐ ยท ๐))) |
44 | 17, 18 | zmulcld 12618 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โ โค) |
45 | 17, 3 | zmulcld 12618 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) ยท ๐) โ โค) |
46 | | dvdstr 16181 |
. . . . . 6
โข ((((๐พ gcd ๐) ยท (๐พ gcd ๐)) โ โค โง ((๐พ gcd ๐) ยท ๐) โ โค โง (๐ ยท ๐) โ โค) โ ((((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ((๐พ gcd ๐) ยท ๐) โง ((๐พ gcd ๐) ยท ๐) โฅ (๐ ยท ๐)) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐ ยท ๐))) |
47 | 44, 45, 4, 46 | syl3anc 1372 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ((๐พ gcd ๐) ยท ๐) โง ((๐พ gcd ๐) ยท ๐) โฅ (๐ ยท ๐)) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐ ยท ๐))) |
48 | 41, 43, 47 | syl2and 609 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (((๐พ gcd ๐) โฅ ๐ โง (๐พ gcd ๐) โฅ ๐) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐ ยท ๐))) |
49 | 27, 24, 48 | mp2and 698 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐ ยท ๐)) |
50 | | dvdsgcd 16430 |
. . . 4
โข ((((๐พ gcd ๐) ยท (๐พ gcd ๐)) โ โค โง ๐พ โ โค โง (๐ ยท ๐) โ โค) โ ((((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ๐พ โง ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐ ยท ๐)) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐พ gcd (๐ ยท ๐)))) |
51 | 44, 1, 4, 50 | syl3anc 1372 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ ๐พ โง ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐ ยท ๐)) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐พ gcd (๐ ยท ๐)))) |
52 | 39, 49, 51 | mp2and 698 |
. 2
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐พ gcd (๐ ยท ๐))) |
53 | | dvdseq 16201 |
. 2
โข ((((๐พ gcd (๐ ยท ๐)) โ โ0 โง ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โ โ0) โง ((๐พ gcd (๐ ยท ๐)) โฅ ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โง ((๐พ gcd ๐) ยท (๐พ gcd ๐)) โฅ (๐พ gcd (๐ ยท ๐)))) โ (๐พ gcd (๐ ยท ๐)) = ((๐พ gcd ๐) ยท (๐พ gcd ๐))) |
54 | 5, 8, 10, 52, 53 | syl22anc 838 |
1
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) = ((๐พ gcd ๐) ยท (๐พ gcd ๐))) |