Step | Hyp | Ref
| Expression |
1 | | gcd0val 11960 |
. . 3
โข (0 gcd 0)
= 0 |
2 | | simprl 529 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ ๐ = 0) |
3 | | simprr 531 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ ๐ = 0) |
4 | 2, 3 | oveq12d 5892 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ (๐ gcd ๐) = (0 gcd 0)) |
5 | | 0nn0 9190 |
. . . . 5
โข 0 โ
โ0 |
6 | 5 | a1i 9 |
. . . 4
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ 0 โ
โ0) |
7 | | 0dvds 11817 |
. . . . . . . . . . 11
โข (๐ โ โค โ (0
โฅ ๐ โ ๐ = 0)) |
8 | 7 | ad2antrr 488 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ (0 โฅ ๐ โ ๐ = 0)) |
9 | 2, 8 | mpbird 167 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ 0 โฅ ๐) |
10 | | 0dvds 11817 |
. . . . . . . . . . 11
โข (๐ โ โค โ (0
โฅ ๐ โ ๐ = 0)) |
11 | 10 | ad2antlr 489 |
. . . . . . . . . 10
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ (0 โฅ ๐ โ ๐ = 0)) |
12 | 3, 11 | mpbird 167 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ 0 โฅ ๐) |
13 | 9, 12 | jca 306 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ (0 โฅ ๐ โง 0 โฅ ๐)) |
14 | 13 | ad2antrr 488 |
. . . . . . 7
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ (0 โฅ ๐ โง 0 โฅ ๐)) |
15 | | 0z 9263 |
. . . . . . . . 9
โข 0 โ
โค |
16 | | breq1 4006 |
. . . . . . . . . . 11
โข (๐ง = 0 โ (๐ง โฅ ๐ โ 0 โฅ ๐)) |
17 | | breq1 4006 |
. . . . . . . . . . . 12
โข (๐ง = 0 โ (๐ง โฅ ๐ โ 0 โฅ ๐)) |
18 | | breq1 4006 |
. . . . . . . . . . . 12
โข (๐ง = 0 โ (๐ง โฅ ๐ โ 0 โฅ ๐)) |
19 | 17, 18 | anbi12d 473 |
. . . . . . . . . . 11
โข (๐ง = 0 โ ((๐ง โฅ ๐ โง ๐ง โฅ ๐) โ (0 โฅ ๐ โง 0 โฅ ๐))) |
20 | 16, 19 | bibi12d 235 |
. . . . . . . . . 10
โข (๐ง = 0 โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ (0 โฅ ๐ โ (0 โฅ ๐ โง 0 โฅ ๐)))) |
21 | 20 | rspcv 2837 |
. . . . . . . . 9
โข (0 โ
โค โ (โ๐ง
โ โค (๐ง โฅ
๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ (0 โฅ ๐ โ (0 โฅ ๐ โง 0 โฅ ๐)))) |
22 | 15, 21 | ax-mp 5 |
. . . . . . . 8
โข
(โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ (0 โฅ ๐ โ (0 โฅ ๐ โง 0 โฅ ๐))) |
23 | 22 | adantl 277 |
. . . . . . 7
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ (0 โฅ ๐ โ (0 โฅ ๐ โง 0 โฅ ๐))) |
24 | 14, 23 | mpbird 167 |
. . . . . 6
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ 0 โฅ ๐) |
25 | | simplr 528 |
. . . . . . . 8
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ ๐ โ โ0) |
26 | 25 | nn0zd 9372 |
. . . . . . 7
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ ๐ โ โค) |
27 | | 0dvds 11817 |
. . . . . . 7
โข (๐ โ โค โ (0
โฅ ๐ โ ๐ = 0)) |
28 | 26, 27 | syl 14 |
. . . . . 6
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ (0 โฅ ๐ โ ๐ = 0)) |
29 | 24, 28 | mpbid 147 |
. . . . 5
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง โ๐ง โ
โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) โ ๐ = 0) |
30 | | dvds0 11812 |
. . . . . . . . 9
โข (๐ง โ โค โ ๐ง โฅ 0) |
31 | 30 | adantl 277 |
. . . . . . . 8
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ ๐ง โฅ 0) |
32 | | breq2 4007 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ง โฅ ๐ โ ๐ง โฅ 0)) |
33 | 32 | ad2antlr 489 |
. . . . . . . 8
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ (๐ง โฅ ๐ โ ๐ง โฅ 0)) |
34 | 31, 33 | mpbird 167 |
. . . . . . 7
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ ๐ง โฅ ๐) |
35 | 2 | ad3antrrr 492 |
. . . . . . . . 9
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ ๐ = 0) |
36 | 31, 35 | breqtrrd 4031 |
. . . . . . . 8
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ ๐ง โฅ ๐) |
37 | 3 | ad3antrrr 492 |
. . . . . . . . 9
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ ๐ = 0) |
38 | 31, 37 | breqtrrd 4031 |
. . . . . . . 8
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ ๐ง โฅ ๐) |
39 | 36, 38 | jca 306 |
. . . . . . 7
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) |
40 | 34, 39 | 2thd 175 |
. . . . . 6
โข
((((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โง ๐ง โ โค) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
41 | 40 | ralrimiva 2550 |
. . . . 5
โข
(((((๐ โ
โค โง ๐ โ
โค) โง (๐ = 0 โง
๐ = 0)) โง ๐ โ โ0)
โง ๐ = 0) โ
โ๐ง โ โค
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
42 | 29, 41 | impbida 596 |
. . . 4
โข ((((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โง ๐ โ โ0) โ
(โ๐ง โ โค
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)) โ ๐ = 0)) |
43 | 6, 42 | riota5 5855 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ (โฉ๐ โ โ0
โ๐ง โ โค
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) = 0) |
44 | 1, 4, 43 | 3eqtr4a 2236 |
. 2
โข (((๐ โ โค โง ๐ โ โค) โง (๐ = 0 โง ๐ = 0)) โ (๐ gcd ๐) = (โฉ๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |
45 | | bezoutlembi 12005 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ โ
โ0 (โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โง โ๐ โ โค โ๐ โ โค ๐ = ((๐ ยท ๐) + (๐ ยท ๐)))) |
46 | | simpl 109 |
. . . . . 6
โข
((โ๐ค โ
โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โง โ๐ โ โค โ๐ โ โค ๐ = ((๐ ยท ๐) + (๐ ยท ๐))) โ โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
47 | 46 | reximi 2574 |
. . . . 5
โข
(โ๐ โ
โ0 (โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โง โ๐ โ โค โ๐ โ โค ๐ = ((๐ ยท ๐) + (๐ ยท ๐))) โ โ๐ โ โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
48 | 45, 47 | syl 14 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ
โ๐ โ
โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
49 | 48 | adantr 276 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โ โ๐ โ โ0
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
50 | | simplll 533 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ ๐ โ โค) |
51 | | simpllr 534 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ ๐ โ โค) |
52 | | simprl 529 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ ๐ โ โ0) |
53 | | breq1 4006 |
. . . . . . . . 9
โข (๐ค = ๐ง โ (๐ค โฅ ๐ โ ๐ง โฅ ๐)) |
54 | | breq1 4006 |
. . . . . . . . . 10
โข (๐ค = ๐ง โ (๐ค โฅ ๐ โ ๐ง โฅ ๐)) |
55 | | breq1 4006 |
. . . . . . . . . 10
โข (๐ค = ๐ง โ (๐ค โฅ ๐ โ ๐ง โฅ ๐)) |
56 | 54, 55 | anbi12d 473 |
. . . . . . . . 9
โข (๐ค = ๐ง โ ((๐ค โฅ ๐ โง ๐ค โฅ ๐) โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
57 | 53, 56 | bibi12d 235 |
. . . . . . . 8
โข (๐ค = ๐ง โ ((๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |
58 | 57 | cbvralv 2703 |
. . . . . . 7
โข
(โ๐ค โ
โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
59 | 58 | biimpi 120 |
. . . . . 6
โข
(โ๐ค โ
โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
60 | 59 | ad2antll 491 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
61 | | simplr 528 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ ยฌ (๐ = 0 โง ๐ = 0)) |
62 | 50, 51, 52, 60, 61 | bezoutlemsup 12009 |
. . . 4
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ ๐ = sup({๐ง โ โค โฃ (๐ง โฅ ๐ โง ๐ง โฅ ๐)}, โ, < )) |
63 | | breq1 4006 |
. . . . . . . . 9
โข (๐ค = ๐ง โ (๐ค โฅ ๐ โ ๐ง โฅ ๐)) |
64 | 63, 56 | bibi12d 235 |
. . . . . . . 8
โข (๐ค = ๐ง โ ((๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |
65 | 64 | cbvralv 2703 |
. . . . . . 7
โข
(โ๐ค โ
โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
66 | 65 | a1i 9 |
. . . . . 6
โข (๐ โ โ0
โ (โ๐ค โ
โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |
67 | 66 | riotabiia 5847 |
. . . . 5
โข
(โฉ๐
โ โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) = (โฉ๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) |
68 | | simprr 531 |
. . . . . 6
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
69 | 50, 51, 52, 68 | bezoutlemeu 12007 |
. . . . . . 7
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ โ!๐ โ โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) |
70 | | breq2 4007 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ค โฅ ๐ โ ๐ค โฅ ๐)) |
71 | 70 | bibi1d 233 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) |
72 | 71 | ralbidv 2477 |
. . . . . . . 8
โข (๐ = ๐ โ (โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) |
73 | 72 | riota2 5852 |
. . . . . . 7
โข ((๐ โ โ0
โง โ!๐ โ
โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) โ (โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ (โฉ๐ โ โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) = ๐)) |
74 | 52, 69, 73 | syl2anc 411 |
. . . . . 6
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ (โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)) โ (โฉ๐ โ โ0 โ๐ค โ โค (๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) = ๐)) |
75 | 68, 74 | mpbid 147 |
. . . . 5
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ (โฉ๐ โ โ0
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐))) = ๐) |
76 | 67, 75 | eqtr3id 2224 |
. . . 4
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ (โฉ๐ โ โ0
โ๐ง โ โค
(๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐))) = ๐) |
77 | | gcdn0val 11961 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โ (๐ gcd ๐) = sup({๐ง โ โค โฃ (๐ง โฅ ๐ โง ๐ง โฅ ๐)}, โ, < )) |
78 | 77 | adantr 276 |
. . . 4
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ (๐ gcd ๐) = sup({๐ง โ โค โฃ (๐ง โฅ ๐ โง ๐ง โฅ ๐)}, โ, < )) |
79 | 62, 76, 78 | 3eqtr4rd 2221 |
. . 3
โข ((((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โง (๐ โ โ0 โง
โ๐ค โ โค
(๐ค โฅ ๐ โ (๐ค โฅ ๐ โง ๐ค โฅ ๐)))) โ (๐ gcd ๐) = (โฉ๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |
80 | 49, 79 | rexlimddv 2599 |
. 2
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ
(๐ = 0 โง ๐ = 0)) โ (๐ gcd ๐) = (โฉ๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |
81 | | gcdmndc 11944 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ
DECID (๐ = 0
โง ๐ =
0)) |
82 | | exmiddc 836 |
. . 3
โข
(DECID (๐ = 0 โง ๐ = 0) โ ((๐ = 0 โง ๐ = 0) โจ ยฌ (๐ = 0 โง ๐ = 0))) |
83 | 81, 82 | syl 14 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ = 0 โง ๐ = 0) โจ ยฌ (๐ = 0 โง ๐ = 0))) |
84 | 44, 80, 83 | mpjaodan 798 |
1
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (โฉ๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) |