Step | Hyp | Ref
| Expression |
1 | | bezoutlemzz 12002 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
2 | 1 | ancoms 268 |
. . 3
โข ((๐ต โ โ0
โง ๐ด โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
3 | 2 | adantll 476 |
. 2
โข (((๐ด โ โค โง ๐ต โ โ0)
โง ๐ด โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
4 | | bezoutlemzz 12002 |
. . . . 5
โข ((-๐ด โ โ0
โง ๐ต โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โง โ๐ก โ โค โ๐ฆ โ โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)))) |
5 | 4 | ancoms 268 |
. . . 4
โข ((๐ต โ โ0
โง -๐ด โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โง โ๐ก โ โค โ๐ฆ โ โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)))) |
6 | 5 | adantll 476 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โง โ๐ก โ โค โ๐ฆ โ โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)))) |
7 | | simpr 110 |
. . . . . . . . . 10
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ง โ โค)
โ ๐ง โ
โค) |
8 | | simpll 527 |
. . . . . . . . . . 11
โข (((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โ ๐ด โ โค) |
9 | 8 | ad2antrr 488 |
. . . . . . . . . 10
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ง โ โค)
โ ๐ด โ
โค) |
10 | | dvdsnegb 11814 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ด โ โค) โ (๐ง โฅ ๐ด โ ๐ง โฅ -๐ด)) |
11 | 7, 9, 10 | syl2anc 411 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ง โ โค)
โ (๐ง โฅ ๐ด โ ๐ง โฅ -๐ด)) |
12 | 11 | biimprd 158 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ง โ โค)
โ (๐ง โฅ -๐ด โ ๐ง โฅ ๐ด)) |
13 | 12 | anim1d 336 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ง โ โค)
โ ((๐ง โฅ -๐ด โง ๐ง โฅ ๐ต) โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) |
14 | 13 | imim2d 54 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ง โ โค)
โ ((๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
15 | 14 | ralimdva 2544 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โง ๐ โ โ0) โ
(โ๐ง โ โค
(๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โ โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
16 | 8 | ad2antrr 488 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ ๐ด โ
โค) |
17 | 16 | zcnd 9375 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ ๐ด โ
โ) |
18 | | simpr 110 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ ๐ก โ
โค) |
19 | 18 | zcnd 9375 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ ๐ก โ
โ) |
20 | | mulneg12 8353 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ก โ โ) โ (-๐ด ยท ๐ก) = (๐ด ยท -๐ก)) |
21 | 17, 19, 20 | syl2anc 411 |
. . . . . . . . . 10
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ (-๐ด ยท ๐ก) = (๐ด ยท -๐ก)) |
22 | 21 | oveq1d 5889 |
. . . . . . . . 9
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)) = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ))) |
23 | 22 | eqeq2d 2189 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ (๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)) โ ๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ)))) |
24 | 23 | rexbidv 2478 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ (โ๐ฆ โ
โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค ๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ)))) |
25 | | znegcl 9283 |
. . . . . . . . . 10
โข (๐ก โ โค โ -๐ก โ
โค) |
26 | | oveq2 5882 |
. . . . . . . . . . . . . 14
โข (๐ฅ = -๐ก โ (๐ด ยท ๐ฅ) = (๐ด ยท -๐ก)) |
27 | 26 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข (๐ฅ = -๐ก โ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ))) |
28 | 27 | eqeq2d 2189 |
. . . . . . . . . . . 12
โข (๐ฅ = -๐ก โ (๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ)))) |
29 | 28 | rexbidv 2478 |
. . . . . . . . . . 11
โข (๐ฅ = -๐ก โ (โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ โ๐ฆ โ โค ๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ)))) |
30 | 29 | rspcev 2841 |
. . . . . . . . . 10
โข ((-๐ก โ โค โง
โ๐ฆ โ โค
๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ))) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
31 | 25, 30 | sylan 283 |
. . . . . . . . 9
โข ((๐ก โ โค โง
โ๐ฆ โ โค
๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ))) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
32 | 31 | ex 115 |
. . . . . . . 8
โข (๐ก โ โค โ
(โ๐ฆ โ โค
๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
33 | 32 | adantl 277 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ (โ๐ฆ โ
โค ๐ = ((๐ด ยท -๐ก) + (๐ต ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
34 | 24, 33 | sylbid 150 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โ0) โง -๐ด โ โ0) โง ๐ โ โ0)
โง ๐ก โ โค)
โ (โ๐ฆ โ
โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
35 | 34 | rexlimdva 2594 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โง ๐ โ โ0) โ
(โ๐ก โ โค
โ๐ฆ โ โค
๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ)) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
36 | 15, 35 | anim12d 335 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โง ๐ โ โ0) โ
((โ๐ง โ โค
(๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โง โ๐ก โ โค โ๐ฆ โ โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
37 | 36 | reximdva 2579 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โ (โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ -๐ด โง ๐ง โฅ ๐ต)) โง โ๐ก โ โค โ๐ฆ โ โค ๐ = ((-๐ด ยท ๐ก) + (๐ต ยท ๐ฆ))) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
38 | 6, 37 | mpd 13 |
. 2
โข (((๐ด โ โค โง ๐ต โ โ0)
โง -๐ด โ
โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
39 | | elznn0 9267 |
. . . 4
โข (๐ด โ โค โ (๐ด โ โ โง (๐ด โ โ0 โจ
-๐ด โ
โ0))) |
40 | 39 | simprbi 275 |
. . 3
โข (๐ด โ โค โ (๐ด โ โ0 โจ
-๐ด โ
โ0)) |
41 | 40 | adantr 276 |
. 2
โข ((๐ด โ โค โง ๐ต โ โ0)
โ (๐ด โ
โ0 โจ -๐ด
โ โ0)) |
42 | 3, 38, 41 | mpjaodan 798 |
1
โข ((๐ด โ โค โง ๐ต โ โ0)
โ โ๐ โ
โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |