Step | Hyp | Ref
| Expression |
1 | | bezout 16425 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
2 | 1 | 3adant1 1131 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
3 | | dvds2ln 16172 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐)))) |
4 | 3 | 3impia 1118 |
. . . . . . . 8
โข (((๐ฅ โ โค โง ๐ฆ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐)) โ ๐พ โฅ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐))) |
5 | 4 | 3coml 1128 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐พ โฅ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐))) |
6 | | simp3l 1202 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ โค) |
7 | | simp12 1205 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
8 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
9 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
10 | | mulcom 11138 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
11 | 8, 9, 10 | syl2an 597 |
. . . . . . . . 9
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
12 | 6, 7, 11 | syl2anc 585 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
13 | | simp3r 1203 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ โค) |
14 | | simp13 1206 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
15 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
16 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
17 | | mulcom 11138 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ ยท ๐) = (๐ ยท ๐ฆ)) |
18 | 15, 16, 17 | syl2an 597 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง ๐ โ โค) โ (๐ฆ ยท ๐) = (๐ ยท ๐ฆ)) |
19 | 13, 14, 18 | syl2anc 585 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฆ ยท ๐) = (๐ ยท ๐ฆ)) |
20 | 12, 19 | oveq12d 7376 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐)) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
21 | 5, 20 | breqtrd 5132 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐พ โฅ ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
22 | | breq2 5110 |
. . . . . 6
โข ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐พ โฅ (๐ gcd ๐) โ ๐พ โฅ ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)))) |
23 | 21, 22 | syl5ibrcom 247 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐))) |
24 | 23 | 3expia 1122 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐)) โ ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐)))) |
25 | 24 | rexlimdvv 3205 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐)) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐))) |
26 | 25 | ex 414 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐)))) |
27 | 2, 26 | mpid 44 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ gcd ๐))) |