Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . 4
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โ ๐ถ โ โค) |
2 | | dvdszrcl 16076 |
. . . . . 6
โข (๐ด โฅ (๐ต ยท ๐ถ) โ (๐ด โ โค โง (๐ต ยท ๐ถ) โ โค)) |
3 | 2 | adantl 483 |
. . . . 5
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โ (๐ด โ โค โง (๐ต ยท ๐ถ) โ โค)) |
4 | 3 | simpld 496 |
. . . 4
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โ ๐ด โ โค) |
5 | | bezout 16359 |
. . . 4
โข ((๐ถ โ โค โง ๐ด โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ถ gcd ๐ด) = ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ))) |
6 | 1, 4, 5 | syl2anc 585 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โ โ๐ฅ โ โค โ๐ฆ โ โค (๐ถ gcd ๐ด) = ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ))) |
7 | 4 | adantr 482 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โ โค) |
8 | | simplll 774 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ต โ โค) |
9 | | simpllr 775 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ถ โ โค) |
10 | | simprl 770 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ โค) |
11 | 9, 10 | zmulcld 12546 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ถ ยท ๐ฅ) โ โค) |
12 | 8, 11 | zmulcld 12546 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ต ยท (๐ถ ยท ๐ฅ)) โ โค) |
13 | | simprr 772 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ โค) |
14 | 7, 13 | zmulcld 12546 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ด ยท ๐ฆ) โ โค) |
15 | 8, 14 | zmulcld 12546 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ต ยท (๐ด ยท ๐ฆ)) โ โค) |
16 | 8, 9 | zmulcld 12546 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ต ยท ๐ถ) โ โค) |
17 | | simplr 768 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ (๐ต ยท ๐ถ)) |
18 | 7, 16, 10, 17 | dvdsmultr1d 16114 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ ((๐ต ยท ๐ถ) ยท ๐ฅ)) |
19 | 8 | zcnd 12541 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ต โ โ) |
20 | 9 | zcnd 12541 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ถ โ โ) |
21 | 10 | zcnd 12541 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ โ) |
22 | 19, 20, 21 | mulassd 11112 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ต ยท ๐ถ) ยท ๐ฅ) = (๐ต ยท (๐ถ ยท ๐ฅ))) |
23 | 18, 22 | breqtrd 5130 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ (๐ต ยท (๐ถ ยท ๐ฅ))) |
24 | 8, 13 | zmulcld 12546 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ต ยท ๐ฆ) โ โค) |
25 | | dvdsmul1 16095 |
. . . . . . . . 9
โข ((๐ด โ โค โง (๐ต ยท ๐ฆ) โ โค) โ ๐ด โฅ (๐ด ยท (๐ต ยท ๐ฆ))) |
26 | 7, 24, 25 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ (๐ด ยท (๐ต ยท ๐ฆ))) |
27 | 7 | zcnd 12541 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โ โ) |
28 | 13 | zcnd 12541 |
. . . . . . . . 9
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ โ) |
29 | 19, 27, 28 | mul12d 11298 |
. . . . . . . 8
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ต ยท (๐ด ยท ๐ฆ)) = (๐ด ยท (๐ต ยท ๐ฆ))) |
30 | 26, 29 | breqtrrd 5132 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ (๐ต ยท (๐ด ยท ๐ฆ))) |
31 | 7, 12, 15, 23, 30 | dvds2addd 16109 |
. . . . . 6
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ ((๐ต ยท (๐ถ ยท ๐ฅ)) + (๐ต ยท (๐ด ยท ๐ฆ)))) |
32 | 11 | zcnd 12541 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ถ ยท ๐ฅ) โ โ) |
33 | 14 | zcnd 12541 |
. . . . . . 7
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ด ยท ๐ฆ) โ โ) |
34 | 19, 32, 33 | adddid 11113 |
. . . . . 6
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ต ยท ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ))) = ((๐ต ยท (๐ถ ยท ๐ฅ)) + (๐ต ยท (๐ด ยท ๐ฆ)))) |
35 | 31, 34 | breqtrrd 5132 |
. . . . 5
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ด โฅ (๐ต ยท ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ)))) |
36 | | oveq2 7358 |
. . . . . 6
โข ((๐ถ gcd ๐ด) = ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ)) โ (๐ต ยท (๐ถ gcd ๐ด)) = (๐ต ยท ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ)))) |
37 | 36 | breq2d 5116 |
. . . . 5
โข ((๐ถ gcd ๐ด) = ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ)) โ (๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด)) โ ๐ด โฅ (๐ต ยท ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ))))) |
38 | 35, 37 | syl5ibrcom 247 |
. . . 4
โข ((((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ถ gcd ๐ด) = ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ)) โ ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด)))) |
39 | 38 | rexlimdvva 3204 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ถ gcd ๐ด) = ((๐ถ ยท ๐ฅ) + (๐ด ยท ๐ฆ)) โ ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด)))) |
40 | 6, 39 | mpd 15 |
. 2
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท ๐ถ)) โ ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) |
41 | | dvdszrcl 16076 |
. . . . 5
โข (๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด)) โ (๐ด โ โค โง (๐ต ยท (๐ถ gcd ๐ด)) โ โค)) |
42 | 41 | adantl 483 |
. . . 4
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ด โ โค โง (๐ต ยท (๐ถ gcd ๐ด)) โ โค)) |
43 | 42 | simpld 496 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ๐ด โ โค) |
44 | 42 | simprd 497 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ต ยท (๐ถ gcd ๐ด)) โ โค) |
45 | | zmulcl 12483 |
. . . 4
โข ((๐ต โ โค โง ๐ถ โ โค) โ (๐ต ยท ๐ถ) โ โค) |
46 | 45 | adantr 482 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ต ยท ๐ถ) โ โค) |
47 | | simpr 486 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) |
48 | | simplr 768 |
. . . . . 6
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ๐ถ โ โค) |
49 | | gcddvds 16318 |
. . . . . 6
โข ((๐ถ โ โค โง ๐ด โ โค) โ ((๐ถ gcd ๐ด) โฅ ๐ถ โง (๐ถ gcd ๐ด) โฅ ๐ด)) |
50 | 48, 43, 49 | syl2anc 585 |
. . . . 5
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ((๐ถ gcd ๐ด) โฅ ๐ถ โง (๐ถ gcd ๐ด) โฅ ๐ด)) |
51 | 50 | simpld 496 |
. . . 4
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ถ gcd ๐ด) โฅ ๐ถ) |
52 | 48, 43 | gcdcld 16323 |
. . . . . 6
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ถ gcd ๐ด) โ
โ0) |
53 | 52 | nn0zd 12538 |
. . . . 5
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ถ gcd ๐ด) โ โค) |
54 | | simpll 766 |
. . . . 5
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ๐ต โ โค) |
55 | | dvdscmul 16100 |
. . . . 5
โข (((๐ถ gcd ๐ด) โ โค โง ๐ถ โ โค โง ๐ต โ โค) โ ((๐ถ gcd ๐ด) โฅ ๐ถ โ (๐ต ยท (๐ถ gcd ๐ด)) โฅ (๐ต ยท ๐ถ))) |
56 | 53, 48, 54, 55 | syl3anc 1372 |
. . . 4
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ((๐ถ gcd ๐ด) โฅ ๐ถ โ (๐ต ยท (๐ถ gcd ๐ด)) โฅ (๐ต ยท ๐ถ))) |
57 | 51, 56 | mpd 15 |
. . 3
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ (๐ต ยท (๐ถ gcd ๐ด)) โฅ (๐ต ยท ๐ถ)) |
58 | 43, 44, 46, 47, 57 | dvdstrd 16112 |
. 2
โข (((๐ต โ โค โง ๐ถ โ โค) โง ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด))) โ ๐ด โฅ (๐ต ยท ๐ถ)) |
59 | 40, 58 | impbida 800 |
1
โข ((๐ต โ โค โง ๐ถ โ โค) โ (๐ด โฅ (๐ต ยท ๐ถ) โ ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด)))) |