Step | Hyp | Ref
| Expression |
1 | | 0z 9264 |
. . . 4
โข 0 โ
โค |
2 | | zdceq 9328 |
. . . 4
โข ((๐ โ โค โง 0 โ
โค) โ DECID ๐ = 0) |
3 | 1, 2 | mpan2 425 |
. . 3
โข (๐ โ โค โ
DECID ๐ =
0) |
4 | | exmiddc 836 |
. . 3
โข
(DECID ๐ = 0 โ (๐ = 0 โจ ยฌ ๐ = 0)) |
5 | | nncn 8927 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
6 | | mul01 8346 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ ยท 0) =
0) |
7 | 6 | oveq2d 5891 |
. . . . . . . 8
โข (๐ โ โ โ (๐ gcd (๐ ยท 0)) = (๐ gcd 0)) |
8 | 5, 7 | syl 14 |
. . . . . . 7
โข (๐ โ โ โ (๐ gcd (๐ ยท 0)) = (๐ gcd 0)) |
9 | 8 | adantr 276 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท 0)) = (๐ gcd 0)) |
10 | | nnnn0 9183 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
11 | | nn0gcdid0 11982 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ gcd 0) = ๐) |
12 | 10, 11 | syl 14 |
. . . . . . 7
โข (๐ โ โ โ (๐ gcd 0) = ๐) |
13 | 12 | adantr 276 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โค) โ (๐ gcd 0) = ๐) |
14 | 9, 13 | eqtrd 2210 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท 0)) = ๐) |
15 | | oveq2 5883 |
. . . . . . 7
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0)) |
16 | 15 | oveq2d 5891 |
. . . . . 6
โข (๐ = 0 โ (๐ gcd (๐ ยท ๐)) = (๐ gcd (๐ ยท 0))) |
17 | 16 | eqeq1d 2186 |
. . . . 5
โข (๐ = 0 โ ((๐ gcd (๐ ยท ๐)) = ๐ โ (๐ gcd (๐ ยท 0)) = ๐)) |
18 | 14, 17 | imbitrrid 156 |
. . . 4
โข (๐ = 0 โ ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐)) |
19 | | df-ne 2348 |
. . . . 5
โข (๐ โ 0 โ ยฌ ๐ = 0) |
20 | | zcn 9258 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
21 | | absmul 11078 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ
(absโ(๐ ยท
๐)) = ((absโ๐) ยท (absโ๐))) |
22 | 5, 20, 21 | syl2an 289 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โค) โ
(absโ(๐ ยท
๐)) = ((absโ๐) ยท (absโ๐))) |
23 | | nnre 8926 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
24 | 10 | nn0ge0d 9232 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 0 โค
๐) |
25 | 23, 24 | absidd 11176 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
(absโ๐) = ๐) |
26 | 25 | oveq1d 5890 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((absโ๐) ยท
(absโ๐)) = (๐ ยท (absโ๐))) |
27 | 26 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โค) โ
((absโ๐) ยท
(absโ๐)) = (๐ ยท (absโ๐))) |
28 | 22, 27 | eqtrd 2210 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โค) โ
(absโ(๐ ยท
๐)) = (๐ ยท (absโ๐))) |
29 | 28 | oveq2d 5891 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (absโ(๐ ยท ๐))) = (๐ gcd (๐ ยท (absโ๐)))) |
30 | 29 | adantr 276 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ (๐ gcd (absโ(๐ ยท ๐))) = (๐ gcd (๐ ยท (absโ๐)))) |
31 | | simpll 527 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ ๐ โ
โ) |
32 | 31 | nnzd 9374 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ ๐ โ
โค) |
33 | | nnz 9272 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
34 | | zmulcl 9306 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
35 | 33, 34 | sylan 283 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
36 | 35 | adantr 276 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ (๐ ยท ๐) โ โค) |
37 | | gcdabs2 11991 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ ยท ๐) โ โค) โ (๐ gcd (absโ(๐ ยท ๐))) = (๐ gcd (๐ ยท ๐))) |
38 | 32, 36, 37 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ (๐ gcd (absโ(๐ ยท ๐))) = (๐ gcd (๐ ยท ๐))) |
39 | | nnabscl 11109 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ
โ) |
40 | | gcdmultiple 12021 |
. . . . . . . . 9
โข ((๐ โ โ โง
(absโ๐) โ
โ) โ (๐ gcd
(๐ ยท
(absโ๐))) = ๐) |
41 | 39, 40 | sylan2 286 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ โค โง ๐ โ 0)) โ (๐ gcd (๐ ยท (absโ๐))) = ๐) |
42 | 41 | anassrs 400 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ (๐ gcd (๐ ยท (absโ๐))) = ๐) |
43 | 30, 38, 42 | 3eqtr3d 2218 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โค) โง ๐ โ 0) โ (๐ gcd (๐ ยท ๐)) = ๐) |
44 | 43 | expcom 116 |
. . . . 5
โข (๐ โ 0 โ ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐)) |
45 | 19, 44 | sylbir 135 |
. . . 4
โข (ยฌ
๐ = 0 โ ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐)) |
46 | 18, 45 | jaoi 716 |
. . 3
โข ((๐ = 0 โจ ยฌ ๐ = 0) โ ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐)) |
47 | 3, 4, 46 | 3syl 17 |
. 2
โข (๐ โ โค โ ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐)) |
48 | 47 | anabsi7 581 |
1
โข ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐) |