Step | Hyp | Ref
| Expression |
1 | | dvds2lem.1 |
. . . . . 6
โข (๐ โ (๐ผ โ โค โง ๐ฝ โ โค)) |
2 | | dvds2lem.2 |
. . . . . 6
โข (๐ โ (๐พ โ โค โง ๐ฟ โ โค)) |
3 | | divides 16139 |
. . . . . . 7
โข ((๐ผ โ โค โง ๐ฝ โ โค) โ (๐ผ โฅ ๐ฝ โ โ๐ฅ โ โค (๐ฅ ยท ๐ผ) = ๐ฝ)) |
4 | | divides 16139 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ฟ โ โค) โ (๐พ โฅ ๐ฟ โ โ๐ฆ โ โค (๐ฆ ยท ๐พ) = ๐ฟ)) |
5 | 3, 4 | bi2anan9 638 |
. . . . . 6
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ฟ โ โค)) โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ (โ๐ฅ โ โค (๐ฅ ยท ๐ผ) = ๐ฝ โง โ๐ฆ โ โค (๐ฆ ยท ๐พ) = ๐ฟ))) |
6 | 1, 2, 5 | syl2anc 585 |
. . . . 5
โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ (โ๐ฅ โ โค (๐ฅ ยท ๐ผ) = ๐ฝ โง โ๐ฆ โ โค (๐ฆ ยท ๐พ) = ๐ฟ))) |
7 | 6 | biimpd 228 |
. . . 4
โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ (โ๐ฅ โ โค (๐ฅ ยท ๐ผ) = ๐ฝ โง โ๐ฆ โ โค (๐ฆ ยท ๐พ) = ๐ฟ))) |
8 | | reeanv 3218 |
. . . 4
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ) โ (โ๐ฅ โ โค (๐ฅ ยท ๐ผ) = ๐ฝ โง โ๐ฆ โ โค (๐ฆ ยท ๐พ) = ๐ฟ)) |
9 | 7, 8 | syl6ibr 252 |
. . 3
โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ))) |
10 | | dvds2lem.4 |
. . . . 5
โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
11 | | dvds2lem.5 |
. . . . 5
โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ) โ (๐ ยท ๐) = ๐)) |
12 | | oveq1 7365 |
. . . . . . 7
โข (๐ง = ๐ โ (๐ง ยท ๐) = (๐ ยท ๐)) |
13 | 12 | eqeq1d 2739 |
. . . . . 6
โข (๐ง = ๐ โ ((๐ง ยท ๐) = ๐ โ (๐ ยท ๐) = ๐)) |
14 | 13 | rspcev 3582 |
. . . . 5
โข ((๐ โ โค โง (๐ ยท ๐) = ๐) โ โ๐ง โ โค (๐ง ยท ๐) = ๐) |
15 | 10, 11, 14 | syl6an 683 |
. . . 4
โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ) โ โ๐ง โ โค (๐ง ยท ๐) = ๐)) |
16 | 15 | rexlimdvva 3206 |
. . 3
โข (๐ โ (โ๐ฅ โ โค โ๐ฆ โ โค ((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ) โ โ๐ง โ โค (๐ง ยท ๐) = ๐)) |
17 | 9, 16 | syld 47 |
. 2
โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ โ๐ง โ โค (๐ง ยท ๐) = ๐)) |
18 | | dvds2lem.3 |
. . 3
โข (๐ โ (๐ โ โค โง ๐ โ โค)) |
19 | | divides 16139 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ง โ โค (๐ง ยท ๐) = ๐)) |
20 | 18, 19 | syl 17 |
. 2
โข (๐ โ (๐ โฅ ๐ โ โ๐ง โ โค (๐ง ยท ๐) = ๐)) |
21 | 17, 20 | sylibrd 259 |
1
โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ ๐ โฅ ๐)) |