Step | Hyp | Ref
| Expression |
1 | | bezout 16489 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
2 | 1 | 3adant1 1127 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
3 | | dvds2ln 16236 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐)))) |
4 | 3 | 3impia 1114 |
. . . . . . . 8
โข (((๐ฅ โ โค โง ๐ฆ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐)) โ ๐พ โฅ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐))) |
5 | 4 | 3coml 1124 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐พ โฅ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐))) |
6 | | simp3l 1198 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ โค) |
7 | | simp12 1201 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
8 | | zcn 12564 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
9 | | zcn 12564 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
10 | | mulcom 11195 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
11 | 8, 9, 10 | syl2an 595 |
. . . . . . . . 9
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
12 | 6, 7, 11 | syl2anc 583 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ๐) = (๐ ยท ๐ฅ)) |
13 | | simp3r 1199 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ โค) |
14 | | simp13 1202 |
. . . . . . . . 9
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) |
15 | | zcn 12564 |
. . . . . . . . . 10
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
16 | | zcn 12564 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
17 | | mulcom 11195 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ โ โ) โ (๐ฆ ยท ๐) = (๐ ยท ๐ฆ)) |
18 | 15, 16, 17 | syl2an 595 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง ๐ โ โค) โ (๐ฆ ยท ๐) = (๐ ยท ๐ฆ)) |
19 | 13, 14, 18 | syl2anc 583 |
. . . . . . . 8
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฆ ยท ๐) = (๐ ยท ๐ฆ)) |
20 | 12, 19 | oveq12d 7422 |
. . . . . . 7
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐) + (๐ฆ ยท ๐)) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
21 | 5, 20 | breqtrd 5167 |
. . . . . 6
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐พ โฅ ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ))) |
22 | | breq2 5145 |
. . . . . 6
โข ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ (๐พ โฅ (๐ gcd ๐) โ ๐พ โฅ ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)))) |
23 | 21, 22 | syl5ibrcom 246 |
. . . . 5
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐))) |
24 | 23 | 3expia 1118 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐)) โ ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐)))) |
25 | 24 | rexlimdvv 3204 |
. . 3
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ โฅ ๐ โง ๐พ โฅ ๐)) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐))) |
26 | 25 | ex 412 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ (โ๐ฅ โ โค โ๐ฆ โ โค (๐ gcd ๐) = ((๐ ยท ๐ฅ) + (๐ ยท ๐ฆ)) โ ๐พ โฅ (๐ gcd ๐)))) |
27 | 2, 26 | mpid 44 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ gcd ๐))) |