Step | Hyp | Ref
| Expression |
1 | | gcdcl 16443 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ
โ0) |
2 | | nn0re 12477 |
. . . . . 6
โข ((๐ gcd ๐) โ โ0 โ (๐ gcd ๐) โ โ) |
3 | | nn0ge0 12493 |
. . . . . 6
โข ((๐ gcd ๐) โ โ0 โ 0 โค
(๐ gcd ๐)) |
4 | 2, 3 | absidd 15365 |
. . . . 5
โข ((๐ gcd ๐) โ โ0 โ
(absโ(๐ gcd ๐)) = (๐ gcd ๐)) |
5 | 1, 4 | syl 17 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ
(absโ(๐ gcd ๐)) = (๐ gcd ๐)) |
6 | 5 | oveq2d 7420 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ๐พ) ยท
(absโ(๐ gcd ๐))) = ((absโ๐พ) ยท (๐ gcd ๐))) |
7 | 6 | 3adant1 1131 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
((absโ๐พ) ยท
(absโ(๐ gcd ๐))) = ((absโ๐พ) ยท (๐ gcd ๐))) |
8 | | zcn 12559 |
. . . 4
โข (๐พ โ โค โ ๐พ โ
โ) |
9 | 1 | nn0cnd 12530 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ โ) |
10 | | absmul 15237 |
. . . 4
โข ((๐พ โ โ โง (๐ gcd ๐) โ โ) โ (absโ(๐พ ยท (๐ gcd ๐))) = ((absโ๐พ) ยท (absโ(๐ gcd ๐)))) |
11 | 8, 9, 10 | syl2an 597 |
. . 3
โข ((๐พ โ โค โง (๐ โ โค โง ๐ โ โค)) โ
(absโ(๐พ ยท
(๐ gcd ๐))) = ((absโ๐พ) ยท (absโ(๐ gcd ๐)))) |
12 | 11 | 3impb 1116 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
(absโ(๐พ ยท
(๐ gcd ๐))) = ((absโ๐พ) ยท (absโ(๐ gcd ๐)))) |
13 | | zcn 12559 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
14 | | zcn 12559 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
15 | | absmul 15237 |
. . . . . . 7
โข ((๐พ โ โ โง ๐ โ โ) โ
(absโ(๐พ ยท
๐)) = ((absโ๐พ) ยท (absโ๐))) |
16 | | absmul 15237 |
. . . . . . 7
โข ((๐พ โ โ โง ๐ โ โ) โ
(absโ(๐พ ยท
๐)) = ((absโ๐พ) ยท (absโ๐))) |
17 | 15, 16 | oveqan12d 7423 |
. . . . . 6
โข (((๐พ โ โ โง ๐ โ โ) โง (๐พ โ โ โง ๐ โ โ)) โ
((absโ(๐พ ยท
๐)) gcd (absโ(๐พ ยท ๐))) = (((absโ๐พ) ยท (absโ๐)) gcd ((absโ๐พ) ยท (absโ๐)))) |
18 | 17 | 3impdi 1351 |
. . . . 5
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ
((absโ(๐พ ยท
๐)) gcd (absโ(๐พ ยท ๐))) = (((absโ๐พ) ยท (absโ๐)) gcd ((absโ๐พ) ยท (absโ๐)))) |
19 | 8, 13, 14, 18 | syl3an 1161 |
. . . 4
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
((absโ(๐พ ยท
๐)) gcd (absโ(๐พ ยท ๐))) = (((absโ๐พ) ยท (absโ๐)) gcd ((absโ๐พ) ยท (absโ๐)))) |
20 | | zmulcl 12607 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
21 | | zmulcl 12607 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โค) |
22 | | gcdabs 16468 |
. . . . . 6
โข (((๐พ ยท ๐) โ โค โง (๐พ ยท ๐) โ โค) โ ((absโ(๐พ ยท ๐)) gcd (absโ(๐พ ยท ๐))) = ((๐พ ยท ๐) gcd (๐พ ยท ๐))) |
23 | 20, 21, 22 | syl2an 597 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค) โง (๐พ โ โค โง ๐ โ โค)) โ
((absโ(๐พ ยท
๐)) gcd (absโ(๐พ ยท ๐))) = ((๐พ ยท ๐) gcd (๐พ ยท ๐))) |
24 | 23 | 3impdi 1351 |
. . . 4
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
((absโ(๐พ ยท
๐)) gcd (absโ(๐พ ยท ๐))) = ((๐พ ยท ๐) gcd (๐พ ยท ๐))) |
25 | | nn0abscl 15255 |
. . . . 5
โข (๐พ โ โค โ
(absโ๐พ) โ
โ0) |
26 | | zabscl 15256 |
. . . . 5
โข (๐ โ โค โ
(absโ๐) โ
โค) |
27 | | zabscl 15256 |
. . . . 5
โข (๐ โ โค โ
(absโ๐) โ
โค) |
28 | | mulgcd 16486 |
. . . . 5
โข
(((absโ๐พ)
โ โ0 โง (absโ๐) โ โค โง (absโ๐) โ โค) โ
(((absโ๐พ) ยท
(absโ๐)) gcd
((absโ๐พ) ยท
(absโ๐))) =
((absโ๐พ) ยท
((absโ๐) gcd
(absโ๐)))) |
29 | 25, 26, 27, 28 | syl3an 1161 |
. . . 4
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
(((absโ๐พ) ยท
(absโ๐)) gcd
((absโ๐พ) ยท
(absโ๐))) =
((absโ๐พ) ยท
((absโ๐) gcd
(absโ๐)))) |
30 | 19, 24, 29 | 3eqtr3d 2781 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) gcd (๐พ ยท ๐)) = ((absโ๐พ) ยท ((absโ๐) gcd (absโ๐)))) |
31 | | gcdabs 16468 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ๐) gcd
(absโ๐)) = (๐ gcd ๐)) |
32 | 31 | 3adant1 1131 |
. . . 4
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
((absโ๐) gcd
(absโ๐)) = (๐ gcd ๐)) |
33 | 32 | oveq2d 7420 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
((absโ๐พ) ยท
((absโ๐) gcd
(absโ๐))) =
((absโ๐พ) ยท
(๐ gcd ๐))) |
34 | 30, 33 | eqtrd 2773 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) gcd (๐พ ยท ๐)) = ((absโ๐พ) ยท (๐ gcd ๐))) |
35 | 7, 12, 34 | 3eqtr4rd 2784 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) gcd (๐พ ยท ๐)) = (absโ(๐พ ยท (๐ gcd ๐)))) |