Step | Hyp | Ref
| Expression |
1 | | bezoutr 16451 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐) + (๐ต ยท ๐))) |
2 | 1 | adantr 482 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐) + (๐ต ยท ๐))) |
3 | | simpr 486 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) |
4 | 2, 3 | breqtrd 5136 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด gcd ๐ต) โฅ 1) |
5 | | gcdcl 16393 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โ
โ0) |
6 | 5 | nn0zd 12532 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด gcd ๐ต) โ โค) |
7 | 6 | ad2antrr 725 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด gcd ๐ต) โ โค) |
8 | | 1nn 12171 |
. . . . . 6
โข 1 โ
โ |
9 | 8 | a1i 11 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ 1 โ
โ) |
10 | | dvdsle 16199 |
. . . . 5
โข (((๐ด gcd ๐ต) โ โค โง 1 โ โ)
โ ((๐ด gcd ๐ต) โฅ 1 โ (๐ด gcd ๐ต) โค 1)) |
11 | 7, 9, 10 | syl2anc 585 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ ((๐ด gcd ๐ต) โฅ 1 โ (๐ด gcd ๐ต) โค 1)) |
12 | 4, 11 | mpd 15 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด gcd ๐ต) โค 1) |
13 | | simpll 766 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด โ โค โง ๐ต โ โค)) |
14 | | oveq1 7369 |
. . . . . . . . . . . . 13
โข (๐ด = 0 โ (๐ด ยท ๐) = (0 ยท ๐)) |
15 | | oveq1 7369 |
. . . . . . . . . . . . 13
โข (๐ต = 0 โ (๐ต ยท ๐) = (0 ยท ๐)) |
16 | 14, 15 | oveqan12d 7381 |
. . . . . . . . . . . 12
โข ((๐ด = 0 โง ๐ต = 0) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) = ((0 ยท ๐) + (0 ยท ๐))) |
17 | | zcn 12511 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
18 | 17 | mul02d 11360 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (0
ยท ๐) =
0) |
19 | | zcn 12511 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
20 | 19 | mul02d 11360 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (0
ยท ๐) =
0) |
21 | 18, 20 | oveqan12d 7381 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ ((0
ยท ๐) + (0 ยท
๐)) = (0 +
0)) |
22 | 16, 21 | sylan9eqr 2799 |
. . . . . . . . . . 11
โข (((๐ โ โค โง ๐ โ โค) โง (๐ด = 0 โง ๐ต = 0)) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) = (0 + 0)) |
23 | | 00id 11337 |
. . . . . . . . . . 11
โข (0 + 0) =
0 |
24 | 22, 23 | eqtrdi 2793 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค) โง (๐ด = 0 โง ๐ต = 0)) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) = 0) |
25 | 24 | adantll 713 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = 0 โง ๐ต = 0)) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) = 0) |
26 | | 0ne1 12231 |
. . . . . . . . . 10
โข 0 โ
1 |
27 | 26 | a1i 11 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = 0 โง ๐ต = 0)) โ 0 โ 1) |
28 | 25, 27 | eqnetrd 3012 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง (๐ด = 0 โง ๐ต = 0)) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) โ 1) |
29 | 28 | ex 414 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ด = 0 โง ๐ต = 0) โ ((๐ด ยท ๐) + (๐ต ยท ๐)) โ 1)) |
30 | 29 | necon2bd 2960 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โ
(((๐ด ยท ๐) + (๐ต ยท ๐)) = 1 โ ยฌ (๐ด = 0 โง ๐ต = 0))) |
31 | 30 | imp 408 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
32 | | gcdn0cl 16389 |
. . . . 5
โข (((๐ด โ โค โง ๐ต โ โค) โง ยฌ
(๐ด = 0 โง ๐ต = 0)) โ (๐ด gcd ๐ต) โ โ) |
33 | 13, 31, 32 | syl2anc 585 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด gcd ๐ต) โ โ) |
34 | | nnle1eq1 12190 |
. . . 4
โข ((๐ด gcd ๐ต) โ โ โ ((๐ด gcd ๐ต) โค 1 โ (๐ด gcd ๐ต) = 1)) |
35 | 33, 34 | syl 17 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ ((๐ด gcd ๐ต) โค 1 โ (๐ด gcd ๐ต) = 1)) |
36 | 12, 35 | mpbid 231 |
. 2
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = 1) โ (๐ด gcd ๐ต) = 1) |
37 | 36 | ex 414 |
1
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โ
(((๐ด ยท ๐) + (๐ต ยท ๐)) = 1 โ (๐ด gcd ๐ต) = 1)) |