Step | Hyp | Ref
| Expression |
1 | | bezout.2 |
. 2
โข ๐บ = inf(๐, โ, < ) |
2 | | bezout.1 |
. . . . 5
โข ๐ = {๐ง โ โ โฃ โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))} |
3 | 2 | ssrab3 4045 |
. . . 4
โข ๐ โ
โ |
4 | | nnuz 12813 |
. . . 4
โข โ =
(โคโฅโ1) |
5 | 3, 4 | sseqtri 3985 |
. . 3
โข ๐ โ
(โคโฅโ1) |
6 | | bezout.3 |
. . . . . 6
โข (๐ โ ๐ด โ โค) |
7 | | bezout.4 |
. . . . . 6
โข (๐ โ ๐ต โ โค) |
8 | 2, 6, 7 | bezoutlem1 16427 |
. . . . 5
โข (๐ โ (๐ด โ 0 โ (absโ๐ด) โ ๐)) |
9 | | ne0i 4299 |
. . . . 5
โข
((absโ๐ด)
โ ๐ โ ๐ โ โ
) |
10 | 8, 9 | syl6 35 |
. . . 4
โข (๐ โ (๐ด โ 0 โ ๐ โ โ
)) |
11 | | eqid 2737 |
. . . . . . 7
โข {๐ง โ โ โฃ
โ๐ฆ โ โค
โ๐ฅ โ โค
๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))} = {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))} |
12 | 11, 7, 6 | bezoutlem1 16427 |
. . . . . 6
โข (๐ โ (๐ต โ 0 โ (absโ๐ต) โ {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))})) |
13 | | rexcom 3276 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
14 | 6 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ โ) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ด โ โ) |
16 | | zcn 12511 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
17 | 16 | ad2antll 728 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ฅ โ โ) |
18 | 15, 17 | mulcld 11182 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ (๐ด ยท ๐ฅ) โ โ) |
19 | 7 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ โ) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ต โ โ) |
21 | | zcn 12511 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
22 | 21 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ๐ฆ โ โ) |
23 | 20, 22 | mulcld 11182 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ (๐ต ยท ๐ฆ) โ โ) |
24 | 18, 23 | addcomd 11364 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))) |
25 | 24 | eqeq2d 2748 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ โค โง ๐ฅ โ โค)) โ (๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ)))) |
26 | 25 | 2rexbidva 3212 |
. . . . . . . . . 10
โข (๐ โ (โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ)))) |
27 | 13, 26 | bitrid 283 |
. . . . . . . . 9
โข (๐ โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ)))) |
28 | 27 | rabbidv 3418 |
. . . . . . . 8
โข (๐ โ {๐ง โ โ โฃ โ๐ฅ โ โค โ๐ฆ โ โค ๐ง = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))} = {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))}) |
29 | 2, 28 | eqtrid 2789 |
. . . . . . 7
โข (๐ โ ๐ = {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))}) |
30 | 29 | eleq2d 2824 |
. . . . . 6
โข (๐ โ ((absโ๐ต) โ ๐ โ (absโ๐ต) โ {๐ง โ โ โฃ โ๐ฆ โ โค โ๐ฅ โ โค ๐ง = ((๐ต ยท ๐ฆ) + (๐ด ยท ๐ฅ))})) |
31 | 12, 30 | sylibrd 259 |
. . . . 5
โข (๐ โ (๐ต โ 0 โ (absโ๐ต) โ ๐)) |
32 | | ne0i 4299 |
. . . . 5
โข
((absโ๐ต)
โ ๐ โ ๐ โ โ
) |
33 | 31, 32 | syl6 35 |
. . . 4
โข (๐ โ (๐ต โ 0 โ ๐ โ โ
)) |
34 | | bezout.5 |
. . . . 5
โข (๐ โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
35 | | neorian 3040 |
. . . . 5
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
36 | 34, 35 | sylibr 233 |
. . . 4
โข (๐ โ (๐ด โ 0 โจ ๐ต โ 0)) |
37 | 10, 33, 36 | mpjaod 859 |
. . 3
โข (๐ โ ๐ โ โ
) |
38 | | infssuzcl 12864 |
. . 3
โข ((๐ โ
(โคโฅโ1) โง ๐ โ โ
) โ inf(๐, โ, < ) โ ๐) |
39 | 5, 37, 38 | sylancr 588 |
. 2
โข (๐ โ inf(๐, โ, < ) โ ๐) |
40 | 1, 39 | eqeltrid 2842 |
1
โข (๐ โ ๐บ โ ๐) |