Step | Hyp | Ref
| Expression |
1 | | 0z 9277 |
. . 3
โข 0 โ
โค |
2 | | 1z 9292 |
. . 3
โข 1 โ
โค |
3 | | bezoutlema.a |
. . . . . . 7
โข (๐ โ ๐ด โ
โ0) |
4 | 3 | nn0cnd 9244 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
5 | 4 | mul01d 8363 |
. . . . 5
โข (๐ โ (๐ด ยท 0) = 0) |
6 | 5 | oveq1d 5903 |
. . . 4
โข (๐ โ ((๐ด ยท 0) + (๐ต ยท 1)) = (0 + (๐ต ยท 1))) |
7 | | bezoutlema.b |
. . . . . . 7
โข (๐ โ ๐ต โ
โ0) |
8 | 7 | nn0cnd 9244 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
9 | | 1cnd 7986 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
10 | 8, 9 | mulcld 7991 |
. . . . 5
โข (๐ โ (๐ต ยท 1) โ
โ) |
11 | 10 | addid2d 8120 |
. . . 4
โข (๐ โ (0 + (๐ต ยท 1)) = (๐ต ยท 1)) |
12 | 8 | mulridd 7987 |
. . . 4
โข (๐ โ (๐ต ยท 1) = ๐ต) |
13 | 6, 11, 12 | 3eqtrrd 2225 |
. . 3
โข (๐ โ ๐ต = ((๐ด ยท 0) + (๐ต ยท 1))) |
14 | | oveq2 5896 |
. . . . . 6
โข (๐ = 0 โ (๐ด ยท ๐ ) = (๐ด ยท 0)) |
15 | 14 | oveq1d 5903 |
. . . . 5
โข (๐ = 0 โ ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)) = ((๐ด ยท 0) + (๐ต ยท ๐ก))) |
16 | 15 | eqeq2d 2199 |
. . . 4
โข (๐ = 0 โ (๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)) โ ๐ต = ((๐ด ยท 0) + (๐ต ยท ๐ก)))) |
17 | | oveq2 5896 |
. . . . . 6
โข (๐ก = 1 โ (๐ต ยท ๐ก) = (๐ต ยท 1)) |
18 | 17 | oveq2d 5904 |
. . . . 5
โข (๐ก = 1 โ ((๐ด ยท 0) + (๐ต ยท ๐ก)) = ((๐ด ยท 0) + (๐ต ยท 1))) |
19 | 18 | eqeq2d 2199 |
. . . 4
โข (๐ก = 1 โ (๐ต = ((๐ด ยท 0) + (๐ต ยท ๐ก)) โ ๐ต = ((๐ด ยท 0) + (๐ต ยท 1)))) |
20 | 16, 19 | rspc2ev 2868 |
. . 3
โข ((0
โ โค โง 1 โ โค โง ๐ต = ((๐ด ยท 0) + (๐ต ยท 1))) โ โ๐ โ โค โ๐ก โ โค ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
21 | 1, 2, 13, 20 | mp3an12i 1351 |
. 2
โข (๐ โ โ๐ โ โค โ๐ก โ โค ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
22 | | bezoutlema.is-bezout |
. . . . 5
โข (๐ โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
23 | | eqeq1 2194 |
. . . . . 6
โข (๐ = ๐ต โ (๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)) โ ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
24 | 23 | 2rexbidv 2512 |
. . . . 5
โข (๐ = ๐ต โ (โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)) โ โ๐ โ โค โ๐ก โ โค ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
25 | 22, 24 | bitrid 192 |
. . . 4
โข (๐ = ๐ต โ (๐ โ โ๐ โ โค โ๐ก โ โค ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
26 | 25 | sbcieg 3007 |
. . 3
โข (๐ต โ โ0
โ ([๐ต / ๐]๐ โ โ๐ โ โค โ๐ก โ โค ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
27 | 7, 26 | syl 14 |
. 2
โข (๐ โ ([๐ต / ๐]๐ โ โ๐ โ โค โ๐ก โ โค ๐ต = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก)))) |
28 | 21, 27 | mpbird 167 |
1
โข (๐ โ [๐ต / ๐]๐) |