Step | Hyp | Ref
| Expression |
1 | | bezoutlembz 12004 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค) โ
โ๐ โ
โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
2 | | simpllr 534 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ๐ง โ โค) |
3 | | simpll 527 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ0)
โ ๐ด โ
โค) |
4 | 3 | ad3antrrr 492 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ๐ด โ โค) |
5 | | simplrl 535 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ๐ฅ โ โค) |
6 | | dvdsmultr1 11837 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ด โ โค โง ๐ฅ โ โค) โ (๐ง โฅ ๐ด โ ๐ง โฅ (๐ด ยท ๐ฅ))) |
7 | 2, 4, 5, 6 | syl3anc 1238 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (๐ง โฅ ๐ด โ ๐ง โฅ (๐ด ยท ๐ฅ))) |
8 | | simplr 528 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ0)
โ ๐ต โ
โค) |
9 | 8 | ad3antrrr 492 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ๐ต โ โค) |
10 | | simplrr 536 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ๐ฆ โ โค) |
11 | | dvdsmultr1 11837 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ต โ โค โง ๐ฆ โ โค) โ (๐ง โฅ ๐ต โ ๐ง โฅ (๐ต ยท ๐ฆ))) |
12 | 2, 9, 10, 11 | syl3anc 1238 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (๐ง โฅ ๐ต โ ๐ง โฅ (๐ต ยท ๐ฆ))) |
13 | 4, 5 | zmulcld 9380 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (๐ด ยท ๐ฅ) โ โค) |
14 | 9, 10 | zmulcld 9380 |
. . . . . . . . . . . 12
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (๐ต ยท ๐ฆ) โ โค) |
15 | | dvds2add 11831 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง (๐ด ยท ๐ฅ) โ โค โง (๐ต ยท ๐ฆ) โ โค) โ ((๐ง โฅ (๐ด ยท ๐ฅ) โง ๐ง โฅ (๐ต ยท ๐ฆ)) โ ๐ง โฅ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
16 | 2, 13, 14, 15 | syl3anc 1238 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ (๐ด ยท ๐ฅ) โง ๐ง โฅ (๐ต ยท ๐ฆ)) โ ๐ง โฅ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
17 | 7, 12, 16 | syl2and 295 |
. . . . . . . . . 10
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ ๐ด โง ๐ง โฅ ๐ต) โ ๐ง โฅ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
18 | | simpr 110 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) |
19 | 18 | breq2d 4015 |
. . . . . . . . . 10
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (๐ง โฅ ๐ โ ๐ง โฅ ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
20 | 17, 19 | sylibrd 169 |
. . . . . . . . 9
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ ๐ด โง ๐ง โฅ ๐ต) โ ๐ง โฅ ๐)) |
21 | | bi3 119 |
. . . . . . . . 9
โข ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โ (((๐ง โฅ ๐ด โง ๐ง โฅ ๐ต) โ ๐ง โฅ ๐) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
22 | 20, 21 | syl5com 29 |
. . . . . . . 8
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โง ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
23 | 22 | ex 115 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง ๐ โ
โ0) โง ๐ง โ โค) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))))) |
24 | 23 | rexlimdvva 2602 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ0)
โง ๐ง โ โค)
โ (โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))))) |
25 | | imdistan 444 |
. . . . . . 7
โข
((โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) โ ((โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โง (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โง (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))))) |
26 | | ancom 266 |
. . . . . . . 8
โข (((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โง (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
27 | | ancom 266 |
. . . . . . . 8
โข (((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โง (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) |
28 | 26, 27 | imbi12i 239 |
. . . . . . 7
โข ((((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) โ ((โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โง (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โง (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))))) |
29 | 25, 28 | bitr4i 187 |
. . . . . 6
โข
((โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)))) โ (((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
30 | 24, 29 | sylib 122 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ0)
โง ๐ง โ โค)
โ (((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
31 | 30 | ralimdva 2544 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ0)
โ (โ๐ง โ
โค ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ โ๐ง โ โค ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
32 | | 0z 9263 |
. . . . . 6
โข 0 โ
โค |
33 | | elex2 2753 |
. . . . . 6
โข (0 โ
โค โ โ๐ง
๐ง โ
โค) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
โข
โ๐ง ๐ง โ โค |
35 | | r19.27mv 3519 |
. . . . 5
โข
(โ๐ง ๐ง โ โค โ
(โ๐ง โ โค
((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
36 | 34, 35 | ax-mp 5 |
. . . 4
โข
(โ๐ง โ
โค ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
37 | | r19.27mv 3519 |
. . . . 5
โข
(โ๐ง ๐ง โ โค โ
(โ๐ง โ โค
((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
38 | 34, 37 | ax-mp 5 |
. . . 4
โข
(โ๐ง โ
โค ((๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |
39 | 31, 36, 38 | 3imtr3g 204 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค) โง ๐ โ โ0)
โ ((โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
40 | 39 | reximdva 2579 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค) โ
(โ๐ โ
โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))))) |
41 | 1, 40 | mpd 13 |
1
โข ((๐ด โ โค โง ๐ต โ โค) โ
โ๐ โ
โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) |