Step | Hyp | Ref
| Expression |
1 | | gcdmultiple 16422 |
. . . . . 6
โข ((๐พ โ โ โง ๐ โ โ) โ (๐พ gcd (๐พ ยท ๐)) = ๐พ) |
2 | 1 | 3adant2 1132 |
. . . . 5
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐พ gcd (๐พ ยท ๐)) = ๐พ) |
3 | 2 | oveq1d 7373 |
. . . 4
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐พ gcd (๐พ ยท ๐)) gcd (๐ ยท ๐)) = (๐พ gcd (๐ ยท ๐))) |
4 | | nnz 12525 |
. . . . . 6
โข (๐พ โ โ โ ๐พ โ
โค) |
5 | 4 | 3ad2ant1 1134 |
. . . . 5
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐พ โ
โค) |
6 | | nnz 12525 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
7 | | zmulcl 12557 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
8 | 4, 6, 7 | syl2an 597 |
. . . . . 6
โข ((๐พ โ โ โง ๐ โ โ) โ (๐พ ยท ๐) โ โค) |
9 | 8 | 3adant2 1132 |
. . . . 5
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐พ ยท ๐) โ โค) |
10 | | nnz 12525 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โค) |
11 | | zmulcl 12557 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
12 | 10, 6, 11 | syl2an 597 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โค) |
13 | 12 | 3adant1 1131 |
. . . . 5
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โค) |
14 | | gcdass 16433 |
. . . . 5
โข ((๐พ โ โค โง (๐พ ยท ๐) โ โค โง (๐ ยท ๐) โ โค) โ ((๐พ gcd (๐พ ยท ๐)) gcd (๐ ยท ๐)) = (๐พ gcd ((๐พ ยท ๐) gcd (๐ ยท ๐)))) |
15 | 5, 9, 13, 14 | syl3anc 1372 |
. . . 4
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐พ gcd (๐พ ยท ๐)) gcd (๐ ยท ๐)) = (๐พ gcd ((๐พ ยท ๐) gcd (๐ ยท ๐)))) |
16 | 3, 15 | eqtr3d 2775 |
. . 3
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐พ gcd (๐ ยท ๐)) = (๐พ gcd ((๐พ ยท ๐) gcd (๐ ยท ๐)))) |
17 | 16 | adantr 482 |
. 2
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) = (๐พ gcd ((๐พ ยท ๐) gcd (๐ ยท ๐)))) |
18 | | nnnn0 12425 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ0) |
19 | | mulgcdr 16436 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ0)
โ ((๐พ ยท ๐) gcd (๐ ยท ๐)) = ((๐พ gcd ๐) ยท ๐)) |
20 | 4, 10, 18, 19 | syl3an 1161 |
. . . . 5
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐พ ยท ๐) gcd (๐ ยท ๐)) = ((๐พ gcd ๐) ยท ๐)) |
21 | | oveq1 7365 |
. . . . 5
โข ((๐พ gcd ๐) = 1 โ ((๐พ gcd ๐) ยท ๐) = (1 ยท ๐)) |
22 | 20, 21 | sylan9eq 2793 |
. . . 4
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ ((๐พ ยท ๐) gcd (๐ ยท ๐)) = (1 ยท ๐)) |
23 | | nncn 12166 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
24 | 23 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
25 | 24 | adantr 482 |
. . . . 5
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ ๐ โ โ) |
26 | 25 | mulid2d 11178 |
. . . 4
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ (1 ยท ๐) = ๐) |
27 | 22, 26 | eqtrd 2773 |
. . 3
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ ((๐พ ยท ๐) gcd (๐ ยท ๐)) = ๐) |
28 | 27 | oveq2d 7374 |
. 2
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ (๐พ gcd ((๐พ ยท ๐) gcd (๐ ยท ๐))) = (๐พ gcd ๐)) |
29 | 17, 28 | eqtrd 2773 |
1
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) = (๐พ gcd ๐)) |