Step | Hyp | Ref
| Expression |
1 | | bezout.3 |
. . . . . . . 8
โข (๐ โ ๐ด โ โค) |
2 | | bezout.4 |
. . . . . . . 8
โข (๐ โ ๐ต โ โค) |
3 | | gcddvds 16390 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค) โ ((๐ด gcd ๐ต) โฅ ๐ด โง (๐ด gcd ๐ต) โฅ ๐ต)) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ด gcd ๐ต) โฅ ๐ด โง (๐ด gcd ๐ต) โฅ ๐ต)) |
5 | 4 | simpld 496 |
. . . . . 6
โข (๐ โ (๐ด gcd ๐ต) โฅ ๐ด) |
6 | 1, 2 | gcdcld 16395 |
. . . . . . . 8
โข (๐ โ (๐ด gcd ๐ต) โ
โ0) |
7 | 6 | nn0zd 12532 |
. . . . . . 7
โข (๐ โ (๐ด gcd ๐ต) โ โค) |
8 | | divides 16145 |
. . . . . . 7
โข (((๐ด gcd ๐ต) โ โค โง ๐ด โ โค) โ ((๐ด gcd ๐ต) โฅ ๐ด โ โ๐ โ โค (๐ ยท (๐ด gcd ๐ต)) = ๐ด)) |
9 | 7, 1, 8 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ด gcd ๐ต) โฅ ๐ด โ โ๐ โ โค (๐ ยท (๐ด gcd ๐ต)) = ๐ด)) |
10 | 5, 9 | mpbid 231 |
. . . . 5
โข (๐ โ โ๐ โ โค (๐ ยท (๐ด gcd ๐ต)) = ๐ด) |
11 | 4 | simprd 497 |
. . . . . 6
โข (๐ โ (๐ด gcd ๐ต) โฅ ๐ต) |
12 | | divides 16145 |
. . . . . . 7
โข (((๐ด gcd ๐ต) โ โค โง ๐ต โ โค) โ ((๐ด gcd ๐ต) โฅ ๐ต โ โ๐ก โ โค (๐ก ยท (๐ด gcd ๐ต)) = ๐ต)) |
13 | 7, 2, 12 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ด gcd ๐ต) โฅ ๐ต โ โ๐ก โ โค (๐ก ยท (๐ด gcd ๐ต)) = ๐ต)) |
14 | 11, 13 | mpbid 231 |
. . . . 5
โข (๐ โ โ๐ก โ โค (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) |
15 | | reeanv 3220 |
. . . . . 6
โข
(โ๐ โ
โค โ๐ก โ
โค ((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (โ๐ โ โค (๐ ยท (๐ด gcd ๐ต)) = ๐ด โง โ๐ก โ โค (๐ก ยท (๐ด gcd ๐ต)) = ๐ต)) |
16 | | bezout.1 |
. . . . . . . . . . 11
โข ๐ = {๐ง โ โ โฃ โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))} |
17 | | bezout.2 |
. . . . . . . . . . 11
โข ๐บ = inf(๐, โ, < ) |
18 | | bezout.5 |
. . . . . . . . . . 11
โข (๐ โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
19 | 16, 1, 2, 17, 18 | bezoutlem2 16428 |
. . . . . . . . . 10
โข (๐ โ ๐บ โ ๐) |
20 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ข โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ข)) |
21 | 20 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ข โ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฆ))) |
22 | 21 | eqeq2d 2748 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ข โ (๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ๐ง = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฆ)))) |
23 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = ๐ฃ โ (๐ต ยท ๐ฆ) = (๐ต ยท ๐ฃ)) |
24 | 23 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ฃ โ ((๐ด ยท ๐ข) + (๐ต ยท ๐ฆ)) = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ))) |
25 | 24 | eqeq2d 2748 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ฃ โ (๐ง = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฆ)) โ ๐ง = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
26 | 22, 25 | cbvrex2vw 3231 |
. . . . . . . . . . . 12
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ข โ โค โ๐ฃ โ โค ๐ง = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ))) |
27 | | eqeq1 2741 |
. . . . . . . . . . . . 13
โข (๐ง = ๐บ โ (๐ง = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
28 | 27 | 2rexbidv 3214 |
. . . . . . . . . . . 12
โข (๐ง = ๐บ โ (โ๐ข โ โค โ๐ฃ โ โค ๐ง = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ โ๐ข โ โค โ๐ฃ โ โค ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
29 | 26, 28 | bitrid 283 |
. . . . . . . . . . 11
โข (๐ง = ๐บ โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ข โ โค โ๐ฃ โ โค ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
30 | 29, 16 | elrab2 3653 |
. . . . . . . . . 10
โข (๐บ โ ๐ โ (๐บ โ โ โง โ๐ข โ โค โ๐ฃ โ โค ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
31 | 19, 30 | sylib 217 |
. . . . . . . . 9
โข (๐ โ (๐บ โ โ โง โ๐ข โ โค โ๐ฃ โ โค ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
32 | 31 | simprd 497 |
. . . . . . . 8
โข (๐ โ โ๐ข โ โค โ๐ฃ โ โค ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ))) |
33 | | simprrl 780 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ โ โค) |
34 | | simprll 778 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ข โ โค) |
35 | 33, 34 | zmulcld 12620 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ ยท ๐ข) โ โค) |
36 | | simprrr 781 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ก โ โค) |
37 | | simprlr 779 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ฃ โ โค) |
38 | 36, 37 | zmulcld 12620 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ก ยท ๐ฃ) โ โค) |
39 | 35, 38 | zaddcld 12618 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ((๐ ยท ๐ข) + (๐ก ยท ๐ฃ)) โ โค) |
40 | 7 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ด gcd ๐ต) โ โค) |
41 | | dvdsmul2 16168 |
. . . . . . . . . . . . . . 15
โข ((((๐ ยท ๐ข) + (๐ก ยท ๐ฃ)) โ โค โง (๐ด gcd ๐ต) โ โค) โ (๐ด gcd ๐ต) โฅ (((๐ ยท ๐ข) + (๐ก ยท ๐ฃ)) ยท (๐ด gcd ๐ต))) |
42 | 39, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ด gcd ๐ต) โฅ (((๐ ยท ๐ข) + (๐ก ยท ๐ฃ)) ยท (๐ด gcd ๐ต))) |
43 | 35 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ ยท ๐ข) โ โ) |
44 | 40 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ด gcd ๐ต) โ โ) |
45 | 38 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ก ยท ๐ฃ) โ โ) |
46 | 33 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ โ โ) |
47 | 34 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ข โ โ) |
48 | 46, 47, 44 | mul32d 11372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ((๐ ยท ๐ข) ยท (๐ด gcd ๐ต)) = ((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข)) |
49 | 36 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ก โ โ) |
50 | 37 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ๐ฃ โ โ) |
51 | 49, 50, 44 | mul32d 11372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ ((๐ก ยท ๐ฃ) ยท (๐ด gcd ๐ต)) = ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ)) |
52 | 48, 51 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (((๐ ยท ๐ข) ยท (๐ด gcd ๐ต)) + ((๐ก ยท ๐ฃ) ยท (๐ด gcd ๐ต))) = (((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข) + ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ))) |
53 | 43, 44, 45, 52 | joinlmuladdmuld 11189 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (((๐ ยท ๐ข) + (๐ก ยท ๐ฃ)) ยท (๐ด gcd ๐ต)) = (((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข) + ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ))) |
54 | 42, 53 | breqtrd 5136 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐ด gcd ๐ต) โฅ (((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข) + ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ))) |
55 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
โข ((๐ ยท (๐ด gcd ๐ต)) = ๐ด โ ((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข) = (๐ด ยท ๐ข)) |
56 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
โข ((๐ก ยท (๐ด gcd ๐ต)) = ๐ต โ ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ) = (๐ต ยท ๐ฃ)) |
57 | 55, 56 | oveqan12d 7381 |
. . . . . . . . . . . . . 14
โข (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข) + ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ)) = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ))) |
58 | 57 | breq2d 5122 |
. . . . . . . . . . . . 13
โข (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ ((๐ด gcd ๐ต) โฅ (((๐ ยท (๐ด gcd ๐ต)) ยท ๐ข) + ((๐ก ยท (๐ด gcd ๐ต)) ยท ๐ฃ)) โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
59 | 54, 58 | syl5ibcom 244 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
60 | | breq2 5114 |
. . . . . . . . . . . . 13
โข (๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ ((๐ด gcd ๐ต) โฅ ๐บ โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)))) |
61 | 60 | imbi2d 341 |
. . . . . . . . . . . 12
โข (๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ ((((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ))))) |
62 | 59, 61 | syl5ibrcom 247 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ข โ โค โง ๐ฃ โ โค) โง (๐ โ โค โง ๐ก โ โค))) โ (๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ))) |
63 | 62 | expr 458 |
. . . . . . . . . 10
โข ((๐ โง (๐ข โ โค โง ๐ฃ โ โค)) โ ((๐ โ โค โง ๐ก โ โค) โ (๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ)))) |
64 | 63 | com23 86 |
. . . . . . . . 9
โข ((๐ โง (๐ข โ โค โง ๐ฃ โ โค)) โ (๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ ((๐ โ โค โง ๐ก โ โค) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ)))) |
65 | 64 | rexlimdvva 3206 |
. . . . . . . 8
โข (๐ โ (โ๐ข โ โค โ๐ฃ โ โค ๐บ = ((๐ด ยท ๐ข) + (๐ต ยท ๐ฃ)) โ ((๐ โ โค โง ๐ก โ โค) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ)))) |
66 | 32, 65 | mpd 15 |
. . . . . . 7
โข (๐ โ ((๐ โ โค โง ๐ก โ โค) โ (((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ))) |
67 | 66 | rexlimdvv 3205 |
. . . . . 6
โข (๐ โ (โ๐ โ โค โ๐ก โ โค ((๐ ยท (๐ด gcd ๐ต)) = ๐ด โง (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ)) |
68 | 15, 67 | biimtrrid 242 |
. . . . 5
โข (๐ โ ((โ๐ โ โค (๐ ยท (๐ด gcd ๐ต)) = ๐ด โง โ๐ก โ โค (๐ก ยท (๐ด gcd ๐ต)) = ๐ต) โ (๐ด gcd ๐ต) โฅ ๐บ)) |
69 | 10, 14, 68 | mp2and 698 |
. . . 4
โข (๐ โ (๐ด gcd ๐ต) โฅ ๐บ) |
70 | 31 | simpld 496 |
. . . . 5
โข (๐ โ ๐บ โ โ) |
71 | | dvdsle 16199 |
. . . . 5
โข (((๐ด gcd ๐ต) โ โค โง ๐บ โ โ) โ ((๐ด gcd ๐ต) โฅ ๐บ โ (๐ด gcd ๐ต) โค ๐บ)) |
72 | 7, 70, 71 | syl2anc 585 |
. . . 4
โข (๐ โ ((๐ด gcd ๐ต) โฅ ๐บ โ (๐ด gcd ๐ต) โค ๐บ)) |
73 | 69, 72 | mpd 15 |
. . 3
โข (๐ โ (๐ด gcd ๐ต) โค ๐บ) |
74 | | breq2 5114 |
. . . . 5
โข (๐ด = 0 โ (๐บ โฅ ๐ด โ ๐บ โฅ 0)) |
75 | 16, 1, 2 | bezoutlem1 16427 |
. . . . . . . 8
โข (๐ โ (๐ด โ 0 โ (absโ๐ด) โ ๐)) |
76 | 16, 1, 2, 17, 18 | bezoutlem3 16429 |
. . . . . . . 8
โข (๐ โ ((absโ๐ด) โ ๐ โ ๐บ โฅ (absโ๐ด))) |
77 | 75, 76 | syld 47 |
. . . . . . 7
โข (๐ โ (๐ด โ 0 โ ๐บ โฅ (absโ๐ด))) |
78 | 70 | nnzd 12533 |
. . . . . . . 8
โข (๐ โ ๐บ โ โค) |
79 | | dvdsabsb 16165 |
. . . . . . . 8
โข ((๐บ โ โค โง ๐ด โ โค) โ (๐บ โฅ ๐ด โ ๐บ โฅ (absโ๐ด))) |
80 | 78, 1, 79 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐บ โฅ ๐ด โ ๐บ โฅ (absโ๐ด))) |
81 | 77, 80 | sylibrd 259 |
. . . . . 6
โข (๐ โ (๐ด โ 0 โ ๐บ โฅ ๐ด)) |
82 | 81 | imp 408 |
. . . . 5
โข ((๐ โง ๐ด โ 0) โ ๐บ โฅ ๐ด) |
83 | | dvds0 16161 |
. . . . . 6
โข (๐บ โ โค โ ๐บ โฅ 0) |
84 | 78, 83 | syl 17 |
. . . . 5
โข (๐ โ ๐บ โฅ 0) |
85 | 74, 82, 84 | pm2.61ne 3031 |
. . . 4
โข (๐ โ ๐บ โฅ ๐ด) |
86 | | breq2 5114 |
. . . . 5
โข (๐ต = 0 โ (๐บ โฅ ๐ต โ ๐บ โฅ 0)) |
87 | | eqid 2737 |
. . . . . . . . . 10
โข {๐ง โ โ โฃ
โ๐ฆ โ โค
โ๐ฅ โ โค
๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))} = {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))} |
88 | 87, 2, 1 | bezoutlem1 16427 |
. . . . . . . . 9
โข (๐ โ (๐ต โ 0 โ (absโ๐ต) โ {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))})) |
89 | | rexcom 3276 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
90 | 1 | zcnd 12615 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ด โ โ) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ด โ โ) |
92 | | zcn 12511 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
93 | 92 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ฅ โ โ) |
94 | 91, 93 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ (๐ด ยท ๐ฅ) โ โ) |
95 | 2 | zcnd 12615 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ต โ โ) |
96 | 95 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ต โ โ) |
97 | | zcn 12511 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
98 | 97 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ฆ โ โ) |
99 | 96, 98 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ (๐ต ยท ๐ฆ) โ โ) |
100 | 94, 99 | addcomd 11364 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))) |
101 | 100 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ (๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ)))) |
102 | 101 | 2rexbidva 3212 |
. . . . . . . . . . . . 13
โข (๐ โ (โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ)))) |
103 | 89, 102 | bitrid 283 |
. . . . . . . . . . . 12
โข (๐ โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ)))) |
104 | 103 | rabbidv 3418 |
. . . . . . . . . . 11
โข (๐ โ {๐ง โ โ โฃ โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))} = {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))}) |
105 | 16, 104 | eqtrid 2789 |
. . . . . . . . . 10
โข (๐ โ ๐ = {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))}) |
106 | 105 | eleq2d 2824 |
. . . . . . . . 9
โข (๐ โ ((absโ๐ต) โ ๐ โ (absโ๐ต) โ {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))})) |
107 | 88, 106 | sylibrd 259 |
. . . . . . . 8
โข (๐ โ (๐ต โ 0 โ (absโ๐ต) โ ๐)) |
108 | 16, 1, 2, 17, 18 | bezoutlem3 16429 |
. . . . . . . 8
โข (๐ โ ((absโ๐ต) โ ๐ โ ๐บ โฅ (absโ๐ต))) |
109 | 107, 108 | syld 47 |
. . . . . . 7
โข (๐ โ (๐ต โ 0 โ ๐บ โฅ (absโ๐ต))) |
110 | | dvdsabsb 16165 |
. . . . . . . 8
โข ((๐บ โ โค โง ๐ต โ โค) โ (๐บ โฅ ๐ต โ ๐บ โฅ (absโ๐ต))) |
111 | 78, 2, 110 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐บ โฅ ๐ต โ ๐บ โฅ (absโ๐ต))) |
112 | 109, 111 | sylibrd 259 |
. . . . . 6
โข (๐ โ (๐ต โ 0 โ ๐บ โฅ ๐ต)) |
113 | 112 | imp 408 |
. . . . 5
โข ((๐ โง ๐ต โ 0) โ ๐บ โฅ ๐ต) |
114 | 86, 113, 84 | pm2.61ne 3031 |
. . . 4
โข (๐ โ ๐บ โฅ ๐ต) |
115 | | dvdslegcd 16391 |
. . . . 5
โข (((๐บ โ โค โง ๐ด โ โค โง ๐ต โ โค) โง ยฌ
(๐ด = 0 โง ๐ต = 0)) โ ((๐บ โฅ ๐ด โง ๐บ โฅ ๐ต) โ ๐บ โค (๐ด gcd ๐ต))) |
116 | 78, 1, 2, 18, 115 | syl31anc 1374 |
. . . 4
โข (๐ โ ((๐บ โฅ ๐ด โง ๐บ โฅ ๐ต) โ ๐บ โค (๐ด gcd ๐ต))) |
117 | 85, 114, 116 | mp2and 698 |
. . 3
โข (๐ โ ๐บ โค (๐ด gcd ๐ต)) |
118 | 6 | nn0red 12481 |
. . . 4
โข (๐ โ (๐ด gcd ๐ต) โ โ) |
119 | 70 | nnred 12175 |
. . . 4
โข (๐ โ ๐บ โ โ) |
120 | 118, 119 | letri3d 11304 |
. . 3
โข (๐ โ ((๐ด gcd ๐ต) = ๐บ โ ((๐ด gcd ๐ต) โค ๐บ โง ๐บ โค (๐ด gcd ๐ต)))) |
121 | 73, 117, 120 | mpbir2and 712 |
. 2
โข (๐ โ (๐ด gcd ๐ต) = ๐บ) |
122 | 121, 19 | eqeltrd 2838 |
1
โข (๐ โ (๐ด gcd ๐ต) โ ๐) |